使用Z3和c＃

Question

獲取不穩定的核心示例我想在C＃實現中使用Z3座標解算器。此代碼非常接近Microsoft本身在「http://z3.codeplex.com/SourceControl/latest#examples/dotnet/Program.cs」中給出的示例。我的代碼是：

using (Context ctx = new Context(new Dictionary<string, string>() { { "proof", "true" } })) 
{ 
... 
Expr x = ctx.MkConst("x", ctx.MkIntSort()); 
Expr y = ctx.MkConst("y", ctx.MkIntSort()); 
Expr zero = ctx.MkNumeral(0, ctx.MkIntSort()); 
Expr one = ctx.MkNumeral(1, ctx.MkIntSort()); 
Expr five = ctx.MkNumeral(5, ctx.MkIntSort()); 

Solver s = ctx.MkSolver(); 

s.Assert(ctx.MkGt((ArithExpr)x, (ArithExpr)zero)); // x > 0 
s.Assert(ctx.MkLt((ArithExpr)y, (ArithExpr)five)); // y < 5 
s.Assert(ctx.MkLt((ArithExpr)x, (ArithExpr)zero)); // x < 0 
s.Assert(ctx.MkEq((ArithExpr)y, ctx.MkAdd((ArithExpr)x, (ArithExpr)one))); // y = x + 1 

Status result = s.Check(); 

if (result == Status.UNSATISFIABLE) 
{ 
    Console.WriteLine("unsat"); 
    Console.WriteLine("proof: {0}", s.Proof); 
    Console.WriteLine("core: "); 
    foreach (Expr c in s.UnsatCore) 
    { 
     Console.WriteLine("{0}", c); 
    } 
} 

但仍然當我到達這個模型的「s.UnsatCore」它是空的。

我自己也嘗試在這樣的斷言進入：

BoolExpr constraint1 = ctx.MkBoolConst("Constraint1"); 
s.AssertAndTrack(ctx.MkGt((ArithExpr)x, (ArithExpr)zero), constraint1); 
BoolExpr constraint2 = ctx.MkBoolConst("Constraint2"); 
s.AssertAndTrack(ctx.MkLt((ArithExpr)y, (ArithExpr)five), constraint2); 
BoolExpr constraint3 = ctx.MkBoolConst("Constraint3"); 
s.AssertAndTrack(ctx.MkLt((ArithExpr)x, (ArithExpr)zero), constraint3); 
BoolExpr constraint4 = ctx.MkBoolConst("Constraint4"); 
s.AssertAndTrack(ctx.MkEq((ArithExpr)y, ctx.MkAdd((ArithExpr)x, (ArithExpr)one)), constraint4); 

我想的UnsatCore返回「constraint1，constrint3」。任何人都可以幫助我做我做錯了什麼？

Answer 1

您是否在創建ctx時啓用了生成證明（Solver.UnsatCore的文檔指出，如果它被禁用，結果爲空）？您需要將Dictionary（「proof - >」true「）傳遞給Context的構造函數來執行此操作。