CODEWITHSUNDEEP
z3z3-fixedpoint
user1487718
user1487718

Reputation:

An error appears when running exist quantifier and fixedpoint Z3 in C#

I tried to use ctx.mkExist in the fixedpoint, howwever, it occurs error said "contains recursive predicate", I don't know why? and How to use ctx.MkExists in fixedpoint?For example: exist (lamda real) that lamb>=0 AND inv(c,i) AND phi(c+lamb,i) => phi(c，i) 

        using (Context ctx = new Context())
        {
            var s = ctx.MkFixedpoint();

            IntSort B = ctx.IntSort;
            BoolSort T = ctx.BoolSort;
            RealSort R = ctx.RealSort;

            FuncDecl phi = ctx.MkFuncDecl("phi", new Sort[] { R,B }, T);
            s.RegisterRelation(phi);
            FuncDecl Inv = ctx.MkFuncDecl("inv", new Sort[] { R, B }, T);
            s.RegisterRelation(Inv);

            RealExpr c= (RealExpr)ctx.MkBound(0, R);
            IntExpr i = (IntExpr) ctx.MkBound(1, B);

            Expr[] InvArg=new Expr[2];
            InvArg[0] = ctx.MkConst("inv0" , Inv.Domain[0]);
            InvArg[1] = ctx.MkConst("inv1", Inv.Domain[1]);

            Expr invExpr = ctx.MkImplies(ctx.MkOr(
                 ctx.MkAnd(ctx.MkEq(InvArg[1], ctx.MkInt(0)), ctx.MkGe((RealExpr)InvArg[0], ctx.MkReal(0))),
                 ctx.MkAnd(ctx.MkEq(InvArg[1], ctx.MkInt(1)), ctx.MkGe((RealExpr)InvArg[0], ctx.MkReal(2)))
                 ),
              (BoolExpr)Inv[InvArg]);
            Quantifier invQ = ctx.MkForall(InvArg, invExpr, 1);
            s.AddRule(invQ);

            RealExpr[] lamb = new RealExpr[1];
            lamb[0] = ctx.MkRealConst("lamb");
            Expr existExpr = ctx.MkAnd(
                (BoolExpr)Inv[c,i],
                (BoolExpr)phi[ctx.MkAdd(c,lamb[0]),i],
                ctx.MkGe(lamb[0], ctx.MkReal(0)));
            BoolExpr t= ctx.MkExists(lamb, existExpr, 1);
            s.AddRule(ctx.MkImplies(t,(BoolExpr)phi[c,i]));
        }

sometimes, there is an error said "AccessViolationException was unhandlered,Attempted to read or write protected memory. This is often an indication that other memory is corrupt." when running to ctx.MkExists()

Upvotes: 1

Views: 235

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 461

The fixedpoint solver only supports universal quantifiers at the top-level. You should rewrite the rule as follows:

        s.AddRule(ctx.MkForall(lamb, 
          ctx.MkImplies((BoolExpr)existExpr,(BoolExpr)phi[c,i])));

Z3 should ideally not result in any access violation. This is typically indicating a bug. I would really appreciate repros for such bugs when/if you encounter them.

Upvotes: 1

Related Questions