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

redoing arrays

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-12-31 15:51:52 -08:00
parent aa901c4e88
commit 0ef0ed3b94
7 changed files with 61 additions and 52 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -517,13 +517,14 @@ namespace array {
unsigned num_vars = get_num_vars(); unsigned num_vars = get_num_vars();
bool change = false; bool change = false;
for (unsigned v = 0; v < num_vars; v++) { for (unsigned v = 0; v < num_vars; 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 (!ctx.is_relevant(n)) if (!ctx.is_relevant(n))
continue; continue;
for (euf::enode* lambda : d.m_parent_lambdas)
propagate_select_axioms(d, lambda);
if (add_as_array_eqs(n)) if (add_as_array_eqs(n))
change = true; change = true;
bool has_default = false; bool has_default = false;

36
src/sat/smt/array_internalize.cpp
View file

@ -49,7 +49,7 @@ namespace array {
if (v == euf::null_theory_var) { if (v == euf::null_theory_var) {
mk_var(n); mk_var(n);
if (is_lambda(n->get_expr())) if (is_lambda(n->get_expr()))
internalize_eh_lambda(n); internalize_lambda_eh(n);
} }
} }
@ -91,18 +91,13 @@ namespace array {
return true; return true;
} }
void solver::internalize_eh_lambda(euf::enode* n) { void solver::internalize_lambda_eh(euf::enode* n) {
SASSERT(is_lambda(n->get_expr()) || a.is_const(n->get_expr()) || a.is_map(n->get_expr()) || a.is_as_array(n->get_expr()));
theory_var v = n->get_th_var(get_id());
push_axiom(default_axiom(n)); push_axiom(default_axiom(n));
add_lambda(v, n); auto& d = get_var_data(find(n));
ctx.push_vec(d.m_lambdas, n);
} }
void solver::internalize_eh(euf::enode* n) { void solver::internalize_eh(euf::enode* n) {
if (is_lambda(n->get_expr())) {
internalize_eh_lambda(n);
return;
}
switch (n->get_decl()->get_decl_kind()) { switch (n->get_decl()->get_decl_kind()) {
case OP_STORE: case OP_STORE:
push_axiom(store_axiom(n)); push_axiom(store_axiom(n));
@ -111,20 +106,19 @@ namespace array {
break; break;
case OP_AS_ARRAY: case OP_AS_ARRAY:
case OP_CONST_ARRAY: case OP_CONST_ARRAY:
internalize_eh_lambda(n); internalize_lambda_eh(n);
// SASSERT(!get_var_data(n->get_th_var(get_id())).m_prop_upward);
break; break;
case OP_ARRAY_EXT: case OP_ARRAY_EXT:
SASSERT(is_array(n->get_arg(0))); SASSERT(is_array(n->get_arg(0)));
push_axiom(extensionality_axiom(n->get_arg(0), n->get_arg(1))); push_axiom(extensionality_axiom(n->get_arg(0), n->get_arg(1)));
break; break;
case OP_ARRAY_DEFAULT: case OP_ARRAY_DEFAULT:
add_parent_default(n->get_arg(0)->get_th_var(get_id()), n); add_parent_default(find(n->get_arg(0)), n);
break; break;
case OP_ARRAY_MAP: case OP_ARRAY_MAP:
for (auto* arg : euf::enode_args(n)) for (auto* arg : euf::enode_args(n))
add_parent_lambda(arg->get_th_var(get_id()), n); add_parent_lambda(find(arg), n);
internalize_eh_lambda(n); internalize_lambda_eh(n);
break; break;
case OP_SET_UNION: case OP_SET_UNION:
case OP_SET_INTERSECT: case OP_SET_INTERSECT:
@ -143,7 +137,7 @@ namespace array {
void solver::relevant_eh(euf::enode* n) { void solver::relevant_eh(euf::enode* n) {
if (is_lambda(n->get_expr())) { if (is_lambda(n->get_expr())) {
set_prop_upward(n->get_th_var(get_id())); set_prop_upward(find(n));
return; return;
} }
if (!is_app(n->get_expr())) if (!is_app(n->get_expr()))
@ -152,23 +146,25 @@ namespace array {
return; return;
switch (n->get_decl()->get_decl_kind()) { switch (n->get_decl()->get_decl_kind()) {
case OP_STORE: case OP_STORE:
add_parent_lambda(n->get_arg(0)->get_th_var(get_id()), n); add_parent_lambda(find(n->get_arg(0)), n);
break; break;
case OP_SELECT: case OP_SELECT:
add_parent_select(n->get_arg(0)->get_th_var(get_id()), n); add_parent_select(find(n->get_arg(0)), n);
break; break;
case OP_AS_ARRAY:
case OP_CONST_ARRAY: case OP_CONST_ARRAY:
set_prop_upward(n->get_th_var(get_id())); case OP_AS_ARRAY:
set_prop_upward(find(n));
add_parent_default(find(n), n);
break; break;
case OP_ARRAY_EXT: case OP_ARRAY_EXT:
break; break;
case OP_ARRAY_DEFAULT: case OP_ARRAY_DEFAULT:
set_prop_upward(n->get_arg(0)->get_th_var(get_id())); set_prop_upward(find(n->get_arg(0)));
break; break;
case OP_ARRAY_MAP: case OP_ARRAY_MAP:
for (auto* arg : euf::enode_args(n)) for (auto* arg : euf::enode_args(n))
set_prop_upward_store(arg); set_prop_upward_store(arg);
set_prop_upward(find(n));
break; break;
case OP_SET_UNION: case OP_SET_UNION:
case OP_SET_INTERSECT: case OP_SET_INTERSECT:

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

@ -186,18 +186,17 @@ namespace array {
if (should_set_prop_upward(d)) if (should_set_prop_upward(d))
set_prop_upward(d); set_prop_upward(d);
ctx.push_vec(d.m_lambdas, lambda); ctx.push_vec(d.m_lambdas, lambda);
if (should_set_prop_upward(d)) { propagate_select_axioms(d, lambda);
set_prop_upward_store(lambda); if (should_set_prop_upward(d))
propagate_select_axioms(d, lambda); set_prop_upward_store(lambda);
}
} }
void solver::add_parent_lambda(theory_var v_child, euf::enode* lambda) { void solver::add_parent_lambda(theory_var v_child, euf::enode* lambda) {
SASSERT(can_beta_reduce(lambda)); SASSERT(can_beta_reduce(lambda));
auto& d = get_var_data(find(v_child)); auto& d = get_var_data(find(v_child));
ctx.push_vec(d.m_parent_lambdas, lambda); ctx.push_vec(d.m_parent_lambdas, lambda);
// if (should_set_prop_upward(d)) if (should_prop_upward(d))
// propagate_select_axioms(d, lambda); propagate_select_axioms(d, lambda);
} }
void solver::add_parent_default(theory_var v, euf::enode* def) { void solver::add_parent_default(theory_var v, euf::enode* def) {
@ -227,12 +226,13 @@ namespace array {
return; return;
auto& d = get_var_data(v); auto& d = get_var_data(v);
if (!d.m_prop_upward)
return;
for (euf::enode* lambda : d.m_lambdas) for (euf::enode* lambda : d.m_lambdas)
propagate_select_axioms(d, lambda); propagate_select_axioms(d, lambda);
if (!should_prop_upward(d))
return;
for (euf::enode* lambda : d.m_parent_lambdas) for (euf::enode* lambda : d.m_parent_lambdas)
propagate_select_axioms(d, lambda); propagate_select_axioms(d, lambda);
} }

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

@ -66,6 +66,7 @@ namespace array {
array_union_find m_find; array_union_find m_find;
theory_var find(theory_var v) { return m_find.find(v); } theory_var find(theory_var v) { return m_find.find(v); }
theory_var find(euf::enode* n) { return find(n->get_th_var(get_id())); }
func_decl_ref_vector const& sort2diff(sort* s); func_decl_ref_vector const& sort2diff(sort* s);
// internalize // internalize
@ -73,8 +74,8 @@ namespace array {
bool visited(expr* e) override; bool visited(expr* e) override;
bool post_visit(expr* e, bool sign, bool root) override; bool post_visit(expr* e, bool sign, bool root) override;
void ensure_var(euf::enode* n); void ensure_var(euf::enode* n);
void internalize_eh_lambda(euf::enode* n);
void internalize_eh(euf::enode* n); void internalize_eh(euf::enode* n);
void internalize_lambda_eh(euf::enode* n);
// axioms // axioms
struct axiom_record { struct axiom_record {
@ -192,7 +193,7 @@ namespace array {
// solving // solving
void add_parent_select(theory_var v_child, euf::enode* select); void add_parent_select(theory_var v_child, euf::enode* select);
void add_parent_default(theory_var v_child, euf::enode* def); void add_parent_default(theory_var v_child, euf::enode* def);
void add_lambda(theory_var v, euf::enode* lambda); void add_lambda(theory_var v, euf::enode* lambda);
void add_parent_lambda(theory_var v_child, euf::enode* lambda); void add_parent_lambda(theory_var v_child, euf::enode* lambda);
void propagate_select_axioms(var_data const& d, euf::enode* a); void propagate_select_axioms(var_data const& d, euf::enode* a);
@ -227,8 +228,6 @@ namespace array {
void set_else(theory_var v, expr* e); void set_else(theory_var v, expr* e);
expr* get_else(theory_var v); expr* get_else(theory_var v);
void internalized(euf::enode* n);
// diagnostics // diagnostics
std::ostream& display_info(std::ostream& out, char const* id, euf::enode_vector const& v) const; std::ostream& display_info(std::ostream& out, char const* id, euf::enode_vector const& v) const;
std::ostream& display(std::ostream& out, axiom_record const& r) const; std::ostream& display(std::ostream& out, axiom_record const& r) const;

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

@ -298,12 +298,9 @@ namespace euf {
void solver::asserted(literal l) { void solver::asserted(literal l) {
if (m_relevancy.enabled() && !m_relevancy.is_relevant(l)) { if (m_relevancy.enabled() && !m_relevancy.is_relevant(l)) {
if (s().lvl(l) <= s().search_lvl()) m_relevancy.asserted(l);
mark_relevant(l); if (!m_relevancy.is_relevant(l))
else {
m_relevancy.asserted(l);
return; return;
}
} }
expr* e = m_bool_var2expr.get(l.var(), nullptr); expr* e = m_bool_var2expr.get(l.var(), nullptr);

42
src/sat/smt/smt_relevant.cpp
View file

@ -241,19 +241,35 @@ namespace smt {
} }
void relevancy::propagate_relevant(euf::enode* n) { void relevancy::propagate_relevant(euf::enode* n) {
m_stack.push_back(n); m_todo.push_back(n);
while (!m_stack.empty()) { while (!m_todo.empty()) {
n = m_stack.back(); n = m_todo.back();
unsigned sz = m_stack.size(); m_todo.pop_back();
for (euf::enode* arg : euf::enode_args(n)) if (n->is_relevant())
if (!arg->is_relevant()) continue;
m_stack.push_back(arg); if (ctx.get_si().is_bool_op(n->get_expr()))
if (sz == m_stack.size()) { continue;
ctx.get_egraph().set_relevant(n); m_stack.push_back(n);
relevant_eh(n); while (!m_stack.empty()) {
for (euf::enode* sib : euf::enode_class(n)) n = m_stack.back();
if (!sib->is_relevant()) unsigned sz = m_stack.size();
mark_relevant(sib); for (euf::enode* arg : euf::enode_args(n))
if (!arg->is_relevant())
m_stack.push_back(arg);
if (sz != m_stack.size())
continue;
if (!n->is_relevant()) {
ctx.get_egraph().set_relevant(n);
relevant_eh(n);
for (euf::enode* sib : euf::enode_class(n))
if (!sib->is_relevant())
m_todo.push_back(sib);
}
if (!ctx.get_manager().inc()) {
m_todo.reset();
m_stack.reset();
return;
}
m_stack.pop_back(); m_stack.pop_back();
} }
} }

2
src/sat/smt/smt_relevant.h
View file

@ -119,7 +119,7 @@ namespace smt {
vector<unsigned_vector> m_occurs; // where do literals occur vector<unsigned_vector> m_occurs; // where do literals occur
unsigned m_qhead = 0; // queue head for relevancy unsigned m_qhead = 0; // queue head for relevancy
svector<std::pair<sat::literal, euf::enode*>> m_queue; // propagation queue for relevancy svector<std::pair<sat::literal, euf::enode*>> m_queue; // propagation queue for relevancy
euf::enode_vector m_stack; euf::enode_vector m_stack, m_todo;
// callbacks during propagation // callbacks during propagation
void relevant_eh(euf::enode* n); void relevant_eh(euf::enode* n);