Let's say I have parsed a constraint in the smt2 format using the following function:
constraint = z3.parse_smt2_file(file_address)
I am wondering if there is an easy way to negate the constraint as in the following and get a model:
solver.add(Not(constraint))
print(solver.model())
Sure. Here's an example. Put this in a.smt2:
(set-logic ALL)
(declare-fun a () Int)
(declare-fun b () Int)
(assert (= a (+ 1 b)))
(assert (= a (* 2 b)))
(check-sat)
Then on the python side:
from z3 import *
constraints = parse_smt2_file('a.smt2')
s = Solver()
s.add(Not(And(*constraints)))
print(s.check())
print(s.model())
This prints:
sat
[b = 1, a = 1]
Note that parse_smt2_file might need to be given the relevant sorts and declarations in general. See the example at: https://z3prover.github.io/api/html/namespacez3py.html#a09fe122cbfbc6d3fa30a79850b2a2414