Z3 .NET存在量詞的API

Question

我正在嘗試使用Z3 .net API來獲取存在量詞expr。 以下是我的代碼：

RealExpr c = ctx.MkRealConst("c"); 
BoolExpr Eqzero = ctx.MkGt(c,ctx.MkReal(0));  
BoolExpr Gezero = ctx.MkGe(c,ctx.MkReal(0)); 
BoolExpr Lttwo = ctx.MkLt(c,ctx.MkReal(2)); 
BoolExpr Gtthree = ctx.MkGt(c,ctx.MkReal(3)); 

BoolExpr b1 = ctx.MkBoolConst("b1"); 
BoolExpr b2 = ctx.MkBoolConst("b2"); 
BoolExpr b3 = ctx.MkBoolConst("b3"); 
BoolExpr b0 = ctx.MkBoolConst("b0"); 

RealExpr[] lamb=new RealExpr[1]; 

lamb[0]=ctx.MkRealConst("lamb"); 

BoolExpr temp=ctx.MkAnd(
    ctx.MkGt(lamb[0],ctx.MkReal(0)), 
    ctx.MkEq(b0,ctx.MkTrue()), 
    ctx.MkEq(b1,ctx.MkTrue()), 
    ctx.MkGe(ctx.MkAdd(c,lamb[0]),ctx.MkReal(0)), 
    ctx.MkLe(ctx.MkAdd(c,lamb[0]),ctx.MkReal(3)), 
    ctx.MkGe(c,ctx.MkReal(0)), 
    ctx.MkLe(c,ctx.MkReal(3)) 
        ); 


BoolExpr exist = ctx.MkExists(lamb, temp, 1, null, null, ctx.MkSymbol("Q2"),   ctx.MkSymbol("skid2")); 

Console.WriteLine(exist.ToString()); 
Solver s1 = ctx.MkSolver(); 
s1.Assert(exist); 
if (s1.Check() == Status.SATISFIABLE) 
{ 
    Console.WriteLine("get pre"); 
    Console.Write(s1); 
} 
else 
{ 
    Console.WriteLine("Not reach"); 
} 
Console.ReadKey(); 

'

對於程序，我得到了以下結果：

(exists ((lamb Real)) 
(! (and (> lamb 0.0) 
     (= b0 true) 
     (= b1 true) 
     (>= (+ c lamb) 0.0) 
     (<= (+ c lamb) 3.0) 
     (>= c 0.0) 
     (<= c 3.0)) 
:skid skid2 
:qid Q2)) 
Not reach 

我的問題是 1.什麼是的意思！在結果/ 2.我無法獲得SAT結果的原因是什麼？ 3.除了Z3網站上的API菜單之外，有人可以提供一些與Z3 .NET API相對應的門派嗎？

非常感謝！

Answer 1

（！...）函數的含義是一種將模式和量詞以及Skolem ID綁定到表達式的註釋。當這條線

BoolExpr exist = ctx.MkExists(lamb, temp, 1, null, null, ctx.MkSymbol("Q2"), ctx.MkSymbol("skid2")); 

改爲

BoolExpr exist = ctx.MkExists(lamb, temp, 1); 

那麼就沒有（！？）輸出。

我不能複製UNSAT結果：當我運行使用Z3 4.0這個例子中，我得到SAT及以下型號：

(define-fun lamb!0() Real 1.0) 
(define-fun c() Real 1.0) 
(define-fun b1() Bool true) 
(define-fun b0() Bool true)