From 3ef05ced2f4a4f3c06029af15459f536ee66a6dc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Feb 2020 19:36:07 -0800 Subject: [PATCH] tuning Signed-off-by: Nikolaj Bjorner --- src/math/lp/lp_params.pyg | 3 +- src/math/lp/nla_params.pyg | 1 + src/smt/asserted_formulas.cpp | 10 ++--- src/smt/smt_context.cpp | 84 ++++++++++++++++------------------- src/smt/smt_context.h | 17 +++---- src/smt/smt_context_inv.cpp | 38 +--------------- src/smt/smt_internalizer.cpp | 55 ++++++++++++++++++----- src/smt/smt_parallel.cpp | 2 +- src/smt/theory_lra.cpp | 26 ----------- 9 files changed, 103 insertions(+), 133 deletions(-) diff --git a/src/math/lp/lp_params.pyg b/src/math/lp/lp_params.pyg index 4c7722b93..074d6310d 100644 --- a/src/math/lp/lp_params.pyg +++ b/src/math/lp/lp_params.pyg @@ -1,11 +1,12 @@ def_module_params('lp', export=True, + description='Parameters for the LP arithmetic solver core', params=( ('rep_freq', UINT, 0, 'the report frequency, in how many iterations print the cost and other info '), ('min', BOOL, False, 'minimize cost'), ('print_stats', BOOL, False, 'print statistic'), ('simplex_strategy', UINT, 0, 'simplex strategy for the solver'), - ('enable_hnf', BOOL, True, 'enable hnf cuts'), + ('enable_hnf', BOOL, True, 'enable hnf (Hermite Normal Form) cuts'), ('bprop_on_pivoted_rows', BOOL, True, 'propagate bounds on rows changed by the pivot operation'), ('nla', BOOL, False, 'call nonlinear integer solver with incremental linearization'), ('print_ext_var_names', BOOL, False, 'print external variable names') diff --git a/src/math/lp/nla_params.pyg b/src/math/lp/nla_params.pyg index fd7f652a4..024dc146b 100644 --- a/src/math/lp/nla_params.pyg +++ b/src/math/lp/nla_params.pyg @@ -1,5 +1,6 @@ def_module_params('nla', export=True, + description='Parameters for non-linear arithmetic solving', params=( ('order', BOOL, True, 'run order lemmas'), ('tangents', BOOL, True, 'run tangent lemmas'), diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 3db9dc172..963356a1b 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -455,7 +455,8 @@ void asserted_formulas::propagate_values() { unsigned num_prop = 0; unsigned num_iterations = 0; - while (!inconsistent() && ++num_iterations < 2) { + unsigned delta_prop = m_formulas.size(); + while (!inconsistent() && m_formulas.size()/20 < delta_prop) { m_expr2depth.reset(); m_scoped_substitution.push(); unsigned prop = num_prop; @@ -478,9 +479,7 @@ void asserted_formulas::propagate_values() { m_scoped_substitution.pop(1); flush_cache(); TRACE("propagate_values", tout << "after:\n"; display(tout);); - if (num_prop == prop) { - break; - } + delta_prop = prop - num_prop; num_prop = prop; } TRACE("asserted_formulas", tout << num_prop << "\n";); @@ -493,7 +492,6 @@ unsigned asserted_formulas::propagate_values(unsigned i) { expr_ref new_n(m); proof_ref new_pr(m); m_rewriter(n, new_n, new_pr); - TRACE("propagate_values", tout << n << "\n" << new_n << "\n";); if (m.proofs_enabled()) { proof * pr = m_formulas[i].get_proof(); new_pr = m.mk_modus_ponens(pr, new_pr); @@ -504,7 +502,7 @@ unsigned asserted_formulas::propagate_values(unsigned i) { m_inconsistent = true; } update_substitution(new_n, new_pr); - return n != new_n ? 1 : 0; + return (n != new_n) ? 1 : 0; } bool asserted_formulas::update_substitution(expr* n, proof* pr) { diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 55ab8cb86..7e607153f 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1387,7 +1387,7 @@ namespace smt { else if (d.is_theory_atom()) { theory * th = m_theories.get_plugin(d.get_theory()); SASSERT(th); - th->assign_eh(v, val == l_true); + th->assign_eh(v, val == l_true); } else if (d.is_quantifier()) { // Remark: when RELEVANCY_LEMMA is true, a quantifier can be asserted to false and marked as relevant. @@ -1804,7 +1804,7 @@ namespace smt { } } bool_var var; - lbool phase; + lbool phase = l_undef; m_case_split_queue->next_case_split(var, phase); if (var == null_bool_var) { @@ -1836,13 +1836,13 @@ namespace smt { // assigning a quantifier to false is equivalent to make it irrelevant. phase = l_false; } + literal l(var, false); if (phase != l_undef) { is_pos = phase == l_true; } else { bool_var_data & d = m_bdata[var]; - if (d.try_true_first()) { is_pos = true; } @@ -1851,21 +1851,25 @@ namespace smt { case PS_THEORY: if (m_phase_cache_on && d.m_phase_available) { is_pos = m_bdata[var].m_phase; + break; } - else if (!m_phase_cache_on && d.is_theory_atom()) { + if (!m_phase_cache_on && d.is_theory_atom()) { theory * th = m_theories.get_plugin(d.get_theory()); - lbool ph = th->get_phase(var); - if (ph != l_undef) { - is_pos = ph == l_true; - } - else { - is_pos = m_phase_default; + lbool th_phase = th->get_phase(var); + if (th_phase != l_undef) { + is_pos = th_phase == l_true; + break; } } - else { - TRACE("phase_selection", tout << "setting to false\n";); - is_pos = m_phase_default; + if (m_lit_occs[l.index()] == 0) { + is_pos = false; + break; } + if (m_lit_occs[(~l).index()] == 0) { + is_pos = true; + break; + } + is_pos = m_phase_default; break; case PS_CACHING: case PS_CACHING_CONSERVATIVE: @@ -1889,8 +1893,7 @@ namespace smt { is_pos = (m_random() % 2 == 0); break; case PS_OCCURRENCE: { - literal l(var); - is_pos = m_lit_occs[l.index()].size() > m_lit_occs[(~l).index()].size(); + is_pos = m_lit_occs[l.index()] > m_lit_occs[(~l).index()]; break; } default: @@ -1900,10 +1903,9 @@ namespace smt { } } - TRACE("decide", tout << "case split " << (is_pos?"pos":"neg") << " p" << var << "\n" - << "activity: " << get_activity(var) << "\n";); - - assign(literal(var, !is_pos), b_justification::mk_axiom(), true); + if (!is_pos) l.neg(); + TRACE("decide", tout << "case split " << l << "\n" << "activity: " << get_activity(var) << "\n";); + assign(l, b_justification::mk_axiom(), true); return true; } @@ -1989,19 +1991,18 @@ namespace smt { /** \brief Update the index used for backward subsumption. */ - void context::remove_lit_occs(clause * cls) { - unsigned num_lits = cls->get_num_literals(); - for (unsigned i = 0; i < num_lits; i++) { - literal l = cls->get_literal(i); - m_lit_occs[l.index()].erase(cls); + void context::remove_lit_occs(clause const& cls) { + int nbv = get_num_bool_vars(); + for (literal l : cls) { + if (l.var() < nbv) + dec_ref(l); } } void context::remove_cls_occs(clause * cls) { remove_watch_literal(cls, 0); remove_watch_literal(cls, 1); - if (lit_occs_enabled()) - remove_lit_occs(cls); + remove_lit_occs(*cls); } /** @@ -2254,19 +2255,9 @@ namespace smt { } } - unsigned num = cls->get_num_literals(); + unsigned num = cls->get_num_literals(); - if (lit_occs_enabled()) { - for (unsigned j = 0; j < num; j++) { - literal l = cls->get_literal(j); - if (l.var() < static_cast(num_bool_vars)) { - // This boolean variable was not deleted during backtracking - // - // So, remove it from lit_occs. - m_lit_occs[l.index()].erase(cls); - } - } - } + remove_lit_occs(*cls); unsigned ilvl = 0; (void)ilvl; @@ -2297,8 +2288,7 @@ namespace smt { add_watch_literal(cls, 0); add_watch_literal(cls, 1); - if (lit_occs_enabled()) - add_lit_occs(cls); + add_lit_occs(*cls); literal l1 = cls->get_literal(0); literal l2 = cls->get_literal(1); @@ -2342,7 +2332,6 @@ namespace smt { v.reset(); } CASSERT("reinit_clauses", check_clauses(m_lemmas)); - CASSERT("reinit_clauses", check_lit_occs()); TRACE("reinit_clauses_bug", display_watch_lists(tout);); } @@ -2498,23 +2487,24 @@ namespace smt { unsigned i = 2; unsigned j = i; + bool is_taut = false; for(; i < s; i++) { literal l = cls[i]; switch(get_assignment(l)) { case l_false: if (m.proofs_enabled()) simp_lits.push_back(~l); - if (lit_occs_enabled()) - m_lit_occs[l.index()].erase(&cls); + dec_ref(l); break; + case l_true: + is_taut = true; + // fallthrough case l_undef: if (i != j) { cls.swap_lits(i, j); } j++; break; - case l_true: - return true; } } @@ -2524,6 +2514,10 @@ namespace smt { SASSERT(j >= 2); } + if (is_taut) { + return true; + } + if (m.proofs_enabled() && !simp_lits.empty()) { SASSERT(m_scope_lvl == m_base_lvl); justification * js = cls.get_justification(); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index e45363132..205f0484a 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -170,7 +170,7 @@ namespace smt { ptr_vector m_bool_var2expr; // bool_var -> expr signed_char_vector m_assignment; //!< mapping literal id -> assignment lbool vector m_watches; //!< per literal - vector m_lit_occs; //!< index for backward subsumption + unsigned_vector m_lit_occs; //!< occurrence count of literals svector m_bdata; //!< mapping bool_var -> data svector m_activity; clause_vector m_aux_clauses; @@ -637,8 +637,6 @@ namespace smt { void remove_watch_literal(clause * cls, unsigned idx); - void remove_lit_occs(clause * cls); - void remove_cls_occs(clause * cls); void del_clause(bool log, clause * cls); @@ -841,9 +839,13 @@ namespace smt { void mk_ite_cnstr(app * n); - bool lit_occs_enabled() const { return m_fparams.m_phase_selection==PS_OCCURRENCE; } + void dec_ref(literal l) { SASSERT(m_lit_occs[l.index()] > 0); m_lit_occs[l.index()]--; } - void add_lit_occs(clause * cls); + void inc_ref(literal l) { m_lit_occs[l.index()]++; } + + void remove_lit_occs(clause const& cls); + + void add_lit_occs(clause const& cls); public: void ensure_internalized(expr* e); @@ -1423,9 +1425,6 @@ namespace smt { bool check_missing_diseq_conflict() const; - bool check_lit_occs(literal l) const; - - bool check_lit_occs() const; #endif // ----------------------------------- // @@ -1571,6 +1570,8 @@ namespace smt { void get_guessed_literals(expr_ref_vector & result); + bool split_binary(app* o, expr*& a, expr_ref& b, expr_ref& c); + void internalize_assertion(expr * n, proof * pr, unsigned generation); void internalize_proxies(expr_ref_vector const& asms, vector>& asm2proxy); diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp index d06710cee..7eff6cd36 100644 --- a/src/smt/smt_context_inv.cpp +++ b/src/smt/smt_context_inv.cpp @@ -32,10 +32,8 @@ namespace smt { bool context::check_clause(clause const * cls) const { SASSERT(is_watching_clause(~cls->get_literal(0), cls)); SASSERT(is_watching_clause(~cls->get_literal(1), cls)); - if (lit_occs_enabled()) { - for (literal l : *cls) { - SASSERT(m_lit_occs[l.index()].contains(const_cast(cls))); - } + for (literal l : *cls) { + SASSERT(m_lit_occs[l.index()] > 0); } return true; } @@ -84,37 +82,6 @@ namespace smt { return true; } - bool context::check_lit_occs(literal l) const { - clause_set const & v = m_lit_occs[l.index()]; - for (clause * cls : v) { - unsigned num = cls->get_num_literals(); - unsigned i = 0; - for (; i < num; i++) - if (cls->get_literal(i) == l) - break; - CTRACE("lit_occs", !(i < num), tout << i << " " << num << "\n"; display_literal(tout, l); tout << "\n"; - display_clause(tout, cls); tout << "\n"; - tout << "l: " << l.index() << " cls: "; - for (unsigned j = 0; j < num; j++) { - tout << cls->get_literal(j).index() << " "; - } - tout << "\n"; - display_clause_detail(tout, cls); tout << "\n";); - SASSERT(i < num); - } - return true; - } - - bool context::check_lit_occs() const { - if (lit_occs_enabled()) { - unsigned num_lits = get_num_bool_vars() * 2; - for (unsigned l_idx = 0; l_idx < num_lits; ++l_idx) { - check_lit_occs(to_literal(l_idx)); - } - } - return true; - } - bool context::check_enode(enode * n) const { SASSERT(n->check_invariant()); bool is_true_eq = n->is_true_eq(); @@ -136,7 +103,6 @@ namespace smt { } bool context::check_invariant() const { - check_lit_occs(); check_bin_watch_lists(); check_clauses(m_aux_clauses); check_clauses(m_lemmas); diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index c7dc3462a..80482a99c 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -182,7 +182,29 @@ namespace smt { } } + bool context::split_binary(app* o, expr*& a, expr_ref& b, expr_ref& c) { + expr* x = nullptr, *y = nullptr, *ny = nullptr, *z = nullptr, *u = nullptr; + if (m.is_or(o, x, y) && + m.is_not(y, ny) && + m.is_or(ny, z, u)) { + a = x; + b = m.is_not(z, z) ? z : m.mk_not(z); + c = m.is_not(u, u) ? u : m.mk_not(u); + return true; + } + if (m.is_or(o, y, x) && + m.is_not(y, ny) && + m.is_or(ny, z, u)) { + a = x; + b = m.is_not(z, z) ? z : m.mk_not(z); + c = m.is_not(u, u) ? u : m.mk_not(u); + return true; + } + return false; + } + #define DEEP_EXPR_THRESHOLD 1024 + /** \brief Internalize an expression asserted into the logical context using the given proof as a justification. @@ -226,6 +248,19 @@ namespace smt { } case OP_OR: { literal_buffer lits; + expr* a = nullptr; + expr_ref b(m), c(m); + // perform light-weight rewriting on clauses. + if (!relevancy() && split_binary(to_app(n), a, b, c)) { + internalize(a, true); + internalize(b, true); + internalize(c, true); + literal lits2[2] = { get_literal(a), get_literal(b) }; + literal lits3[2] = { get_literal(a), get_literal(c) }; + mk_root_clause(2, lits2, pr); + mk_root_clause(2, lits3, pr); + break; + } for (expr * arg : *to_app(n)) { internalize(arg, true); lits.push_back(get_literal(arg)); @@ -882,11 +917,9 @@ namespace smt { SASSERT(m_assignment.size() == m_watches.size()); m_watches[l.index()] .reset(); m_watches[not_l.index()] .reset(); - if (lit_occs_enabled()) { - m_lit_occs.reserve(aux); - m_lit_occs[l.index()] .reset(); - m_lit_occs[not_l.index()] .reset(); - } + m_lit_occs.reserve(aux, 0); + m_lit_occs[l.index()] = 0; + m_lit_occs[not_l.index()] = 0; bool_var_data & data = m_bdata[v]; unsigned iscope_lvl = m_scope_lvl; // record when the boolean variable was internalized. data.init(iscope_lvl); @@ -1357,11 +1390,14 @@ namespace smt { if (j && !j->in_region()) m_justifications.push_back(j); assign(lits[0], j); + inc_ref(lits[0]); return nullptr; case 2: if (use_binary_clause_opt(lits[0], lits[1], lemma)) { literal l1 = lits[0]; literal l2 = lits[1]; + inc_ref(l1); + inc_ref(l2); m_watches[(~l1).index()].insert_literal(l2); m_watches[(~l2).index()].insert_literal(l1); if (get_assignment(l2) == l_false) { @@ -1425,8 +1461,7 @@ namespace smt { assign(cls->get_literal(0), b_justification(cls)); } - if (lit_occs_enabled()) - add_lit_occs(cls); + add_lit_occs(*cls); TRACE("add_watch_literal_bug", display_clause_detail(tout, cls);); TRACE("mk_clause_result", display_clause_detail(tout, cls);); @@ -1435,9 +1470,9 @@ namespace smt { }} } - void context::add_lit_occs(clause * cls) { - for (literal l : *cls) { - m_lit_occs[l.index()].insert(cls); + void context::add_lit_occs(clause const& cls) { + for (literal l : cls) { + inc_ref(l); } } diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 5b32574c3..70979372f 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -37,7 +37,7 @@ namespace smt { // try first sequential with a low conflict budget to make super easy problems cheap ctx.get_fparams().m_max_conflicts = std::min(thread_max_conflicts, 40u); result = ctx.check(asms.size(), asms.c_ptr()); - if (result != l_undef || ctx.m_num_conflicts < max_conflicts) { + if (result != l_undef || (result == l_undef && ctx.m_num_conflicts < ctx.get_fparams().m_max_conflicts)) { return result; } #else diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index c39b8f3ce..2a3efa7de 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2189,32 +2189,6 @@ public: nla::lemma m_lemma; - // lp::lar_term mk_term(nla::polynomial const& poly) { - // lp::lar_term term; - // for (auto const& mon : poly) { - // SASSERT(!mon.empty()); - // if (mon.size() == 1) { - // term.add_var(mon[0]); - // } - // else { - // // create the expression corresponding to the product. - // // internalize it. - // // extract the theory var representing the product. - // // convert the theory var back to lpvar - // expr_ref_vector mul(m); - // for (lpvar v : mon) { - // theory_var w = lp().local_to_external(v); - // mul.push_back(get_enode(w)->get_owner()); - // } - // app_ref t(a.mk_mul(mul.size(), mul.c_ptr()), m); - // VERIFY(internalize_term(t)); - // theory_var w = ctx().get_enode(t)->get_th_var(get_id()); - // term.add_var(lp().external_to_local(w)); - // } - // } - // return term; - // } - void false_case_of_check_nla() { literal_vector core; for (auto const& ineq : m_lemma.ineqs()) {