mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

move has-default up before merge of parents

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-09-24 14:40:30 -07:00
parent aadb1a2d44
commit 6f2fde87d1
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/sat/smt/array_solver.cpp
View file

@ -164,6 +164,10 @@ namespace array {
auto& d2 = get_var_data(v2); auto& d2 = get_var_data(v2);
if (d2.m_prop_upward && !d1.m_prop_upward) if (d2.m_prop_upward && !d1.m_prop_upward)
set_prop_upward(v1); set_prop_upward(v1);
if (d1.m_has_default && !d2.m_has_default)
add_parent_default(v2);
if (!d1.m_has_default && d2.m_has_default)
add_parent_default(v1);
for (euf::enode* lambda : d2.m_lambdas) for (euf::enode* lambda : d2.m_lambdas)
add_lambda(v1, lambda); add_lambda(v1, lambda);
for (euf::enode* lambda : d2.m_parent_lambdas) for (euf::enode* lambda : d2.m_parent_lambdas)
@ -172,10 +176,6 @@ namespace array {
add_parent_select(v1, select); add_parent_select(v1, select);
if (is_lambda(e1) || is_lambda(e2)) if (is_lambda(e1) || is_lambda(e2))
push_axiom(congruence_axiom(n1, n2)); push_axiom(congruence_axiom(n1, n2));
if (d1.m_has_default && !d2.m_has_default)
add_parent_default(v2);
if (!d1.m_has_default && d2.m_has_default)
add_parent_default(v1);
} }
void solver::add_parent_select(theory_var v_child, euf::enode* select) { void solver::add_parent_select(theory_var v_child, euf::enode* select) {