CODEWITHSUNDEEP
z3
user1770051
user1770051

Reputation: 149

How to get only "true" variables from SAT model?

Consider that I have a simple SMT-lib formula:

(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)

When SAT solver gives a model. It provides all variables with there true/false values. But I want only "True" value assigned variables. It is possible with Z3??

Upvotes: 4

Views: 1196

Answers (1)

Taylor T. Johnson
Taylor T. Johnson

Reputation: 2884

Here's a z3py script that accomplishes this. http://rise4fun.com/Z3Py/fp5k

I think to interact with / traverse the model, you need to work with an 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]

Upvotes: 5

Related Questions