0

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

foobar
  • 571
  • 1
  • 5
  • 20

1 Answers1

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/

alias
  • 28,120
  • 2
  • 23
  • 40
  • Yes, this looks more clear. However, the question remains: How to get the domains of the variables in the later parts of the code, something like: `x1.get_domain() = [0,1]`? – foobar Dec 15 '22 at 15:48
  • 1
    You can't. Those are separate expressions and have nothing to do with x1/x2 etc. If you really want, you can build your own class of expressions that kept track of these things for you, and translated to pySMT, but that's a fair amount of work and not sure if there's ROI in it. – alias Dec 15 '22 at 15:51
  • if impossible, can I get the lower and upper bounds? `x1.get_lower_bound() = 0` `x1.get_upper_bound() = 1` The domain can then be constructed if they are integers. – foobar Dec 15 '22 at 16:00
  • 1
    Those bounds are what you're writing in your program. So, you can keep track of them in any way you like. Note that until you call `get_model` (or equivalent), pySMT doesn't do anything with your formulas: They're merely syntax waiting to be sent to the backend SMT solver. – alias Dec 15 '22 at 16:11