Z3_get_ast_id的Z3意义

Question

我想知道Z3_get_ast_id()的语义。什么时候两个表达式会有相同的id？如果两个表达式是使用相同的上下文和相同的参数和操作码创建的，那么id是否相同？

我还看到有Z3_get_ast_hash()。也请告诉我这个函数的语义。

Answer 1

    The identifier is unique up to structural equality. Thus, two ast nodes
    created by the same context and having the same children and same function symbols
    have the same identifiers. Ast nodes created in the same context, but having
    different children or different functions have different identifiers.
    Variables and quantifiers are also assigned different identifiers according to
    their structure.        

您可以将Z3_get_ast_id与Z3_get_ast_hash互换使用