CODEWITHSUNDEEP
z3smtz3py
z3_test
z3_test

Reputation: 19

How to display specific unsat constraint, not whole core (Z3, Python)

How i can list only specific constraint result from my unsat core? I have a lot of conditions and printing whole core doesn't print all. I read that it can be done with assert_and_track and unsat_core commands. I found some examples but they don't works. Any experience with this?

s.assert_and_track(A > B, 'p1')
s.assert_and_track(B > C, 'p2')
if s.check() == sat:
  print('ok')
else:
  c = s.unsat_core
  print(c) <- this print all core

So how to print only p1 or p2 (just true/false result) ? e.g. p2 = false, or it can be displayed in way as is displayed in print(c) mode - but just for p1.

Upvotes: 0

Views: 1073

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8393

The easiest way to achieve that is to simply save a map of labels to constraints, for this examples we can do 

M = {}
M['p1'] = (A > B)
M['p2'] = (B > C)
M['p3'] = (C > A)

so that later we can print the core in terms of those constraints, for instance as follows

core = s.unsat_core()
for e in core:
    print(M[str(e)])

Of course this will also work if you want to print only some entries instead of all of them.

Upvotes: 0

Related Questions