【问题标题】：Find values which make binary expression evaluate to true查找使二进制表达式计算为真的值
【发布时间】：2013-02-25 21:31:05
【问题描述】：
给定一个像'x = 11 or x > 20'这样的表达式，并且假设已经有一个可用的表达式解析树（例如[或[ [and [= [var:x] [11] ] ] [> [var:x] [20] ] ])，我怎样才能找到导致这个表达式计算为真的 x 的范围/集合？
对语法的一些限制是：
- 表达式中只有一个变量（示例中为 x），因此没有像 x + 2 这样的表达式
- 只有比较运算符，但可以是空的吗？ [字符串表达式] 在表达式中
- 没有算术表达式或函数调用 - 所以像 x + 2
【问题讨论】：
标签：
algorithm
parsing
expression
【解决方案1】：
SMT 求解器的一个简单替代方案是：
- 提取表达式中使用的所有数字
- 对数字列表进行排序
- 对于列表 x 中的每个点，计算 x-eps、x 和 x+eps 处的表达式（其中 eps 是一个小数）
表达式的值只能在这些点发生变化，并且由于它们是按排序顺序排列的，您只需将结果连接在一起即可找到 x 允许值的完整列表。
【解决方案2】：
听起来像 Yices 或 Z3 这样的 SMT 求解器会为您提供帮助。对于您的问题，它们是一种“大枪”，但应该可以解决问题。 SMT 求解器类似于 SAT 求解器，实际上是使用非布尔变量的可满足性问题。