如何使用pysmt同时计算同时包含整数和实数的公式

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

此代码将显示：PysmtTypeError: The Formula

((h + e + l + l + o) = (p + y + s + m + t))

is not well-formed.

Answer 1

SMTLib/z3 是类型语言（与 Python 不同）。这意味着您无法将整数与实数值进行比较：这是类型不匹配。特别是，混合这些类型可能会导致无法判定的问题。 （稍后会详细介绍。）

为了使您的程序类型正确，您应该通过更改方程式将整数转换为实数：

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

至：

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

从整数到实数的转换是通过 ToReal 函数实现的。一般来说，这样的转换会使问题变得复杂：也就是说，一旦使用

ToReal

，问题就不再是在逻辑的可判定片段中。 （准确地说，实数算术是可判定的，但是如果您将通过从

Int

到

ToReal

转换而获得的问题放入其中，则逻辑变得半可判定。这是因为您可以以其他方式求解任意丢番图方程，即已知是不可判定的。但这也许超出了本次讨论的重点。）

幸运的是，即使混合整数和实数，您的问题也足够简单，求解器可以处理。如果您进行上述更改并运行它，您将得到：

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

这是混合整数/实数问题的解决方案。