mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

#6112

Browse source 
add q->get_qid() to comparison of quantifiers
This commit is contained in:
Nikolaj Bjorner 2022-07-05 13:17:04 -07:00
parent a251595467
commit 6e53621146
1 changed files with 23 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

42
src/ast/ast.cpp
View file

@ -471,26 +471,30 @@ bool compare_nodes(ast const * n1, ast const * n2) {
return return
to_var(n1)->get_idx() == to_var(n2)->get_idx() && to_var(n1)->get_idx() == to_var(n2)->get_idx() &&
to_var(n1)->get_sort() == to_var(n2)->get_sort(); to_var(n1)->get_sort() == to_var(n2)->get_sort();
case AST_QUANTIFIER: case AST_QUANTIFIER: {
quantifier const* q1 = to_quantifier(n1);
quantifier const* q2 = to_quantifier(n2);
return return
to_quantifier(n1)->get_kind() == to_quantifier(n2)->get_kind() && q1->get_kind() == q2->get_kind() &&
to_quantifier(n1)->get_num_decls() == to_quantifier(n2)->get_num_decls() && q1->get_num_decls() == q2->get_num_decls() &&
compare_arrays(to_quantifier(n1)->get_decl_sorts(), compare_arrays(q1->get_decl_sorts(),
to_quantifier(n2)->get_decl_sorts(), q2->get_decl_sorts(),
to_quantifier(n1)->get_num_decls()) && q1->get_num_decls()) &&
compare_arrays(to_quantifier(n1)->get_decl_names(), compare_arrays(q1->get_decl_names(),
to_quantifier(n2)->get_decl_names(), q2->get_decl_names(),
to_quantifier(n1)->get_num_decls()) && q1->get_num_decls()) &&
to_quantifier(n1)->get_expr() == to_quantifier(n2)->get_expr() && q1->get_expr() == q2->get_expr() &&
to_quantifier(n1)->get_weight() == to_quantifier(n2)->get_weight() && q1->get_weight() == q2->get_weight() &&
to_quantifier(n1)->get_num_patterns() == to_quantifier(n2)->get_num_patterns() && q1->get_num_patterns() == q2->get_num_patterns() &&
compare_arrays(to_quantifier(n1)->get_patterns(), q1->get_qid() == q2->get_qid() &&
to_quantifier(n2)->get_patterns(), compare_arrays(q1->get_patterns(),
to_quantifier(n1)->get_num_patterns()) && q2->get_patterns(),
to_quantifier(n1)->get_num_no_patterns() == to_quantifier(n2)->get_num_no_patterns() && q1->get_num_patterns()) &&
compare_arrays(to_quantifier(n1)->get_no_patterns(), q1->get_num_no_patterns() == q2->get_num_no_patterns() &&
to_quantifier(n2)->get_no_patterns(), compare_arrays(q1->get_no_patterns(),
to_quantifier(n1)->get_num_no_patterns()); q2->get_no_patterns(),
q1->get_num_no_patterns());
}
default: default:
UNREACHABLE(); UNREACHABLE();
} }