Representing an SMT formula

Question

Making a Boolean formula in PySMT is simple:

from pysmt.shortcuts import *
from pysmt.typing import INT
x1 = Symbol("x1")
x2 = Symbol("x2")

formula = Or(x1, x2)
model = get_model(formula)
print(model)

Moreover, an SMT formula has this shape:

x1 = Symbol("x1", INT)
x2 = Symbol("x2", INT)
x1_domain = And(GE(x1, Int(0)), LE(x1, Int(1)))
x2_domain = And(GE(x2, Int(0)), LE(x2, Int(1)))

I realize this works:

equation = Equals(Minus(x1, x2), Plus(x1, x2))
formula = And(equation, x1_domain, x2_domain)
model = get_model(formula)

However, instead of equations, how about I just make a formula in this form:

# formula = Or(x1, x2) # ?

Answer 1

You can make it a little more palatable:

from pysmt.shortcuts import *
from pysmt.typing import INT

x1 = Symbol("x1", INT)
x2 = Symbol("x2", INT)
x1_domain = And(x1 >= 0, x1 <= 1)
x2_domain = And(x2 >= 0, x2 <= 1)

equation = Equals(x1 - x2, x1 + x2)
formula = And(equation, x1_domain, x2_domain)
print(formula)

model = get_model(formula)
print(model)

That is, literals and comparisons work. Unfortunately that's where it ends. You cannot use && for And, == for Equals etc. This is because Python doesn't allow overloading of booleans like this: https://peps.python.org/pep-0335/