2

给定一个像 'x < 10 and x >= 11 or x > 20' 这样的表达式，并且假设已经有一个可用的表达式解析树（例如 [or [ [and [< [var:x] [10] ] [>= [var:x] [11] ] ] [> [var:x] [20] ] ])，我怎样才能找到导致该表达式计算为真的 x 的范围/集合？

对语法的一些限制是：

  1. 表达式中只有一个变量（示例中为 x），因此没有像 x + 2 < y 这样的表达式
  2. 只有比较运算符，但可能是空的？[字符串表达式] 在表达式中
  3. 没有算术表达式或函数调用 - 所以像 x + 2 < 3 或 x < someFunc() 这样的事情是不可能的
4

2 回答 2

1

SMT 求解器的一个简单替代方案是：

  1. 提取表达式中使用的所有数字
  2. 对数字列表进行排序
  3. 对于列表 x 中的每个点，计算 x-eps、x 和 x+eps 处的表达式（其中 eps 是一个小数）

表达式的值只能在这些点发生变化，并且由于它们是按排序顺序排列的，因此您只需将结果连接在一起即可找到 x 允许值的完整列表。

于 2013-02-25T21:48:56.840 回答
0

听起来像 Yices 或 Z3 这样的 SMT 求解器会为您提供帮助。对于您的问题，它们是一种“大枪”，但应该可以解决问题。SMT求解器就像类固醇上的SAT求解器，您所拥有的实际上是使用非布尔变量的可满足性问题。

于 2013-02-25T21:34:24.520 回答