From aa901c4e88438559186e408ab87854173670878d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 31 Dec 2021 11:53:40 -0800 Subject: [PATCH] axiom solver improvements --- src/ast/rewriter/th_rewriter.cpp | 4 +- src/sat/smt/array_axioms.cpp | 7 +- src/sat/smt/array_internalize.cpp | 109 ++++++++++++++----------- src/sat/smt/array_solver.cpp | 12 +-- src/sat/smt/array_solver.h | 12 ++- src/sat/smt/euf_ackerman.cpp | 10 +-- src/sat/smt/euf_solver.cpp | 11 ++- src/tactic/bv/elim_small_bv_tactic.cpp | 8 +- 8 files changed, 98 insertions(+), 75 deletions(-) diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 097dff6db..2aaf4626c 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -627,7 +627,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { count_down_subterm_references(result, reference_map); // Any term that was newly introduced by the rewrite step is only referenced within / reachable from the result term. - for (auto kv : reference_map) { + for (auto const& kv : reference_map) { if (kv.m_value == 0) { m().trace_stream() << "[attach-enode] #" << kv.m_key->get_id() << " 0\n"; } @@ -691,7 +691,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { return; if (m_new_subst) { m_rep.reset(); - for (auto kv : m_subst->sub()) + for (auto const& kv : m_subst->sub()) m_rep.insert(kv.m_key, kv.m_value); m_new_subst = false; } diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp index 62f111ea6..6f823aee7 100644 --- a/src/sat/smt/array_axioms.cpp +++ b/src/sat/smt/array_axioms.cpp @@ -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 _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; } } diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp index b74d46fe6..da129f30f 100644 --- a/src/sat/smt/array_internalize.cpp +++ b/src/sat/smt/array_internalize.cpp @@ -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: diff --git a/src/sat/smt/array_solver.cpp b/src/sat/smt/array_solver.cpp index 15978747c..83fa15f41 100644 --- a/src/sat/smt/array_solver.cpp +++ b/src/sat/smt/array_solver.cpp @@ -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); } /** diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h index 74788254b..b4fd0d95e 100644 --- a/src/sat/smt/array_solver.h +++ b/src/sat/smt/array_solver.h @@ -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; diff --git a/src/sat/smt/euf_ackerman.cpp b/src/sat/smt/euf_ackerman.cpp index 941b1e0ac..c26835f99 100644 --- a/src/sat/smt/euf_ackerman.cpp +++ b/src/sat/smt/euf_ackerman.cpp @@ -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 _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); diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index b8bd601e3..8f7c34719 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -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); diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp index 12c756c6e..02ec522c6 100644 --- a/src/tactic/bv/elim_small_bv_tactic.cpp +++ b/src/tactic/bv/elim_small_bv_tactic.cpp @@ -145,11 +145,13 @@ class elim_small_bv_tactic : public tactic { "; sort = " << mk_ismt2_pp(s, m) << "; body = " << mk_ismt2_pp(body, m) << std::endl;); - if (bv_sz >= 31ul || ((unsigned)(1ul << bv_sz)) + num_steps > m_max_steps) { + if (bv_sz >= 31) + return false; + unsigned max_num = 1u << bv_sz; + if (max_num > m_max_steps || max_num + num_steps > m_max_steps) return false; - } - for (unsigned j = 0; j < (1ul << bv_sz) && !max_steps_exceeded(num_steps); j++) { + for (unsigned j = 0; j < max_num && !max_steps_exceeded(num_steps); j++) { expr_ref n(m_util.mk_numeral(j, bv_sz), m); new_bodies.push_back(replace_var(uv, num_decls, max_var_idx_p1, i, s, body, n)); num_steps++;