在C＃中运行存在量词和定点Z3当出现错误 [英] An error appears when running exist quantifier and fixedpoint Z3 in C#

问题描述

我试图在定点使用ctx.mkExist，howwever，它错误说的包含递归predicate ，我不知道为什么会发生？以及如何使用ctx.MkExists在定点？例如：
 存在（LAMDA实）羊羔> = 0和INV（C，I）和Phi（C +羊肉，I）=>岛（C，I）

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]));
        }

有时候，有一个错误说 AccessViolationException 被unhandlered，尝试读取或写入受保护的内存。这通常是指示其他内存已损坏。运行时ctx.MkExists（）

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()

推荐答案

的定点求解器只支持顶级全称量词。
你应该重写规则如下：

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应理想不会导致任何访问冲突。这通常是指示的错误。
我真的AP preciate repros这样的错误，当/如果遇到他们。

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.

这篇关于在C＃中运行存在量词和定点Z3当出现错误的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！