mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

#5429

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-07-30 15:34:12 -07:00
parent 31267e6ab8
commit 1488bf81ae
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -174,6 +174,7 @@ namespace array {
ctx.push_vec(get_var_data(v_child).m_parent_selects, select);
euf::enode* child = var2enode(v_child);
TRACE("array", tout << "v" << v_child << " - " << ctx.bpp(select) << " " << ctx.bpp(child) << " prop: " << should_prop_upward(get_var_data(v_child)) << "\n";);
TRACE("array", tout << "can beta reduce " << can_beta_reduce(child) << "\n";);
if (can_beta_reduce(child))
push_axiom(select_axiom(select, child));
propagate_parent_select_axioms(v_child);
@ -227,6 +228,12 @@ namespace array {
auto& d = get_var_data(v);
for (euf::enode* lambda : d.m_lambdas) {
expr* e = lambda->get_expr();
if (a.is_const(e) || a.is_map(e))
propagate_select_axioms(d, lambda);
}
for (euf::enode* lambda : d.m_parent_lambdas)
propagate_select_axioms(d, lambda);
}