在 C# 中运行存在量词和定点 Z3 时出现错误

Question

我试图在定点中使用ctx.mkExist，无论如何，它发生错误说"包含递归谓词"，我不知道为什么？ 以及如何使用 ctx。Mk在定点中存在？例如： 存在（lamda real）那 lamb>=0 和 inv（c，i） 和 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]));
        }

有时会出现错误说"访问违规异常未处理，试图读取或写入受保护的内存。这通常表示其他内存已损坏。MkExists（）

Answer 1

定点求解器仅支持顶层的通用量词。您应该按如下方式重写规则：

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

理想情况下，Z3 不应导致任何访问冲突。这通常表示存在错误。当您遇到此类错误时，我将非常感谢它们的重现。