考虑到我有一个简单的 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可以吗??
考虑到我有一个简单的 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可以吗??
这是一个完成此任务的 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]