CODEWITHSUNDEEP
pythonz3z3py
Sergey
Sergey

Reputation: 21

Usage of z3py unsat cores together with z3.Optimize()

I'm using z3 python api. I would like to use the unsat core functionality of Z3 on the one side and being able to do optimization towards some criteria on the other.

So if I do wann use unsat cores I do the following:

self.solver = z3.Solver()
self._solver.assert_and_track(constraint1, error_message1)
self._solver.assert_and_track(constraint2, error_message2)
...
self._solver.check()

if len(self._solver.unsat_core()) > 0
  print (self._solver.unsat_core())

That works just fine. But I would additionally to that be able to use the maximize() and minimize() functions from z3.Optimize(). This instance of the solver though seems not to offer unsat cores. Is it possible to use those together?

Also I've seen online that instead of using the assert_and_track() function it is possible to use implication for tracking unsat cores: Implies(p1, constraint1). What is the difference here?

Upvotes: 1

Views: 331

Answers (1)

alias
alias

Reputation: 30450

Z3 does not support optimization and unsat-core generation at the same time. Here's the relevant ticket from about two months ago: https://github.com/Z3Prover/z3/issues/1577

Note that this is not because it cannot be implemented: It's just that they haven't implemented this yet. Registering your request there might motivate them to add support!

Regarding your question for tracking unsat-cores using implication: I believe that's essentially what assert_and_track does. You can see its source code here: https://github.com/Z3Prover/z3/blob/d2c937a989ea360e9cba06583eccaa257c75870f/src/api/python/z3/z3.py#L6418-L6446 Is it not working for you for some reason?

Upvotes: 0

Related Questions