mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-27 05:26:01 +00:00
Code Activity

axiom solver improvements

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-12-31 11:53:40 -08:00
parent 79f0ceac4c
commit aa901c4e88
8 changed files with 98 additions and 75 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -537,8 +537,8 @@ namespace array {
m_delay_qhead = 0;
for (; m_delay_qhead < sz; ++m_delay_qhead)
if (m_axiom_trail[m_delay_qhead].is_delayed() && assert_axiom(m_delay_qhead))
change = true;
if (m_axiom_trail[m_delay_qhead].is_delayed() && assert_axiom(m_delay_qhead))
change = true;
flet<bool> _enable_delay(m_enable_delay, false);
if (unit_propagate())
change = true;
@ -561,7 +561,8 @@ namespace array {
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()));
sat::literal eq = eq_internalize(_e, p->get_expr());
add_unit(eq);
change = true;
}
}

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

@ -49,7 +49,7 @@ namespace array {
if (v == euf::null_theory_var) {
mk_var(n);
if (is_lambda(n->get_expr()))
internalize_lambda(n);
internalize_eh_lambda(n);
}
}
@ -57,46 +57,6 @@ namespace array {
ensure_var(n);
}
void solver::internalize_store(euf::enode* n) {
//std::cout << "store th-var " << n->get_th_var(get_id()) << "\n";
add_parent_lambda(n->get_arg(0)->get_th_var(get_id()), n);
push_axiom(store_axiom(n));
add_lambda(n->get_th_var(get_id()), n);
SASSERT(!get_var_data(n->get_th_var(get_id())).m_prop_upward);
}
void solver::internalize_map(euf::enode* n) {
for (auto* arg : euf::enode_args(n)) {
add_parent_lambda(arg->get_th_var(get_id()), n);
set_prop_upward(arg);
}
push_axiom(default_axiom(n));
add_lambda(n->get_th_var(get_id()), n);
//SASSERT(!get_var_data(n->get_th_var(get_id())).m_prop_upward);
}
void solver::internalize_lambda(euf::enode* n) {
SASSERT(is_lambda(n->get_expr()) || a.is_const(n->get_expr()) || a.is_as_array(n->get_expr()));
theory_var v = n->get_th_var(get_id());
push_axiom(default_axiom(n));
add_lambda(v, n);
set_prop_upward(v);
}
void solver::internalize_select(euf::enode* n) {
add_parent_select(n->get_arg(0)->get_th_var(get_id()), n);
}
void solver::internalize_ext(euf::enode* n) {
SASSERT(is_array(n->get_arg(0)));
push_axiom(extensionality_axiom(n->get_arg(0), n->get_arg(1)));
}
void solver::internalize_default(euf::enode* n) {
add_parent_default(n->get_arg(0)->get_th_var(get_id()), n);
set_prop_upward(n);
}
bool solver::visited(expr* e) {
euf::enode* n = expr2enode(e);
return n && n->is_attached_to(get_id());
@ -125,35 +85,90 @@ namespace array {
mk_var(n);
for (auto* arg : euf::enode_args(n))
ensure_var(arg);
internalize_eh(n);
if (ctx.is_relevant(n) || !ctx.relevancy().enabled())
relevant_eh(n);
return true;
}
void solver::internalize_eh_lambda(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));
add_lambda(v, 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()) {
case OP_STORE:
push_axiom(store_axiom(n));
break;
case OP_SELECT:
break;
case OP_AS_ARRAY:
case OP_CONST_ARRAY:
internalize_eh_lambda(n);
// SASSERT(!get_var_data(n->get_th_var(get_id())).m_prop_upward);
break;
case OP_ARRAY_EXT:
SASSERT(is_array(n->get_arg(0)));
push_axiom(extensionality_axiom(n->get_arg(0), n->get_arg(1)));
break;
case OP_ARRAY_DEFAULT:
add_parent_default(n->get_arg(0)->get_th_var(get_id()), n);
break;
case OP_ARRAY_MAP:
for (auto* arg : euf::enode_args(n))
add_parent_lambda(arg->get_th_var(get_id()), n);
internalize_eh_lambda(n);
break;
case OP_SET_UNION:
case OP_SET_INTERSECT:
case OP_SET_DIFFERENCE:
case OP_SET_COMPLEMENT:
case OP_SET_SUBSET:
case OP_SET_HAS_SIZE:
case OP_SET_CARD:
ctx.unhandled_function(n->get_decl());
break;
default:
UNREACHABLE();
break;
}
}
void solver::relevant_eh(euf::enode* n) {
if (is_lambda(n->get_expr())) {
set_prop_upward(n->get_th_var(get_id()));
return;
}
if (!is_app(n->get_expr()))
return;
if (n->get_decl()->get_family_id() != a.get_family_id())
return;
switch (n->get_decl()->get_decl_kind()) {
case OP_STORE:
internalize_store(n);
add_parent_lambda(n->get_arg(0)->get_th_var(get_id()), n);
break;
case OP_SELECT:
internalize_select(n);
add_parent_select(n->get_arg(0)->get_th_var(get_id()), n);
break;
case OP_AS_ARRAY:
case OP_CONST_ARRAY:
internalize_lambda(n);
set_prop_upward(n->get_th_var(get_id()));
break;
case OP_ARRAY_EXT:
internalize_ext(n);
break;
case OP_ARRAY_DEFAULT:
internalize_default(n);
set_prop_upward(n->get_arg(0)->get_th_var(get_id()));
break;
case OP_ARRAY_MAP:
internalize_map(n);
for (auto* arg : euf::enode_args(n))
set_prop_upward_store(arg);
break;
case OP_SET_UNION:
case OP_SET_INTERSECT:

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

@ -187,7 +187,7 @@ namespace array {
set_prop_upward(d);
ctx.push_vec(d.m_lambdas, lambda);
if (should_set_prop_upward(d)) {
set_prop_upward(lambda);
set_prop_upward_store(lambda);
propagate_select_axioms(d, lambda);
}
}
@ -196,8 +196,8 @@ namespace array {
SASSERT(can_beta_reduce(lambda));
auto& d = get_var_data(find(v_child));
ctx.push_vec(d.m_parent_lambdas, lambda);
if (should_set_prop_upward(d))
propagate_select_axioms(d, lambda);
// if (should_set_prop_upward(d))
// propagate_select_axioms(d, lambda);
}
void solver::add_parent_default(theory_var v, euf::enode* def) {
@ -227,6 +227,8 @@ namespace array {
return;
auto& d = get_var_data(v);
if (!d.m_prop_upward)
return;
for (euf::enode* lambda : d.m_lambdas)
propagate_select_axioms(d, lambda);
@ -246,14 +248,14 @@ namespace array {
set_prop_upward(d);
}
void solver::set_prop_upward(euf::enode* n) {
void solver::set_prop_upward_store(euf::enode* n) {
if (a.is_store(n->get_expr()))
set_prop_upward(n->get_arg(0)->get_th_var(get_id()));
}
void solver::set_prop_upward(var_data& d) {
for (auto* p : d.m_lambdas)
set_prop_upward(p);
set_prop_upward_store(p);
}
/**

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

@ -73,12 +73,8 @@ namespace array {
bool visited(expr* e) override;
bool post_visit(expr* e, bool sign, bool root) override;
void ensure_var(euf::enode* n);
void internalize_store(euf::enode* n);
void internalize_select(euf::enode* n);
void internalize_lambda(euf::enode* n);
void internalize_ext(euf::enode* n);
void internalize_default(euf::enode* n);
void internalize_map(euf::enode* n);
void internalize_eh_lambda(euf::enode* n);
void internalize_eh(euf::enode* n);
// axioms
struct axiom_record {
@ -205,7 +201,7 @@ namespace array {
void set_prop_upward(theory_var v);
void set_prop_upward(var_data& d);
void set_prop_upward(euf::enode* n);
void set_prop_upward_store(euf::enode* n);
unsigned get_lambda_equiv_size(var_data const& d) const;
bool should_set_prop_upward(var_data const& d) const;
bool should_prop_upward(var_data const& d) const;
@ -231,6 +227,8 @@ namespace array {
void set_else(theory_var v, expr* e);
expr* get_else(theory_var v);
void internalized(euf::enode* n);
// diagnostics
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;

10
src/sat/smt/euf_ackerman.cpp
View file

@ -176,10 +176,10 @@ namespace euf {
unsigned sz = a->get_num_args();
for (unsigned i = 0; i < sz; ++i) {
expr_ref eq(m.mk_eq(a->get_arg(i), b->get_arg(i)), m);
expr_ref eq = s.mk_eq(a->get_arg(i), b->get_arg(i));
lits.push_back(~s.mk_literal(eq));
}
expr_ref eq(m.mk_eq(a, b), m);
expr_ref eq = s.mk_eq(a, b);
lits.push_back(s.mk_literal(eq));
s.s().mk_clause(lits, sat::status::th(true, m.get_basic_family_id()));
}
@ -187,9 +187,9 @@ namespace euf {
void ackerman::add_eq(expr* a, expr* b, expr* c) {
flet<bool> _is_redundant(s.m_is_redundant, true);
sat::literal lits[3];
expr_ref eq1(m.mk_eq(a, c), m);
expr_ref eq2(m.mk_eq(b, c), m);
expr_ref eq3(m.mk_eq(a, b), m);
expr_ref eq1(s.mk_eq(a, c), m);
expr_ref eq2(s.mk_eq(b, c), m);
expr_ref eq3(s.mk_eq(a, b), m);
TRACE("ack", tout << mk_pp(a, m) << " " << mk_pp(b, m) << " " << mk_pp(c, m) << "\n";);
lits[0] = ~s.mk_literal(eq1);
lits[1] = ~s.mk_literal(eq2);

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

@ -296,9 +296,14 @@ namespace euf {
}
void solver::asserted(literal l) {
if (m_relevancy.enabled() && !m_relevancy.is_relevant(l)) {
m_relevancy.asserted(l);
return;
if (s().lvl(l) <= s().search_lvl())
mark_relevant(l);
else {
m_relevancy.asserted(l);
return;
}
}
expr* e = m_bool_var2expr.get(l.var(), nullptr);
@ -742,7 +747,7 @@ namespace euf {
void solver::relevant_eh(euf::enode* n) {
if (m_qsolver)
m_qsolver->relevant_eh(n);
for (auto thv : enode_th_vars(n)) {
for (auto const& thv : enode_th_vars(n)) {
auto* th = m_id2solver.get(thv.get_id(), nullptr);
if (th && th != m_qsolver)
th->relevant_eh(n);