时间戳

首页 > 解决方案 > z3py：符号表达式不能转换为具体的布尔值？

python - z3py：符号表达式不能转换为具体的布尔值？

问题描述

from z3 import *
x = Real('x')
s = Solver()
s.add(x > 1 or x < -1)
print(s.check())
if s.check() == sat:
    print(s.model())

我想解决一个或表达式，我该怎么做？当 z3 告诉我“符号表达式不能转换为具体的布尔值”时

标签： pythonz3smtz3py

解决方案

Pythonor没有符号意识。相反，使用z3py's Or：

from z3 import *
x = Real('x')
s = Solver()
s.add(Or(x > 1, x < -1))
r = s.check()
print(r)
if r == sat:
    print(s.model())

这打印：

sat
[x = -2]

请注意，我还可以check通过首先将结果存储在变量中来避免对 的两次单独调用。（我在上面调用r过。）一般来说，第二次调用check会很便宜，因为你没有在第一次之后添加任何约束，但这使得意图更清晰。

推荐阅读