C# API를 사용하여 z3 고정 점에서 fun 정의하는 방법

Question

고정 소수점 규칙에 사용할 수있는 함수를 정의하고 싶습니다. 예를 들어 : "정의-재미"에 대한 API가 없다는 것을 말한다

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

, 그것은 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)); 
} 

를 작성하고 당신이 "초기화"를 적용 할 경우이 기능을 사용할 수 있습니다.