java在Z3中有效地检查两个约束的语法等价性

Question

假设我有两个约束（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

但随着约束规模的增加，这两种选择都会带来巨大的开销。e、 g.在Expr中调用toString（）方法对于大型约束非常昂贵

两个问题：

1. 如何在Z3（Java版本）中有效地检查两个约束在语法上是否相同

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

Answer 1

Expr类派生自AST，它有equals、compareTo和hashCode函数用于此目的。因为Z3使用了hash consing，所以这是非常有效的，基本上只是比较指针（在Java中是一个cast）