mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 12:58:44 +00:00
Code Activity

#5545

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-20 13:57:34 -07:00
parent 1352aa06f3
commit 2c266a96c8
3 changed files with 27 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/sat/smt/array_axioms.cpp
View file

@ -532,19 +532,22 @@ namespace array {
if (!get_config().m_array_delay_exp_axiom) if (!get_config().m_array_delay_exp_axiom)
return false; return false;
unsigned num_vars = get_num_vars(); unsigned num_vars = get_num_vars();
bool change = false;
for (unsigned v = 0; v < num_vars; v++) { for (unsigned v = 0; v < num_vars; v++) {
propagate_parent_select_axioms(v); propagate_parent_select_axioms(v);
auto& d = get_var_data(v); auto& d = get_var_data(v);
if (!d.m_prop_upward) if (!d.m_prop_upward)
continue; continue;
euf::enode* n = var2enode(v); euf::enode* n = var2enode(v);
if (add_as_array_eqs(n))
change = true;
bool has_default = false; bool has_default = false;
for (euf::enode* p : euf::enode_parents(n)) for (euf::enode* p : euf::enode_parents(n))
has_default |= a.is_default(p->get_expr()); has_default |= a.is_default(p->get_expr());
if (has_default) if (has_default)
propagate_parent_default(v); propagate_parent_default(v);
} }
bool change = false;
unsigned sz = m_axiom_trail.size(); unsigned sz = m_axiom_trail.size();
m_delay_qhead = 0; m_delay_qhead = 0;
@ -557,6 +560,27 @@ namespace array {
return change; return change;
} }
bool solver::add_as_array_eqs(euf::enode* n) {
func_decl* f = nullptr;
bool change = false;
if (!a.is_as_array(n->get_expr(), f))
return false;
for (unsigned i = 0; i < ctx.get_egraph().enodes_of(f).size(); ++i) {
euf::enode* p = ctx.get_egraph().enodes_of(f)[i];
expr_ref_vector select(m);
select.push_back(n->get_expr());
for (expr* arg : *to_app(p->get_expr()))
select.push_back(arg);
expr_ref _e(a.mk_select(select.size(), select.data()), m);
euf::enode* e = e_internalize(_e);
if (e->get_root() != p->get_root()) {
add_unit(eq_internalize(_e, p->get_expr()));
change = true;
}
}
return change;
}
bool solver::add_interface_equalities() { bool solver::add_interface_equalities() {
sbuffer<theory_var> roots; sbuffer<theory_var> roots;
collect_defaults(); collect_defaults();

1
src/sat/smt/array_solver.h
View file

@ -184,6 +184,7 @@ namespace array {
bool assert_default_store_axiom(app* store); bool assert_default_store_axiom(app* store);
bool assert_congruent_axiom(expr* e1, expr* e2); bool assert_congruent_axiom(expr* e1, expr* e2);
bool add_delayed_axioms(); bool add_delayed_axioms();
bool add_as_array_eqs(euf::enode* n);
bool has_unitary_domain(app* array_term); bool has_unitary_domain(app* array_term);
bool has_large_domain(expr* array_term); bool has_large_domain(expr* array_term);

2
src/sat/smt/euf_solver.cpp
View file

@ -869,7 +869,7 @@ namespace euf {
if (b != sat::null_bool_var) { if (b != sat::null_bool_var) {
m_bool_var2expr.setx(b, n->get_expr(), nullptr); m_bool_var2expr.setx(b, n->get_expr(), nullptr);
SASSERT(r->m.is_bool(n->get_sort())); SASSERT(r->m.is_bool(n->get_sort()));
IF_VERBOSE(1, verbose_stream() << "set bool_var " << r->bpp(n) << "\n"); IF_VERBOSE(11, verbose_stream() << "set bool_var " << r->bpp(n) << "\n");
} }
} }
for (auto* s_orig : m_id2solver) { for (auto* s_orig : m_id2solver) {