CODEWITHSUNDEEP
pythonlogicz3smtz3py
Others
Others

Reputation: 3023

Is there a way to use solver.unsat_core, without using solver.assert_and_track?

Is there any way to make the following code work, and print out a valid unsat core?

from z3 import *

a = Int('a')
b = Int('b')

s = Solver()
s.add(a == 1)
s.add(a == 2)
s.add(b == 3)

s.check()

# This prints [], and I would like it to print [a == 1, a == 2]
print(s.unsat_core())

I know I could do this instead:

from z3 import *

a = Int('a')
b = Int('b')

s = Solver()
s.assert_and_track(a == 1, 'p1')
s.assert_and_track(a == 2, 'p2')
s.assert_and_track(b == 3, 'p3')

s.check()
# This prints [p1, p2]
print(s.unsat_core())

But for the real project I'm working on, it would be painful to go through and give names to every constraint (due to their volume, as well as how they're generated.)

Upvotes: 1

Views: 577

Answers (1)

alias
alias

Reputation: 30525

Not unless you implement it yourself. Unsat core extraction requires labeling the constraints, see top of page 67 of this document: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf

Having said that, you can build a "database" of your assertions by defining your own version of add that first makes up a name and inserts it, and then do the reverse lookup in a function my_unsat_core that you would similarly define. If you were to implement this in a generic way, Z3 folks might be interested in incorporating it into their API as well. Would be a nice addition.

Upvotes: 1

Related Questions