2

簡単な 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ソルバーがモデルを与えるとき。すべての変数に真/偽の値を提供します。しかし、変数に割り当てられた「True」値のみが必要です。Z3で可能ですか??

4

1 に答える 1

3

これを実現する 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]
于 2012-10-24T03:16:20.237 に答える