如何使用 C# API 在 z3 定点中定义乐趣

Question

我想定义可以在定点规则中使用的函数。 例如：

(declare-var int1 Int)
(declare-var int2 Int)
(declare-rel phi( Int Int))
(define-fun init((a Int)(b Int)) Bool
    (and
        (= a 0)
        (= b 0)
    )
)

(rule ( =>
    (init int1 int2)
    (phi int1 int2))
)

(query (and (phi int1 int2) (= int1 0)))   

据说“define-fun”没有api，应该在API中翻译成量词。 我尝试使用 c# api 来实现它。但是，我得到了错误的答案。 （结果应该是可满足的，然而，它是不可满足的） 代码：

using (Context ctx = new Context())
{
    var s = ctx.MkFixedpoint();
    Solver slover = ctx.MkSolver();
    IntSort B = ctx.IntSort;
    RealSort R = ctx.RealSort;
    BoolSort T = ctx.BoolSort;
    IntExpr int1 = (IntExpr) ctx.MkBound(0, B);
    IntExpr int2 = (IntExpr) ctx.MkBound(1, B);
    FuncDecl phi = ctx.MkFuncDecl("phi", new Sort[] {B, B }, T);
    FuncDecl init = ctx.MkFuncDecl("init", new Sort[] {B, B}, T);
    s.RegisterRelation(phi);
    s.RegisterRelation(init);
    Expr[] initBound = new Expr[2];
    initBound[0] = ctx.MkConst("init" + 0, init.Domain[0]);
    initBound[1] = ctx.MkConst("init" + 1, init.Domain[1]);
    Expr initExpr = ctx.MkEq((BoolExpr)init[initBound],
    ctx.MkAnd(ctx.MkEq(initBound[0], ctx.MkInt(0)), ctx.MkEq(initBound[1], ctx.MkInt(0))));
    Quantifier q = ctx.MkForall(initBound, initExpr, 1);
    slover.Assert(q);
    s.AddRule(ctx.MkImplies((BoolExpr)init[int1, int2],
    (BoolExpr)phi[int1, int2]));
    Status a = s.Query(ctx.MkAnd((BoolExpr)phi[int1,int2],ctx.MkEq(int1, ctx.MkInt(0))));
}

有什么问题？

Answer 1

下面是宏变成规则的版本。

var s = ctx.MkFixedpoint();
IntSort B = ctx.IntSort;
BoolSort T = ctx.BoolSort;
IntExpr int1 = (IntExpr) ctx.MkBound(0, B);
IntExpr int2 = (IntExpr) ctx.MkBound(1, B);
FuncDecl phi = ctx.MkFuncDecl("phi", new Sort[] {B, B }, T);
FuncDecl init = ctx.MkFuncDecl("init", new Sort[] {B, B}, T);
s.RegisterRelation(phi);
s.RegisterRelation(init);
Expr[] initBound = new Expr[2];
initBound[0] = ctx.MkConst("init" + 0, init.Domain[0]);
initBound[1] = ctx.MkConst("init" + 1, init.Domain[1]);
Expr initExpr = ctx.MkImplies(
      ctx.MkAnd(ctx.MkEq(initBound[0], ctx.MkInt(0)), ctx.MkEq(initBound[1], ctx.MkInt(0))),
              (BoolExpr)init[initBound]);

Quantifier q = ctx.MkForall(initBound, initExpr, 1);

s.AddRule(q);
s.AddRule(ctx.MkImplies((BoolExpr)init[int1, int2], (BoolExpr)phi[int1, int2]));

Status a = s.Query(ctx.MkAnd((BoolExpr)phi[int1,int2],ctx.MkEq(int1, ctx.MkInt(0))));

Console.WriteLine("{0}",a);

Console.WriteLine("{0}", s.GetAnswer());

也可以写一个函数

Term init(Context ctx, Term a, Term b) { 
   Term zero = ctx.MkInt(0);
   return ctx.MkAnd(ctx.MkEq(a,zero),ctx.MkEq(b,zero));
}

并在应用“init”的地方使用此函数。