1

固定小数点ルールで使用できる関数を定義したいと思います。例えば：

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

どうしたの？

4

1 に答える 1

2

以下は、マクロがルールに変換されるバージョンです。

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」を適用する場合は、この関数を使用します。

于 2012-07-03T13:37:43.817 に答える