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