Is it the same as define in SMTLIB? Or is the only way to define a function on my own? If z3 has a way to do that via its python binding that would work for me also.
is there a way to express "if and only if" in SMTLIB?
Viewed 253
1 Answers
In SMTLib, iff is simply = over booleans:
(declare-fun a () Bool)
(declare-fun b () Bool)
(assert (= a b))
In z3py, you can use the regular equality comparison:
from z3 import *
a, b = Bools('a b')
s = Solver()
s.add(a == b)
Related