Z3检查两个表达式是否相同

Question

在我的代码中添加约束时，我发现我必须将相同的约束添加到表达式向量中多次。是否有任何API来检测两个表达式是否完全相同，以便我可以删除多余的表达式？

Answer 1

表达式总是内化为唯一的指针。因此，如果使用相同的子表达式构建两个表达式，则指向它们的指针将相同。你可以简单地使用指针相等。

表达式也有所谓的“标识符”。获取标识符的C调用称为Z3_ast_get_id，其他编程语言中有相应的调用 （来自C++，您仍然需要使用来自C＃和Java的Z3_ast_get_id，它被称为“Id”/“id”）。