如何使用PySMT同时计算包含整数与实数的公式？

AI 小北

2026-7-2

解决PySMT中整数与实数类型不兼容的公式错误

你遇到的PysmtTypeError是因为PySMT是强类型约束的SMT工具，不允许直接比较或运算不同类型的表达式。你的代码里sum_hello是整数（INT）类型的求和结果，sum_pysmt是实数（REAL）类型，直接用Equals把两者放在一起违反了类型一致性要求。

解决方法

需要将整数类型的表达式转换为实数类型，使用PySMT提供的ToReal()函数，让比较两边的类型统一为REAL。同时，整数求和结果与Int(25)的比较可以保留原类型，确保类型匹配。

修改后的完整代码

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_int = Plus(hello)  # 整数类型的求和结果
sum_hello_real = ToReal(sum_hello_int)  # 转换为实数类型
sum_pysmt = Plus(pysmt)  # 实数类型的求和结果

# 拆分条件：同类型表达式之间进行比较
problem = And(Equals(sum_hello_int, Int(25)),
              Equals(sum_hello_real, sum_pysmt))
formula = And(domains_1, domains_2, problem)

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

model = get_model(formula, solver_name="z3")
if model:
    print("\nFound solution:")
    for sym in hello + pysmt:
        print(f"{sym} = {model.get_value(sym)}")
else:
    print("No solution found")