Negate a parsed smtlib2 expression using Python API

Question

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())

Answer 1

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