奇怪的結果，當我問Z3尋找其他解決

Question

我使用Z3作爲一個簡單的SAT求解器，斷言命題範圍如下：

let ctx = new Context() 
let x = ctx.MkBoolConst("x") 
let y = ctx.MkBoolConst("y") 
let z = ctx.MkBoolConst("z") 
let f = ctx.MkOr(ctx.MkAnd(x,y), ctx.MkAnd(ctx.MkNot(x),z)) 
let s = ctx.MkSolver() 
s.Assert(f) 
assert (s.Check() = Status.SATISFIABLE) 
let r= [s.Model.Eval(x); s.Model.Eval(y); s.Model.Eval(z)] 
printfn "%A" r 

預期它返回

[false; true; true] 

。然而，當我嘗試通過採取和發現的分配和否定這一點，把它加回到Z3求解

let mkB(z3_lit:BoolExpr,bvalue:Expr) = 
    if (bvalue:?> BoolExpr).IsTrue then z3_lit else ctx.MkNot z3_lit 
let founds = List.map mkB (List.zip [x;y;z] r) 
let and_founds = ctx.MkAnd (List.toArray(founds)) 
let negated = ctx.MkNot and_founds 
s.Assert negated 
assert (s.Check() = Status.SATISFIABLE) 
let r2 = [s.Model.Eval(x); s.Model.Eval(y); s.Model.Eval(z)] 
printfn "%A" r2 

問Z3爲進一步的解決辦法，我得到一個奇怪的分配到z。即：

[true; true; z] 

爲什麼分配到z這是以前true改爲z？

Answer 1

如果我沒有弄錯，獲取一個變量作爲自己的模型意味着這是一個「不關心」：z的任何值都會給你一個有效的模型。事實上，在這種情況下，該條款已經被x和y是真正的滿足。

如果你想Z3完成你的模型，你可以看看this question。

此外，C API至少定義了一個Z3_model_eval的額外參數，您可以使用該參數向Z3指示您需要所有變量的值。