【发布时间】：2014-09-26 23:01:57
【问题描述】：
在我的代码中添加约束时，我发现我必须多次将相同的约束添加到表达式向量中。是否有任何 API 可以检测两个表达式是否完全相同，以便我可以删除多余的表达式？
【问题讨论】：
标签： z3
【发布时间】：2014-09-26 23:01:57
【问题描述】：
表达式总是被内化为唯一的指针。因此，如果您使用相同的子表达式构建两个表达式，则指向它们的指针将相同。您可以简单地使用指针相等。
表达式也有所谓的“标识符”。获取标识符的 C 调用称为 Z3_ast_get_id，其他编程语言的其他 API 中有相应的调用 （在 C++ 中你仍然必须使用 Z3_ast_get_id，在 C# 和 Java 中，它被称为“Id”/“id”）。
【讨论】：
-
还有一个问题，我注意到 Z3_get_ast_id 的返回类型是无符号的，所以有 2^32 个 id。两个表达式是否有可能具有相同的 id，因为我猜可能有超过 2^32 个表达式？