mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

#5379

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-07-06 18:58:27 +02:00
parent af5b2a4179
commit c2595b9bc8
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/ast/ast.cpp
View file

@ -559,10 +559,11 @@ unsigned get_node_hash(ast const * n) {
return to_sort(n)->get_name().hash();
else
return combine_hash(to_sort(n)->get_name().hash(), to_sort(n)->get_info()->hash());
case AST_FUNC_DECL:
case AST_FUNC_DECL: {
unsigned h = combine_hash(to_func_decl(n)->get_name().hash(), to_func_decl(n)->get_range()->hash());
return ast_array_hash(to_func_decl(n)->get_domain(), to_func_decl(n)->get_arity(),
to_func_decl(n)->get_info() == nullptr ?
to_func_decl(n)->get_name().hash() : combine_hash(to_func_decl(n)->get_name().hash(), to_func_decl(n)->get_info()->hash()));
combine_hash(h, to_func_decl(n)->get_info() == nullptr ? 0 : to_func_decl(n)->get_info()->hash()));
}
case AST_APP:
return ast_array_hash(to_app(n)->get_args(),
to_app(n)->get_num_args(),