Search code examples
z3smt

is there a way to express "if and only if" in SMTLIB?

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.

Solution

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