mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

ast compare_nodes: fail faster when comparing quantifier expressions

Browse source
This commit is contained in:
Nuno Lopes 2023-08-20 14:09:04 +01:00
parent c469c6e1d5
commit 8210aafb69
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/ast.cpp
View file

@ -479,15 +479,15 @@ bool compare_nodes(ast const * n1, ast const * n2) {
return
q1->get_kind() == q2->get_kind() &&
q1->get_num_decls() == q2->get_num_decls() &&
q1->get_expr() == q2->get_expr() &&
q1->get_weight() == q2->get_weight() &&
q1->get_num_patterns() == q2->get_num_patterns() &&
compare_arrays(q1->get_decl_sorts(),
q2->get_decl_sorts(),
q1->get_num_decls()) &&
compare_arrays(q1->get_decl_names(),
q2->get_decl_names(),
q1->get_num_decls()) &&
q1->get_expr() == q2->get_expr() &&
q1->get_weight() == q2->get_weight() &&
q1->get_num_patterns() == q2->get_num_patterns() &&
((q1->get_qid().is_numerical() && q2->get_qid().is_numerical()) ||
(q1->get_qid() == q2->get_qid())) &&
compare_arrays(q1->get_patterns(),