Bad kernels in Z3 Python
I am working with Python API Z3 trying to incorporate it into a research tool I am writing. I have a question about extracting an unsatisfactory kernel using the Python interface.
I have the following simple request:
(set-option :produce-unsat-cores true)
(assert (! (not (= (_ bv0 32) (_ bv0 32))) :named __constraint0))
(check-sat)
(get-unsat-core)
(exit)
Running this request through the z3 executable (for Z3 4.1 ), I get the expected output:
unsat
(__constraint0)
For Z3 4.3 I am getting segmentation error:
unsat
Segmentation fault
This is not the main question, although it was an intriguing observation. Then I changed the request (inside the file) as
(assert (! (not (= (_ bv0 32) (_ bv0 32))) :named __constraint0))
(exit)
Using a file handler, I passed the contents of this file (in the `queryStr 'variable) to the following Python code:
import z3
...
solver = z3.Solver()
solver.reset()
solver.add(z3.parse_smt2_string(queryStr))
querySatResult = solver.check()
if querySatResult == z3.sat:
...
elif querySatResult == z3.unsat:
print solver.unsat_core()
I am getting an empty list from the `unsat_core ': [] function. Am I using this function incorrectly? The docstring for the function suggests that I should instead be doing something similar to
solver.add(z3.Implies(p1, z3.Not(0 == 0)))
However, I was wondering if the query could be used as is, since it conforms to the SMT-LIB v2.0 standards (I believe) and if I am missing something obvious.
source to share
The crash you observed has been fixed and the fix will be available in the next version. If you try the "unstable" (work in progress) branch, you should get the expected behavior. You can get an unstable branch with
git clone https://git01.codeplex.com/z3 -b unstable
The API parse_smt2_string
provides only basic support for parsing formulas in SMT 2.0 format. It doesn't preserve annotations :named
. We'll look at this and other limitations in future releases. At the same time, we have to use "response literals" such as p1
form statements:
solver.add(z3.Implies(p1, z3.Not(0 == 0)))
In the "unstable" branch, we also support the following new API. It "mimics" the assertions :named
used in the SMT 2.0 standard.
def assert_and_track(self, a, p):
"""Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
If `p` is a string, it will be automatically converted into a Boolean constant.
>>> x = Int('x')
>>> p3 = Bool('p3')
>>> s = Solver()
>>> s.set(unsat_core=True)
>>> s.assert_and_track(x > 0, 'p1')
>>> s.assert_and_track(x != 1, 'p2')
>>> s.assert_and_track(x < 0, p3)
>>> print(s.check())
unsat
>>> c = s.unsat_core()
>>> len(c)
2
>>> Bool('p1') in c
True
>>> Bool('p2') in c
False
>>> p3 in c
True
"""
...
source to share