如何從SAT模型中獲取「真實」變量？

Question

想想看，我有一個簡單的SMT-lib的公式：

(declare-const a Bool) 
(declare-const b Bool) 
(declare-const c Bool) 
(declare-const d Bool) 
(assert (or a b)) 
(assert (or d c)) 
(check-sat) 
(get-model) 

當SAT求解器給出了一個模型。它提供了有真/假值的所有變量。但我只想要「真」價值分配變量。這可能與Z3？

Answer 1

這是一個完成此操作的z3py腳本。 http://rise4fun.com/Z3Py/fp5k

我認爲要與模型交互/遍歷模型，您需要使用API​​。

a,b,c,d = Bools('a b c d') 

s = Solver() 

s.add(Or(a, b)) 
s.add(Or(c, d)) 

s.check() 
m = s.model() 
print m 

for t in m.decls(): 
    if is_true(m[t]): 
    print t 
    print m[t]