在 Z3 中有效地检查两个约束的句法等价答案

【问题标题】：Checking syntactic equivalence of two constraints efficiently in Z3在 Z3 中有效地检查两个约束的句法等价
【发布时间】：2014-08-11 20:33:44
【问题描述】：

假设我有两个约束（c1，c2），我想检查它们是否语法相同：

c1: f(x)>1 && g(y)=2
c2: f(x)>1 && g(y)=2

选项 1：我们可以把它变成一个可满足性问题，就像这篇文章： Whether two boolexpr are equal

选项 2：我们也可以把它们变成字符串并比较相等性：

if(c1.toString().equals(c2.toString()))
    ///do somthing

但是随着约束大小的增加，这两个选项都会产生很大的开销。例如在 Expr 中调用 toString() 方法对于大型约束非常昂贵。

两个问题：

如何在Z3(Java版)中高效地检查两个约束在语法上是否相同？
如果我们对 1 没有好的解决方案，我正在考虑为 Expr 对象编写一个包装器并使用工厂方法来避免从 Z3 生成重复的（语法上）对象.然后我必须设计自己的 equal() 和 hashCode() 函数。但到目前为止我仍然想不出一个有效的方法。

【问题讨论】：

标签： java performance z3

【解决方案1】：

Expr 类派生自 AST，它具有用于此目的的 equals、compareTo 和 hashCode 函数。由于 Z3 使用了 hash consing，这非常有效，本质上只是比较指针（在 Java 中是一个强制转换）。

【讨论】：

非常感谢。我假设 AST 的 equals() 方法只检查两个实例是否完全相同。愚蠢的我。

【解决方案2】：

不是真正的答案，但评论太长了。

在 Expr 中调用 toString() 方法对于大型约束非常昂贵。

我建议查看toString 实现。它速度慢的一个可能原因是：愚蠢的字符串连接而不是使用StringBuilder。如果是这样，那么您可能希望提供更快的实现。但是，无论如何，解决打印时间过长的 CSP 是徒劳的。

如何在 Z3 中有效地检查两个约束在语法上是否相同

我敢打赌，使用 toString 不是可行的方法，因为 a && b 和 b && a 是等价的，但它们的字符串表示不是。

您可能需要使用交换性、关联性以及其他规则来规范化表达式。为此，您需要在条款上进行一些任意但equals-一致的排序。

您肯定不想检查所有成对的约束是否相等。在这里，根据哈希码将约束放入桶中会有所帮助。不知道，如果提供的hashCode 可用于此目的。

然后我必须设计自己的 equal() 和 hashCode() 函数。但到目前为止我仍然想不出一个有效的方法。

标准化后应该相当简单。如果您因此进行规范化并将每个表达式映射到规范表示（就像String#intern 所做的那样），那么您可以对equals 使用引用相等。对于hashCode，您需要每个树节点的组合公式，例如，您可以将a && b 的哈希码计算为f(111 * ha + hb)，其中ha 和hb 是a 和@987654336 的哈希码@ 分别是 f(x) = x ^ (x>>15) 或类似的东西。

【讨论】：