How to use pysmt to calculate formulas containing both integers and real numbers simultaneously

Question

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

hello = [Symbol(s, INT) for s in "hello"]
pysmt = [Symbol(s, REAL) for s in "pysmt"]
domains_1 = And([And(GE(l, Int(1)),
                   LT(l, Int(10))) for l in hello])
domains_2 = And([And(GE(l, Real(1)),
                   LT(l, Real(10))) for l in pysmt])

sum_hello = Plus(hello) # n-ary operators can take lists
sum_pysmt = Plus(pysmt) # as arguments
problem = And(Equals(sum_hello, sum_pysmt),
              Equals(sum_hello, Int(25)))
formula = And(domains_1, domains_2, problem)

print("Serialization of the formula:")
print(formula)

model = get_model(formula, solver_name="z3")
if model:
  print(model)
else:
  print("No solution found")

This code will display: PysmtTypeError: The formula ((h + e + l + l + o) = (p + y + s + m + t)) is not well-formed.

Answer 1

SMTLib/z3 are typed-languages (unlike Python). Meaning you cannot compare an integer to a real-value: That's a type-mismatch. Furthermore, mixing such types can lead to undecidable problems. (More on that later.)

To make your program type-correct, you should cast the integer to a real, by changing your equation:

problem = And(Equals(sum_hello, sum_pysmt),
              Equals(sum_hello, Int(25)))

to:

problem = And(Equals(ToReal(sum_hello), sum_pysmt),
              Equals(sum_hello, Int(25)))

Conversion from integer to real is achieved by the ToReal function. In general, such conversions complicate the problem: That is, once you use ToReal, the problem is no longer in the decidable fragment of the logic. (To be precise, real-arithmetic is decidable, but if you cast problems in it obtained by conversion from Int via ToReal, the logic becomes semi-decidable. This follows because you could otherwise solver arbitrary Diophantine equations, which is known to be undecidable. But perhaps that's beyond the point for this discussion.)

The lucky news is that your problem is simple enough for the solver to handle, even with mixing integers and reals. If you make the above change and run it, you get:

l := 7
y := 4.0
o := 1
s := 1.0
m := 1.0
e := 1
t := 19/2
p := 19/2
h := 9

which is a solution to the mixed integer/real problem.