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