Представление формулы SMT

Question

Создать логическую формулу в PySMT очень просто:

      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)

Более того, формула SMT имеет такой вид:

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

Я понимаю, что это работает:

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

Однако, вместо уравнений, как насчет того, чтобы я просто составил формулу в таком виде:

# formula = Or(x1, x2) # ?