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

Question

假设我有两个约束(c1,c2),我想检查它们是否语法相同:

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

选项1:我们可以把这变成一个可满足性问题,就像这篇文章: 两个boolexpr是否相等

选项2:我们也可以将它们变成字符串并比较相等:

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

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

两个问题:

1. 如何在Z3(Java版本)中检查两个约束在语法上是否完全相同？

2. 如果我们没有1的好解决方案,我正在考虑为Expr对象编写一个包装器并使用工厂方法来避免从Z3生成重复(语法)对象.然后我必须设计自己的equal()和hashCode()函数.但到目前为止,我仍然无法找到一种有效的方法.

Answer 1

Expr 类派生自 AST，它具有用于此目的的equals、compareTo、 和hashCode函数。由于 Z3 使用散列 consing，因此非常高效，本质上只是指针的比较（以及 Java 中的强制转换）。