From 7063ad81cce2d6020c2495ca96d938ff504efb02 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 25 Mar 2018 19:42:06 -0700 Subject: [PATCH 01/24] updates Signed-off-by: Nikolaj Bjorner --- scripts/vsts-mac.sh | 18 ++++++++++++++++++ src/opt/opt_solver.h | 2 +- src/opt/optsmt.cpp | 2 +- 3 files changed, 20 insertions(+), 2 deletions(-) create mode 100644 scripts/vsts-mac.sh diff --git a/scripts/vsts-mac.sh b/scripts/vsts-mac.sh new file mode 100644 index 000000000..959dccbbd --- /dev/null +++ b/scripts/vsts-mac.sh @@ -0,0 +1,18 @@ +#!/bin/sh + +cd .. +mkdir build +CSC=/usr/bin/csc GACUTIL=/usr/bin/gacutil CXX=clang++ CC=clang python scripts/mk_make.py --java --python +cd build +make +make test-z3 +make cpp_example +make c_example +# make java_example +# make python_example +./cpp_example +./test_capi + +git clone https://github.com/z3prover/z3test.git z3test +ls +python z3test/scripts/test_benchmarks.py ./z3 ./z3test/regressions/smt2 \ No newline at end of file diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 4d2f39416..af4be915d 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -117,7 +117,7 @@ namespace opt { void maximize_objectives(expr_ref_vector& blockers); inf_eps const & saved_objective_value(unsigned obj_index); inf_eps current_objective_value(unsigned obj_index); - model* get_model(unsigned obj_index) { return m_models[obj_index]; } + model* get_model_idx(unsigned obj_index) { return m_models[obj_index]; } bool objective_is_model_valid(unsigned obj_index) const { return m_valid_objectives[obj_index]; } diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index f8f75fbfd..dd396126d 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -46,7 +46,7 @@ namespace opt { for (unsigned i = 0; i < src.size(); ++i) { if (src[i] >= dst[i]) { dst[i] = src[i]; - m_models.set(i, m_s->get_model(i)); + m_models.set(i, m_s->get_model_idx(i)); m_s->get_labels(m_labels); m_lower_fmls[i] = fmls[i].get(); if (dst[i].is_pos() && !dst[i].is_finite()) { // review: likely done already. From 96b717f494e02c7e510995d36f156b2546c2f84c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 26 Mar 2018 15:17:41 -0700 Subject: [PATCH 02/24] propagate during asymmetric branching Signed-off-by: Nikolaj Bjorner --- src/sat/sat_asymm_branch.cpp | 14 +++----------- src/sat/sat_solver.cpp | 2 +- 2 files changed, 4 insertions(+), 12 deletions(-) diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index a6e036408..3e306370d 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -108,7 +108,6 @@ namespace sat { int64 limit = -m_asymm_branch_limit; std::stable_sort(clauses.begin(), clauses.end(), clause_size_lt()); m_counter -= clauses.size(); - SASSERT(s.m_qhead == s.m_trail.size()); clause_vector::iterator it = clauses.begin(); clause_vector::iterator it2 = it; clause_vector::iterator end = clauses.end(); @@ -120,7 +119,6 @@ namespace sat { } break; } - SASSERT(s.m_qhead == s.m_trail.size()); clause & c = *(*it); if (m_counter < limit || s.inconsistent() || c.was_removed()) { *it2 = *it; @@ -414,19 +412,16 @@ namespace sat { s.assign(c[0], justification()); s.propagate_core(false); scoped_d.del_clause(); - SASSERT(s.inconsistent() || s.m_qhead == s.m_trail.size()); return false; // check_missed_propagation() may fail, since m_clauses is not in a consistent state. case 2: SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef); s.mk_bin_clause(c[0], c[1], c.is_learned()); scoped_d.del_clause(); - SASSERT(s.m_qhead == s.m_trail.size()); return false; default: c.shrink(new_sz); if (s.m_config.m_drat) s.m_drat.add(c, true); // if (s.m_config.m_drat) s.m_drat.del(c0); // TBD - SASSERT(s.m_qhead == s.m_trail.size()); return true; } } @@ -445,12 +440,8 @@ namespace sat { bool asymm_branch::process(clause & c) { TRACE("asymm_branch_detail", tout << "processing: " << c << "\n";); SASSERT(s.scope_lvl() == 0); - SASSERT(s.m_qhead == s.m_trail.size()); SASSERT(!s.inconsistent()); -#ifdef Z3DEBUG - unsigned trail_sz = s.m_trail.size(); -#endif unsigned sz = c.size(); SASSERT(sz > 0); unsigned i; @@ -468,14 +459,15 @@ namespace sat { // try asymmetric branching // clause must not be used for propagation + s.propagate(false); + if (s.inconsistent()) + return true; scoped_detach scoped_d(s, c); unsigned new_sz = c.size(); unsigned flip_position = m_rand(c.size()); bool found_conflict = flip_literal_at(c, flip_position, new_sz); SASSERT(!s.inconsistent()); SASSERT(s.scope_lvl() == 0); - SASSERT(trail_sz == s.m_trail.size()); - SASSERT(s.m_qhead == s.m_trail.size()); if (!found_conflict) { // clause size can't be reduced. return true; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index a2ef176a1..10b813fc9 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -324,7 +324,7 @@ namespace sat { case 2: mk_bin_clause(lits[0], lits[1], learned); if (learned && m_par) m_par->share_clause(*this, lits[0], lits[1]); - return 0; + return nullptr; case 3: return mk_ter_clause(lits, learned); default: From d60d0b8a7ab5645619c41ca6cbffa3933e438cbf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 26 Mar 2018 15:19:14 -0700 Subject: [PATCH 03/24] fix indent Signed-off-by: Nikolaj Bjorner --- src/sat/sat_asymm_branch.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index 3e306370d..d6932c9c0 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -459,9 +459,9 @@ namespace sat { // try asymmetric branching // clause must not be used for propagation - s.propagate(false); - if (s.inconsistent()) - return true; + s.propagate(false); + if (s.inconsistent()) + return true; scoped_detach scoped_d(s, c); unsigned new_sz = c.size(); unsigned flip_position = m_rand(c.size()); From 51d62684e1c94349496513232346e3af114147f7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 26 Mar 2018 15:51:00 -0700 Subject: [PATCH 04/24] move propagation to after binary clause addition Signed-off-by: Nikolaj Bjorner --- src/sat/sat_asymm_branch.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index 3e306370d..ae6db1f6c 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -416,6 +416,7 @@ namespace sat { case 2: SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef); s.mk_bin_clause(c[0], c[1], c.is_learned()); + if (s.m_trail.size() > s.m_qhead) s.propagate_core(false); scoped_d.del_clause(); return false; default: @@ -459,9 +460,7 @@ namespace sat { // try asymmetric branching // clause must not be used for propagation - s.propagate(false); - if (s.inconsistent()) - return true; + scoped_detach scoped_d(s, c); unsigned new_sz = c.size(); unsigned flip_position = m_rand(c.size()); From aa2721517ba17938f257e678debda78f87d3d456 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 30 Mar 2018 16:24:22 -0700 Subject: [PATCH 05/24] model conversion and acce tracking Signed-off-by: Nikolaj Bjorner --- .../ackermannize_bv_tactic.cpp | 2 +- src/sat/sat_asymm_branch.cpp | 22 +++++++--- src/sat/sat_model_converter.cpp | 10 ++--- src/sat/sat_simplifier.cpp | 43 +++++++++++++++---- src/sat/sat_solver.cpp | 8 ++++ src/tactic/goal.cpp | 3 ++ 6 files changed, 67 insertions(+), 21 deletions(-) diff --git a/src/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp index f0e960644..df230a7e2 100644 --- a/src/ackermannization/ackermannize_bv_tactic.cpp +++ b/src/ackermannization/ackermannize_bv_tactic.cpp @@ -52,7 +52,7 @@ public: result.push_back(resg.get()); // report model if (g->models_enabled()) { - g->add(mk_ackermannize_bv_model_converter(m, lackr.get_info())); + resg->add(mk_ackermannize_bv_model_converter(m, lackr.get_info())); } resg->inc_depth(); diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index 971e86d95..65003a6e4 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -333,13 +333,18 @@ namespace sat { if (!m_to_delete.empty()) { unsigned j = 0; for (unsigned i = 0; i < c.size(); ++i) { - if (!m_to_delete.contains(c[i])) { - c[j] = c[i]; - ++j; - } - else { - m_pos.erase(c[i]); - m_neg.erase(~c[i]); + literal lit = c[i]; + switch (s.value(lit)) { + case l_true: + scoped_d.del_clause(); + return false; + case l_false: + break; + default: + if (!m_to_delete.contains(lit)) { + c[j++] = lit; + } + break; } } return re_attach(scoped_d, c, j); @@ -359,6 +364,7 @@ namespace sat { } bool asymm_branch::flip_literal_at(clause const& c, unsigned flip_index, unsigned& new_sz) { + VERIFY(s.m_trail.size() == s.m_qhead); bool found_conflict = false; unsigned i = 0, sz = c.size(); s.push(); @@ -399,6 +405,7 @@ namespace sat { } bool asymm_branch::re_attach(scoped_detach& scoped_d, clause& c, unsigned new_sz) { + VERIFY(s.m_trail.size() == s.m_qhead); m_elim_literals += c.size() - new_sz; if (c.is_learned()) { m_elim_learned_literals += c.size() - new_sz; @@ -415,6 +422,7 @@ namespace sat { return false; // check_missed_propagation() may fail, since m_clauses is not in a consistent state. case 2: SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef); + VERIFY(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef); s.mk_bin_clause(c[0], c[1], c.is_learned()); if (s.m_trail.size() > s.m_qhead) s.propagate_core(false); scoped_d.del_clause(); diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index 9bda5cf3d..6b0eb1a7c 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -75,7 +75,7 @@ namespace sat { void model_converter::operator()(model & m) const { vector::const_iterator begin = m_entries.begin(); vector::const_iterator it = m_entries.end(); - bool first = true; + bool first = false; // true; //SASSERT(!m_solver || m_solver->check_clauses(m)); while (it != begin) { --it; @@ -99,8 +99,8 @@ namespace sat { process_stack(m, clause, st->stack()); } sat = false; - if (false && first && m_solver && !m_solver->check_clauses(m)) { - display(std::cout, *it) << "\n"; + if (first && m_solver && !m_solver->check_clauses(m)) { + IF_VERBOSE(0, display(verbose_stream() << "after processing stack\n", *it) << "\n"); first = false; } ++index; @@ -125,8 +125,8 @@ namespace sat { m[v] = sign ? l_false : l_true; // if (first) std::cout << "set: " << l << "\n"; sat = true; - if (false && first && m_solver && !m_solver->check_clauses(m)) { - display(std::cout, *it) << "\n";; + if (first && m_solver && !m_solver->check_clauses(m)) { + IF_VERBOSE(0, display(verbose_stream() << "after flipping undef\n", *it) << "\n"); first = false; } } diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index be0222d3b..6ef0be83a 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -939,6 +939,19 @@ namespace sat { bool operator==(clause_ante const& a) const { return a.m_lit1 == m_lit1 && a.m_lit2 == m_lit2 && a.m_clause == m_clause; } + std::ostream& display(std::ostream& out) const { + if (cls()) { + out << *cls() << " "; + } + if (lit1() != null_literal) { + out << lit1() << " "; + } + if (lit2() != null_literal) { + out << lit2() << " "; + } + out << "\n"; + return out; + } }; class queue { @@ -1154,10 +1167,14 @@ namespace sat { \brief idx is the index of the blocked literal. m_tautology contains literals that were used to establish that the current members of m_covered_clause is blocked. This routine removes literals that were not relevant to establishing it was blocked. + + It has a bug: literals that are used to prune tautologies during resolution intersection should be included + in the dependencies. */ void minimize_covered_clause(unsigned idx) { // IF_VERBOSE(0, verbose_stream() << "minimize: " << m_covered_clause // << " @ " << idx << "\n" << "tautology: " << m_tautology << "\n";); + literal _blocked = m_covered_clause[idx]; for (literal l : m_tautology) VERIFY(s.is_marked(l)); for (literal l : m_covered_clause) s.unmark_visited(l); for (literal l : m_tautology) s.mark_visited(l); @@ -1167,8 +1184,18 @@ namespace sat { if (m_covered_antecedent[i] == clause_ante()) s.mark_visited(lit); if (s.is_marked(lit)) idx = i; } + if (_blocked.var() == 16774 && false) { + IF_VERBOSE(0, verbose_stream() << "covered: " << m_covered_clause << "\n"; + verbose_stream() << "tautology: " << m_tautology << "\n"; + verbose_stream() << "index: " << idx << "\n"; + for (unsigned i = idx; i > 0; --i) { + m_covered_antecedent[i].display(verbose_stream() << "ante " << m_covered_clause[i] << ":"); + }); + } for (unsigned i = idx; i > 0; --i) { literal lit = m_covered_clause[i]; + s.mark_visited(lit); + continue; if (!s.is_marked(lit)) continue; clause_ante const& ante = m_covered_antecedent[i]; if (ante.cls()) { @@ -1205,6 +1232,9 @@ namespace sat { // unsigned sz0 = m_covered_clause.size(); m_covered_clause.resize(j); VERIFY(j >= m_clause.size()); + if (_blocked.var() == 16774 && false) { + IF_VERBOSE(0, verbose_stream() << "covered: " << m_covered_clause << "\n"); + } // IF_VERBOSE(0, verbose_stream() << "reduced from size " << sz0 << " to " << m_covered_clause << "\n" << m_clause << "\n";); } @@ -1282,7 +1312,7 @@ namespace sat { for (unsigned i = 0; i < m_covered_clause.size(); ++i) { literal lit = m_covered_clause[i]; if (resolution_intersection(lit, false)) { - blocked = m_covered_clause[i]; + blocked = m_covered_clause[i]; minimize_covered_clause(i); return true; } @@ -1531,13 +1561,10 @@ namespace sat { return; } for (literal l2 : m_intersection) { - l2.neg(); - watched* w = find_binary_watch(s.get_wlist(~l), l2); + watched* w = find_binary_watch(s.get_wlist(~l), ~l2); if (!w) { - IF_VERBOSE(100, verbose_stream() << "bca " << l << " " << l2 << "\n";); - s.get_wlist(~l).push_back(watched(l2, true)); - VERIFY(!find_binary_watch(s.get_wlist(~l2), l)); - s.get_wlist(~l2).push_back(watched(l, true)); + IF_VERBOSE(10, verbose_stream() << "bca " << l << " " << ~l2 << "\n";); + s.s.mk_bin_clause(l, ~l2, true); ++s.m_num_bca; } } @@ -1997,7 +2024,7 @@ namespace sat { sat_simplifier_params p(_p); m_cce = p.cce(); m_acce = p.acce(); - m_bca = p.bca(); + m_bca = false && p.bca(); // disabled m_abce = p.abce(); m_ate = p.ate(); m_bce_delay = p.bce_delay(); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 10b813fc9..1617b487b 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -333,6 +333,13 @@ namespace sat { } void solver::mk_bin_clause(literal l1, literal l2, bool learned) { +#if 0 + if ((l1 == literal(5981, false) && l2 == literal(16764, false)) || + (l2 == literal(5981, false) && l1 == literal(16764, false))) { + IF_VERBOSE(0, display(verbose_stream())); + //VERIFY(false); + } +#endif if (find_binary_watch(get_wlist(~l1), ~l2)) { assign(l1, justification()); return; @@ -1656,6 +1663,7 @@ namespace sat { if (!check_clauses(m_model)) { IF_VERBOSE(0, verbose_stream() << "failure checking clauses on transformed model\n";); + IF_VERBOSE(10, m_mc.display(verbose_stream())); throw solver_exception("check model failed"); } diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp index c7b730099..5252a410d 100644 --- a/src/tactic/goal.cpp +++ b/src/tactic/goal.cpp @@ -85,6 +85,9 @@ goal::goal(goal const & src, bool): m_core_enabled(src.unsat_core_enabled()), m_inconsistent(false), m_precision(src.m_precision) { + m_mc = src.m_mc.get(); + m_pc = src.m_pc.get(); + m_dc = src.m_dc.get(); } goal::~goal() { From 55eb11d91b853dc1a3234b706a538b8f10228d2e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 31 Mar 2018 13:26:20 -0700 Subject: [PATCH 06/24] fix bug in blocked clause elimination: it was ignoring unit literals Signed-off-by: Nikolaj Bjorner --- src/sat/sat_model_converter.cpp | 20 ++++++++++++------- src/sat/sat_simplifier.cpp | 6 +++--- src/sat/sat_solver.cpp | 13 +++++------- src/tactic/bv/bit_blaster_model_converter.cpp | 15 +++----------- src/tactic/smtlogics/qfufbv_tactic.cpp | 16 ++++++++------- 5 files changed, 33 insertions(+), 37 deletions(-) diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index 6b0eb1a7c..c9d046197 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -79,21 +79,27 @@ namespace sat { //SASSERT(!m_solver || m_solver->check_clauses(m)); while (it != begin) { --it; - SASSERT(it->get_kind() != ELIM_VAR || m[it->var()] == l_undef); - // if it->get_kind() == BLOCK_LIT, then it might be the case that m[it->var()] != l_undef, + bool_var v0 = it->var(); + SASSERT(it->get_kind() != ELIM_VAR || m[v0] == l_undef); + // if it->get_kind() == BLOCK_LIT, then it might be the case that m[v] != l_undef, // and the following procedure flips its value. bool sat = false; bool var_sign = false; unsigned index = 0; literal_vector clause; - VERIFY(legal_to_flip(it->var())); + VERIFY(legal_to_flip(v0)); for (literal l : it->m_clauses) { if (l == null_literal) { // end of clause + if (v0 == 36858) + IF_VERBOSE(0, verbose_stream() << "clause: " << clause << "\n"; + for (literal lit : clause) verbose_stream() << m[lit.var()] << " "; + verbose_stream() << "\n";); + elim_stack* st = it->m_elim_stack[index]; if (!sat) { - VERIFY(legal_to_flip(it->var())); - m[it->var()] = var_sign ? l_false : l_true; + VERIFY(legal_to_flip(v0)); + m[v0] = var_sign ? l_false : l_true; } if (st) { process_stack(m, clause, st->stack()); @@ -115,11 +121,11 @@ namespace sat { bool_var v = l.var(); if (v >= m.size()) std::cout << v << " model size: " << m.size() << "\n"; VERIFY(v < m.size()); - if (v == it->var()) + if (v == v0) var_sign = sign; if (value_at(l, m) == l_true) sat = true; - else if (!sat && v != it->var() && m[v] == l_undef) { + else if (!sat && v != v0 && m[v] == l_undef) { VERIFY(legal_to_flip(v)); // clause can be satisfied by assigning v. m[v] = sign ? l_false : l_true; diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 6ef0be83a..642fca348 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1007,7 +1007,7 @@ namespace sat { } bool process_var(bool_var v) { - return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v); + return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v) && s.value(v) == l_undef; } enum elim_type { @@ -1184,7 +1184,7 @@ namespace sat { if (m_covered_antecedent[i] == clause_ante()) s.mark_visited(lit); if (s.is_marked(lit)) idx = i; } - if (_blocked.var() == 16774 && false) { + if (false && _blocked.var() == 16774) { IF_VERBOSE(0, verbose_stream() << "covered: " << m_covered_clause << "\n"; verbose_stream() << "tautology: " << m_tautology << "\n"; verbose_stream() << "index: " << idx << "\n"; @@ -1232,7 +1232,7 @@ namespace sat { // unsigned sz0 = m_covered_clause.size(); m_covered_clause.resize(j); VERIFY(j >= m_clause.size()); - if (_blocked.var() == 16774 && false) { + if (false && _blocked.var() == 16774) { IF_VERBOSE(0, verbose_stream() << "covered: " << m_covered_clause << "\n"); } // IF_VERBOSE(0, verbose_stream() << "reduced from size " << sz0 << " to " << m_covered_clause << "\n" << m_clause << "\n";); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 1617b487b..7def379e0 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -333,13 +333,6 @@ namespace sat { } void solver::mk_bin_clause(literal l1, literal l2, bool learned) { -#if 0 - if ((l1 == literal(5981, false) && l2 == literal(16764, false)) || - (l2 == literal(5981, false) && l1 == literal(16764, false))) { - IF_VERBOSE(0, display(verbose_stream())); - //VERIFY(false); - } -#endif if (find_binary_watch(get_wlist(~l1), ~l2)) { assign(l1, justification()); return; @@ -487,6 +480,8 @@ namespace sat { return reinit; } + static unsigned s_count = 0; + void solver::attach_clause(clause & c, bool & reinit) { SASSERT(c.size() > 2); reinit = false; @@ -1674,7 +1669,9 @@ namespace sat { if (!m_clone->check_model(m_model)) { //IF_VERBOSE(0, display(verbose_stream())); //IF_VERBOSE(0, display_watches(verbose_stream())); - //IF_VERBOSE(0, m_mc.display(verbose_stream())); + IF_VERBOSE(0, m_mc.display(verbose_stream())); + IF_VERBOSE(0, display_units(verbose_stream())); + //IF_VERBOSE(0, m_clone->display(verbose_stream() << "clone\n")); throw solver_exception("check model failed (for cloned solver)"); } } diff --git a/src/tactic/bv/bit_blaster_model_converter.cpp b/src/tactic/bv/bit_blaster_model_converter.cpp index 785ecb57e..5474700c3 100644 --- a/src/tactic/bv/bit_blaster_model_converter.cpp +++ b/src/tactic/bv/bit_blaster_model_converter.cpp @@ -52,7 +52,7 @@ struct bit_blaster_model_converter : public model_converter { m_newbits.push_back(f); } - virtual ~bit_blaster_model_converter() { + ~bit_blaster_model_converter() override { } void collect_bits(obj_hashtable & bits) { @@ -123,10 +123,7 @@ struct bit_blaster_model_converter : public model_converter { SASSERT(is_uninterp_const(bit)); func_decl * bit_decl = to_app(bit)->get_decl(); expr * bit_val = old_model->get_const_interp(bit_decl); - if (bit_val == 0) { - goto bail; - } - if (m().is_true(bit_val)) + if (bit_val != nullptr && m().is_true(bit_val)) val++; } } @@ -141,18 +138,12 @@ struct bit_blaster_model_converter : public model_converter { func_decl * bit_decl = to_app(bit)->get_decl(); expr * bit_val = old_model->get_const_interp(bit_decl); // remark: if old_model does not assign bit_val, then assume it is false. - if (bit_val == 0) { - goto bail; - } - if (!util.is_zero(bit_val)) + if (bit_val != nullptr && !util.is_zero(bit_val)) val++; } } new_val = util.mk_numeral(val, bv_sz); new_model->register_decl(m_vars.get(i), new_val); - continue; - bail: - new_model->register_decl(m_vars.get(i), mk_bv(bs, *old_model)); } } diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index 7e64b9c2c..b762f6b09 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -40,6 +40,7 @@ Notes: #include "tactic/smtlogics/qfbv_tactic.h" #include "solver/tactic2solver.h" #include "tactic/bv/bv_bound_chk_tactic.h" +#include "ackermannization/ackermannize_bv_tactic.h" /////////////// class qfufbv_ackr_tactic : public tactic { @@ -158,13 +159,14 @@ static tactic * mk_qfufbv_preamble1(ast_manager & m, params_ref const & p) { static tactic * mk_qfufbv_preamble(ast_manager & m, params_ref const & p) { return and_then(mk_simplify_tactic(m), - mk_propagate_values_tactic(m), - mk_solve_eqs_tactic(m), - mk_elim_uncnstr_tactic(m), - if_no_proofs(if_no_unsat_cores(mk_reduce_args_tactic(m))), - if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))), - mk_max_bv_sharing_tactic(m) - ); + mk_propagate_values_tactic(m), + mk_solve_eqs_tactic(m), + mk_elim_uncnstr_tactic(m), + if_no_proofs(if_no_unsat_cores(mk_reduce_args_tactic(m))), + if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))), + mk_max_bv_sharing_tactic(m), + if_no_proofs(if_no_unsat_cores(mk_ackermannize_bv_tactic(m,p))) + ); } tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) { From 528dc8a3f8cbbd9f3d4fb017cf87d13fedb810af Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 31 Mar 2018 17:05:22 -0700 Subject: [PATCH 07/24] disable bdd variable elimination Signed-off-by: Nikolaj Bjorner --- src/sat/sat_clause_use_list.h | 9 +++++ src/sat/sat_elim_eqs.cpp | 2 +- src/sat/sat_elim_vars.cpp | 9 ++--- src/sat/sat_elim_vars.h | 2 +- src/sat/sat_model_converter.cpp | 5 --- src/sat/sat_simplifier.cpp | 12 +++++-- src/sat/sat_simplifier.h | 1 + src/sat/sat_solver.cpp | 3 +- src/tactic/portfolio/parallel_tactic.cpp | 45 +++++++++++++++--------- src/tactic/smtlogics/qfbv_tactic.cpp | 2 ++ 10 files changed, 58 insertions(+), 32 deletions(-) diff --git a/src/sat/sat_clause_use_list.h b/src/sat/sat_clause_use_list.h index c028ad713..90c2d7779 100644 --- a/src/sat/sat_clause_use_list.h +++ b/src/sat/sat_clause_use_list.h @@ -124,6 +124,15 @@ namespace sat { }; iterator mk_iterator() const { return iterator(const_cast(this)->m_clauses); } + + std::ostream& display(std::ostream& out) const { + iterator it = mk_iterator(); + while (!it.at_end()) { + out << it.curr() << "\n"; + it.next(); + } + return out; + } }; }; diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp index 11c1d4780..870aa7fe2 100644 --- a/src/sat/sat_elim_eqs.cpp +++ b/src/sat/sat_elim_eqs.cpp @@ -199,7 +199,7 @@ namespace sat { literal r = roots[v]; SASSERT(v != r.var()); bool root_ok = !m_solver.is_external(v) || m_solver.set_root(l, r); - if (m_solver.is_external(v) && (m_solver.is_incremental() || !root_ok)) { + if (m_solver.is_assumption(v) || (m_solver.is_external(v) && (m_solver.is_incremental() || !root_ok))) { // cannot really eliminate v, since we have to notify extension of future assignments m_solver.mk_bin_clause(~l, r, false); m_solver.mk_bin_clause(l, ~r, false); diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp index 34f871a8f..a80807450 100644 --- a/src/sat/sat_elim_vars.cpp +++ b/src/sat/sat_elim_vars.cpp @@ -101,7 +101,7 @@ namespace sat{ pos_occs.reset(); neg_occs.reset(); literal_vector lits; - add_clauses(b, lits); + add_clauses(v, b, lits); return true; } @@ -157,7 +157,7 @@ namespace sat{ return b; } - void elim_vars::add_clauses(bdd const& b, literal_vector& lits) { + void elim_vars::add_clauses(bool_var v0, bdd const& b, literal_vector& lits) { if (b.is_true()) { // no-op } @@ -167,6 +167,7 @@ namespace sat{ if (simp.cleanup_clause(c)) return; + if (v0 == 39063) IF_VERBOSE(0, verbose_stream() << "bdd: " << c << "\n"); switch (c.size()) { case 0: s.set_conflict(justification()); @@ -198,10 +199,10 @@ namespace sat{ else { unsigned v = m_vars[b.var()]; lits.push_back(literal(v, false)); - add_clauses(b.lo(), lits); + add_clauses(v0, b.lo(), lits); lits.pop_back(); lits.push_back(literal(v, true)); - add_clauses(b.hi(), lits); + add_clauses(v0, b.hi(), lits); lits.pop_back(); } } diff --git a/src/sat/sat_elim_vars.h b/src/sat/sat_elim_vars.h index ba5a02d67..b62fdc5db 100644 --- a/src/sat/sat_elim_vars.h +++ b/src/sat/sat_elim_vars.h @@ -57,7 +57,7 @@ namespace sat { bdd make_clauses(literal lit); bdd mk_literal(literal l); void get_clauses(bdd const& b, literal_vector& lits, clause_vector& clauses, literal_vector& units); - void add_clauses(bdd const& b, literal_vector& lits); + void add_clauses(bool_var v, bdd const& b, literal_vector& lits); bool elim_var(bool_var v, bdd const& b); bdd elim_var(bool_var v); diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index c9d046197..c2a4858f7 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -91,11 +91,6 @@ namespace sat { for (literal l : it->m_clauses) { if (l == null_literal) { // end of clause - if (v0 == 36858) - IF_VERBOSE(0, verbose_stream() << "clause: " << clause << "\n"; - for (literal lit : clause) verbose_stream() << m[lit.var()] << " "; - verbose_stream() << "\n";); - elim_stack* st = it->m_elim_stack[index]; if (!sat) { VERIFY(legal_to_flip(v0)); diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 642fca348..bac790698 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1518,6 +1518,14 @@ namespace sat { } void block_covered_clause(clause& c, literal l, model_converter::kind k) { + if (false && l.var() == 39021) { + IF_VERBOSE(0, verbose_stream() << "blocked: " << l << " @ " << c << " :covered " << m_covered_clause << "\n"; + s.m_use_list.display(verbose_stream() << "use " << l << ":", l); + s.m_use_list.display(verbose_stream() << "use " << ~l << ":", ~l); + /*s.s.display(verbose_stream());*/ + ); + + } TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";); SASSERT(!s.is_external(l)); model_converter::entry& new_entry = mc.mk(k, l.var()); @@ -1563,7 +1571,6 @@ namespace sat { for (literal l2 : m_intersection) { watched* w = find_binary_watch(s.get_wlist(~l), ~l2); if (!w) { - IF_VERBOSE(10, verbose_stream() << "bca " << l << " " << ~l2 << "\n";); s.s.mk_bin_clause(l, ~l2, true); ++s.m_num_bca; } @@ -1934,6 +1941,7 @@ namespace sat { m_new_cls.reset(); if (!resolve(c1, c2, pos_l, m_new_cls)) continue; + // if (v == 39063) IF_VERBOSE(0, verbose_stream() << "elim: " << c1 << " + " << c2 << " -> " << m_new_cls << "\n"); TRACE("resolution_new_cls", tout << c1 << "\n" << c2 << "\n-->\n" << m_new_cls << "\n";); if (cleanup_clause(m_new_cls)) continue; // clause is already satisfied. @@ -2045,7 +2053,7 @@ namespace sat { m_subsumption = p.subsumption(); m_subsumption_limit = p.subsumption_limit(); m_elim_vars = p.elim_vars(); - m_elim_vars_bdd = p.elim_vars_bdd(); + m_elim_vars_bdd = false && p.elim_vars_bdd(); // buggy m_elim_vars_bdd_delay = p.elim_vars_bdd_delay(); m_incremental_mode = s.get_config().m_incremental && !p.override_incremental(); } diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index 086111f84..a777e07a4 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -47,6 +47,7 @@ namespace sat { clause_use_list & get(literal l) { return m_use_list[l.index()]; } clause_use_list const & get(literal l) const { return m_use_list[l.index()]; } void finalize() { m_use_list.finalize(); } + std::ostream& display(std::ostream& out, literal l) const { return m_use_list[l.index()].display(out); } }; class simplifier { diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 7def379e0..299b1f704 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1654,11 +1654,10 @@ namespace sat { // m_mc.set_solver(nullptr); m_mc(m_model); - if (!check_clauses(m_model)) { IF_VERBOSE(0, verbose_stream() << "failure checking clauses on transformed model\n";); - IF_VERBOSE(10, m_mc.display(verbose_stream())); + // IF_VERBOSE(10, m_mc.display(verbose_stream())); throw solver_exception("check model failed"); } diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp index 4a5af3679..b19bab487 100644 --- a/src/tactic/portfolio/parallel_tactic.cpp +++ b/src/tactic/portfolio/parallel_tactic.cpp @@ -114,10 +114,10 @@ class parallel_tactic : public tactic { dec_wait(); return st; } - { - std::unique_lock lock(m_mutex); - m_cond.wait(lock); - } + { + std::unique_lock lock(m_mutex); + m_cond.wait(lock); + } dec_wait(); } return nullptr; @@ -233,7 +233,9 @@ class parallel_tactic : public tactic { void inc_depth(unsigned inc) { m_depth += inc; } - void inc_width(unsigned w) { m_width *= w; } + void inc_width(unsigned w) { + m_width *= w; + } double get_width() const { return m_width; } @@ -280,14 +282,14 @@ class parallel_tactic : public tactic { void set_cube_params() { unsigned cutoff = m_cube_cutoff; double fraction = m_cube_fraction; - if (m_depth == 1 && cutoff > 0) { - fraction = 0; // use fixed cubing at depth 1. + if (true || (m_depth == 1 && cutoff > 0)) { + m_params.set_sym("lookahead.cube.cutoff", symbol("depth")); + m_params.set_uint("lookahead.cube.depth", std::max(m_depth, 10u)); } else { - cutoff = 0; // use dynamic cubing beyond depth 1 + m_params.set_sym("lookahead.cube.cutoff", symbol("adaptive_psat")); + m_params.set_double("lookahead.cube.fraction", fraction); } - m_params.set_uint ("lookahead.cube.cutoff", cutoff); - m_params.set_double("lookahead.cube.fraction", fraction); get_solver().updt_params(m_params); } @@ -329,6 +331,7 @@ private: task_queue m_queue; std::mutex m_mutex; double m_progress; + unsigned m_branches; bool m_has_undef; bool m_allsat; unsigned m_num_unsat; @@ -341,20 +344,27 @@ private: m_has_undef = false; m_allsat = false; m_num_unsat = 0; + m_branches = 0; m_exn_code = 0; m_params.set_bool("override_incremental", true); } + void add_branches(unsigned b) { + std::lock_guard lock(m_mutex); + m_branches += b; + } + void close_branch(solver_state& s, lbool status) { double f = 100.0 / s.get_width(); { std::lock_guard lock(m_mutex); m_progress += f; + --m_branches; } - IF_VERBOSE(1, verbose_stream() << "(tactic.parallel :progress " << m_progress << "% "; + IF_VERBOSE(0, verbose_stream() << "(tactic.parallel :progress " << m_progress << "% "; if (status == l_true) verbose_stream() << ":status sat "; if (status == l_undef) verbose_stream() << ":status unknown "; - verbose_stream() << ":unsat " << m_num_unsat << ")\n";); + verbose_stream() << ":unsat " << m_num_unsat << " :branches " << m_branches << ")\n";); } void report_sat(solver_state& s) { @@ -401,7 +411,7 @@ private: cube.reset(); cube.append(s.split_cubes(1)); SASSERT(cube.size() <= 1); - IF_VERBOSE(2, verbose_stream() << "(sat.parallel :split-cube " << cube.size() << ")\n";); + IF_VERBOSE(2, verbose_stream() << "(tactic.parallel :split-cube " << cube.size() << ")\n";); if (!s.cubes().empty()) m_queue.add_task(s.clone()); if (!cube.empty()) s.assert_cube(cube.get(0)); s.inc_depth(1); @@ -430,8 +440,8 @@ private: cubes.push_back(mk_and(c)); } - IF_VERBOSE(1, verbose_stream() << "(parallel_tactic :cubes " << cubes.size() << ")\n";); - IF_VERBOSE(10, verbose_stream() << "(parallel_tactic :cubes " << cubes << ")\n";); + IF_VERBOSE(1, verbose_stream() << "(tactic.parallel :cubes " << cubes.size() << ")\n";); + IF_VERBOSE(12, verbose_stream() << "(tactic.parallel :cubes " << cubes << ")\n";); if (cubes.empty()) { report_unsat(s); @@ -439,6 +449,7 @@ private: } else { s.inc_width(cubes.size()); + add_branches(cubes.size()); s.set_cubes(cubes); s.set_type(conquer_task); goto conquer; @@ -462,7 +473,7 @@ private: } if (canceled(s)) return; } - IF_VERBOSE(1, verbose_stream() << "(parallel_tactic :cubes " << cubes.size() << " :hard-cubes " << hard_cubes.size() << ")\n";); + IF_VERBOSE(1, verbose_stream() << "(tactic.parallel :cubes " << cubes.size() << " :hard-cubes " << hard_cubes.size() << ")\n";); if (hard_cubes.empty()) return; s.set_cubes(hard_cubes); @@ -534,7 +545,7 @@ private: m_stats.display(out); m_queue.display(out); std::lock_guard lock(m_mutex); - out << "(parallel_tactic :unsat " << m_num_unsat << " :progress " << m_progress << "% :models " << m_models.size() << ")\n"; + out << "(tactic.parallel :unsat " << m_num_unsat << " :progress " << m_progress << "% :models " << m_models.size() << ")\n"; return out; } diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index b69069864..f28129a52 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -28,6 +28,7 @@ Notes: #include "tactic/bv/bv_size_reduction_tactic.h" #include "tactic/aig/aig_tactic.h" #include "sat/tactic/sat_tactic.h" +#include "tactic/portfolio/parallel_tactic.h" #include "ackermannization/ackermannize_bv_tactic.h" #define MEMLIMIT 300 @@ -130,6 +131,7 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { tactic * new_sat = cond(mk_produce_proofs_probe(), and_then(mk_simplify_tactic(m), mk_smt_tactic()), + //mk_parallel_tactic(m, p)); mk_sat_tactic(m)); return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic()); From a954ab7d8db1c62a6bcb295da21e63a821b69248 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Apr 2018 08:38:01 -0700 Subject: [PATCH 08/24] flip literals in ATEs produced using RI Signed-off-by: Nikolaj Bjorner --- src/sat/sat_asymm_branch.cpp | 1 + src/sat/sat_big.cpp | 4 +- src/sat/sat_model_converter.cpp | 76 ++++++++++---- src/sat/sat_model_converter.h | 23 +++-- src/sat/sat_simplifier.cpp | 172 +++++++++++++++++++++++--------- src/sat/sat_solver.cpp | 29 ++++-- src/sat/sat_solver.h | 4 + 7 files changed, 224 insertions(+), 85 deletions(-) diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index 65003a6e4..b2053c68f 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -410,6 +410,7 @@ namespace sat { if (c.is_learned()) { m_elim_learned_literals += c.size() - new_sz; } + switch(new_sz) { case 0: s.set_conflict(justification()); diff --git a/src/sat/sat_big.cpp b/src/sat/sat_big.cpp index 2f1a3727f..27b87d4c9 100644 --- a/src/sat/sat_big.cpp +++ b/src/sat/sat_big.cpp @@ -194,7 +194,9 @@ namespace sat { if (u != get_parent(v) && safe_reach(u, v)) { ++elim; add_del(~u, v); - // IF_VERBOSE(1, verbose_stream() << "remove " << u << " -> " << v << "\n"); + if (s.get_config().m_drat) s.m_drat.del(~u, v); + s.m_mc.stackv().reset(); // TBD: brittle code + s.add_ate(~u, v); if (find_binary_watch(wlist, ~v)) { IF_VERBOSE(10, verbose_stream() << "binary: " << ~u << "\n"); s.assign(~u, justification()); diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index c2a4858f7..bebb3e384 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -75,33 +75,41 @@ namespace sat { void model_converter::operator()(model & m) const { vector::const_iterator begin = m_entries.begin(); vector::const_iterator it = m_entries.end(); - bool first = false; // true; + bool first = true; // false; // true; // false; // true; //SASSERT(!m_solver || m_solver->check_clauses(m)); while (it != begin) { --it; bool_var v0 = it->var(); - SASSERT(it->get_kind() != ELIM_VAR || m[v0] == l_undef); - // if it->get_kind() == BLOCK_LIT, then it might be the case that m[v] != l_undef, + SASSERT(it->get_kind() != ELIM_VAR || v0 == null_bool_var || m[v0] == l_undef); + // if it->get_kind() == BCE, then it might be the case that m[v] != l_undef, // and the following procedure flips its value. bool sat = false; bool var_sign = false; unsigned index = 0; literal_vector clause; - VERIFY(legal_to_flip(v0)); + VERIFY(v0 == null_bool_var || legal_to_flip(v0)); for (literal l : it->m_clauses) { if (l == null_literal) { // end of clause - elim_stack* st = it->m_elim_stack[index]; - if (!sat) { + if (!sat && it->get_kind() == ATE) { + IF_VERBOSE(0, display(verbose_stream() << "violated ate\n", *it) << "\n"); + IF_VERBOSE(0, for (unsigned v = 0; v < m.size(); ++v) verbose_stream() << v << " := " << m[v] << "\n";); + IF_VERBOSE(0, display(verbose_stream())); + exit(0); + first = false; + } + if (!sat && it->get_kind() != ATE && v0 != null_bool_var) { VERIFY(legal_to_flip(v0)); m[v0] = var_sign ? l_false : l_true; } + elim_stack* st = it->m_elim_stack[index]; if (st) { process_stack(m, clause, st->stack()); } sat = false; if (first && m_solver && !m_solver->check_clauses(m)) { IF_VERBOSE(0, display(verbose_stream() << "after processing stack\n", *it) << "\n"); + IF_VERBOSE(0, display(verbose_stream())); first = false; } ++index; @@ -191,17 +199,43 @@ namespace sat { entry & e = m_entries.back(); SASSERT(e.var() == v); SASSERT(e.get_kind() == k); - VERIFY(legal_to_flip(v)); + VERIFY(v == null_bool_var || legal_to_flip(v)); return e; } + void model_converter::add_ate(clause const& c) { + if (stackv().empty()) return; + insert(mk(ATE, null_bool_var), c); + } + + void model_converter::add_ate(literal_vector const& lits) { + if (stackv().empty()) return; + insert(mk(ATE, null_bool_var), lits); + } + + void model_converter::add_ate(literal l1, literal l2) { + if (stackv().empty()) return; + insert(mk(ATE, null_bool_var), l1, l2); + } + + void model_converter::add_elim_stack(entry & e) { + e.m_elim_stack.push_back(stackv().empty() ? nullptr : alloc(elim_stack, stackv())); +#if 0 + if (!stackv().empty() && e.get_kind() == ATE) { + IF_VERBOSE(0, display(verbose_stream(), e) << "\n"); + } +#endif + for (auto const& s : stackv()) VERIFY(legal_to_flip(s.second.var())); + stackv().reset(); + } + void model_converter::insert(entry & e, clause const & c) { SASSERT(c.contains(e.var())); SASSERT(m_entries.begin() <= &e); SASSERT(&e < m_entries.end()); for (literal l : c) e.m_clauses.push_back(l); e.m_clauses.push_back(null_literal); - e.m_elim_stack.push_back(nullptr); + add_elim_stack(e); TRACE("sat_mc_bug", tout << "adding: " << c << "\n";); } @@ -212,7 +246,7 @@ namespace sat { e.m_clauses.push_back(l1); e.m_clauses.push_back(l2); e.m_clauses.push_back(null_literal); - e.m_elim_stack.push_back(nullptr); + add_elim_stack(e); TRACE("sat_mc_bug", tout << "adding (binary): " << l1 << " " << l2 << "\n";); } @@ -224,18 +258,17 @@ namespace sat { for (unsigned i = 0; i < sz; ++i) e.m_clauses.push_back(c[i]); e.m_clauses.push_back(null_literal); - e.m_elim_stack.push_back(nullptr); + add_elim_stack(e); // TRACE("sat_mc_bug", tout << "adding (wrapper): "; for (literal l : c) tout << l << " "; tout << "\n";); } - void model_converter::insert(entry & e, literal_vector const& c, elim_stackv const& elims) { + void model_converter::insert(entry & e, literal_vector const& c) { SASSERT(c.contains(literal(e.var(), false)) || c.contains(literal(e.var(), true))); SASSERT(m_entries.begin() <= &e); SASSERT(&e < m_entries.end()); for (literal l : c) e.m_clauses.push_back(l); e.m_clauses.push_back(null_literal); - e.m_elim_stack.push_back(elims.empty() ? nullptr : alloc(elim_stack, elims)); - for (auto const& s : elims) VERIFY(legal_to_flip(s.second.var())); + add_elim_stack(e); TRACE("sat_mc_bug", tout << "adding: " << c << "\n";); } @@ -246,7 +279,7 @@ namespace sat { vector::const_iterator it = m_entries.begin(); vector::const_iterator end = m_entries.end(); for (; it != end; ++it) { - SASSERT(it->var() < num_vars); + SASSERT(it->var() == null_bool_var || it->var() < num_vars); if (it->get_kind() == ELIM_VAR) { svector::const_iterator it2 = it; it2++; @@ -276,7 +309,8 @@ namespace sat { } std::ostream& model_converter::display(std::ostream& out, entry const& entry) const { - out << " (" << entry.get_kind() << " " << entry.var(); + out << " (" << entry.get_kind() << " "; + if (entry.var() != null_bool_var) out << entry.var(); bool start = true; unsigned index = 0; for (literal l : entry.m_clauses) { @@ -306,7 +340,7 @@ namespace sat { } out << ")"; for (literal l : entry.m_clauses) { - if (l != null_literal) { + if (l != null_literal && l.var() != null_bool_var) { if (false && m_solver && m_solver->was_eliminated(l.var())) out << "\neliminated: " << l; } } @@ -333,7 +367,7 @@ namespace sat { for (entry const& e : m_entries) { for (literal l : e.m_clauses) { if (l != null_literal) { - if (l.var() > result) + if (l.var() != null_bool_var && l.var() > result) result = l.var(); } } @@ -372,9 +406,11 @@ namespace sat { update_stack.push_back(null_literal); } } - swap(e.var(), clause.size(), clause); - update_stack.append(clause); - update_stack.push_back(null_literal); + if (e.var() != null_bool_var) { + swap(e.var(), clause.size(), clause); + update_stack.append(clause); + update_stack.push_back(null_literal); + } clause.reset(); } else { diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h index bc60844ca..65e132729 100644 --- a/src/sat/sat_model_converter.h +++ b/src/sat/sat_model_converter.h @@ -66,11 +66,11 @@ namespace sat { unsigned ref_count() const { return m_refcount; } }; - enum kind { ELIM_VAR = 0, BLOCK_LIT, CCE, ACCE }; + enum kind { ELIM_VAR = 0, BCE, CCE, ACCE, ABCE, ATE }; class entry { friend class model_converter; - unsigned m_var:30; - unsigned m_kind:2; + bool_var m_var; + kind m_kind; literal_vector m_clauses; // the different clauses are separated by null_literal sref_vector m_elim_stack; entry(kind k, bool_var v): m_var(v), m_kind(k) {} @@ -82,11 +82,12 @@ namespace sat { m_elim_stack.append(src.m_elim_stack); } bool_var var() const { return m_var; } - kind get_kind() const { return static_cast(m_kind); } + kind get_kind() const { return m_kind; } }; private: vector m_entries; solver const* m_solver; + elim_stackv m_elim_stack; void process_stack(model & m, literal_vector const& clause, elim_stackv const& stack) const; @@ -96,6 +97,8 @@ namespace sat { void swap(bool_var v, unsigned sz, literal_vector& clause); + void add_elim_stack(entry & e); + public: model_converter(); ~model_converter(); @@ -103,11 +106,17 @@ namespace sat { void operator()(model & m) const; model_converter& operator=(model_converter const& other); + elim_stackv& stackv() { return m_elim_stack; } + entry & mk(kind k, bool_var v); void insert(entry & e, clause const & c); void insert(entry & e, literal l1, literal l2); void insert(entry & e, clause_wrapper const & c); - void insert(entry & c, literal_vector const& covered_clause, elim_stackv const& elim_stack); + void insert(entry & c, literal_vector const& covered_clause); + + void add_ate(literal_vector const& lits); + void add_ate(literal l1, literal l2); + void add_ate(clause const& c); bool empty() const { return m_entries.empty(); } @@ -137,9 +146,11 @@ namespace sat { inline std::ostream& operator<<(std::ostream& out, model_converter::kind k) { switch (k) { case model_converter::ELIM_VAR: out << "elim"; break; - case model_converter::BLOCK_LIT: out << "blocked"; break; + case model_converter::BCE: out << "bce"; break; case model_converter::CCE: out << "cce"; break; case model_converter::ACCE: out << "acce"; break; + case model_converter::ABCE: out << "abce"; break; + case model_converter::ATE: out << "ate"; break; } return out; } diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index bac790698..52c7236a0 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -939,16 +939,21 @@ namespace sat { bool operator==(clause_ante const& a) const { return a.m_lit1 == m_lit1 && a.m_lit2 == m_lit2 && a.m_clause == m_clause; } - std::ostream& display(std::ostream& out) const { + std::ostream& display(std::ostream& out, literal lit) const { if (cls()) { out << *cls() << " "; } + else { + out << "(" << ~lit; + } if (lit1() != null_literal) { - out << lit1() << " "; + out << " " << lit1(); } if (lit2() != null_literal) { - out << lit2() << " "; + out << " " << lit2(); } + if (!cls()) out << ")"; + if (from_ri()) out << "ri"; out << "\n"; return out; } @@ -978,7 +983,7 @@ namespace sat { simplifier & s; int m_counter; - model_converter & mc; + model_converter & m_mc; queue m_queue; literal_vector m_covered_clause; // covered clause @@ -987,7 +992,6 @@ namespace sat { literal_vector m_tautology; // literals that are used in blocking tautology literal_vector m_new_intersection; svector m_in_intersection; - sat::model_converter::elim_stackv m_elim_stack; unsigned m_ala_qhead; clause_wrapper m_clause; @@ -995,7 +999,7 @@ namespace sat { vector & wlist): s(_s), m_counter(limit), - mc(_mc), + m_mc(_mc), m_queue(l, wlist), m_clause(null_literal, null_literal) { m_in_intersection.resize(s.s.num_vars() * 2, false); @@ -1069,6 +1073,7 @@ namespace sat { m_tautology.reset(); if (!process_var(l.var())) return false; bool first = true; + VERIFY(s.value(l) == l_undef); for (watched & w : s.get_wlist(l)) { // when adding a blocked clause, then all non-learned clauses have to be considered for the // resolution intersection. @@ -1184,18 +1189,18 @@ namespace sat { if (m_covered_antecedent[i] == clause_ante()) s.mark_visited(lit); if (s.is_marked(lit)) idx = i; } - if (false && _blocked.var() == 16774) { + if (false) { IF_VERBOSE(0, verbose_stream() << "covered: " << m_covered_clause << "\n"; verbose_stream() << "tautology: " << m_tautology << "\n"; verbose_stream() << "index: " << idx << "\n"; for (unsigned i = idx; i > 0; --i) { - m_covered_antecedent[i].display(verbose_stream() << "ante " << m_covered_clause[i] << ":"); + m_covered_antecedent[i].display(verbose_stream(), m_covered_clause[i]); }); } for (unsigned i = idx; i > 0; --i) { literal lit = m_covered_clause[i]; - s.mark_visited(lit); - continue; + //s.mark_visited(lit); + //continue; if (!s.is_marked(lit)) continue; clause_ante const& ante = m_covered_antecedent[i]; if (ante.cls()) { @@ -1222,13 +1227,16 @@ namespace sat { clause_ante const& ante = m_covered_antecedent[i]; if (ante.from_ri() && blocked != ante.lit1()) { blocked = ante.lit1(); - m_elim_stack.push_back(std::make_pair(j, blocked)); + VERIFY(s.value(blocked) == l_undef); + m_mc.stackv().push_back(std::make_pair(j, blocked)); } m_covered_clause[j++] = lit; s.unmark_visited(lit); } } for (literal l : m_covered_clause) VERIFY(!s.is_marked(l)); + for (bool_var v = 0; v < s.s.num_vars(); ++v) VERIFY(!s.is_marked(literal(v, true)) && !s.is_marked(literal(v, false))); + // unsigned sz0 = m_covered_clause.size(); m_covered_clause.resize(j); VERIFY(j >= m_clause.size()); @@ -1263,6 +1271,7 @@ namespace sat { return true; } if (!s.is_marked(~lit)) { + // if (m_covered_clause[0].var() == 10219) IF_VERBOSE(0, verbose_stream() << "ala: " << l << " " << lit << "\n"); m_covered_clause.push_back(~lit); m_covered_antecedent.push_back(clause_ante(l, false)); s.mark_visited(~lit); @@ -1292,6 +1301,7 @@ namespace sat { if (lit1 == null_literal) { return true; } + // if (m_covered_clause[0].var() == 10219) IF_VERBOSE(0, verbose_stream() << "ala: " << c << " " << lit1 << "\n"); m_covered_clause.push_back(~lit1); m_covered_antecedent.push_back(clause_ante(c)); s.mark_visited(~lit1); @@ -1332,13 +1342,17 @@ namespace sat { return sz0 * 400 < m_covered_clause.size(); } + void reset_mark() { + for (literal l : m_covered_clause) s.unmark_visited(l); + } + template elim_type cce(literal& blocked, model_converter::kind& k) { - bool is_tautology = false, first = true; + bool first = true; unsigned sz = 0, sz0 = m_covered_clause.size(); for (literal l : m_covered_clause) s.mark_visited(l); shuffle(m_covered_clause.size(), m_covered_clause.c_ptr(), s.s.m_rand); - m_elim_stack.reset(); + m_mc.stackv().reset(); m_ala_qhead = 0; switch (et) { @@ -1349,7 +1363,7 @@ namespace sat { k = model_converter::ACCE; break; default: - k = model_converter::BLOCK_LIT; + k = model_converter::BCE; break; } @@ -1361,48 +1375,77 @@ namespace sat { * and then check if any of the first sz0 literals are blocked. */ - while (!is_tautology && m_covered_clause.size() > sz && !above_threshold(sz0)) { - SASSERT(!is_tautology); + if (et == ate_t) { + bool ala = add_ala(); + reset_mark(); + m_covered_clause.shrink(sz0); + return ala ? ate_t : no_t; + } - if ((et == abce_t || et == acce_t || et == ate_t) && add_ala()) { - for (literal l : m_covered_clause) s.unmark_visited(l); + while (m_covered_clause.size() > sz && !above_threshold(sz0)) { + + if ((et == abce_t || et == acce_t) && add_ala()) { + reset_mark(); + if (first) { + m_covered_clause.shrink(sz0); + } + else { + /* + * tautology depends on resolution intersection. + * literals used for resolution intersection may have to be flipped. + */ + m_tautology.reset(); + for (literal l : m_covered_clause) { + m_tautology.push_back(l); + s.mark_visited(l); + } + minimize_covered_clause(m_covered_clause.size()-1); + } return ate_t; } - if (et == ate_t) { - for (literal l : m_covered_clause) s.unmark_visited(l); - return no_t; - } - if (first) { for (unsigned i = 0; i < sz0; ++i) { if (check_abce_tautology(m_covered_clause[i])) { blocked = m_covered_clause[i]; - is_tautology = true; - break; + reset_mark(); +#if 0 + if (sz0 == 3 && blocked.var() == 10219) { + IF_VERBOSE(0, verbose_stream() << "abce: " << m_covered_clause << "\n"; + for (literal l : m_covered_clause) verbose_stream() << s.value(l) << "\n"; + ); + literal l = blocked; + clause_use_list & neg_occs = s.m_use_list.get(~l); + for (auto it = neg_occs.mk_iterator(); !it.at_end(); it.next()) { + clause & c = it.curr(); + IF_VERBOSE(0, verbose_stream() << c << "\n"); + } + } +#endif + m_covered_clause.shrink(sz0); + if (et == bce_t) return bce_t; + k = model_converter::ABCE; + return abce_t; } } - first = false; } + first = false; - if (is_tautology || et == abce_t || et == bce_t) { - for (literal l : m_covered_clause) s.unmark_visited(l); - m_covered_clause.shrink(sz0); - if (!is_tautology) return no_t; - if (et == bce_t) return bce_t; - return abce_t; + if (et == abce_t || et == bce_t) { + break; } /* * Add resolution intersection while checking if the clause becomes a tautology. */ sz = m_covered_clause.size(); - if (et == cce_t || et == acce_t) { - is_tautology = add_cla(blocked); + if ((et == cce_t || et == acce_t) && add_cla(blocked)) { + reset_mark(); + return et; } } - for (literal l : m_covered_clause) s.unmark_visited(l); - return is_tautology ? et : no_t; + reset_mark(); + return no_t; } // perform covered clause elimination. @@ -1463,13 +1506,14 @@ namespace sat { case ate_t: w.set_learned(true); s.s.set_learned1(l2, l, true); + m_mc.add_ate(m_covered_clause); break; case no_t: break; default: - block_covered_binary(w, l, blocked, k); w.set_learned(true); s.s.set_learned1(l2, l, true); + block_covered_binary(w, l, blocked, k); break; } } @@ -1487,7 +1531,8 @@ namespace sat { inc_bc(r); switch (r) { case ate_t: - s.set_learned(c); + m_mc.add_ate(m_covered_clause); + s.set_learned(c); break; case no_t: break; @@ -1518,32 +1563,33 @@ namespace sat { } void block_covered_clause(clause& c, literal l, model_converter::kind k) { - if (false && l.var() == 39021) { + if (false) { IF_VERBOSE(0, verbose_stream() << "blocked: " << l << " @ " << c << " :covered " << m_covered_clause << "\n"; s.m_use_list.display(verbose_stream() << "use " << l << ":", l); s.m_use_list.display(verbose_stream() << "use " << ~l << ":", ~l); - /*s.s.display(verbose_stream());*/ + display_watch_list(verbose_stream() << ~l << ": ", s.s.m_cls_allocator, s.get_wlist(l)) << "\n"; + display_watch_list(verbose_stream() << l << ": ", s.s.m_cls_allocator, s.get_wlist(~l)) << "\n"; ); } TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";); SASSERT(!s.is_external(l)); - model_converter::entry& new_entry = mc.mk(k, l.var()); + model_converter::entry& new_entry = m_mc.mk(k, l.var()); for (literal lit : c) { if (lit != l && process_var(lit.var())) { m_queue.decreased(~lit); } } - mc.insert(new_entry, m_covered_clause, m_elim_stack); + m_mc.insert(new_entry, m_covered_clause); } void block_covered_binary(watched const& w, literal l1, literal blocked, model_converter::kind k) { SASSERT(!s.is_external(blocked)); - model_converter::entry& new_entry = mc.mk(k, blocked.var()); + model_converter::entry& new_entry = m_mc.mk(k, blocked.var()); literal l2 = w.get_literal(); TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l1 << "\n";); s.set_learned(l1, l2); - mc.insert(new_entry, m_covered_clause, m_elim_stack); + m_mc.insert(new_entry, m_covered_clause); m_queue.decreased(~l2); } @@ -1571,6 +1617,13 @@ namespace sat { for (literal l2 : m_intersection) { watched* w = find_binary_watch(s.get_wlist(~l), ~l2); if (!w) { +#if 0 + IF_VERBOSE(0, verbose_stream() << "bca " << l << " " << ~l2 << "\n"); + if (l.var() == 10219 && l2.var() == 10202) { + IF_VERBOSE(0, s.s.display(verbose_stream())); + exit(0); + } +#endif s.s.mk_bin_clause(l, ~l2, true); ++s.m_num_bca; } @@ -1777,13 +1830,19 @@ namespace sat { } void simplifier::save_clauses(model_converter::entry & mc_entry, clause_wrapper_vector const & cs) { - model_converter & mc = s.m_mc; for (auto & e : cs) { - mc.insert(mc_entry, e); + s.m_mc.insert(mc_entry, e); } } void simplifier::add_non_learned_binary_clause(literal l1, literal l2) { +#if 0 + if ((l1.var() == 2039 || l2.var() == 2039) && + (l1.var() == 27042 || l2.var() == 27042)) { + IF_VERBOSE(1, verbose_stream() << "add_bin: " << l1 << " " << l2 << "\n"); + } +#endif +#if 0 watched* w; watch_list & wlist1 = get_wlist(~l1); watch_list & wlist2 = get_wlist(~l2); @@ -1804,6 +1863,9 @@ namespace sat { else { wlist2.push_back(watched(l1, false)); } +#else + s.mk_bin_clause(l1, l2, false); +#endif } /** @@ -1820,6 +1882,11 @@ namespace sat { watch_list::iterator end2 = wlist2.end(); for (; it2 != end2; ++it2) { if (it2->is_binary_clause() && it2->get_literal() == l) { + if ((l.var() == 2039 || l2.var() == 2039) && + (l.var() == 27042 || l2.var() == 27042)) { + IF_VERBOSE(1, verbose_stream() << "remove_bin: " << l << " " << l2 << "\n"); + } + TRACE("bin_clause_bug", tout << "removing: " << l << " " << it2->get_literal() << "\n";); m_sub_bin_todo.erase(bin_clause(l2, l, it2->is_learned())); continue; @@ -1920,6 +1987,13 @@ namespace sat { m_elim_counter -= num_pos * num_neg + before_lits; + if (false) { + literal l(v, false); + IF_VERBOSE(0, + verbose_stream() << "elim: " << l << "\n"; + display_watch_list(verbose_stream() << ~l << ": ", s.m_cls_allocator, get_wlist(l)) << "\n"; + display_watch_list(verbose_stream() << l << ": ", s.m_cls_allocator, get_wlist(~l)) << "\n";); + } // eliminate variable ++s.m_stats.m_elim_var_res; VERIFY(!is_external(v)); @@ -1936,12 +2010,14 @@ namespace sat { m_elim_counter -= num_pos * num_neg + before_lits; + + for (auto & c1 : m_pos_cls) { for (auto & c2 : m_neg_cls) { m_new_cls.reset(); if (!resolve(c1, c2, pos_l, m_new_cls)) continue; - // if (v == 39063) IF_VERBOSE(0, verbose_stream() << "elim: " << c1 << " + " << c2 << " -> " << m_new_cls << "\n"); + if (false && v == 27041) IF_VERBOSE(0, verbose_stream() << "elim: " << c1 << " + " << c2 << " -> " << m_new_cls << "\n"); TRACE("resolution_new_cls", tout << c1 << "\n" << c2 << "\n-->\n" << m_new_cls << "\n";); if (cleanup_clause(m_new_cls)) continue; // clause is already satisfied. @@ -2053,7 +2129,7 @@ namespace sat { m_subsumption = p.subsumption(); m_subsumption_limit = p.subsumption_limit(); m_elim_vars = p.elim_vars(); - m_elim_vars_bdd = false && p.elim_vars_bdd(); // buggy + m_elim_vars_bdd = false && p.elim_vars_bdd(); // buggy? m_elim_vars_bdd_delay = p.elim_vars_bdd_delay(); m_incremental_mode = s.get_config().m_incremental && !p.override_incremental(); } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 299b1f704..da11ed3a1 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -333,6 +333,12 @@ namespace sat { } void solver::mk_bin_clause(literal l1, literal l2, bool learned) { +#if 0 + if ((l1.var() == 2039 || l2.var() == 2039) && + (l1.var() == 27042 || l2.var() == 27042)) { + IF_VERBOSE(1, verbose_stream() << "mk_bin: " << l1 << " " << l2 << " " << learned << "\n"); + } +#endif if (find_binary_watch(get_wlist(~l1), ~l2)) { assign(l1, justification()); return; @@ -345,13 +351,13 @@ namespace sat { if (w0) { if (w0->is_learned() && !learned) { w0->set_learned(false); - } - w0 = find_binary_watch(get_wlist(~l2), l1); - } - if (w0) { - if (w0->is_learned() && !learned) { - w0->set_learned(false); - } + } + else { + return; + } + w0 = find_binary_watch(get_wlist(~l2), l1); + VERIFY(w0); + w0->set_learned(false); return; } if (m_config.m_drat) @@ -671,7 +677,6 @@ namespace sat { TRACE("sat_assign_core", tout << l << " " << j << " level: " << scope_lvl() << "\n";); if (at_base_lvl()) { if (m_config.m_drat) m_drat.add(l, !j.is_none()); - j = justification(); // erase justification for level 0 } m_assignment[l.index()] = l_true; @@ -1215,7 +1220,7 @@ namespace sat { } } if (num_in > 0 || num_out > 0) { - IF_VERBOSE(1, verbose_stream() << "(sat-sync out: " << num_out << " in: " << num_in << ")\n";); + IF_VERBOSE(2, verbose_stream() << "(sat-sync out: " << num_out << " in: " << num_in << ")\n";); } } } @@ -1657,7 +1662,11 @@ namespace sat { if (!check_clauses(m_model)) { IF_VERBOSE(0, verbose_stream() << "failure checking clauses on transformed model\n";); - // IF_VERBOSE(10, m_mc.display(verbose_stream())); + IF_VERBOSE(10, m_mc.display(verbose_stream())); + //IF_VERBOSE(0, display_units(verbose_stream())); + //IF_VERBOSE(0, display(verbose_stream())); + IF_VERBOSE(0, for (bool_var v = 0; v < num; v++) verbose_stream() << v << ": " << m_model[v] << "\n";); + throw solver_exception("check model failed"); } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index c56c033a0..1bf78ab8c 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -236,6 +236,10 @@ namespace sat { void set_learned(clause& c, bool learned); void set_learned(literal l1, literal l2, bool learned); void set_learned1(literal l1, literal l2, bool learned); + void add_ate(clause& c) { m_mc.add_ate(c); } + void add_ate(literal l1, literal l2) { m_mc.add_ate(l1, l2); } + void add_ate(literal_vector const& lits) { m_mc.add_ate(lits); } + class scoped_disable_checkpoint { solver& s; public: From 21738d9750aa5902173ad47df61f5f4c7dcaf9d2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Apr 2018 15:59:55 -0700 Subject: [PATCH 09/24] fixes Signed-off-by: Nikolaj Bjorner --- src/sat/sat_model_converter.cpp | 3 ++- src/sat/sat_simplifier.cpp | 14 ++++---------- 2 files changed, 6 insertions(+), 11 deletions(-) diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index bebb3e384..b097b3462 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -75,7 +75,7 @@ namespace sat { void model_converter::operator()(model & m) const { vector::const_iterator begin = m_entries.begin(); vector::const_iterator it = m_entries.end(); - bool first = true; // false; // true; // false; // true; + bool first = false; // true; // false; // // true; //SASSERT(!m_solver || m_solver->check_clauses(m)); while (it != begin) { --it; @@ -101,6 +101,7 @@ namespace sat { if (!sat && it->get_kind() != ATE && v0 != null_bool_var) { VERIFY(legal_to_flip(v0)); m[v0] = var_sign ? l_false : l_true; + //IF_VERBOSE(0, verbose_stream() << "assign " << v0 << " "<< m[v0] << "\n"); } elim_stack* st = it->m_elim_stack[index]; if (st) { diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 52c7236a0..3f6c2d6ca 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1174,7 +1174,8 @@ namespace sat { This routine removes literals that were not relevant to establishing it was blocked. It has a bug: literals that are used to prune tautologies during resolution intersection should be included - in the dependencies. + in the dependencies. They may get used in some RI prunings and then they have to be included to avoid flipping + RI literals. */ void minimize_covered_clause(unsigned idx) { // IF_VERBOSE(0, verbose_stream() << "minimize: " << m_covered_clause @@ -1199,8 +1200,8 @@ namespace sat { } for (unsigned i = idx; i > 0; --i) { literal lit = m_covered_clause[i]; - //s.mark_visited(lit); - //continue; + s.mark_visited(lit); + continue; if (!s.is_marked(lit)) continue; clause_ante const& ante = m_covered_antecedent[i]; if (ante.cls()) { @@ -1617,13 +1618,6 @@ namespace sat { for (literal l2 : m_intersection) { watched* w = find_binary_watch(s.get_wlist(~l), ~l2); if (!w) { -#if 0 - IF_VERBOSE(0, verbose_stream() << "bca " << l << " " << ~l2 << "\n"); - if (l.var() == 10219 && l2.var() == 10202) { - IF_VERBOSE(0, s.s.display(verbose_stream())); - exit(0); - } -#endif s.s.mk_bin_clause(l, ~l2, true); ++s.m_num_bca; } From f2dfc0dc24c8594ae4d1181bfbb4b1848d057a94 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Apr 2018 15:46:21 -0700 Subject: [PATCH 10/24] including all touched tautology literals each round Signed-off-by: Nikolaj Bjorner --- src/sat/sat_simplifier.cpp | 25 ++++++++++++++++++------ src/tactic/portfolio/CMakeLists.txt | 2 ++ src/tactic/portfolio/parallel_tactic.cpp | 16 +-------------- src/tactic/smtlogics/qfbv_tactic.cpp | 7 ++++--- 4 files changed, 26 insertions(+), 24 deletions(-) diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 52c7236a0..ae156cb4b 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1069,8 +1069,8 @@ namespace sat { // Find literals that are in the intersection of all resolvents with l. // bool resolution_intersection(literal l, bool adding) { + unsigned tsz = m_tautology.size(); reset_intersection(); - m_tautology.reset(); if (!process_var(l.var())) return false; bool first = true; VERIFY(s.value(l) == l_undef); @@ -1086,6 +1086,7 @@ namespace sat { } if (!first || s.is_marked(lit)) { reset_intersection(); + m_tautology.shrink(tsz); return false; // intersection is empty or does not add anything new. } first = false; @@ -1122,22 +1123,30 @@ namespace sat { for (literal lit : m_new_intersection) add_intersection(lit); } - if (m_intersection.empty()) + if (m_intersection.empty()) { + m_tautology.shrink(tsz); return false; + } } } + if (m_intersection.empty()) { + m_tautology.shrink(tsz); + } // if (first) IF_VERBOSE(0, verbose_stream() << "taut: " << m_tautology << "\n";); return first; } bool check_abce_tautology(literal l) { - m_tautology.reset(); + unsigned tsz = m_tautology.size(); if (!process_var(l.var())) return false; for (watched & w : s.get_wlist(l)) { if (w.is_binary_non_learned_clause()) { literal lit = w.get_literal(); VERIFY(lit != ~l); - if (!s.is_marked(~lit)) return false; + if (!s.is_marked(~lit)) { + m_tautology.shrink(tsz); + return false; + } m_tautology.push_back(~lit); } } @@ -1153,7 +1162,10 @@ namespace sat { break; } } - if (!tautology) return false; + if (!tautology) { + m_tautology.shrink(tsz); + return false; + } } return true; } @@ -1352,6 +1364,7 @@ namespace sat { unsigned sz = 0, sz0 = m_covered_clause.size(); for (literal l : m_covered_clause) s.mark_visited(l); shuffle(m_covered_clause.size(), m_covered_clause.c_ptr(), s.s.m_rand); + m_tautology.reset(); m_mc.stackv().reset(); m_ala_qhead = 0; @@ -1394,7 +1407,6 @@ namespace sat { * tautology depends on resolution intersection. * literals used for resolution intersection may have to be flipped. */ - m_tautology.reset(); for (literal l : m_covered_clause) { m_tautology.push_back(l); s.mark_visited(l); @@ -1610,6 +1622,7 @@ namespace sat { Then the following binary clause is blocked: l \/ ~l' */ void bca(literal l) { + m_tautology.reset(); if (resolution_intersection(l, true)) { // this literal is pure. return; diff --git a/src/tactic/portfolio/CMakeLists.txt b/src/tactic/portfolio/CMakeLists.txt index 055251467..ed5ec8cf7 100644 --- a/src/tactic/portfolio/CMakeLists.txt +++ b/src/tactic/portfolio/CMakeLists.txt @@ -18,6 +18,8 @@ z3_add_component(portfolio smtlogic_tactics subpaving_tactic ufbv_tactic + PYG_FILES + parallel_params.pyg TACTIC_HEADERS default_tactic.h fd_solver.h diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp index b19bab487..e01e58051 100644 --- a/src/tactic/portfolio/parallel_tactic.cpp +++ b/src/tactic/portfolio/parallel_tactic.cpp @@ -159,8 +159,6 @@ class parallel_tactic : public tactic { ref m_solver; // solver state unsigned m_depth; // number of nested calls to cubing double m_width; // estimate of fraction of problem handled by state - unsigned m_cube_cutoff; // saved configuration value - double m_cube_fraction; // saved configuration value unsigned m_restart_max; // saved configuration value expr_ref_vector cube_literals(expr* cube) { @@ -185,8 +183,6 @@ class parallel_tactic : public tactic { m_depth(0), m_width(1.0) { - m_cube_cutoff = p.get_uint("sat.lookahead.cube.cutoff", 8); - m_cube_fraction = p.get_double("sat.lookahead.cube.fraction", 0.4); m_restart_max = p.get_uint("sat.restart.max", 10); } @@ -280,17 +276,7 @@ class parallel_tactic : public tactic { } void set_cube_params() { - unsigned cutoff = m_cube_cutoff; - double fraction = m_cube_fraction; - if (true || (m_depth == 1 && cutoff > 0)) { - m_params.set_sym("lookahead.cube.cutoff", symbol("depth")); - m_params.set_uint("lookahead.cube.depth", std::max(m_depth, 10u)); - } - else { - m_params.set_sym("lookahead.cube.cutoff", symbol("adaptive_psat")); - m_params.set_double("lookahead.cube.fraction", fraction); - } - get_solver().updt_params(m_params); + // get_solver().updt_params(m_params); } void set_conquer_params() { diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index f28129a52..0eb235791 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -29,6 +29,7 @@ Notes: #include "tactic/aig/aig_tactic.h" #include "sat/tactic/sat_tactic.h" #include "tactic/portfolio/parallel_tactic.h" +#include "tactic/portfolio/parallel_params.hpp" #include "ackermannization/ackermannize_bv_tactic.h" #define MEMLIMIT 300 @@ -128,11 +129,11 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { - + parallel_params pp(p); + bool use_parallel = pp.enable(); tactic * new_sat = cond(mk_produce_proofs_probe(), and_then(mk_simplify_tactic(m), mk_smt_tactic()), - //mk_parallel_tactic(m, p)); - mk_sat_tactic(m)); + use_parallel ? mk_parallel_tactic(m, p): mk_sat_tactic(m)); return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic()); From d57bca8f8cd7cd0de8c14b76a28c131085c9a213 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Apr 2018 10:43:55 +0800 Subject: [PATCH 11/24] fixes Signed-off-by: Nikolaj Bjorner --- src/sat/sat_lookahead.cpp | 2 +- src/sat/sat_model_converter.cpp | 2 +- src/sat/sat_simplifier.cpp | 9 +-- src/tactic/core/elim_uncnstr_tactic.cpp | 33 +++------ src/tactic/portfolio/CMakeLists.txt | 2 - src/tactic/portfolio/parallel_tactic.cpp | 88 ++++++++++++++++-------- src/tactic/smtlogics/CMakeLists.txt | 1 + src/tactic/smtlogics/qfbv_tactic.cpp | 2 +- 8 files changed, 78 insertions(+), 61 deletions(-) diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 5b89b4dfd..0d737500a 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -1832,7 +1832,7 @@ namespace sat { unsigned dl_truth = base + m_lookahead.size() * m_config.m_dl_max_iterations; scoped_level _sl(*this, dl_truth); //SASSERT(get_level(m_trail.back()) == dl_truth); - IF_VERBOSE(2, verbose_stream() << "(sat-lookahead :double " << l << " :depth " << m_trail_lim.size() << ")\n";); + IF_VERBOSE(3, verbose_stream() << "(sat-lookahead :double " << l << " :depth " << m_trail_lim.size() << ")\n";); lookahead_backtrack(); assign(l); propagate(); diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index b097b3462..22cab35ea 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -75,7 +75,7 @@ namespace sat { void model_converter::operator()(model & m) const { vector::const_iterator begin = m_entries.begin(); vector::const_iterator it = m_entries.end(); - bool first = false; // true; // false; // // true; + bool first = false; // true; // false; // // true; //SASSERT(!m_solver || m_solver->check_clauses(m)); while (it != begin) { --it; diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index c048740ac..9c57c79ed 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1129,7 +1129,8 @@ namespace sat { } } } - if (m_intersection.empty()) { + // remove tautology literals if literal has no resolution intersection + if (m_intersection.empty() && !first) { m_tautology.shrink(tsz); } // if (first) IF_VERBOSE(0, verbose_stream() << "taut: " << m_tautology << "\n";); @@ -1202,7 +1203,7 @@ namespace sat { if (m_covered_antecedent[i] == clause_ante()) s.mark_visited(lit); if (s.is_marked(lit)) idx = i; } - if (false) { + if (false && _blocked.var() == 8074) { IF_VERBOSE(0, verbose_stream() << "covered: " << m_covered_clause << "\n"; verbose_stream() << "tautology: " << m_tautology << "\n"; verbose_stream() << "index: " << idx << "\n"; @@ -1212,8 +1213,8 @@ namespace sat { } for (unsigned i = idx; i > 0; --i) { literal lit = m_covered_clause[i]; - s.mark_visited(lit); - continue; + //s.mark_visited(lit); + //continue; if (!s.is_marked(lit)) continue; clause_ante const& ante = m_covered_antecedent[i]; if (ante.cls()) { diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index 2f961f9bc..0fd25100e 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -552,7 +552,7 @@ class elim_uncnstr_tactic : public tactic { // The result of bv_le is not just introducing a new fresh name, // we need a side condition. // TODO: the correct proof step - return 0; + return nullptr; } if (uncnstr(arg1)) { // v <= t @@ -804,20 +804,17 @@ class elim_uncnstr_tactic : public tactic { ast_manager & m() { return m_manager; } void init_mc(bool produce_models) { - if (!produce_models) { - m_mc = 0; - return; + m_mc = nullptr; + if (produce_models) { + m_mc = alloc(mc, m(), "elim_uncstr"); } - m_mc = alloc(mc, m(), "elim_uncstr"); } void init_rw(bool produce_proofs) { m_rw = alloc(rw, m(), produce_proofs, m_vars, m_mc.get(), m_max_memory, m_max_steps); } - void operator()(goal_ref const & g, - goal_ref_buffer & result) { - bool produce_models = g->models_enabled(); + void operator()(goal_ref const & g, goal_ref_buffer & result) { bool produce_proofs = g->proofs_enabled(); TRACE("elim_uncnstr_bug", g->display(tout);); @@ -832,14 +829,9 @@ class elim_uncnstr_tactic : public tactic { } bool modified = true; TRACE("elim_uncnstr", tout << "unconstrained variables...\n"; - obj_hashtable::iterator it = m_vars.begin(); - obj_hashtable::iterator end = m_vars.end(); - for (; it != end; ++it) { - expr * v = *it; - tout << mk_ismt2_pp(v, m()) << " "; - } + for (expr * v : m_vars) tout << mk_ismt2_pp(v, m()) << " "; tout << "\n";); - init_mc(produce_models); + init_mc(g->models_enabled()); init_rw(produce_proofs); expr_ref new_f(m()); @@ -866,14 +858,9 @@ class elim_uncnstr_tactic : public tactic { else { app_ref_vector & fresh_vars = m_rw->cfg().m_fresh_vars; m_num_elim_apps = fresh_vars.size(); - if (produce_models && !fresh_vars.empty()) { - generic_model_converter * fmc = alloc(generic_model_converter, m(), "elim_uncnstr"); - for (app * f : fresh_vars) - fmc->hide(f); - g->add(concat(fmc, m_mc.get())); - } - else { - g->set((model_converter*)nullptr); + if (m_mc.get()) { + for (app * f : fresh_vars) m_mc->hide(f); + g->add(m_mc.get()); } } m_mc = 0; diff --git a/src/tactic/portfolio/CMakeLists.txt b/src/tactic/portfolio/CMakeLists.txt index ed5ec8cf7..055251467 100644 --- a/src/tactic/portfolio/CMakeLists.txt +++ b/src/tactic/portfolio/CMakeLists.txt @@ -18,8 +18,6 @@ z3_add_component(portfolio smtlogic_tactics subpaving_tactic ufbv_tactic - PYG_FILES - parallel_params.pyg TACTIC_HEADERS default_tactic.h fd_solver.h diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp index e01e58051..999dbc2e0 100644 --- a/src/tactic/portfolio/parallel_tactic.cpp +++ b/src/tactic/portfolio/parallel_tactic.cpp @@ -42,6 +42,7 @@ Notes: #include "solver/solver2tactic.h" #include "tactic/tactic.h" #include "tactic/portfolio/fd_solver.h" +#include "tactic/smtlogics/parallel_params.hpp" class parallel_tactic : public tactic { @@ -150,10 +151,27 @@ class parallel_tactic : public tactic { }; + class cube_var { + expr_ref_vector m_vars; + expr_ref m_cube; + public: + cube_var(expr* c, expr_ref_vector& vs): + m_vars(vs), m_cube(c, vs.get_manager()) {} + + cube_var operator()(ast_translation& tr) { + expr_ref_vector vars(tr.to()); + for (expr* v : m_vars) vars.push_back(tr(v)); + return cube_var(tr(m_cube.get()), vars); + } + + expr* cube() const { return m_cube; } + expr_ref_vector const& vars() { return m_vars; } + }; + class solver_state { task_type m_type; // current work role of the task scoped_ptr m_manager; // ownership handle to ast_manager - expr_ref_vector m_cubes; // set of cubes to process by task + vector m_cubes; // set of cubes to process by task expr_ref_vector m_asserted_cubes; // set of cubes asserted on the current solver params_ref m_params; // configuration parameters ref m_solver; // solver state @@ -176,14 +194,14 @@ class parallel_tactic : public tactic { solver_state(ast_manager* m, solver* s, params_ref const& p, task_type t): m_type(t), m_manager(m), - m_cubes(s->get_manager()), m_asserted_cubes(s->get_manager()), m_params(p), m_solver(s), m_depth(0), m_width(1.0) { - m_restart_max = p.get_uint("sat.restart.max", 10); + parallel_params pp(p); + m_restart_max = pp.restart_max(); } ast_manager& m() { return m_solver->get_manager(); } @@ -199,7 +217,7 @@ class parallel_tactic : public tactic { ast_translation tr(m, *new_m); solver* s = m_solver->translate(*new_m, m_params); solver_state* st = alloc(solver_state, new_m, s, m_params, m_type); - for (expr* c : m_cubes) st->m_cubes.push_back(tr(c)); + for (auto & c : m_cubes) st->m_cubes.push_back(c(tr)); for (expr* c : m_asserted_cubes) st->m_asserted_cubes.push_back(tr(c)); st->m_depth = m_depth; st->m_width = m_width; @@ -210,11 +228,11 @@ class parallel_tactic : public tactic { void set_type(task_type t) { m_type = t; } - expr_ref_vector const& cubes() const { SASSERT(m_type == conquer_task); return m_cubes; } + vector const& cubes() const { SASSERT(m_type == conquer_task); return m_cubes; } // remove up to n cubes from list of cubes. - expr_ref_vector split_cubes(unsigned n) { - expr_ref_vector result(m()); + vector split_cubes(unsigned n) { + vector result; while (n-- > 0 && !m_cubes.empty()) { result.push_back(m_cubes.back()); m_cubes.pop_back(); @@ -222,7 +240,7 @@ class parallel_tactic : public tactic { return result; } - void set_cubes(expr_ref_vector const& c) { + void set_cubes(vector& c) { m_cubes.reset(); m_cubes.append(c); } @@ -280,16 +298,18 @@ class parallel_tactic : public tactic { } void set_conquer_params() { + m_params.set_bool("gc.initial", true); m_params.set_bool("lookahead_simplify", false); m_params.set_uint("restart.max", m_restart_max); get_solver().updt_params(m_params); } void set_simplify_params(bool pb_simp, bool retain_blocked) { + parallel_params pp(m_params); m_params.set_bool("cardinality.solver", pb_simp); m_params.set_sym ("pb.solver", pb_simp ? symbol("solver") : symbol("circuit")); if (m_params.get_uint("inprocess.max", UINT_MAX) == UINT_MAX) - m_params.set_uint("inprocess.max", 2); + m_params.set_uint("inprocess.max", pp.inprocess_max()); m_params.set_bool("lookahead_simplify", true); m_params.set_uint("restart.max", UINT_MAX); m_params.set_bool("retain_blocked_clauses", retain_blocked); @@ -350,7 +370,7 @@ private: IF_VERBOSE(0, verbose_stream() << "(tactic.parallel :progress " << m_progress << "% "; if (status == l_true) verbose_stream() << ":status sat "; if (status == l_undef) verbose_stream() << ":status unknown "; - verbose_stream() << ":unsat " << m_num_unsat << " :branches " << m_branches << ")\n";); + verbose_stream() << ":unsat " << m_num_unsat << " :open-branches " << m_branches << ")\n";); } void report_sat(solver_state& s) { @@ -371,9 +391,11 @@ private: } void report_unsat(solver_state& s) { + { + std::lock_guard lock(m_mutex); + ++m_num_unsat; + } close_branch(s, l_false); - std::lock_guard lock(m_mutex); - ++m_num_unsat; } void report_undef(solver_state& s) { @@ -383,7 +405,11 @@ private: void cube_and_conquer(solver_state& s) { ast_manager& m = s.m(); - expr_ref_vector cubes(m), cube(m), hard_cubes(m); + // expr_ref_vector cube(m), hard_cubes(m); + vector cube, hard_cubes, cubes; + expr_ref_vector vars(m); + + add_branches(1); switch (s.type()) { case cube_task: goto cube; @@ -399,7 +425,11 @@ private: SASSERT(cube.size() <= 1); IF_VERBOSE(2, verbose_stream() << "(tactic.parallel :split-cube " << cube.size() << ")\n";); if (!s.cubes().empty()) m_queue.add_task(s.clone()); - if (!cube.empty()) s.assert_cube(cube.get(0)); + if (!cube.empty()) { + s.assert_cube(cube.get(0).cube()); + vars.reset(); + vars.append(cube.get(0).vars()); + } s.inc_depth(1); // simplify @@ -414,7 +444,6 @@ private: cubes.reset(); s.set_cube_params(); while (true) { - expr_ref_vector vars(m); expr_ref_vector c = s.get_solver().cube(vars, UINT_MAX); // TBD tune this if (c.empty()) { report_undef(s); @@ -423,11 +452,11 @@ private: if (m.is_false(c.back())) { break; } - cubes.push_back(mk_and(c)); + cubes.push_back(cube_var(mk_and(c), vars)); + IF_VERBOSE(2, verbose_stream() << "(tactic.parallel :cube " << cubes.size() << " :vars " << vars.size() << ")\n"); } IF_VERBOSE(1, verbose_stream() << "(tactic.parallel :cubes " << cubes.size() << ")\n";); - IF_VERBOSE(12, verbose_stream() << "(tactic.parallel :cubes " << cubes << ")\n";); if (cubes.empty()) { report_unsat(s); @@ -435,7 +464,7 @@ private: } else { s.inc_width(cubes.size()); - add_branches(cubes.size()); + add_branches(cubes.size() - 1); s.set_cubes(cubes); s.set_type(conquer_task); goto conquer; @@ -451,9 +480,9 @@ private: s.set_conquer_params(); hard_cubes.reset(); - for (expr * c : cubes) { - switch (s.solve(c)) { - case l_undef: hard_cubes.push_back(c); break; + for (cube_var& cv : cubes) { + switch (s.solve(cv.cube())) { + case l_undef: hard_cubes.push_back(cv); break; case l_true: report_sat(s); break; case l_false: report_unsat(s); break; } @@ -580,6 +609,15 @@ public: result.push_back(g.get()); } + virtual void collect_param_descrs(param_descrs & r) { + r.insert("conquer_batch_size", CPK_UINT, "(default: 1000) batch size of cubes to conquer"); + } + + unsigned conquer_batch_size() const { + parallel_params pp(m_params); + return pp.conquer_batch_size(); + } + void cleanup() { m_queue.reset(); init(); @@ -593,14 +631,6 @@ public: m_params.copy(p); } - virtual void collect_param_descrs(param_descrs & r) { - r.insert("conquer_batch_size", CPK_UINT, "(default: 1000) batch size of cubes to conquer"); - } - - unsigned conquer_batch_size() const { - return m_params.get_uint("conquer_batch_size", 1000); - } - virtual void collect_statistics(statistics & st) const { st.copy(m_stats); st.update("par unsat", m_num_unsat); diff --git a/src/tactic/smtlogics/CMakeLists.txt b/src/tactic/smtlogics/CMakeLists.txt index 2741334b4..09b145316 100644 --- a/src/tactic/smtlogics/CMakeLists.txt +++ b/src/tactic/smtlogics/CMakeLists.txt @@ -26,6 +26,7 @@ z3_add_component(smtlogic_tactics smt_tactic PYG_FILES qfufbv_tactic_params.pyg + parallel_params.pyg TACTIC_HEADERS nra_tactic.h qfaufbv_tactic.h diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index 0eb235791..25741c09e 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -29,7 +29,7 @@ Notes: #include "tactic/aig/aig_tactic.h" #include "sat/tactic/sat_tactic.h" #include "tactic/portfolio/parallel_tactic.h" -#include "tactic/portfolio/parallel_params.hpp" +#include "tactic/smtlogics/parallel_params.hpp" #include "ackermannization/ackermannize_bv_tactic.h" #define MEMLIMIT 300 From f7e49501af7c87f25109de4430214349c7ec479a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 13 Apr 2018 16:22:36 -0700 Subject: [PATCH 12/24] updates Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/pb2bv_rewriter.cpp | 156 +++++++++++++++++--------- src/sat/sat_config.cpp | 4 +- src/sat/sat_config.h | 3 +- src/sat/sat_solver/inc_sat_solver.cpp | 3 + 4 files changed, 109 insertions(+), 57 deletions(-) diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index 179773c34..9fc6bf7b3 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -56,9 +56,7 @@ struct pb2bv_rewriter::imp { rational m_k; vector m_coeffs; bool m_keep_cardinality_constraints; - bool m_keep_pb_constraints; - bool m_pb_num_system; - bool m_pb_totalizer; + symbol m_pb_solver; unsigned m_min_arity; template @@ -85,7 +83,7 @@ struct pb2bv_rewriter::imp { struct compare_coeffs { bool operator()(ca const& x, ca const& y) const { - return x.first < y.first; + return x.first > y.first; } }; @@ -126,11 +124,12 @@ struct pb2bv_rewriter::imp { if (i + 1 < sz && !m_coeffs[i+1].is_neg()) tout << "+ "; } switch (is_le) { - case l_true: tout << "<= "; break; + case l_true: tout << "<= "; break; case l_undef: tout << "= "; break; case l_false: tout << ">= "; break; } tout << k << "\n";); + if (k.is_zero()) { if (is_le != l_false) { return expr_ref(m.mk_not(::mk_or(m_args)), m); @@ -143,7 +142,7 @@ struct pb2bv_rewriter::imp { return expr_ref((is_le == l_false)?m.mk_true():m.mk_false(), m); } - if (m_pb_totalizer) { + if (m_pb_solver == "totalizer") { expr_ref result(m); switch (is_le) { case l_true: if (mk_le_tot(sz, args, k, result)) return result; else break; @@ -152,7 +151,7 @@ struct pb2bv_rewriter::imp { } } - if (m_pb_num_system) { + if (m_pb_solver == "sorting") { expr_ref result(m); switch (is_le) { case l_true: if (mk_le(sz, args, k, result)) return result; else break; @@ -161,6 +160,15 @@ struct pb2bv_rewriter::imp { } } + if (m_pb_solver == "segmented") { + expr_ref result(m); + switch (is_le) { + case l_true: return mk_seg_le(k); + case l_false: return mk_seg_ge(k); + case l_undef: break; + } + } + // fall back to divide and conquer encoding. SASSERT(k.is_pos()); expr_ref zero(m), bound(m); @@ -486,14 +494,82 @@ struct pb2bv_rewriter::imp { return true; } - expr_ref mk_and(expr_ref& a, expr_ref& b) { + /** + \brief Segment based encoding. + The PB terms are partitoned into segments, such that each segment contains arguments with the same cofficient. + The segments are sorted, such that the segment with highest coefficient is first. + Then for each segment create circuits based on sorting networks the arguments of the segment. + */ + + expr_ref mk_seg_ge(rational const& k) { + rational bound(-k); + for (unsigned i = 0; i < m_args.size(); ++i) { + m_args[i] = mk_not(m_args[i].get()); + bound += m_coeffs[i]; + } + return mk_seg_le(bound); + } + + expr_ref mk_seg_le(rational const& k) { + sort_args(); + unsigned sz = m_args.size(); + expr* const* args = m_args.c_ptr(); + + // Create sorted entries. + vector> outs; + vector coeffs; + for (unsigned i = 0, seg_size = 0; i < sz; i += seg_size) { + seg_size = segment_size(i); + ptr_vector out; + m_sort.sorting(seg_size, args + i, out); + out.push_back(m.mk_false()); + outs.push_back(out); + coeffs.push_back(m_coeffs[i]); + } + return mk_seg_le_rec(outs, coeffs, 0, k); + } + + expr_ref mk_seg_le_rec(vector> const& outs, vector const& coeffs, unsigned i, rational const& k) { + rational const& c = coeffs[i]; + ptr_vector const& out = outs[i]; + if (k.is_neg()) { + return expr_ref(m.mk_false(), m); + } + if (i == outs.size()) { + return expr_ref(m.mk_true(), m); + } + if (i + 1 == outs.size() && k >= rational(out.size()-1)*c) { + return expr_ref(m.mk_true(), m); + } + expr_ref_vector fmls(m); + fmls.push_back(m.mk_implies(m.mk_not(out[0]), mk_seg_le_rec(outs, coeffs, i + 1, k))); + rational k1; + for (unsigned j = 0; j + 1 < out.size(); ++j) { + k1 = k - rational(j+1)*c; + if (k1.is_neg()) { + fmls.push_back(m.mk_not(out[j])); + break; + } + fmls.push_back(m.mk_implies(m.mk_and(out[j], m.mk_not(out[j+1])), mk_seg_le_rec(outs, coeffs, i + 1, k1))); + } + return ::mk_and(fmls); + } + + // The number of arguments with the same coefficient. + unsigned segment_size(unsigned start) const { + unsigned i = start; + while (i < m_args.size() && m_coeffs[i] == m_coeffs[start]) ++i; + return i - start; + } + + expr_ref mk_and(expr_ref& a, expr_ref& b) { if (m.is_true(a)) return b; if (m.is_true(b)) return a; if (m.is_false(a)) return a; if (m.is_false(b)) return b; return expr_ref(m.mk_and(a, b), m); } - + expr_ref mk_or(expr_ref& a, expr_ref& b) { if (m.is_true(a)) return a; if (m.is_true(b)) return b; @@ -607,12 +683,12 @@ struct pb2bv_rewriter::imp { m_trail(m), m_args(m), m_keep_cardinality_constraints(false), - m_keep_pb_constraints(false), - m_pb_num_system(false), - m_pb_totalizer(false), + m_pb_solver(symbol("solver")), m_min_arity(9) {} + void set_pb_solver(symbol const& s) { m_pb_solver = s; } + bool mk_app(bool full, func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { if (f->get_family_id() == pb.get_family_id() && mk_pb(full, f, sz, args, result)) { // skip @@ -756,13 +832,13 @@ struct pb2bv_rewriter::imp { result = m_sort.ge(full, pb.get_k(f).get_unsigned(), sz, args); ++m_imp.m_compile_card; } - else if (pb.is_eq(f) && pb.get_k(f).is_unsigned() && has_small_coefficients(f) && m_keep_pb_constraints) { + else if (pb.is_eq(f) && pb.get_k(f).is_unsigned() && has_small_coefficients(f) && m_pb_solver == "solver") { return false; } - else if (pb.is_le(f) && pb.get_k(f).is_unsigned() && has_small_coefficients(f) && m_keep_pb_constraints) { + else if (pb.is_le(f) && pb.get_k(f).is_unsigned() && has_small_coefficients(f) && m_pb_solver == "solver") { return false; } - else if (pb.is_ge(f) && pb.get_k(f).is_unsigned() && has_small_coefficients(f) && m_keep_pb_constraints) { + else if (pb.is_ge(f) && pb.get_k(f).is_unsigned() && has_small_coefficients(f) && m_pb_solver == "solver") { return false; } else { @@ -811,17 +887,6 @@ struct pb2bv_rewriter::imp { m_keep_cardinality_constraints = f; } - void keep_pb_constraints(bool f) { - m_keep_pb_constraints = f; - } - - void pb_num_system(bool f) { - m_pb_num_system = f; - } - - void pb_totalizer(bool f) { - m_pb_totalizer = f; - } void set_at_most1(sorting_network_encoding enc) { m_sort.cfg().m_encoding = enc; } }; @@ -836,9 +901,7 @@ struct pb2bv_rewriter::imp { } card2bv_rewriter_cfg(imp& i, ast_manager & m):m_r(i, m) {} void keep_cardinality_constraints(bool f) { m_r.keep_cardinality_constraints(f); } - void keep_pb_constraints(bool f) { m_r.keep_pb_constraints(f); } - void pb_num_system(bool f) { m_r.pb_num_system(f); } - void pb_totalizer(bool f) { m_r.pb_totalizer(f); } + void set_pb_solver(symbol const& s) { m_r.set_pb_solver(s); } void set_at_most1(sorting_network_encoding enc) { m_r.set_at_most1(enc); } }; @@ -850,9 +913,7 @@ struct pb2bv_rewriter::imp { rewriter_tpl(m, false, m_cfg), m_cfg(i, m) {} void keep_cardinality_constraints(bool f) { m_cfg.keep_cardinality_constraints(f); } - void keep_pb_constraints(bool f) { m_cfg.keep_pb_constraints(f); } - void pb_num_system(bool f) { m_cfg.pb_num_system(f); } - void pb_totalizer(bool f) { m_cfg.pb_totalizer(f); } + void set_pb_solver(symbol const& s) { m_cfg.set_pb_solver(s); } void set_at_most1(sorting_network_encoding e) { m_cfg.set_at_most1(e); } void rewrite(expr* e, expr_ref& r, proof_ref& p) { expr_ref ee(e, m()); @@ -875,26 +936,15 @@ struct pb2bv_rewriter::imp { gparams::get_module("sat").get_bool("cardinality.solver", false); } - bool keep_pb() const { + symbol pb_solver() const { params_ref const& p = m_params; - return - p.get_bool("keep_pb_constraints", false) || - p.get_bool("sat.pb.solver", false) || - p.get_bool("pb.solver", false) || - gparams::get_module("sat").get_sym("pb.solver", symbol()) == symbol("solver") ; + symbol s = p.get_sym("sat.pb.solver", symbol()); + if (s != symbol()) return s; + s = p.get_sym("pb.solver", symbol()); + if (s != symbol()) return s; + return gparams::get_module("sat").get_sym("pb.solver", symbol("solver")); } - bool pb_num_system() const { - return m_params.get_bool("pb_num_system", false) || - gparams::get_module("sat").get_sym("pb.solver", symbol()) == symbol("sorting"); - } - - bool pb_totalizer() const { - return m_params.get_bool("pb_totalizer", false) || - gparams::get_module("sat").get_sym("pb.solver", symbol()) == symbol("totalizer"); - } - - sorting_network_encoding atmost1_encoding() const { symbol enc = m_params.get_sym("atmost1_encoding", symbol()); if (enc == symbol()) { @@ -920,16 +970,12 @@ struct pb2bv_rewriter::imp { void updt_params(params_ref const & p) { m_params.append(p); m_rw.keep_cardinality_constraints(keep_cardinality()); - m_rw.keep_pb_constraints(keep_pb()); - m_rw.pb_num_system(pb_num_system()); - m_rw.pb_totalizer(pb_totalizer()); + m_rw.set_pb_solver(pb_solver()); m_rw.set_at_most1(atmost1_encoding()); } void collect_param_descrs(param_descrs& r) const { r.insert("keep_cardinality_constraints", CPK_BOOL, "(default: true) retain cardinality constraints (don't bit-blast them) and use built-in cardinality solver"); - r.insert("keep_pb_constraints", CPK_BOOL, "(default: true) retain pb constraints (don't bit-blast them) and use built-in pb solver"); - r.insert("pb_num_system", CPK_BOOL, "(default: false) use pb number system encoding"); - r.insert("pb_totalizer", CPK_BOOL, "(default: false) use pb totalizer encoding"); + r.insert("pb.solver", CPK_SYMBOL, "(default: solver) retain pb constraints (don't bit-blast them) and use built-in pb solver"); } unsigned get_num_steps() const { return m_rw.get_num_steps(); } diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 2439be36f..812e65abf 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -178,8 +178,10 @@ namespace sat { m_pb_solver = PB_TOTALIZER; else if (s == symbol("solver")) m_pb_solver = PB_SOLVER; + else if (s == symbol("segmented")) + m_pb_solver = PB_SEGMENTED; else - throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting"); + throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting, segmented"); m_card_solver = p.cardinality_solver(); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index c70d52a90..6a704ab44 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -54,7 +54,8 @@ namespace sat { PB_SOLVER, PB_CIRCUIT, PB_SORTING, - PB_TOTALIZER + PB_TOTALIZER, + PB_SEGMENTED }; enum reward_t { diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 4d7325ecb..a7499590b 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -281,9 +281,12 @@ public: m_params.append(p); sat_params p1(p); m_params.set_bool("keep_cardinality_constraints", p1.cardinality_solver()); + m_params.set_sym("pb.solver", p1.pb_solver()); + m_params.set_bool("keep_pb_constraints", m_solver.get_config().m_pb_solver == sat::PB_SOLVER); m_params.set_bool("pb_num_system", m_solver.get_config().m_pb_solver == sat::PB_SORTING); m_params.set_bool("pb_totalizer", m_solver.get_config().m_pb_solver == sat::PB_TOTALIZER); + m_params.set_bool("xor_solver", p1.xor_solver()); m_solver.updt_params(m_params); m_solver.set_incremental(is_incremental() && !override_incremental()); From a3e651156af910705a7c8b70e10cfc960e533a54 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 13 Apr 2018 16:23:35 -0700 Subject: [PATCH 13/24] parallel params Signed-off-by: Nikolaj Bjorner --- src/tactic/smtlogics/parallel_params.pyg | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 src/tactic/smtlogics/parallel_params.pyg diff --git a/src/tactic/smtlogics/parallel_params.pyg b/src/tactic/smtlogics/parallel_params.pyg new file mode 100644 index 000000000..70c4ccdd0 --- /dev/null +++ b/src/tactic/smtlogics/parallel_params.pyg @@ -0,0 +1,10 @@ +def_module_params('parallel', + description='parameters for parallel solver', + class_name='parallel_params', + export=True, + params=( + ('enable', BOOL, False, 'enable parallel solver by default on selected tactics (for QF_BV)'), + ('conquer_batch_size', UINT, 1000, 'number of cubes to batch together for fast conquer'), + ('inprocess.max', UINT, 2, 'maximal number of inprocessing steps during simplification'), + ('restart.max', UINT, 100, 'maximal number of restarts during conquer phase'), + )) From c5a30285a8100dbd1f0569a8d887f78eeada713e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 13 Apr 2018 17:03:49 -0700 Subject: [PATCH 14/24] add filter cubes parameter Signed-off-by: Nikolaj Bjorner --- src/tactic/portfolio/parallel_tactic.cpp | 8 +++++++- src/tactic/smtlogics/parallel_params.pyg | 1 + 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp index 999dbc2e0..bc28a7b37 100644 --- a/src/tactic/portfolio/parallel_tactic.cpp +++ b/src/tactic/portfolio/parallel_tactic.cpp @@ -443,8 +443,9 @@ private: // extract cubes. cubes.reset(); s.set_cube_params(); + unsigned cutoff = UINT_MAX; while (true) { - expr_ref_vector c = s.get_solver().cube(vars, UINT_MAX); // TBD tune this + expr_ref_vector c = s.get_solver().cube(vars, cutoff); if (c.empty()) { report_undef(s); return; @@ -618,6 +619,11 @@ public: return pp.conquer_batch_size(); } + bool filter_cubes() const { + parallel_params pp(m_params); + return pp.filter_cubes(); + } + void cleanup() { m_queue.reset(); init(); diff --git a/src/tactic/smtlogics/parallel_params.pyg b/src/tactic/smtlogics/parallel_params.pyg index 70c4ccdd0..58da305f4 100644 --- a/src/tactic/smtlogics/parallel_params.pyg +++ b/src/tactic/smtlogics/parallel_params.pyg @@ -7,4 +7,5 @@ def_module_params('parallel', ('conquer_batch_size', UINT, 1000, 'number of cubes to batch together for fast conquer'), ('inprocess.max', UINT, 2, 'maximal number of inprocessing steps during simplification'), ('restart.max', UINT, 100, 'maximal number of restarts during conquer phase'), + ('filter_cubes', BOOL, False, 'filter cubes using a short running check'), )) From d58a9d25284b52af7ca5e0d304504c5fcca52e85 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 13 Apr 2018 22:04:14 -0700 Subject: [PATCH 15/24] fix accounting for branches Signed-off-by: Nikolaj Bjorner --- src/tactic/portfolio/parallel_tactic.cpp | 142 ++++++++++++++++++++++- 1 file changed, 139 insertions(+), 3 deletions(-) diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp index bc28a7b37..9b9e74629 100644 --- a/src/tactic/portfolio/parallel_tactic.cpp +++ b/src/tactic/portfolio/parallel_tactic.cpp @@ -208,6 +208,8 @@ class parallel_tactic : public tactic { solver& get_solver() { return *m_solver; } + solver* copy_solver() { return m_solver->translate(m_solver->get_manager(), m_params); } + solver const& get_solver() const { return *m_solver; } solver_state* clone() { @@ -405,12 +407,9 @@ private: void cube_and_conquer(solver_state& s) { ast_manager& m = s.m(); - // expr_ref_vector cube(m), hard_cubes(m); vector cube, hard_cubes, cubes; expr_ref_vector vars(m); - add_branches(1); - switch (s.type()) { case cube_task: goto cube; case conquer_task: goto conquer; @@ -497,6 +496,142 @@ private: goto cube; } + void cube_and_conquer2(solver_state& s) { + ast_manager& m = s.m(); + vector cube, hard_cubes, cubes; + expr_ref_vector vars(m); + SASSERT(s.type() == cube_task); + + // extract up to one cube and add it. + cube.reset(); + cube.append(s.split_cubes(1)); + SASSERT(cube.size() <= 1); + IF_VERBOSE(2, verbose_stream() << "(tactic.parallel :split-cube " << cube.size() << ")\n";); + if (!s.cubes().empty()) m_queue.add_task(s.clone()); + if (!cube.empty()) { + s.assert_cube(cube.get(0).cube()); + vars.reset(); + vars.append(cube.get(0).vars()); + } + s.inc_depth(1); + + // simplify + switch (s.simplify()) { + case l_undef: break; + case l_true: report_sat(s); return; + case l_false: report_unsat(s); return; + } + if (canceled(s)) return; + + // extract cubes. + cubes.reset(); + s.set_cube_params(); + solver_ref conquer = s.copy_solver(); + unsigned cutoff = UINT_MAX; + while (true) { + expr_ref_vector c = s.get_solver().cube(vars, cutoff); + if (c.empty()) { + report_undef(s); + return; + } + if (m.is_false(c.back())) { + break; + } + lbool is_sat = conquer->check_sat(c); + switch (is_sat) { + case l_false: { + // TBD: minimize core instead. + expr_ref_vector core(m); + conquer->get_unsat_core(core); + obj_hashtable hcore; + for (expr* e : core) hcore.insert(e); + for (unsigned i = c.size(); i-- > 0; ) { + if (hcore.contains(c[i].get())) { + cutoff = i; + break; + } + } + break; + } + case l_true: + report_sat(s); + return; + case l_undef: + IF_VERBOSE(2, verbose_stream() << "(tactic.parallel :cube " << cubes.size() << " :vars " << vars.size() << ")\n"); + cubes.push_back(cube_var(mk_and(c), vars)); + cutoff = UINT_MAX; + break; + } + // TBD flush cube task early + } + + IF_VERBOSE(1, verbose_stream() << "(tactic.parallel :cubes " << cubes.size() << ")\n";); + + if (cubes.empty()) { + report_unsat(s); + return; + } + else { + s.inc_width(cubes.size()); + add_branches(cubes.size() - 1); + NOT_IMPLEMENTED_YET(); + // TBD add as a cube task. + } + } + + expr_ref_vector baktrack(expr_ref_vector const& c) { + + } + +#if 0 + public BoolExpr[] Backtrack(Statistics stats, BoolExpr[] _asms) + { + int count = _asms.Count(); + stats.Stopwatch.Start(); + var asms = new List(_asms); + _Backtrack(stats, asms); + stats.AddBacktrackStats((uint)(count - asms.Count()), stats.Stopwatch.Elapsed()); + return asms.ToArray(); + } + + public void _Backtrack(Statistics stats, List asms) + { + HashSet core = new HashSet(Solver.UnsatCore); + while (asms.Count > 0 && !core.Contains(asms.Last())) + { + asms.RemoveAt(asms.Count - 1); + } + stats.Cores++; + Solver.Add(!Context.MkAnd(core)); + if (asms.Count > 0) + { + BoolExpr last = asms.Last(); + BoolExpr not_last = last.IsNot ? (BoolExpr)last.Args[0] : Context.MkNot(last); + asms.RemoveAt(asms.Count - 1); + asms.Add(not_last); + Status status = CheckSat(null, asms); + asms.RemoveAt(asms.Count - 1); + if (status != Status.UNSATISFIABLE) + { + asms.Add(last); + return; + } + core = new HashSet(Solver.UnsatCore); + if (core.Contains(not_last)) + { + stats.Cores++; + Solver.Add(!Context.MkAnd(core)); + status = CheckSat(null, asms); + } + if (status == Status.UNSATISFIABLE) + { + _Backtrack(stats, asms); + } + } + } + +#endif + bool canceled(solver_state& s) { if (s.canceled()) { m_has_undef = true; @@ -509,6 +644,7 @@ private: void run_solver() { try { + add_branches(1); while (solver_state* st = m_queue.get_task()) { cube_and_conquer(*st); collect_statistics(*st); From 252fb4af6e6689adf9756a0ab31033d3cc9e6550 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Apr 2018 15:34:33 -0700 Subject: [PATCH 16/24] add backtracking conquer Signed-off-by: Nikolaj Bjorner --- src/sat/sat_config.cpp | 1 + src/sat/sat_config.h | 2 + src/sat/sat_params.pyg | 5 +- src/sat/sat_solver.cpp | 2 +- src/tactic/portfolio/parallel_tactic.cpp | 331 +++++++++++++---------- src/tactic/smtlogics/parallel_params.pyg | 4 +- 6 files changed, 192 insertions(+), 153 deletions(-) diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 812e65abf..2597967df 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -119,6 +119,7 @@ namespace sat { m_simplify_mult2 = _p.get_double("simplify_mult2", 1.5); m_simplify_max = _p.get_uint("simplify_max", 500000); // -------------------------------- + m_simplify_delay = p.simplify_delay(); s = p.gc(); if (s == symbol("dyn_psm")) diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 6a704ab44..20d966dd1 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -116,6 +116,7 @@ namespace sat { unsigned m_simplify_mult1; double m_simplify_mult2; unsigned m_simplify_max; + unsigned m_simplify_delay; unsigned m_variable_decay; @@ -126,6 +127,7 @@ namespace sat { unsigned m_gc_k; bool m_gc_burst; + bool m_minimize_lemmas; bool m_dyn_sub_res; bool m_core_minimize; diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 56a5b6e6c..320ddaf9e 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -24,6 +24,7 @@ def_module_params('sat', ('gc.small_lbd', UINT, 3, 'learned clauses with small LBD are never deleted (only used in dyn_psm)'), ('gc.k', UINT, 7, 'learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm)'), ('gc.burst', BOOL, True, 'perform eager garbage collection during initialization'), + ('simplify.delay', UINT, 0, 'set initial delay of simplification by a conflict count'), ('minimize_lemmas', BOOL, True, 'minimize learned clauses'), ('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'), ('core.minimize', BOOL, False, 'minimize computed core'), @@ -42,9 +43,9 @@ def_module_params('sat', ('local_search_mode', SYMBOL, 'wsat', 'local search algorithm, either default wsat or qsat'), ('unit_walk', BOOL, False, 'use unit-walk search instead of CDCL'), ('unit_walk_threads', UINT, 0, 'number of unit-walk search threads to find satisfiable solution'), - ('lookahead.cube.cutoff', SYMBOL, 'adaptive_freevars', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'), + ('lookahead.cube.cutoff', SYMBOL, 'depth', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'), ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive_freevars or adaptive_psat'), - ('lookahead.cube.depth', UINT, 10, 'cut-off depth to create cubes. Used when lookahead.cube.cutoff is depth.'), + ('lookahead.cube.depth', UINT, 1, 'cut-off depth to create cubes. Used when lookahead.cube.cutoff is depth.'), ('lookahead.cube.freevars', DOUBLE, 0.8, 'cube free fariable fraction. Used when lookahead.cube.cutoff is freevars'), ('lookahead.cube.psat.var_exp', DOUBLE, 1, 'free variable exponent for PSAT cutoff'), ('lookahead.cube.psat.clause_base', DOUBLE, 2, 'clause base for PSAT cutoff'), diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index da11ed3a1..fb992d57e 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1503,7 +1503,7 @@ namespace sat { m_restarts = 0; m_simplifications = 0; m_conflicts_since_init = 0; - m_next_simplify = 0; + m_next_simplify = m_config.m_simplify_delay; m_min_d_tk = 1.0; m_search_lvl = 0; m_conflicts_since_gc = 0; diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp index 9b9e74629..988ab2ec4 100644 --- a/src/tactic/portfolio/parallel_tactic.cpp +++ b/src/tactic/portfolio/parallel_tactic.cpp @@ -107,6 +107,11 @@ class parallel_tactic : public tactic { } } + bool is_idle() { + std::lock_guard lock(m_mutex); + return m_tasks.empty() && m_num_waiters > 0; + } + solver_state* get_task() { while (!m_shutdown) { inc_wait(); @@ -153,19 +158,21 @@ class parallel_tactic : public tactic { class cube_var { expr_ref_vector m_vars; - expr_ref m_cube; + expr_ref_vector m_cube; public: - cube_var(expr* c, expr_ref_vector& vs): - m_vars(vs), m_cube(c, vs.get_manager()) {} + cube_var(expr_ref_vector& c, expr_ref_vector& vs): + m_vars(vs), m_cube(c) {} cube_var operator()(ast_translation& tr) { expr_ref_vector vars(tr.to()); + expr_ref_vector cube(tr.to()); for (expr* v : m_vars) vars.push_back(tr(v)); - return cube_var(tr(m_cube.get()), vars); + for (expr* c : m_cube) cube.push_back(tr(c)); + return cube_var(cube, vars); } - expr* cube() const { return m_cube; } - expr_ref_vector const& vars() { return m_vars; } + expr_ref_vector const& cube() const { return m_cube; } + expr_ref_vector const& vars() const { return m_vars; } }; class solver_state { @@ -179,17 +186,6 @@ class parallel_tactic : public tactic { double m_width; // estimate of fraction of problem handled by state unsigned m_restart_max; // saved configuration value - expr_ref_vector cube_literals(expr* cube) { - expr_ref_vector literals(m()); - if (m().is_and(cube)) { - literals.append(to_app(cube)->get_num_args(), to_app(cube)->get_args()); - } - else { - literals.push_back(cube); - } - return literals; - } - public: solver_state(ast_manager* m, solver* s, params_ref const& p, task_type t): m_type(t), @@ -212,12 +208,12 @@ class parallel_tactic : public tactic { solver const& get_solver() const { return *m_solver; } - solver_state* clone() { + solver_state* clone(solver* s0 = nullptr) { SASSERT(!m_cubes.empty()); ast_manager& m = m_solver->get_manager(); ast_manager* new_m = alloc(ast_manager, m, !m.proof_mode()); ast_translation tr(m, *new_m); - solver* s = m_solver->translate(*new_m, m_params); + solver* s = (s0 ? s0 : m_solver.get())->translate(*new_m, m_params); solver_state* st = alloc(solver_state, new_m, s, m_params, m_type); for (auto & c : m_cubes) st->m_cubes.push_back(c(tr)); for (expr* c : m_asserted_cubes) st->m_asserted_cubes.push_back(tr(c)); @@ -284,15 +280,14 @@ class parallel_tactic : public tactic { return r; } - void assert_cube(expr* cube) { + void assert_cube(expr_ref_vector const& cube) { get_solver().assert_expr(cube); - m_asserted_cubes.append(cube_literals(cube)); + m_asserted_cubes.append(cube); } - lbool solve(expr* cube) { + lbool solve(expr_ref_vector const& cube) { set_conquer_params(); - expr_ref_vector literals = cube_literals(cube); - return get_solver().check_sat(literals); + return get_solver().check_sat(cube); } void set_cube_params() { @@ -300,22 +295,33 @@ class parallel_tactic : public tactic { } void set_conquer_params() { - m_params.set_bool("gc.initial", true); - m_params.set_bool("lookahead_simplify", false); - m_params.set_uint("restart.max", m_restart_max); - get_solver().updt_params(m_params); + set_conquer_params(get_solver()); + } + + void set_conquer_params(solver& s) { + params_ref p; + p.copy(m_params); + p.set_bool("gc.burst", true); // apply eager gc + p.set_uint("simplify.delay", 1000); // delay simplification by 1000 conflicts + p.set_bool("lookahead_simplify", false); + p.set_uint("restart.max", m_restart_max); + p.set_uint("inprocess.max", UINT_MAX); // base bounds on restart.max + s.updt_params(p); } void set_simplify_params(bool pb_simp, bool retain_blocked) { parallel_params pp(m_params); - m_params.set_bool("cardinality.solver", pb_simp); - m_params.set_sym ("pb.solver", pb_simp ? symbol("solver") : symbol("circuit")); - if (m_params.get_uint("inprocess.max", UINT_MAX) == UINT_MAX) - m_params.set_uint("inprocess.max", pp.inprocess_max()); - m_params.set_bool("lookahead_simplify", true); - m_params.set_uint("restart.max", UINT_MAX); - m_params.set_bool("retain_blocked_clauses", retain_blocked); - get_solver().updt_params(m_params); + params_ref p; + p.copy(m_params); + + p.set_bool("cardinality.solver", pb_simp); + p.set_sym ("pb.solver", pb_simp ? symbol("solver") : symbol("circuit")); + if (p.get_uint("inprocess.max", UINT_MAX) == UINT_MAX) + p.set_uint("inprocess.max", pp.inprocess_max()); + p.set_bool("lookahead_simplify", true); + p.set_uint("restart.max", UINT_MAX); + p.set_bool("retain_blocked_clauses", retain_blocked); + get_solver().updt_params(p); } bool canceled() { @@ -340,6 +346,8 @@ private: std::mutex m_mutex; double m_progress; unsigned m_branches; + unsigned m_backtrack_frequency; + unsigned m_conquer_threshold; bool m_has_undef; bool m_allsat; unsigned m_num_unsat; @@ -351,15 +359,32 @@ private: m_progress = 0; m_has_undef = false; m_allsat = false; - m_num_unsat = 0; - m_branches = 0; + m_branches = 0; + m_num_unsat = 0; + m_backtrack_frequency = 10; + m_conquer_threshold = 10; m_exn_code = 0; m_params.set_bool("override_incremental", true); } + void log_branches(lbool status) { + IF_VERBOSE(0, verbose_stream() << "(tactic.parallel :progress " << m_progress << "% "; + if (status == l_true) verbose_stream() << ":status sat "; + if (status == l_undef) verbose_stream() << ":status unknown "; + verbose_stream() << ":closed " << m_num_unsat << " :open " << m_branches << ")\n";); + } + void add_branches(unsigned b) { + { + std::lock_guard lock(m_mutex); + m_branches += b; + } + log_branches(l_false); + } + + void dec_branch() { std::lock_guard lock(m_mutex); - m_branches += b; + --m_branches; } void close_branch(solver_state& s, lbool status) { @@ -369,10 +394,7 @@ private: m_progress += f; --m_branches; } - IF_VERBOSE(0, verbose_stream() << "(tactic.parallel :progress " << m_progress << "% "; - if (status == l_true) verbose_stream() << ":status sat "; - if (status == l_undef) verbose_stream() << ":status unknown "; - verbose_stream() << ":unsat " << m_num_unsat << " :open-branches " << m_branches << ")\n";); + log_branches(status); } void report_sat(solver_state& s) { @@ -392,11 +414,13 @@ private: } } + void inc_unsat() { + std::lock_guard lock(m_mutex); + ++m_num_unsat; + } + void report_unsat(solver_state& s) { - { - std::lock_guard lock(m_mutex); - ++m_num_unsat; - } + inc_unsat(); close_branch(s, l_false); } @@ -405,7 +429,7 @@ private: close_branch(s, l_undef); } - void cube_and_conquer(solver_state& s) { + void cube_and_conquer1(solver_state& s) { ast_manager& m = s.m(); vector cube, hard_cubes, cubes; expr_ref_vector vars(m); @@ -452,7 +476,7 @@ private: if (m.is_false(c.back())) { break; } - cubes.push_back(cube_var(mk_and(c), vars)); + cubes.push_back(cube_var(c, vars)); IF_VERBOSE(2, verbose_stream() << "(tactic.parallel :cube " << cubes.size() << " :vars " << vars.size() << ")\n"); } @@ -500,8 +524,9 @@ private: ast_manager& m = s.m(); vector cube, hard_cubes, cubes; expr_ref_vector vars(m); - SASSERT(s.type() == cube_task); + cube_again: + SASSERT(s.type() == cube_task); // extract up to one cube and add it. cube.reset(); cube.append(s.split_cubes(1)); @@ -515,7 +540,9 @@ private: } s.inc_depth(1); + simplify_again: // simplify + if (canceled(s)) return; switch (s.simplify()) { case l_undef: break; case l_true: report_sat(s); return; @@ -526,112 +553,124 @@ private: // extract cubes. cubes.reset(); s.set_cube_params(); - solver_ref conquer = s.copy_solver(); + solver_ref conquer; + unsigned cutoff = UINT_MAX; - while (true) { + bool first = true; + unsigned num_backtracks = 0, width = 0; + while (cutoff > 0 && !canceled(s)) { expr_ref_vector c = s.get_solver().cube(vars, cutoff); if (c.empty()) { - report_undef(s); - return; + goto simplify_again; } if (m.is_false(c.back())) { break; } - lbool is_sat = conquer->check_sat(c); - switch (is_sat) { - case l_false: { - // TBD: minimize core instead. - expr_ref_vector core(m); - conquer->get_unsat_core(core); - obj_hashtable hcore; - for (expr* e : core) hcore.insert(e); - for (unsigned i = c.size(); i-- > 0; ) { - if (hcore.contains(c[i].get())) { - cutoff = i; - break; - } - } - break; + lbool is_sat = l_undef; + if (width >= m_conquer_threshold && !conquer) { + conquer = s.copy_solver(); + s.set_conquer_params(*conquer.get()); } + if (conquer) { + is_sat = conquer->check_sat(c); + } + switch (is_sat) { + case l_false: + cutoff = c.size(); + backtrack(*conquer.get(), c, (num_backtracks++) % m_backtrack_frequency == 0); + if (cutoff != c.size()) { + IF_VERBOSE(0, verbose_stream() << "(tactic.parallel :backtrack " << cutoff << " -> " << c.size() << ")\n"); + cutoff = c.size(); + } + inc_unsat(); + log_branches(l_false); + break; + case l_true: report_sat(s); + if (conquer) { + collect_statistics(*conquer.get()); + } return; + case l_undef: - IF_VERBOSE(2, verbose_stream() << "(tactic.parallel :cube " << cubes.size() << " :vars " << vars.size() << ")\n"); - cubes.push_back(cube_var(mk_and(c), vars)); + ++width; + IF_VERBOSE(2, verbose_stream() << "(tactic.parallel :cube " << c.size() << " :vars " << vars.size() << ")\n"); + cubes.push_back(cube_var(c, vars)); cutoff = UINT_MAX; break; - } - // TBD flush cube task early - } - - IF_VERBOSE(1, verbose_stream() << "(tactic.parallel :cubes " << cubes.size() << ")\n";); - if (cubes.empty()) { + } + if (cubes.size() >= conquer_batch_size() || (!cubes.empty() && m_queue.is_idle())) { + spawn_cubes(s, std::max(2u, width), cubes); + first = false; + cubes.reset(); + } + } + + if (conquer) { + collect_statistics(*conquer.get()); + } + + if (cubes.empty() && first) { report_unsat(s); + } + else if (cubes.empty()) { + dec_branch(); return; } else { - s.inc_width(cubes.size()); - add_branches(cubes.size() - 1); - NOT_IMPLEMENTED_YET(); - // TBD add as a cube task. + s.inc_width(width); + add_branches(cubes.size()-1); + s.set_cubes(cubes); + goto cube_again; + } + } + + void spawn_cubes(solver_state& s, unsigned width, vector& cubes) { + if (cubes.empty()) return; + add_branches(cubes.size()); + s.set_cubes(cubes); + solver_state* s1 = s.clone(); + s1->inc_width(width); + m_queue.add_task(s1); + } + + /* + * \brief backtrack from unsatisfiable core + */ + void backtrack(solver& s, expr_ref_vector& asms, bool full) { + ast_manager& m = s.get_manager(); + expr_ref_vector core(m); + obj_hashtable hcore; + s.get_unsat_core(core); + while (!asms.empty() && !core.contains(asms.back())) asms.pop_back(); + if (!full) return; + + //s.assert_expr(m.mk_not(mk_and(core))); + if (!asms.empty()) { + expr* last = asms.back(); + expr_ref not_last(mk_not(m, last), m); + asms.pop_back(); + asms.push_back(not_last); + lbool r = s.check_sat(asms); + asms.pop_back(); + if (r != l_false) { + asms.push_back(last); + return; + } + core.reset(); + s.get_unsat_core(core); + if (core.contains(not_last)) { + //s.assert_expr(m.mk_not(mk_and(core))); + r = s.check_sat(asms); + } + if (r == l_false) { + backtrack(s, asms, full); + } } } - expr_ref_vector baktrack(expr_ref_vector const& c) { - - } - -#if 0 - public BoolExpr[] Backtrack(Statistics stats, BoolExpr[] _asms) - { - int count = _asms.Count(); - stats.Stopwatch.Start(); - var asms = new List(_asms); - _Backtrack(stats, asms); - stats.AddBacktrackStats((uint)(count - asms.Count()), stats.Stopwatch.Elapsed()); - return asms.ToArray(); - } - - public void _Backtrack(Statistics stats, List asms) - { - HashSet core = new HashSet(Solver.UnsatCore); - while (asms.Count > 0 && !core.Contains(asms.Last())) - { - asms.RemoveAt(asms.Count - 1); - } - stats.Cores++; - Solver.Add(!Context.MkAnd(core)); - if (asms.Count > 0) - { - BoolExpr last = asms.Last(); - BoolExpr not_last = last.IsNot ? (BoolExpr)last.Args[0] : Context.MkNot(last); - asms.RemoveAt(asms.Count - 1); - asms.Add(not_last); - Status status = CheckSat(null, asms); - asms.RemoveAt(asms.Count - 1); - if (status != Status.UNSATISFIABLE) - { - asms.Add(last); - return; - } - core = new HashSet(Solver.UnsatCore); - if (core.Contains(not_last)) - { - stats.Cores++; - Solver.Add(!Context.MkAnd(core)); - status = CheckSat(null, asms); - } - if (status == Status.UNSATISFIABLE) - { - _Backtrack(stats, asms); - } - } - } - -#endif - bool canceled(solver_state& s) { if (s.canceled()) { m_has_undef = true; @@ -644,9 +683,8 @@ private: void run_solver() { try { - add_branches(1); while (solver_state* st = m_queue.get_task()) { - cube_and_conquer(*st); + cube_and_conquer2(*st); collect_statistics(*st); m_queue.task_done(st); if (st->m().canceled()) m_queue.shutdown(); @@ -669,11 +707,16 @@ private: } void collect_statistics(solver_state& s) { + collect_statistics(s.get_solver()); + } + + void collect_statistics(solver& s) { std::lock_guard lock(m_mutex); - s.get_solver().collect_statistics(m_stats); + s.collect_statistics(m_stats); } lbool solve(model_ref& mdl) { + add_branches(1); vector threads; for (unsigned i = 0; i < m_num_threads; ++i) threads.push_back(std::thread([this]() { run_solver(); })); @@ -706,7 +749,7 @@ public: parallel_tactic(ast_manager& m, params_ref const& p) : m_manager(m), m_params(p) { - init(); + init(); } void operator ()(const goal_ref & g,goal_ref_buffer & result) { @@ -746,23 +789,13 @@ public: result.push_back(g.get()); } - virtual void collect_param_descrs(param_descrs & r) { - r.insert("conquer_batch_size", CPK_UINT, "(default: 1000) batch size of cubes to conquer"); - } - unsigned conquer_batch_size() const { parallel_params pp(m_params); return pp.conquer_batch_size(); } - bool filter_cubes() const { - parallel_params pp(m_params); - return pp.filter_cubes(); - } - void cleanup() { m_queue.reset(); - init(); } tactic* translate(ast_manager& m) { @@ -771,6 +804,8 @@ public: virtual void updt_params(params_ref const & p) { m_params.copy(p); + parallel_params pp(p); + m_conquer_threshold = pp.conquer_threshold(); } virtual void collect_statistics(statistics & st) const { diff --git a/src/tactic/smtlogics/parallel_params.pyg b/src/tactic/smtlogics/parallel_params.pyg index 58da305f4..84f4eb2c4 100644 --- a/src/tactic/smtlogics/parallel_params.pyg +++ b/src/tactic/smtlogics/parallel_params.pyg @@ -6,6 +6,6 @@ def_module_params('parallel', ('enable', BOOL, False, 'enable parallel solver by default on selected tactics (for QF_BV)'), ('conquer_batch_size', UINT, 1000, 'number of cubes to batch together for fast conquer'), ('inprocess.max', UINT, 2, 'maximal number of inprocessing steps during simplification'), - ('restart.max', UINT, 100, 'maximal number of restarts during conquer phase'), - ('filter_cubes', BOOL, False, 'filter cubes using a short running check'), + ('restart.max', UINT, 5, 'maximal number of restarts during conquer phase'), + ('conquer_threshold', UINT, 10, 'number of cubes generated before simple conquer solver is created'), )) From 012a96fd81b0ff75cde519f6ab85dd113e8094e7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 15 Apr 2018 16:16:48 -0700 Subject: [PATCH 17/24] adding smt parallel solving Signed-off-by: Nikolaj Bjorner --- src/sat/sat_lookahead.cpp | 2 +- src/sat/sat_lookahead.h | 2 +- src/smt/params/smt_params.cpp | 1 + src/smt/params/smt_params.h | 1 + src/smt/params/smt_params_helper.pyg | 1 + src/smt/smt_context.cpp | 20 ++++- src/smt/smt_context.h | 4 + src/smt/smt_kernel.cpp | 12 ++- src/smt/smt_kernel.h | 5 ++ src/smt/smt_solver.cpp | 54 +++++++++++-- src/tactic/portfolio/CMakeLists.txt | 1 + src/tactic/portfolio/parallel_tactic.cpp | 96 ++++++++++++++---------- src/tactic/portfolio/parallel_tactic.h | 13 +++- src/tactic/smtlogics/nra_tactic.cpp | 6 +- src/tactic/smtlogics/parallel_params.pyg | 11 ++- src/tactic/smtlogics/qfbv_tactic.cpp | 7 +- src/tactic/smtlogics/qflia_tactic.cpp | 11 +-- 17 files changed, 174 insertions(+), 73 deletions(-) diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 0d737500a..d4d1e615f 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -1034,7 +1034,7 @@ namespace sat { } if (m_s.m_ext) { - m_ext = m_s.m_ext->copy(this, learned); + // m_ext = m_s.m_ext->copy(this, learned); } propagate(); m_qhead = m_trail.size(); diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index b86b7cb14..3213c5a80 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -247,7 +247,7 @@ namespace sat { stats m_stats; model m_model; cube_state m_cube_state; - scoped_ptr m_ext; + //scoped_ptr m_ext; // --------------------------------------- // truth values diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index a8eb81a2e..3ad20cf90 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -39,6 +39,7 @@ void smt_params::updt_local_params(params_ref const & _p) { m_timeout = p.timeout(); m_rlimit = p.rlimit(); m_max_conflicts = p.max_conflicts(); + m_restart_max = p.restart_max(); m_core_validate = p.core_validate(); m_logic = _p.get_sym("logic", m_logic); m_string_solver = p.string_solver(); diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index b01499c04..32b634626 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -99,6 +99,7 @@ struct smt_params : public preprocessor_params, unsigned m_phase_caching_off; bool m_minimize_lemmas; unsigned m_max_conflicts; + unsigned m_restart_max; bool m_simplify_clauses; unsigned m_tick; bool m_display_features; diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index c6749f678..2f16c5798 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -21,6 +21,7 @@ def_module_params(module_name='smt', ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'), ('rlimit', UINT, 0, 'resource limit (0 means no limit)'), ('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts before giving up.'), + ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'), ('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'), ('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'), ('mbqi.max_cexs_incr', UINT, 0, 'increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI'), diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 4535b29c2..cdfdd208f 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1829,6 +1829,15 @@ namespace smt { m_bvar_inc *= INV_ACTIVITY_LIMIT; } + expr* context::next_decision() { + bool_var var; + lbool phase; + m_case_split_queue->next_case_split(var, phase); + if (var == null_bool_var) return m_manager.mk_true(); + m_case_split_queue->unassign_var_eh(var); + return bool_var2expr(var); + } + /** \brief Execute next clase split, return false if there are no more case splits to be performed. @@ -3433,6 +3442,7 @@ namespace smt { m_num_conflicts = 0; m_num_conflicts_since_restart = 0; m_num_conflicts_since_lemma_gc = 0; + m_num_restarts = 0; m_restart_threshold = m_fparams.m_restart_initial; m_restart_outer_threshold = m_fparams.m_restart_initial; m_agility = 0.0; @@ -3564,7 +3574,7 @@ namespace smt { inc_limits(); if (status == l_true || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) { SASSERT(!inconsistent()); - IF_VERBOSE(2, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations + IF_VERBOSE(2, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations << " :decisions " << m_stats.m_num_decisions << " :conflicts " << m_stats.m_num_conflicts << " :restart " << m_restart_threshold; if (m_fparams.m_restart_strategy == RS_IN_OUT_GEOMETRIC) { @@ -3573,9 +3583,10 @@ namespace smt { if (m_fparams.m_restart_adaptive) { verbose_stream() << " :agility " << m_agility; } - verbose_stream() << ")" << std::endl; verbose_stream().flush();); + verbose_stream() << ")\n"); // execute the restart m_stats.m_num_restarts++; + m_num_restarts++; if (m_scope_lvl > curr_lvl) { pop_scope(m_scope_lvl - curr_lvl); SASSERT(at_search_level()); @@ -3593,6 +3604,11 @@ namespace smt { status = l_false; return false; } + if (m_num_restarts >= m_fparams.m_restart_max) { + status = l_undef; + m_last_search_failure = NUM_CONFLICTS; + return false; + } } if (m_fparams.m_simplify_clauses) simplify_clauses(); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 8a4fc9471..ed78b9825 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -889,6 +889,8 @@ namespace smt { unsigned m_num_conflicts; unsigned m_num_conflicts_since_restart; unsigned m_num_conflicts_since_lemma_gc; + unsigned m_num_restarts; + unsigned m_num_simplifications; unsigned m_restart_threshold; unsigned m_restart_outer_threshold; unsigned m_luby_idx; @@ -1030,6 +1032,8 @@ namespace smt { enode * get_enode_eq_to(func_decl * f, unsigned num_args, enode * const * args); + expr* next_decision(); + protected: bool decide(); diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index a7948725c..78e33c7dd 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -175,11 +175,15 @@ namespace smt { void get_guessed_literals(expr_ref_vector & result) { m_kernel.get_guessed_literals(result); } - + + expr* next_decision() { + return m_kernel.next_decision(); + } + void collect_statistics(::statistics & st) const { m_kernel.collect_statistics(st); } - + void reset_statistics() { } @@ -347,6 +351,10 @@ namespace smt { m_imp->get_guessed_literals(result); } + expr* kernel::next_decision() { + return m_imp->next_decision(); + } + void kernel::display(std::ostream & out) const { m_imp->display(out); } diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index d10cab4f3..d15790429 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -212,6 +212,11 @@ namespace smt { */ void get_guessed_literals(expr_ref_vector & result); + /** + \brief return the next case split literal. + */ + expr* next_decision(); + /** \brief (For debubbing purposes) Prints the state of the kernel */ diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 780495e9c..2a7d52a48 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -30,9 +30,35 @@ Notes: namespace smt { class smt_solver : public solver_na2as { + + struct cuber { + smt_solver& m_solver; + unsigned m_round; + expr_ref m_result; + cuber(smt_solver& s): + m_solver(s), + m_round(0), + m_result(s.get_manager()) {} + expr_ref cube() { + switch (m_round) { + case 0: + m_result = m_solver.m_context.next_decision(); + break; + case 1: + m_result = m_solver.get_manager().mk_not(m_result); + break; + default: + m_result = m_solver.get_manager().mk_false(); + break; + } + ++m_round; + return m_result; + } + }; + smt_params m_smt_params; smt::kernel m_context; - progress_callback * m_callback; + cuber* m_cuber; symbol m_logic; bool m_minimizing_core; bool m_core_extend_patterns; @@ -45,6 +71,7 @@ namespace smt { solver_na2as(m), m_smt_params(p), m_context(m, m_smt_params), + m_cuber(nullptr), m_minimizing_core(false), m_core_extend_patterns(false), m_core_extend_patterns_max_distance(UINT_MAX), @@ -72,6 +99,7 @@ namespace smt { virtual ~smt_solver() { dec_ref_values(get_manager(), m_name2assertion); + dealloc(m_cuber); } virtual void updt_params(params_ref const & p) { @@ -204,7 +232,6 @@ namespace smt { virtual ast_manager & get_manager() const { return m_context.m(); } virtual void set_progress_callback(progress_callback * callback) { - m_callback = callback; m_context.set_progress_callback(callback); } @@ -217,13 +244,24 @@ namespace smt { return m_context.get_formula(idx); } - virtual expr_ref lookahead(expr_ref_vector const& assumptions, expr_ref_vector const& candidates) { + virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned cutoff) { ast_manager& m = get_manager(); - return expr_ref(m.mk_true(), m); - } - - virtual expr_ref_vector cube(expr_ref_vector&, unsigned) { - return expr_ref_vector(get_manager()); + if (!m_cuber) { + m_cuber = alloc(cuber, *this); + } + expr_ref result = m_cuber->cube(); + expr_ref_vector lits(m); + if (m.is_false(result)) { + dealloc(m_cuber); + m_cuber = nullptr; + } + if (m.is_true(result)) { + dealloc(m_cuber); + m_cuber = nullptr; + return lits; + } + lits.push_back(result); + return lits; } struct collect_fds_proc { diff --git a/src/tactic/portfolio/CMakeLists.txt b/src/tactic/portfolio/CMakeLists.txt index 055251467..e16992f9a 100644 --- a/src/tactic/portfolio/CMakeLists.txt +++ b/src/tactic/portfolio/CMakeLists.txt @@ -8,6 +8,7 @@ z3_add_component(portfolio pb2bv_solver.cpp smt_strategic_solver.cpp solver2lookahead.cpp + solver_sat_extension.cpp COMPONENT_DEPENDENCIES aig_tactic fp diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp index 988ab2ec4..fed4bde0a 100644 --- a/src/tactic/portfolio/parallel_tactic.cpp +++ b/src/tactic/portfolio/parallel_tactic.cpp @@ -41,8 +41,13 @@ Notes: #include "solver/solver.h" #include "solver/solver2tactic.h" #include "tactic/tactic.h" +#include "tactic/tactical.h" #include "tactic/portfolio/fd_solver.h" #include "tactic/smtlogics/parallel_params.hpp" +#include "smt/tactic/smt_tactic.h" +#include "smt/smt_solver.h" +#include "sat/sat_solver/inc_sat_solver.h" +#include "sat/tactic/sat_tactic.h" class parallel_tactic : public tactic { @@ -184,7 +189,6 @@ class parallel_tactic : public tactic { ref m_solver; // solver state unsigned m_depth; // number of nested calls to cubing double m_width; // estimate of fraction of problem handled by state - unsigned m_restart_max; // saved configuration value public: solver_state(ast_manager* m, solver* s, params_ref const& p, task_type t): @@ -196,8 +200,6 @@ class parallel_tactic : public tactic { m_depth(0), m_width(1.0) { - parallel_params pp(p); - m_restart_max = pp.restart_max(); } ast_manager& m() { return m_solver->get_manager(); } @@ -255,27 +257,12 @@ class parallel_tactic : public tactic { lbool simplify() { lbool r = l_undef; - if (m_depth == 1) { - IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-1)\n";); - set_simplify_params(true, true); // retain PB, retain blocked - r = get_solver().check_sat(0,0); - if (r != l_undef) return r; - - // copy over the resulting clauses with a configuration that blasts PB constraints - set_simplify_params(false, true); - expr_ref_vector fmls(m()); - get_solver().get_assertions(fmls); - model_converter_ref mc = get_solver().get_model_converter(); - m_solver = mk_fd_solver(m(), m_params); - m_solver->set_model_converter(mc.get()); - m_solver->assert_expr(fmls); - } - IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-2)\n";); - set_simplify_params(false, true); // remove PB, retain blocked + IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-1)\n";); + set_simplify_params(true); // retain blocked r = get_solver().check_sat(0,0); if (r != l_undef) return r; - IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-3)\n";); - set_simplify_params(false, false); // remove any PB, remove blocked + IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-2)\n";); + set_simplify_params(false); // remove blocked r = get_solver().check_sat(0,0); return r; } @@ -299,27 +286,26 @@ class parallel_tactic : public tactic { } void set_conquer_params(solver& s) { + parallel_params pp(m_params); params_ref p; p.copy(m_params); p.set_bool("gc.burst", true); // apply eager gc p.set_uint("simplify.delay", 1000); // delay simplification by 1000 conflicts p.set_bool("lookahead_simplify", false); - p.set_uint("restart.max", m_restart_max); + p.set_uint("restart.max", pp.conquer_restart_max()); p.set_uint("inprocess.max", UINT_MAX); // base bounds on restart.max s.updt_params(p); } - void set_simplify_params(bool pb_simp, bool retain_blocked) { + void set_simplify_params(bool retain_blocked) { parallel_params pp(m_params); + double mul = pp.simplify_multiplier(); + unsigned mult = (mul == 0 ? 1 : std::max((unsigned)1, static_cast(m_depth * mul))); params_ref p; p.copy(m_params); - - p.set_bool("cardinality.solver", pb_simp); - p.set_sym ("pb.solver", pb_simp ? symbol("solver") : symbol("circuit")); - if (p.get_uint("inprocess.max", UINT_MAX) == UINT_MAX) - p.set_uint("inprocess.max", pp.inprocess_max()); + p.set_uint("inprocess.max", pp.simplify_inprocess_max() * mult); + p.set_uint("restart.max", pp.simplify_restart_max() * mult); p.set_bool("lookahead_simplify", true); - p.set_uint("restart.max", UINT_MAX); p.set_bool("retain_blocked_clauses", retain_blocked); get_solver().updt_params(p); } @@ -337,6 +323,7 @@ class parallel_tactic : public tactic { private: + solver_ref m_solver; ast_manager& m_manager; params_ref m_params; sref_vector m_models; @@ -355,7 +342,8 @@ private: std::string m_exn_msg; void init() { - m_num_threads = omp_get_num_procs(); // TBD adjust by possible threads used inside each solver. + parallel_params pp(m_params); + m_num_threads = std::min((unsigned)omp_get_num_procs(), pp.threads_max()); m_progress = 0; m_has_undef = false; m_allsat = false; @@ -375,6 +363,7 @@ private: } void add_branches(unsigned b) { + if (b == 0) return; { std::lock_guard lock(m_mutex); m_branches += b; @@ -617,7 +606,6 @@ private: } else if (cubes.empty()) { dec_branch(); - return; } else { s.inc_width(width); @@ -746,15 +734,16 @@ private: public: - parallel_tactic(ast_manager& m, params_ref const& p) : - m_manager(m), + parallel_tactic(solver* s, params_ref const& p) : + m_solver(s), + m_manager(s->get_manager()), m_params(p) { init(); } void operator ()(const goal_ref & g,goal_ref_buffer & result) { ast_manager& m = g->m(); - solver* s = mk_fd_solver(m, m_params); + solver* s = m_solver->translate(m, m_params); solver_state* st = alloc(solver_state, 0, s, m_params, cube_task); m_queue.add_task(st); expr_ref_vector clauses(m); @@ -799,7 +788,8 @@ public: } tactic* translate(ast_manager& m) { - return alloc(parallel_tactic, m, m_params); + solver* s = m_solver->translate(m, m_params); + return alloc(parallel_tactic, s, m_params); } virtual void updt_params(params_ref const & p) { @@ -817,12 +807,40 @@ public: virtual void reset_statistics() { m_stats.reset(); } - }; -tactic * mk_parallel_tactic(ast_manager& m, params_ref const& p) { - return alloc(parallel_tactic, m, p); +tactic * mk_parallel_qffd_tactic(ast_manager& m, params_ref const& p) { + solver* s = mk_fd_solver(m, p); + return alloc(parallel_tactic, s, p); } +tactic * mk_parallel_tactic(solver* s, params_ref const& p) { + return alloc(parallel_tactic, s, p); +} + + +tactic * mk_psat_tactic(ast_manager& m, params_ref const& p) { + parallel_params pp(p); + bool use_parallel = pp.enable(); + return pp.enable() ? mk_parallel_tactic(mk_inc_sat_solver(m, p), p) : mk_sat_tactic(m); +} + +tactic * mk_psmt_tactic(ast_manager& m, params_ref const& p, symbol const& logic) { + parallel_params pp(p); + bool use_parallel = pp.enable(); + return pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_smt_tactic(p); +} + +tactic * mk_psmt_tactic_using(ast_manager& m, bool auto_config, params_ref const& _p, symbol const& logic) { + parallel_params pp(_p); + bool use_parallel = pp.enable(); + params_ref p = _p; + p.set_bool("auto_config", auto_config); + return using_params(pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_smt_tactic(p), p); +} + +tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p) { + return mk_parallel_tactic(mk_smt_solver(m, p, symbol::null), p); +} diff --git a/src/tactic/portfolio/parallel_tactic.h b/src/tactic/portfolio/parallel_tactic.h index 8fd9a29fa..f3dc36d0e 100644 --- a/src/tactic/portfolio/parallel_tactic.h +++ b/src/tactic/portfolio/parallel_tactic.h @@ -21,11 +21,20 @@ Notes: class solver; class tactic; +class solver; -tactic * mk_parallel_tactic(ast_manager& m, params_ref const& p); +tactic * mk_parallel_tactic(solver* s, params_ref const& p); +tactic * mk_parallel_qffd_tactic(ast_manager& m, params_ref const& p); +tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p); + +// create parallel sat/smt tactics if parallel.enable=true, otherwise return sequential versions. +tactic * mk_psat_tactic(ast_manager& m, params_ref const& p); +tactic * mk_psmt_tactic(ast_manager& m, params_ref const& p, symbol const& logic = symbol::null); +tactic * mk_psmt_tactic_using(ast_manager& m, bool auto_config, params_ref const& p, symbol const& logic = symbol::null); /* - ADD_TACTIC("qffdp", "builtin strategy for solving QF_FD problems in parallel.", "mk_parallel_tactic(m, p)") + ADD_TACTIC("pqffd", "builtin strategy for solving QF_FD problems in parallel.", "mk_parallel_qffd_tactic(m, p)") + ADD_TACTIC("psmt", "builtin strategy for SMT tactic in parallel.", "mk_parallel_smt_tactic(m, p)") */ #endif diff --git a/src/tactic/smtlogics/nra_tactic.cpp b/src/tactic/smtlogics/nra_tactic.cpp index 381bc4bb6..a9b32e5a8 100644 --- a/src/tactic/smtlogics/nra_tactic.cpp +++ b/src/tactic/smtlogics/nra_tactic.cpp @@ -19,13 +19,13 @@ Notes: #include "tactic/tactical.h" #include "tactic/core/simplify_tactic.h" #include "tactic/core/propagate_values_tactic.h" -#include "smt/tactic/smt_tactic.h" #include "tactic/core/nnf_tactic.h" +#include "tactic/arith/probe_arith.h" +#include "smt/tactic/smt_tactic.h" #include "qe/qe_tactic.h" #include "qe/nlqsat.h" -#include "nlsat/tactic/qfnra_nlsat_tactic.h" #include "qe/qe_lite.h" -#include "tactic/arith/probe_arith.h" +#include "nlsat/tactic/qfnra_nlsat_tactic.h" tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) { params_ref p1 = p; diff --git a/src/tactic/smtlogics/parallel_params.pyg b/src/tactic/smtlogics/parallel_params.pyg index 84f4eb2c4..590fc02d2 100644 --- a/src/tactic/smtlogics/parallel_params.pyg +++ b/src/tactic/smtlogics/parallel_params.pyg @@ -4,8 +4,11 @@ def_module_params('parallel', export=True, params=( ('enable', BOOL, False, 'enable parallel solver by default on selected tactics (for QF_BV)'), - ('conquer_batch_size', UINT, 1000, 'number of cubes to batch together for fast conquer'), - ('inprocess.max', UINT, 2, 'maximal number of inprocessing steps during simplification'), - ('restart.max', UINT, 5, 'maximal number of restarts during conquer phase'), - ('conquer_threshold', UINT, 10, 'number of cubes generated before simple conquer solver is created'), + ('threads.max', UINT, 10000, 'caps maximal number of threads below the number of processors'), + ('simplify.multiplier', DOUBLE, 0, 'restart and inprocess max is increased by depth * simplify.multipler, unless the multiplier is 0'), + ('conquer.batch_size', UINT, 1000, 'number of cubes to batch together for fast conquer'), + ('conquer.threshold', UINT, 10, 'number of cubes generated before simple conquer solver is created'), + ('conquer.restart.max', UINT, 5, 'maximal number of restarts during conquer phase'), + ('simplify.restart.max', UINT, 5000, 'maximal number of restarts during simplification phase'), + ('simplify.inprocess.max', UINT, 2, 'maximal number of inprocessing steps during simplification'), )) diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index 25741c09e..68f054640 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -28,6 +28,7 @@ Notes: #include "tactic/bv/bv_size_reduction_tactic.h" #include "tactic/aig/aig_tactic.h" #include "sat/tactic/sat_tactic.h" +#include "sat/sat_solver/inc_sat_solver.h" #include "tactic/portfolio/parallel_tactic.h" #include "tactic/smtlogics/parallel_params.hpp" #include "ackermannization/ackermannize_bv_tactic.h" @@ -129,12 +130,10 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { - parallel_params pp(p); - bool use_parallel = pp.enable(); tactic * new_sat = cond(mk_produce_proofs_probe(), and_then(mk_simplify_tactic(m), mk_smt_tactic()), - use_parallel ? mk_parallel_tactic(m, p): mk_sat_tactic(m)); + mk_psat_tactic(m, p)); - return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic()); + return mk_qfbv_tactic(m, p, new_sat, mk_psmt_tactic(m, p)); } diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp index 248829c49..b30103f43 100644 --- a/src/tactic/smtlogics/qflia_tactic.cpp +++ b/src/tactic/smtlogics/qflia_tactic.cpp @@ -24,7 +24,6 @@ Notes: #include "tactic/core/solve_eqs_tactic.h" #include "tactic/core/elim_uncnstr_tactic.h" #include "smt/tactic/smt_tactic.h" -// include"mip_tactic.h" #include "tactic/arith/add_bounds_tactic.h" #include "tactic/arith/pb2bv_tactic.h" #include "tactic/arith/lia2pb_tactic.h" @@ -35,6 +34,7 @@ Notes: #include "sat/tactic/sat_tactic.h" #include "tactic/arith/bound_manager.h" #include "tactic/arith/probe_arith.h" +#include "tactic/portfolio/parallel_tactic.h" struct quasi_pb_probe : public probe { virtual result operator()(goal const & g) { @@ -42,10 +42,7 @@ struct quasi_pb_probe : public probe { bound_manager bm(g.m()); bm(g); rational l, u; bool st; - bound_manager::iterator it = bm.begin(); - bound_manager::iterator end = bm.end(); - for (; it != end; ++it) { - expr * t = *it; + for (expr * t : bm) { if (bm.has_lower(t, l, st) && bm.has_upper(t, u, st) && (l.is_zero() || l.is_one()) && (u.is_zero() || u.is_one())) continue; if (found_non_01) @@ -93,7 +90,7 @@ static tactic * mk_bv2sat_tactic(ast_manager & m) { mk_max_bv_sharing_tactic(m), mk_bit_blaster_tactic(m), mk_aig_tactic(), - mk_sat_tactic(m)), + mk_sat_tactic(m, solver_p)), solver_p); } @@ -224,7 +221,7 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) { using_params(mk_lia2sat_tactic(m), quasi_pb_p), mk_fail_if_undecided_tactic()), mk_bounded_tactic(m), - mk_smt_tactic())), + mk_psmt_tactic(m, p))), main_p); st->updt_params(p); From cd35caff5237c1e6d24f069cb2e3a144b76595a4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 16 Apr 2018 03:18:57 -0700 Subject: [PATCH 18/24] clean up parallel tactic Signed-off-by: Nikolaj Bjorner --- src/ast/ast_translation.h | 14 ++ src/sat/sat_solver/inc_sat_solver.cpp | 9 +- src/tactic/portfolio/parallel_tactic.cpp | 216 ++++++----------------- src/tactic/smtlogics/parallel_params.pyg | 5 +- 4 files changed, 81 insertions(+), 163 deletions(-) diff --git a/src/ast/ast_translation.h b/src/ast/ast_translation.h index 47517a073..d5e29e785 100644 --- a/src/ast/ast_translation.h +++ b/src/ast/ast_translation.h @@ -71,6 +71,11 @@ public: template T * operator()(T const * n) { + return translate(n); + } + + template + T * translate(T const * n) { if (&from() == &to()) return const_cast(n); SASSERT(!n || from().contains(const_cast(n))); ast * r = process(n); @@ -78,9 +83,17 @@ public: return static_cast(r); } + ast_manager & from() const { return m_from_manager; } ast_manager & to() const { return m_to_manager; } + template + ref_vector operator()(ref_vector const& src) { + ref_vector dst(to()); + for (expr* v : src) dst.push_back(translate(v)); + return dst; + } + void reset_cache(); void cleanup(); @@ -100,6 +113,7 @@ inline expr * translate(expr const * e, ast_manager & from, ast_manager & to) { return ast_translation(from, to)(e); } + class expr_dependency_translation { ast_translation & m_translation; ptr_vector m_buffer; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index a7499590b..760110e82 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -31,11 +31,11 @@ Notes: #include "tactic/arith/card2bv_tactic.h" #include "tactic/bv/bit_blaster_tactic.h" #include "tactic/core/simplify_tactic.h" +#include "tactic/core/solve_eqs_tactic.h" +#include "tactic/bv/bit_blaster_model_converter.h" #include "model/model_smt2_pp.h" #include "model/model_v2_pp.h" #include "model/model_evaluator.h" -#include "tactic/bv/bit_blaster_model_converter.h" -#include "tactic/core/propagate_values_tactic.h" #include "sat/sat_solver.h" #include "sat/sat_params.hpp" #include "sat/tactic/goal2sat.h" @@ -501,7 +501,10 @@ public: simp2_p.set_bool("elim_and", true); simp2_p.set_bool("blast_distinct", true); m_preprocess = - and_then(mk_card2bv_tactic(m, m_params), // updates model converter + and_then(mk_simplify_tactic(m), + mk_propagate_values_tactic(m), + //time consuming if done in inner loop: mk_solve_eqs_tactic(m, simp2_p), + mk_card2bv_tactic(m, m_params), // updates model converter using_params(mk_simplify_tactic(m), simp2_p), mk_max_bv_sharing_tactic(m), mk_bit_blaster_tactic(m, m_bb_rewriter.get()), // updates model converter diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp index fed4bde0a..b3f5dfc30 100644 --- a/src/tactic/portfolio/parallel_tactic.cpp +++ b/src/tactic/portfolio/parallel_tactic.cpp @@ -16,20 +16,16 @@ Author: Miguel Neves Notes: - A task comprises of a non-empty sequence of cubes, a type and parameters - - If in the cube state, the solver performs the following: + + It invokes the following procedure: 1. Clone the state with the remaining cubes if there is more than one cube. Re-enqueue the remaining cubes. 2. Apply simplifications and pre-processing according to configuration. 3. Cube using the parameter settings prescribed in m_params. - 4. Create a conquer state with the produced cubes. - If in the conquer state, the solver performs the following - 1. Pass the cubes as assumptions and solve each sub-cube with a prescribed resource bound. - 2. Assemble cubes that could not be solved and create a cube state. + 4. Optionally pass the cubes as assumptions and solve each sub-cube with a prescribed resource bound. + 5. Assemble cubes that could not be solved and create a cube state. - --*/ #include @@ -52,8 +48,6 @@ Notes: class parallel_tactic : public tactic { - enum task_type { cube_task, conquer_task }; - class solver_state; class task_queue { @@ -169,11 +163,7 @@ class parallel_tactic : public tactic { m_vars(vs), m_cube(c) {} cube_var operator()(ast_translation& tr) { - expr_ref_vector vars(tr.to()); - expr_ref_vector cube(tr.to()); - for (expr* v : m_vars) vars.push_back(tr(v)); - for (expr* c : m_cube) cube.push_back(tr(c)); - return cube_var(cube, vars); + return cube_var(tr(m_cube), tr(m_vars)); } expr_ref_vector const& cube() const { return m_cube; } @@ -181,9 +171,8 @@ class parallel_tactic : public tactic { }; class solver_state { - task_type m_type; // current work role of the task scoped_ptr m_manager; // ownership handle to ast_manager - vector m_cubes; // set of cubes to process by task + vector m_cubes; // set of cubes to process by task expr_ref_vector m_asserted_cubes; // set of cubes asserted on the current solver params_ref m_params; // configuration parameters ref m_solver; // solver state @@ -191,8 +180,7 @@ class parallel_tactic : public tactic { double m_width; // estimate of fraction of problem handled by state public: - solver_state(ast_manager* m, solver* s, params_ref const& p, task_type t): - m_type(t), + solver_state(ast_manager* m, solver* s, params_ref const& p): m_manager(m), m_asserted_cubes(s->get_manager()), m_params(p), @@ -210,13 +198,13 @@ class parallel_tactic : public tactic { solver const& get_solver() const { return *m_solver; } - solver_state* clone(solver* s0 = nullptr) { + solver_state* clone() { SASSERT(!m_cubes.empty()); ast_manager& m = m_solver->get_manager(); - ast_manager* new_m = alloc(ast_manager, m, !m.proof_mode()); + ast_manager* new_m = alloc(ast_manager, m, m.proof_mode()); ast_translation tr(m, *new_m); - solver* s = (s0 ? s0 : m_solver.get())->translate(*new_m, m_params); - solver_state* st = alloc(solver_state, new_m, s, m_params, m_type); + solver* s = m_solver.get()->translate(*new_m, m_params); + solver_state* st = alloc(solver_state, new_m, s, m_params); for (auto & c : m_cubes) st->m_cubes.push_back(c(tr)); for (expr* c : m_asserted_cubes) st->m_asserted_cubes.push_back(tr(c)); st->m_depth = m_depth; @@ -224,11 +212,7 @@ class parallel_tactic : public tactic { return st; } - task_type type() const { return m_type; } - - void set_type(task_type t) { m_type = t; } - - vector const& cubes() const { SASSERT(m_type == conquer_task); return m_cubes; } + vector const& cubes() const { return m_cubes; } // remove up to n cubes from list of cubes. vector split_cubes(unsigned n) { @@ -247,9 +231,7 @@ class parallel_tactic : public tactic { void inc_depth(unsigned inc) { m_depth += inc; } - void inc_width(unsigned w) { - m_width *= w; - } + void inc_width(unsigned w) { m_width *= w; } double get_width() const { return m_width; } @@ -272,13 +254,7 @@ class parallel_tactic : public tactic { m_asserted_cubes.append(cube); } - lbool solve(expr_ref_vector const& cube) { - set_conquer_params(); - return get_solver().check_sat(cube); - } - - void set_cube_params() { - // get_solver().updt_params(m_params); + void set_cube_params() { } void set_conquer_params() { @@ -299,10 +275,11 @@ class parallel_tactic : public tactic { void set_simplify_params(bool retain_blocked) { parallel_params pp(m_params); - double mul = pp.simplify_multiplier(); - unsigned mult = (mul == 0 ? 1 : std::max((unsigned)1, static_cast(m_depth * mul))); params_ref p; p.copy(m_params); + double exp = pp.simplify_exp(); + exp = std::max(exp, 1.0); + unsigned mult = static_cast(pow(exp, m_depth - 1)); p.set_uint("inprocess.max", pp.simplify_inprocess_max() * mult); p.set_uint("restart.max", pp.simplify_restart_max() * mult); p.set_bool("lookahead_simplify", true); @@ -323,23 +300,23 @@ class parallel_tactic : public tactic { private: - solver_ref m_solver; - ast_manager& m_manager; - params_ref m_params; + solver_ref m_solver; + ast_manager& m_manager; + params_ref m_params; sref_vector m_models; - unsigned m_num_threads; - statistics m_stats; - task_queue m_queue; - std::mutex m_mutex; - double m_progress; - unsigned m_branches; - unsigned m_backtrack_frequency; - unsigned m_conquer_threshold; - bool m_has_undef; - bool m_allsat; - unsigned m_num_unsat; - int m_exn_code; - std::string m_exn_msg; + unsigned m_num_threads; + statistics m_stats; + task_queue m_queue; + std::mutex m_mutex; + double m_progress; + unsigned m_branches; + unsigned m_backtrack_frequency; + unsigned m_conquer_delay; + volatile bool m_has_undef; + bool m_allsat; + unsigned m_num_unsat; + int m_exn_code; + std::string m_exn_msg; void init() { parallel_params pp(m_params); @@ -349,8 +326,8 @@ private: m_allsat = false; m_branches = 0; m_num_unsat = 0; - m_backtrack_frequency = 10; - m_conquer_threshold = 10; + m_backtrack_frequency = pp.conquer_backtrack_frequency(); + m_conquer_delay = pp.conquer_delay(); m_exn_code = 0; m_params.set_bool("override_incremental", true); } @@ -418,104 +395,12 @@ private: close_branch(s, l_undef); } - void cube_and_conquer1(solver_state& s) { - ast_manager& m = s.m(); - vector cube, hard_cubes, cubes; - expr_ref_vector vars(m); - - switch (s.type()) { - case cube_task: goto cube; - case conquer_task: goto conquer; - } - - cube: - SASSERT(s.type() == cube_task); - - // extract up to one cube and add it. - cube.reset(); - cube.append(s.split_cubes(1)); - SASSERT(cube.size() <= 1); - IF_VERBOSE(2, verbose_stream() << "(tactic.parallel :split-cube " << cube.size() << ")\n";); - if (!s.cubes().empty()) m_queue.add_task(s.clone()); - if (!cube.empty()) { - s.assert_cube(cube.get(0).cube()); - vars.reset(); - vars.append(cube.get(0).vars()); - } - s.inc_depth(1); - - // simplify - switch (s.simplify()) { - case l_undef: break; - case l_true: report_sat(s); return; - case l_false: report_unsat(s); return; - } - if (canceled(s)) return; - - // extract cubes. - cubes.reset(); - s.set_cube_params(); - unsigned cutoff = UINT_MAX; - while (true) { - expr_ref_vector c = s.get_solver().cube(vars, cutoff); - if (c.empty()) { - report_undef(s); - return; - } - if (m.is_false(c.back())) { - break; - } - cubes.push_back(cube_var(c, vars)); - IF_VERBOSE(2, verbose_stream() << "(tactic.parallel :cube " << cubes.size() << " :vars " << vars.size() << ")\n"); - } - - IF_VERBOSE(1, verbose_stream() << "(tactic.parallel :cubes " << cubes.size() << ")\n";); - - if (cubes.empty()) { - report_unsat(s); - return; - } - else { - s.inc_width(cubes.size()); - add_branches(cubes.size() - 1); - s.set_cubes(cubes); - s.set_type(conquer_task); - goto conquer; - } - - conquer: - SASSERT(s.type() == conquer_task); - - // extract a batch of cubes - cubes.reset(); - cubes.append(s.split_cubes(conquer_batch_size())); - if (!s.cubes().empty()) m_queue.add_task(s.clone()); - - s.set_conquer_params(); - hard_cubes.reset(); - for (cube_var& cv : cubes) { - switch (s.solve(cv.cube())) { - case l_undef: hard_cubes.push_back(cv); break; - case l_true: report_sat(s); break; - case l_false: report_unsat(s); break; - } - if (canceled(s)) return; - } - IF_VERBOSE(1, verbose_stream() << "(tactic.parallel :cubes " << cubes.size() << " :hard-cubes " << hard_cubes.size() << ")\n";); - if (hard_cubes.empty()) return; - - s.set_cubes(hard_cubes); - s.set_type(cube_task); - goto cube; - } - - void cube_and_conquer2(solver_state& s) { + void cube_and_conquer(solver_state& s) { ast_manager& m = s.m(); vector cube, hard_cubes, cubes; expr_ref_vector vars(m); cube_again: - SASSERT(s.type() == cube_task); // extract up to one cube and add it. cube.reset(); cube.append(s.split_cubes(1)); @@ -527,9 +412,9 @@ private: vars.reset(); vars.append(cube.get(0).vars()); } - s.inc_depth(1); simplify_again: + s.inc_depth(1); // simplify if (canceled(s)) return; switch (s.simplify()) { @@ -539,6 +424,9 @@ private: } if (canceled(s)) return; + if (memory_pressure()) { + goto simplify_again; + } // extract cubes. cubes.reset(); s.set_cube_params(); @@ -556,7 +444,7 @@ private: break; } lbool is_sat = l_undef; - if (width >= m_conquer_threshold && !conquer) { + if (width >= m_conquer_delay && !conquer) { conquer = s.copy_solver(); s.set_conquer_params(*conquer.get()); } @@ -669,10 +557,14 @@ private: } } + bool memory_pressure() { + return memory::above_high_watermark(); + } + void run_solver() { try { while (solver_state* st = m_queue.get_task()) { - cube_and_conquer2(*st); + cube_and_conquer(*st); collect_statistics(*st); m_queue.task_done(st); if (st->m().canceled()) m_queue.shutdown(); @@ -725,10 +617,17 @@ private: } std::ostream& display(std::ostream& out) { + unsigned n_models, n_unsat; + double n_progress; + { + std::lock_guard lock(m_mutex); + n_models = m_models.size(); + n_unsat = m_num_unsat; + n_progress = m_progress; + } m_stats.display(out); m_queue.display(out); - std::lock_guard lock(m_mutex); - out << "(tactic.parallel :unsat " << m_num_unsat << " :progress " << m_progress << "% :models " << m_models.size() << ")\n"; + out << "(tactic.parallel :unsat " << n_unsat << " :progress " << n_progress << "% :models " << n_models << ")\n"; return out; } @@ -744,7 +643,7 @@ public: void operator ()(const goal_ref & g,goal_ref_buffer & result) { ast_manager& m = g->m(); solver* s = m_solver->translate(m, m_params); - solver_state* st = alloc(solver_state, 0, s, m_params, cube_task); + solver_state* st = alloc(solver_state, 0, s, m_params); m_queue.add_task(st); expr_ref_vector clauses(m); ptr_vector assumptions; @@ -795,7 +694,7 @@ public: virtual void updt_params(params_ref const & p) { m_params.copy(p); parallel_params pp(p); - m_conquer_threshold = pp.conquer_threshold(); + m_conquer_delay = pp.conquer_delay(); } virtual void collect_statistics(statistics & st) const { @@ -804,6 +703,7 @@ public: st.update("par models", m_models.size()); st.update("par progress", m_progress); } + virtual void reset_statistics() { m_stats.reset(); } diff --git a/src/tactic/smtlogics/parallel_params.pyg b/src/tactic/smtlogics/parallel_params.pyg index 590fc02d2..58c00aa97 100644 --- a/src/tactic/smtlogics/parallel_params.pyg +++ b/src/tactic/smtlogics/parallel_params.pyg @@ -5,10 +5,11 @@ def_module_params('parallel', params=( ('enable', BOOL, False, 'enable parallel solver by default on selected tactics (for QF_BV)'), ('threads.max', UINT, 10000, 'caps maximal number of threads below the number of processors'), - ('simplify.multiplier', DOUBLE, 0, 'restart and inprocess max is increased by depth * simplify.multipler, unless the multiplier is 0'), ('conquer.batch_size', UINT, 1000, 'number of cubes to batch together for fast conquer'), - ('conquer.threshold', UINT, 10, 'number of cubes generated before simple conquer solver is created'), ('conquer.restart.max', UINT, 5, 'maximal number of restarts during conquer phase'), + ('conquer.delay', UINT, 10, 'delay of cubes until applying conquer'), + ('conquer.backtrack_frequency', UINT, 10, 'frequency to apply core minimization during conquer'), + ('simplify.exp', DOUBLE, 1, 'restart and inprocess max is multipled by simplify.exp ^ depth'), ('simplify.restart.max', UINT, 5000, 'maximal number of restarts during simplification phase'), ('simplify.inprocess.max', UINT, 2, 'maximal number of inprocessing steps during simplification'), )) From a37303a045c298a96c9b32573a596f81fea42d38 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 16 Apr 2018 08:21:21 -0700 Subject: [PATCH 19/24] move parallel-tactic to solver level Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 9 +++++ src/sat/sat_solver/inc_sat_solver.h | 4 ++ src/sat/tactic/sat_tactic.cpp | 3 ++ src/smt/tactic/smt_tactic.cpp | 33 +++++++++++---- src/smt/tactic/smt_tactic.h | 5 +++ src/solver/CMakeLists.txt | 3 ++ .../portfolio => solver}/parallel_tactic.cpp | 33 +-------------- src/solver/parallel_tactic.h | 27 +++++++++++++ .../parallel_tactic_params.pyg} | 2 +- src/tactic/portfolio/CMakeLists.txt | 3 -- src/tactic/portfolio/fd_solver.cpp | 7 ++++ src/tactic/portfolio/fd_solver.h | 2 + src/tactic/portfolio/parallel_tactic.h | 40 ------------------- src/tactic/smtlogics/CMakeLists.txt | 1 - src/tactic/smtlogics/qfbv_tactic.cpp | 2 - src/tactic/smtlogics/qflia_tactic.cpp | 1 - 16 files changed, 89 insertions(+), 86 deletions(-) rename src/{tactic/portfolio => solver}/parallel_tactic.cpp (95%) create mode 100644 src/solver/parallel_tactic.h rename src/{tactic/smtlogics/parallel_params.pyg => solver/parallel_tactic_params.pyg} (95%) delete mode 100644 src/tactic/portfolio/parallel_tactic.h diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 760110e82..7c0b6cae5 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -24,6 +24,8 @@ Notes: #include "ast/ast_util.h" #include "solver/solver.h" #include "solver/tactic2solver.h" +#include "solver/parallel_params.hpp" +#include "solver/parallel_tactic.h" #include "tactic/tactical.h" #include "tactic/aig/aig_tactic.h" #include "tactic/core/propagate_values_tactic.h" @@ -39,6 +41,7 @@ Notes: #include "sat/sat_solver.h" #include "sat/sat_params.hpp" #include "sat/tactic/goal2sat.h" +#include "sat/tactic/sat_tactic.h" #include "sat/sat_simplifier_params.hpp" // incremental SAT solver. @@ -865,3 +868,9 @@ void inc_sat_display(std::ostream& out, solver& _s, unsigned sz, expr*const* sof s.display_weighted(out, sz, soft, weights.c_ptr()); } + +tactic * mk_psat_tactic(ast_manager& m, params_ref const& p) { + parallel_params pp(p); + bool use_parallel = pp.enable(); + return pp.enable() ? mk_parallel_tactic(mk_inc_sat_solver(m, p, false), p) : mk_sat_tactic(m); +} diff --git a/src/sat/sat_solver/inc_sat_solver.h b/src/sat/sat_solver/inc_sat_solver.h index fb4b05b91..71ec48b99 100644 --- a/src/sat/sat_solver/inc_sat_solver.h +++ b/src/sat/sat_solver/inc_sat_solver.h @@ -22,8 +22,12 @@ Notes: #include "solver/solver.h" +class tactic; + solver* mk_inc_sat_solver(ast_manager& m, params_ref const& p, bool incremental_mode = true); +tactic* mk_psat_tactic(ast_manager& m, params_ref const& p); + void inc_sat_display(std::ostream& out, solver& s, unsigned sz, expr*const* soft, rational const* _weights); diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index 6beec79c9..d810c76bb 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -20,6 +20,8 @@ Notes: #include "tactic/tactical.h" #include "sat/tactic/goal2sat.h" #include "sat/sat_solver.h" +#include "solver/parallel_tactic.h" +#include "solver/parallel_params.hpp" #include "model/model_v2_pp.h" class sat_tactic : public tactic { @@ -215,3 +217,4 @@ tactic * mk_sat_preprocessor_tactic(ast_manager & m, params_ref const & p) { return t; } + diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index 97b6d89d7..0359e2031 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -16,19 +16,21 @@ Author: Notes: --*/ -#include "tactic/tactic.h" -#include "tactic/tactical.h" +#include "util/lp/lp_params.hpp" +#include "ast/rewriter/rewriter_types.h" +#include "ast/ast_util.h" #include "smt/smt_kernel.h" #include "smt/params/smt_params.h" #include "smt/params/smt_params_helper.hpp" -#include "util/lp/lp_params.hpp" -#include "ast/rewriter/rewriter_types.h" -#include "tactic/generic_model_converter.h" -#include "ast/ast_util.h" -#include "solver/solver2tactic.h" #include "smt/smt_solver.h" +#include "tactic/tactic.h" +#include "tactic/tactical.h" +#include "tactic/generic_model_converter.h" +#include "solver/solver2tactic.h" #include "solver/solver.h" #include "solver/mus.h" +#include "solver/parallel_tactic.h" +#include "solver/parallel_params.hpp" typedef obj_map expr2expr_map; @@ -301,3 +303,20 @@ tactic * mk_smt_tactic_using(bool auto_config, params_ref const & _p) { return using_params(r, p); } +tactic * mk_psmt_tactic(ast_manager& m, params_ref const& p, symbol const& logic) { + parallel_params pp(p); + bool use_parallel = pp.enable(); + return pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_smt_tactic(p); +} + +tactic * mk_psmt_tactic_using(ast_manager& m, bool auto_config, params_ref const& _p, symbol const& logic) { + parallel_params pp(_p); + bool use_parallel = pp.enable(); + params_ref p = _p; + p.set_bool("auto_config", auto_config); + return using_params(pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_smt_tactic(p), p); +} + +tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p) { + return mk_parallel_tactic(mk_smt_solver(m, p, symbol::null), p); +} diff --git a/src/smt/tactic/smt_tactic.h b/src/smt/tactic/smt_tactic.h index c7b91d032..fbee950c2 100644 --- a/src/smt/tactic/smt_tactic.h +++ b/src/smt/tactic/smt_tactic.h @@ -31,8 +31,13 @@ tactic * mk_smt_tactic(params_ref const & p = params_ref()); // syntax sugar for using_params(mk_smt_tactic(), p) where p = (:auto_config, auto_config) tactic * mk_smt_tactic_using(bool auto_config = true, params_ref const & p = params_ref()); +tactic * mk_psmt_tactic(ast_manager& m, params_ref const& p, symbol const& logic = symbol::null); +tactic * mk_psmt_tactic_using(ast_manager& m, bool auto_config, params_ref const& p, symbol const& logic = symbol::null); +tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p); + /* ADD_TACTIC("smt", "apply a SAT based SMT solver.", "mk_smt_tactic(p)") + ADD_TACTIC("psmt", "builtin strategy for SMT tactic in parallel.", "mk_parallel_smt_tactic(m, p)") */ #endif diff --git a/src/solver/CMakeLists.txt b/src/solver/CMakeLists.txt index 1ffdc35e1..c8e206f7f 100644 --- a/src/solver/CMakeLists.txt +++ b/src/solver/CMakeLists.txt @@ -3,6 +3,7 @@ z3_add_component(solver check_sat_result.cpp combined_solver.cpp mus.cpp + parallel_tactic.cpp smt_logics.cpp solver.cpp solver_na2as.cpp @@ -14,4 +15,6 @@ z3_add_component(solver tactic PYG_FILES combined_solver_params.pyg + parallel_params.pyg + ) diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp similarity index 95% rename from src/tactic/portfolio/parallel_tactic.cpp rename to src/solver/parallel_tactic.cpp index b3f5dfc30..748ee5d64 100644 --- a/src/tactic/portfolio/parallel_tactic.cpp +++ b/src/solver/parallel_tactic.cpp @@ -39,7 +39,8 @@ Notes: #include "tactic/tactic.h" #include "tactic/tactical.h" #include "tactic/portfolio/fd_solver.h" -#include "tactic/smtlogics/parallel_params.hpp" +#include "solver/parallel_tactic.h" +#include "solver/parallel_params.hpp" #include "smt/tactic/smt_tactic.h" #include "smt/smt_solver.h" #include "sat/sat_solver/inc_sat_solver.h" @@ -710,37 +711,7 @@ public: }; - -tactic * mk_parallel_qffd_tactic(ast_manager& m, params_ref const& p) { - solver* s = mk_fd_solver(m, p); - return alloc(parallel_tactic, s, p); -} - tactic * mk_parallel_tactic(solver* s, params_ref const& p) { return alloc(parallel_tactic, s, p); } - -tactic * mk_psat_tactic(ast_manager& m, params_ref const& p) { - parallel_params pp(p); - bool use_parallel = pp.enable(); - return pp.enable() ? mk_parallel_tactic(mk_inc_sat_solver(m, p), p) : mk_sat_tactic(m); -} - -tactic * mk_psmt_tactic(ast_manager& m, params_ref const& p, symbol const& logic) { - parallel_params pp(p); - bool use_parallel = pp.enable(); - return pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_smt_tactic(p); -} - -tactic * mk_psmt_tactic_using(ast_manager& m, bool auto_config, params_ref const& _p, symbol const& logic) { - parallel_params pp(_p); - bool use_parallel = pp.enable(); - params_ref p = _p; - p.set_bool("auto_config", auto_config); - return using_params(pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_smt_tactic(p), p); -} - -tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p) { - return mk_parallel_tactic(mk_smt_solver(m, p, symbol::null), p); -} diff --git a/src/solver/parallel_tactic.h b/src/solver/parallel_tactic.h new file mode 100644 index 000000000..ae8fb6041 --- /dev/null +++ b/src/solver/parallel_tactic.h @@ -0,0 +1,27 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + parallel_tactic.h + +Abstract: + + Parallel tactic in the style of Treengeling. + +Author: + + Nikolaj Bjorner (nbjorner) 2017-10-9 + +Notes: + +--*/ +#ifndef PARALLEL_TACTIC_H_ +#define PARALLEL_TACTIC_H_ + +class tactic; +class solver; + +tactic * mk_parallel_tactic(solver* s, params_ref const& p); + +#endif diff --git a/src/tactic/smtlogics/parallel_params.pyg b/src/solver/parallel_tactic_params.pyg similarity index 95% rename from src/tactic/smtlogics/parallel_params.pyg rename to src/solver/parallel_tactic_params.pyg index 58c00aa97..6d633a6af 100644 --- a/src/tactic/smtlogics/parallel_params.pyg +++ b/src/solver/parallel_tactic_params.pyg @@ -1,6 +1,6 @@ def_module_params('parallel', description='parameters for parallel solver', - class_name='parallel_params', + class_name='parallel_tactic_params', export=True, params=( ('enable', BOOL, False, 'enable parallel solver by default on selected tactics (for QF_BV)'), diff --git a/src/tactic/portfolio/CMakeLists.txt b/src/tactic/portfolio/CMakeLists.txt index e16992f9a..2b714cc2c 100644 --- a/src/tactic/portfolio/CMakeLists.txt +++ b/src/tactic/portfolio/CMakeLists.txt @@ -4,11 +4,9 @@ z3_add_component(portfolio default_tactic.cpp enum2bv_solver.cpp fd_solver.cpp - parallel_tactic.cpp pb2bv_solver.cpp smt_strategic_solver.cpp solver2lookahead.cpp - solver_sat_extension.cpp COMPONENT_DEPENDENCIES aig_tactic fp @@ -22,5 +20,4 @@ z3_add_component(portfolio TACTIC_HEADERS default_tactic.h fd_solver.h - parallel_tactic.h ) diff --git a/src/tactic/portfolio/fd_solver.cpp b/src/tactic/portfolio/fd_solver.cpp index 946b3b30c..b0d95baee 100644 --- a/src/tactic/portfolio/fd_solver.cpp +++ b/src/tactic/portfolio/fd_solver.cpp @@ -24,6 +24,8 @@ Notes: #include "tactic/portfolio/pb2bv_solver.h" #include "tactic/portfolio/bounded_int2bv_solver.h" #include "solver/solver2tactic.h" +#include "solver/parallel_tactic.h" +#include "solver/parallel_params.hpp" solver * mk_fd_solver(ast_manager & m, params_ref const & p, bool incremental_mode) { solver* s = mk_inc_sat_solver(m, p, incremental_mode); @@ -36,3 +38,8 @@ solver * mk_fd_solver(ast_manager & m, params_ref const & p, bool incremental_mo tactic * mk_fd_tactic(ast_manager & m, params_ref const& p) { return mk_solver2tactic(mk_fd_solver(m, p, false)); } + +tactic * mk_parallel_qffd_tactic(ast_manager& m, params_ref const& p) { + solver* s = mk_fd_solver(m, p); + return mk_parallel_tactic(s, p); +} diff --git a/src/tactic/portfolio/fd_solver.h b/src/tactic/portfolio/fd_solver.h index 1e107ac20..e1c5b909c 100644 --- a/src/tactic/portfolio/fd_solver.h +++ b/src/tactic/portfolio/fd_solver.h @@ -27,9 +27,11 @@ class tactic; solver * mk_fd_solver(ast_manager & m, params_ref const & p, bool incremental_mode = true); tactic * mk_fd_tactic(ast_manager & m, params_ref const & p); +tactic * mk_parallel_qffd_tactic(ast_manager& m, params_ref const& p); /* ADD_TACTIC("qffd", "builtin strategy for solving QF_FD problems.", "mk_fd_tactic(m, p)") + ADD_TACTIC("pqffd", "builtin strategy for solving QF_FD problems in parallel.", "mk_parallel_qffd_tactic(m, p)") */ #endif diff --git a/src/tactic/portfolio/parallel_tactic.h b/src/tactic/portfolio/parallel_tactic.h deleted file mode 100644 index f3dc36d0e..000000000 --- a/src/tactic/portfolio/parallel_tactic.h +++ /dev/null @@ -1,40 +0,0 @@ -/*++ -Copyright (c) 2017 Microsoft Corporation - -Module Name: - - parallel_tactic.h - -Abstract: - - Parallel tactic in the style of Treengeling. - -Author: - - Nikolaj Bjorner (nbjorner) 2017-10-9 - -Notes: - ---*/ -#ifndef PARALLEL_TACTIC_H_ -#define PARALLEL_TACTIC_H_ - -class solver; -class tactic; -class solver; - -tactic * mk_parallel_tactic(solver* s, params_ref const& p); -tactic * mk_parallel_qffd_tactic(ast_manager& m, params_ref const& p); -tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p); - -// create parallel sat/smt tactics if parallel.enable=true, otherwise return sequential versions. -tactic * mk_psat_tactic(ast_manager& m, params_ref const& p); -tactic * mk_psmt_tactic(ast_manager& m, params_ref const& p, symbol const& logic = symbol::null); -tactic * mk_psmt_tactic_using(ast_manager& m, bool auto_config, params_ref const& p, symbol const& logic = symbol::null); - -/* - ADD_TACTIC("pqffd", "builtin strategy for solving QF_FD problems in parallel.", "mk_parallel_qffd_tactic(m, p)") - ADD_TACTIC("psmt", "builtin strategy for SMT tactic in parallel.", "mk_parallel_smt_tactic(m, p)") -*/ - -#endif diff --git a/src/tactic/smtlogics/CMakeLists.txt b/src/tactic/smtlogics/CMakeLists.txt index 09b145316..2741334b4 100644 --- a/src/tactic/smtlogics/CMakeLists.txt +++ b/src/tactic/smtlogics/CMakeLists.txt @@ -26,7 +26,6 @@ z3_add_component(smtlogic_tactics smt_tactic PYG_FILES qfufbv_tactic_params.pyg - parallel_params.pyg TACTIC_HEADERS nra_tactic.h qfaufbv_tactic.h diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index 68f054640..bc93b4e7b 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -29,8 +29,6 @@ Notes: #include "tactic/aig/aig_tactic.h" #include "sat/tactic/sat_tactic.h" #include "sat/sat_solver/inc_sat_solver.h" -#include "tactic/portfolio/parallel_tactic.h" -#include "tactic/smtlogics/parallel_params.hpp" #include "ackermannization/ackermannize_bv_tactic.h" #define MEMLIMIT 300 diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp index b30103f43..60210259d 100644 --- a/src/tactic/smtlogics/qflia_tactic.cpp +++ b/src/tactic/smtlogics/qflia_tactic.cpp @@ -34,7 +34,6 @@ Notes: #include "sat/tactic/sat_tactic.h" #include "tactic/arith/bound_manager.h" #include "tactic/arith/probe_arith.h" -#include "tactic/portfolio/parallel_tactic.h" struct quasi_pb_probe : public probe { virtual result operator()(goal const & g) { From 0150a4bf3feacf71d06c29f81ab5e2f13987d23a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 16 Apr 2018 10:08:10 -0700 Subject: [PATCH 20/24] add params Signed-off-by: Nikolaj Bjorner --- src/solver/parallel_params.pyg | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 src/solver/parallel_params.pyg diff --git a/src/solver/parallel_params.pyg b/src/solver/parallel_params.pyg new file mode 100644 index 000000000..58c00aa97 --- /dev/null +++ b/src/solver/parallel_params.pyg @@ -0,0 +1,15 @@ +def_module_params('parallel', + description='parameters for parallel solver', + class_name='parallel_params', + export=True, + params=( + ('enable', BOOL, False, 'enable parallel solver by default on selected tactics (for QF_BV)'), + ('threads.max', UINT, 10000, 'caps maximal number of threads below the number of processors'), + ('conquer.batch_size', UINT, 1000, 'number of cubes to batch together for fast conquer'), + ('conquer.restart.max', UINT, 5, 'maximal number of restarts during conquer phase'), + ('conquer.delay', UINT, 10, 'delay of cubes until applying conquer'), + ('conquer.backtrack_frequency', UINT, 10, 'frequency to apply core minimization during conquer'), + ('simplify.exp', DOUBLE, 1, 'restart and inprocess max is multipled by simplify.exp ^ depth'), + ('simplify.restart.max', UINT, 5000, 'maximal number of restarts during simplification phase'), + ('simplify.inprocess.max', UINT, 2, 'maximal number of inprocessing steps during simplification'), + )) From 8ccec28cb9923b9f7dcfc1d56865d50dfe6c75e8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 16 Apr 2018 10:08:55 -0700 Subject: [PATCH 21/24] remove extra file Signed-off-by: Nikolaj Bjorner --- src/solver/parallel_tactic_params.pyg | 15 --------------- 1 file changed, 15 deletions(-) delete mode 100644 src/solver/parallel_tactic_params.pyg diff --git a/src/solver/parallel_tactic_params.pyg b/src/solver/parallel_tactic_params.pyg deleted file mode 100644 index 6d633a6af..000000000 --- a/src/solver/parallel_tactic_params.pyg +++ /dev/null @@ -1,15 +0,0 @@ -def_module_params('parallel', - description='parameters for parallel solver', - class_name='parallel_tactic_params', - export=True, - params=( - ('enable', BOOL, False, 'enable parallel solver by default on selected tactics (for QF_BV)'), - ('threads.max', UINT, 10000, 'caps maximal number of threads below the number of processors'), - ('conquer.batch_size', UINT, 1000, 'number of cubes to batch together for fast conquer'), - ('conquer.restart.max', UINT, 5, 'maximal number of restarts during conquer phase'), - ('conquer.delay', UINT, 10, 'delay of cubes until applying conquer'), - ('conquer.backtrack_frequency', UINT, 10, 'frequency to apply core minimization during conquer'), - ('simplify.exp', DOUBLE, 1, 'restart and inprocess max is multipled by simplify.exp ^ depth'), - ('simplify.restart.max', UINT, 5000, 'maximal number of restarts during simplification phase'), - ('simplify.inprocess.max', UINT, 2, 'maximal number of inprocessing steps during simplification'), - )) From 563f337997a0e684c20eee62e6862dd73e3cd91d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 27 Apr 2018 17:59:03 +0200 Subject: [PATCH 22/24] testing memory defragmentation, prefetch, delay ate Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 1 + src/sat/ba_solver.cpp | 4 +- src/sat/sat_allocator.h | 101 ++++++++++++++++++ src/sat/sat_clause.cpp | 17 ++- src/sat/sat_clause.h | 10 +- src/sat/sat_config.cpp | 3 + src/sat/sat_config.h | 3 + src/sat/sat_drat.cpp | 10 +- src/sat/sat_elim_vars.cpp | 4 +- src/sat/sat_iff3_finder.cpp | 4 +- src/sat/sat_integrity_checker.cpp | 8 +- src/sat/sat_params.pyg | 3 + src/sat/sat_simplifier.cpp | 14 ++- src/sat/sat_solver.cpp | 165 +++++++++++++++++++++++++----- src/sat/sat_solver.h | 27 +++-- src/sat/sat_var_queue.h | 2 + src/util/heap.h | 8 +- 17 files changed, 320 insertions(+), 64 deletions(-) create mode 100644 src/sat/sat_allocator.h diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 7cc0ccb12..0106554fc 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -253,6 +253,7 @@ bool zstring::contains(zstring const& other) const { int zstring::indexof(zstring const& other, int offset) const { SASSERT(offset >= 0); + if (static_cast(offset) <= length() && other.length() == 0) return offset; if (static_cast(offset) == length()) return -1; if (other.length() + offset > length()) return -1; unsigned last = length() - other.length(); diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index 0ead8bb40..9340ac635 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -2245,8 +2245,8 @@ namespace sat { IF_VERBOSE(0, verbose_stream() << "Discrepancy of watched literal: " << l << " id: " << c.id() << " clause: " << c << (found?" is watched, but shouldn't be":" not watched, but should be") << "\n"; - display_watch_list(verbose_stream() << l << ": ", s().m_cls_allocator, get_wlist(l)) << "\n"; - display_watch_list(verbose_stream() << ~l << ": ", s().m_cls_allocator, get_wlist(~l)) << "\n"; + s().display_watch_list(verbose_stream() << l << ": ", get_wlist(l)) << "\n"; + s().display_watch_list(verbose_stream() << ~l << ": ", get_wlist(~l)) << "\n"; verbose_stream() << "value: " << value(l) << " level: " << lvl(l) << "\n"; display(verbose_stream(), c, true); if (c.lit() != null_literal) verbose_stream() << value(c.lit()) << "\n";); diff --git a/src/sat/sat_allocator.h b/src/sat/sat_allocator.h new file mode 100644 index 000000000..1cbef04e0 --- /dev/null +++ b/src/sat/sat_allocator.h @@ -0,0 +1,101 @@ +/*++ +Copyright (c) 2018 Microsoft Corporation + +Module Name: + + sat_allocator.h + +Abstract: + + Small object allocator suitable for clauses + +Author: + + Nikolaj bjorner (nbjorner) 2018-04-26. + +Revision History: +--*/ + +#ifndef SAT_ALLOCATOR_H_ +#define SAT_ALLOCATOR_H_ + +#include "util/vector.h" +#include "util/machine.h" + +class sat_allocator { + static const unsigned CHUNK_SIZE = (1 << 16); + static const unsigned SMALL_OBJ_SIZE = 512; + static const unsigned MASK = ((1 << PTR_ALIGNMENT) - 1); + static const unsigned NUM_FREE = 1 + (SMALL_OBJ_SIZE >> PTR_ALIGNMENT); + struct chunk { + char * m_curr; + char m_data[CHUNK_SIZE]; + chunk():m_curr(m_data) {} + }; + ptr_vector m_chunks; + void * m_chunk_ptr; + ptr_vector m_free[NUM_FREE]; + size_t m_alloc_size; + char const * m_id; + + unsigned align_size(size_t sz) const { + return free_slot_id(sz) << PTR_ALIGNMENT; + } + unsigned free_slot_id(size_t size) const { + return (static_cast(size >> PTR_ALIGNMENT) + ((0 != (size & MASK)) ? 1u : 0u)); + } +public: + sat_allocator(char const * id = "unknown"): m_id(id), m_alloc_size(0), m_chunk_ptr(nullptr) {} + ~sat_allocator() { reset(); } + void reset() { + for (chunk * ch : m_chunks) dealloc(ch); + m_chunks.reset(); + for (unsigned i = 0; i < NUM_FREE; ++i) m_free[i].reset(); + m_alloc_size = 0; + m_chunk_ptr = nullptr; + } + void * allocate(size_t size) { + m_alloc_size += size; + if (size >= SMALL_OBJ_SIZE) { + return memory::allocate(size); + } + unsigned slot_id = free_slot_id(size); + if (!m_free[slot_id].empty()) { + void* result = m_free[slot_id].back(); + m_free[slot_id].pop_back(); + return result; + } + if (m_chunks.empty()) { + m_chunks.push_back(alloc(chunk)); + m_chunk_ptr = m_chunks.back(); + } + + unsigned sz = align_size(size); + if ((char*)m_chunk_ptr + sz > (char*)m_chunks.back() + CHUNK_SIZE) { + m_chunks.push_back(alloc(chunk)); + m_chunk_ptr = m_chunks.back(); + } + void * result = m_chunk_ptr; + m_chunk_ptr = (char*)m_chunk_ptr + sz; + return result; + } + + void deallocate(size_t size, void * p) { + m_alloc_size -= size; + if (size >= SMALL_OBJ_SIZE) { + memory::deallocate(p); + } + else { + m_free[free_slot_id(size)].push_back(p); + } + } + size_t get_allocation_size() const { return m_alloc_size; } +}; + +inline void * operator new(size_t s, sat_allocator & r) { return r.allocate(s); } +inline void * operator new[](size_t s, sat_allocator & r) { return r.allocate(s); } +inline void operator delete(void * p, sat_allocator & r) { UNREACHABLE(); } +inline void operator delete[](void * p, sat_allocator & r) { UNREACHABLE(); } + +#endif /* SAT_ALLOCATOR_H_ */ + diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp index f433f884d..f9caffe94 100644 --- a/src/sat/sat_clause.cpp +++ b/src/sat/sat_clause.cpp @@ -135,12 +135,15 @@ namespace sat { m_allocator("clause-allocator") { } + void clause_allocator::finalize() { + m_allocator.reset(); + } + clause * clause_allocator::get_clause(clause_offset cls_off) const { SASSERT(cls_off == reinterpret_cast(reinterpret_cast(cls_off))); return reinterpret_cast(cls_off); } - clause_offset clause_allocator::get_offset(clause const * cls) const { SASSERT(cls == reinterpret_cast(reinterpret_cast(cls))); return reinterpret_cast(cls); @@ -155,6 +158,18 @@ namespace sat { return cls; } + clause * clause_allocator::copy_clause(clause const& other) { + size_t size = clause::get_obj_size(other.size()); + void * mem = m_allocator.allocate(size); + clause * cls = new (mem) clause(m_id_gen.mk(), other.size(), other.m_lits, other.is_learned()); + cls->m_reinit_stack = other.on_reinit_stack(); + cls->m_glue = other.glue(); + cls->m_psm = other.psm(); + cls->m_frozen = other.frozen(); + cls->m_approx = other.approx(); + return cls; + } + void clause_allocator::del_clause(clause * cls) { TRACE("sat_clause", tout << "delete: " << cls->id() << " " << *cls << "\n";); m_id_gen.recycle(cls->id()); diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h index c7273f57d..c42427afb 100644 --- a/src/sat/sat_clause.h +++ b/src/sat/sat_clause.h @@ -19,10 +19,11 @@ Revision History: #ifndef SAT_CLAUSE_H_ #define SAT_CLAUSE_H_ -#include "sat/sat_types.h" #include "util/small_object_allocator.h" #include "util/id_gen.h" #include "util/map.h" +#include "sat/sat_types.h" +#include "sat/sat_allocator.h" #ifdef _MSC_VER #pragma warning(disable : 4200) @@ -133,13 +134,16 @@ namespace sat { \brief Simple clause allocator that allows uint (32bit integers) to be used to reference clauses (even in 64bit machines). */ class clause_allocator { - small_object_allocator m_allocator; - id_gen m_id_gen; + small_object_allocator m_allocator; + id_gen m_id_gen; public: clause_allocator(); + void finalize(); + size_t get_allocation_size() const { return m_allocator.get_allocation_size(); } clause * get_clause(clause_offset cls_off) const; clause_offset get_offset(clause const * ptr) const; clause * mk_clause(unsigned num_lits, literal const * lits, bool learned); + clause * copy_clause(clause const& other); void del_clause(clause * cls); }; diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 2597967df..f7e2e2404 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -41,6 +41,7 @@ namespace sat { else throw sat_param_exception("invalid restart strategy"); + m_restart_fast = p.restart_fast(); s = p.phase(); if (s == symbol("always_false")) m_phase = PS_ALWAYS_FALSE; @@ -60,6 +61,7 @@ namespace sat { m_restart_initial = p.restart_initial(); m_restart_factor = p.restart_factor(); m_restart_max = p.restart_max(); + m_propagate_prefetch = p.propagate_prefetch(); m_inprocess_max = p.inprocess_max(); m_random_freq = p.random_freq(); @@ -139,6 +141,7 @@ namespace sat { m_gc_small_lbd = p.gc_small_lbd(); m_gc_k = std::min(255u, p.gc_k()); m_gc_burst = p.gc_burst(); + m_gc_defrag = p.gc_defrag(); m_minimize_lemmas = p.minimize_lemmas(); m_core_minimize = p.core_minimize(); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 20d966dd1..f04973d13 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -85,7 +85,9 @@ namespace sat { unsigned m_phase_caching_on; unsigned m_phase_caching_off; bool m_phase_sticky; + bool m_propagate_prefetch; restart_strategy m_restart; + bool m_restart_fast; unsigned m_restart_initial; double m_restart_factor; // for geometric case unsigned m_restart_max; @@ -126,6 +128,7 @@ namespace sat { unsigned m_gc_small_lbd; unsigned m_gc_k; bool m_gc_burst; + bool m_gc_defrag; bool m_minimize_lemmas; diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index fd2b6fa79..00a3fa076 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -42,7 +42,7 @@ namespace sat { for (unsigned i = 0; i < m_proof.size(); ++i) { clause* c = m_proof[i]; if (c && (c->size() == 2 || m_status[i] == status::deleted || m_status[i] == status::external)) { - s.m_cls_allocator.del_clause(c); + s.dealloc_clause(c); } } } @@ -118,7 +118,7 @@ namespace sat { if (st == status::learned) { verify(2, lits); } - clause* c = s.m_cls_allocator.mk_clause(2, lits, st == status::learned); + clause* c = s.alloc_clause(2, lits, st == status::learned); m_proof.push_back(c); m_status.push_back(st); unsigned idx = m_watched_clauses.size(); @@ -452,7 +452,7 @@ namespace sat { case 0: add(); break; case 1: append(lits[0], status::external); break; default: { - clause* c = s.m_cls_allocator.mk_clause(lits.size(), lits.c_ptr(), true); + clause* c = s.alloc_clause(lits.size(), lits.c_ptr(), true); append(*c, status::external); break; } @@ -468,7 +468,7 @@ namespace sat { case 1: append(c[0], status::learned); break; default: { verify(c.size(), c.begin()); - clause* cl = s.m_cls_allocator.mk_clause(c.size(), c.c_ptr(), true); + clause* cl = s.alloc_clause(c.size(), c.c_ptr(), true); append(*cl, status::external); break; } @@ -490,7 +490,7 @@ namespace sat { TRACE("sat", tout << "del: " << c << "\n";); if (m_out) dump(c.size(), c.begin(), status::deleted); if (m_check) { - clause* c1 = s.m_cls_allocator.mk_clause(c.size(), c.begin(), c.is_learned()); + clause* c1 = s.alloc_clause(c.size(), c.begin(), c.is_learned()); append(*c1, status::deleted); } } diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp index a80807450..299fbace1 100644 --- a/src/sat/sat_elim_vars.cpp +++ b/src/sat/sat_elim_vars.cpp @@ -185,7 +185,7 @@ namespace sat{ s.m_stats.m_mk_ter_clause++; else s.m_stats.m_mk_clause++; - clause* cp = s.m_cls_allocator.mk_clause(c.size(), c.c_ptr(), false); + clause* cp = s.alloc_clause(c.size(), c.c_ptr(), false); s.m_clauses.push_back(cp); simp.m_use_list.insert(*cp); if (simp.m_sub_counter > 0) @@ -214,7 +214,7 @@ namespace sat{ } if (b.is_false()) { if (lits.size() > 1) { - clause* c = s.m_cls_allocator.mk_clause(lits.size(), lits.c_ptr(), false); + clause* c = s.alloc_clause(lits.size(), lits.c_ptr(), false); clauses.push_back(c); } else { diff --git a/src/sat/sat_iff3_finder.cpp b/src/sat/sat_iff3_finder.cpp index af7a6f438..32bf70414 100644 --- a/src/sat/sat_iff3_finder.cpp +++ b/src/sat/sat_iff3_finder.cpp @@ -136,9 +136,9 @@ namespace sat { TRACE("iff3_finder", tout << "visiting: " << x << "\n"; tout << "pos:\n"; - display_watch_list(tout, s.m_cls_allocator, pos_wlist); + s.display_watch_list(tout, pos_wlist); tout << "\nneg:\n"; - display_watch_list(tout, s.m_cls_allocator, neg_wlist); + s.display_watch_list(tout, neg_wlist); tout << "\n--------------\n";); // traverse the ternary clauses x \/ l1 \/ l2 bool_var curr_v1 = null_bool_var; diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp index 7f56e2b36..32feaa2c7 100644 --- a/src/sat/sat_integrity_checker.cpp +++ b/src/sat/sat_integrity_checker.cpp @@ -66,7 +66,7 @@ namespace sat { if (c.size() == 3) { CTRACE("sat_ter_watch_bug", !contains_watched(s.get_wlist(~c[0]), c[1], c[2]), tout << c << "\n"; tout << "watch_list:\n"; - sat::display_watch_list(tout, s.m_cls_allocator, s.get_wlist(~c[0])); + s.display_watch_list(tout, s.get_wlist(~c[0])); tout << "\n";); VERIFY(contains_watched(s.get_wlist(~c[0]), c[1], c[2])); VERIFY(contains_watched(s.get_wlist(~c[1]), c[0], c[2])); @@ -164,9 +164,9 @@ namespace sat { tout << "was_eliminated1: " << s.was_eliminated(l.var()); tout << " was_eliminated2: " << s.was_eliminated(w.get_literal().var()); tout << " learned: " << w.is_learned() << "\n"; - sat::display_watch_list(tout, s.m_cls_allocator, wlist); + s.display_watch_list(tout, wlist); tout << "\n"; - sat::display_watch_list(tout, s.m_cls_allocator, s.get_wlist(~(w.get_literal()))); + s.display_watch_list(tout, s.get_wlist(~(w.get_literal()))); tout << "\n";); VERIFY(find_binary_watch(s.get_wlist(~(w.get_literal())), l)); break; @@ -176,7 +176,7 @@ namespace sat { VERIFY(w.get_literal1().index() < w.get_literal2().index()); break; case watched::CLAUSE: - VERIFY(!s.m_cls_allocator.get_clause(w.get_clause_offset())->was_removed()); + VERIFY(!s.get_clause(w.get_clause_offset()).was_removed()); break; default: break; diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 320ddaf9e..cf6ecc4f5 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -6,9 +6,11 @@ def_module_params('sat', ('phase.caching.on', UINT, 400, 'phase caching on period (in number of conflicts)'), ('phase.caching.off', UINT, 100, 'phase caching off period (in number of conflicts)'), ('phase.sticky', BOOL, False, 'use sticky phase caching for local search'), + ('propagate.prefetch', BOOL, True, 'prefetch watch lists for assigned literals'), ('restart', SYMBOL, 'luby', 'restart strategy: luby or geometric'), ('restart.initial', UINT, 100, 'initial restart (number of conflicts)'), ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'), + ('restart.fast', BOOL, False, 'use fast restart strategy.'), ('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'), ('variable_decay', UINT, 120, 'multiplier (divided by 100) for the VSIDS activity increement'), ('inprocess.max', UINT, UINT_MAX, 'maximal number of inprocessing passes'), @@ -24,6 +26,7 @@ def_module_params('sat', ('gc.small_lbd', UINT, 3, 'learned clauses with small LBD are never deleted (only used in dyn_psm)'), ('gc.k', UINT, 7, 'learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm)'), ('gc.burst', BOOL, True, 'perform eager garbage collection during initialization'), + ('gc.defrag', BOOL, True, 'defragment clauses when garbage collecting'), ('simplify.delay', UINT, 0, 'set initial delay of simplification by a conflict count'), ('minimize_lemmas', BOOL, True, 'minimize learned clauses'), ('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'), diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 9c57c79ed..314b661ea 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -100,7 +100,7 @@ namespace sat { !m_learned_in_use_lists && m_num_calls >= m_bce_delay && single_threaded(); } - bool simplifier::ate_enabled() const { return m_ate; } + bool simplifier::ate_enabled() const { return m_num_calls >= m_bce_delay && m_ate; } bool simplifier::bce_enabled() const { return bce_enabled_base() && (m_bce || m_bce_at == m_num_calls || m_acce || m_abce || m_cce); } bool simplifier::acce_enabled() const { return bce_enabled_base() && m_acce; } bool simplifier::cce_enabled() const { return bce_enabled_base() && (m_cce || m_acce); } @@ -1581,8 +1581,8 @@ namespace sat { IF_VERBOSE(0, verbose_stream() << "blocked: " << l << " @ " << c << " :covered " << m_covered_clause << "\n"; s.m_use_list.display(verbose_stream() << "use " << l << ":", l); s.m_use_list.display(verbose_stream() << "use " << ~l << ":", ~l); - display_watch_list(verbose_stream() << ~l << ": ", s.s.m_cls_allocator, s.get_wlist(l)) << "\n"; - display_watch_list(verbose_stream() << l << ": ", s.s.m_cls_allocator, s.get_wlist(~l)) << "\n"; + s.s.display_watch_list(verbose_stream() << ~l << ": ", s.get_wlist(l)) << "\n"; + s.s.display_watch_list(verbose_stream() << l << ": ", s.get_wlist(~l)) << "\n"; ); } @@ -1999,8 +1999,8 @@ namespace sat { literal l(v, false); IF_VERBOSE(0, verbose_stream() << "elim: " << l << "\n"; - display_watch_list(verbose_stream() << ~l << ": ", s.m_cls_allocator, get_wlist(l)) << "\n"; - display_watch_list(verbose_stream() << l << ": ", s.m_cls_allocator, get_wlist(~l)) << "\n";); + s.display_watch_list(verbose_stream() << ~l << ": ", get_wlist(l)) << "\n"; + s.display_watch_list(verbose_stream() << l << ": ", get_wlist(~l)) << "\n";); } // eliminate variable ++s.m_stats.m_elim_var_res; @@ -2018,8 +2018,6 @@ namespace sat { m_elim_counter -= num_pos * num_neg + before_lits; - - for (auto & c1 : m_pos_cls) { for (auto & c2 : m_neg_cls) { m_new_cls.reset(); @@ -2046,7 +2044,7 @@ namespace sat { s.m_stats.m_mk_ter_clause++; else s.m_stats.m_mk_clause++; - clause * new_c = s.m_cls_allocator.mk_clause(m_new_cls.size(), m_new_cls.c_ptr(), false); + clause * new_c = s.alloc_clause(m_new_cls.size(), m_new_cls.c_ptr(), false); if (s.m_config.m_drat) s.m_drat.add(*new_c, true); s.m_clauses.push_back(new_c); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index fb992d57e..792883977 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -36,7 +36,8 @@ namespace sat { m_rlimit(l), m_checkpoint_enabled(true), m_config(p), - m_par(0), + m_par(nullptr), + m_cls_allocator_idx(false), m_par_syncing_clauses(false), m_par_id(0), m_cleaner(*this), @@ -78,7 +79,7 @@ namespace sat { void solver::del_clauses(clause_vector& clauses) { for (clause * cp : clauses) - m_cls_allocator.del_clause(cp); + dealloc_clause(cp); clauses.reset(); ++m_stats.m_non_learned_generation; } @@ -298,7 +299,7 @@ namespace sat { if (m_config.m_drat && !m_drat.is_cleaned(c)) { m_drat.del(c); } - m_cls_allocator.del_clause(&c); + dealloc_clause(&c); m_stats.m_del_clause++; } @@ -396,7 +397,7 @@ namespace sat { clause * solver::mk_ter_clause(literal * lits, bool learned) { m_stats.m_mk_ter_clause++; - clause * r = m_cls_allocator.mk_clause(3, lits, learned); + clause * r = alloc_clause(3, lits, learned); bool reinit = attach_ter_clause(*r); if (reinit && !learned) push_reinit_stack(*r); if (m_config.m_drat) m_drat.add(*r, learned); @@ -435,7 +436,7 @@ namespace sat { clause * solver::mk_nary_clause(unsigned num_lits, literal * lits, bool learned) { m_stats.m_mk_clause++; - clause * r = m_cls_allocator.mk_clause(num_lits, lits, learned); + clause * r = alloc_clause(num_lits, lits, learned); SASSERT(!learned || r->is_learned()); bool reinit = attach_nary_clause(*r); if (reinit && !learned) push_reinit_stack(*r); @@ -452,7 +453,7 @@ namespace sat { bool solver::attach_nary_clause(clause & c) { bool reinit = false; - clause_offset cls_off = m_cls_allocator.get_offset(&c); + clause_offset cls_off = cls_allocator().get_offset(&c); if (!at_base_lvl()) { if (c.is_learned()) { unsigned w2_idx = select_learned_watch_lit(c); @@ -511,6 +512,85 @@ namespace sat { } } + bool solver::memory_pressure() { + return 3*cls_allocator().get_allocation_size()/2 + memory::get_allocation_size() > memory::get_max_memory_size(); + } + + struct solver::cmp_activity { + solver& s; + cmp_activity(solver& s):s(s) {} + bool operator()(bool_var v1, bool_var v2) const { + return s.m_activity[v1] > s.m_activity[v2]; + } + }; + + void solver::defrag_clauses() { + if (memory_pressure()) return; + IF_VERBOSE(1, verbose_stream() << "(sat-defrag)\n"); + clause_allocator& alloc = m_cls_allocator[!m_cls_allocator_idx]; + ptr_vector new_clauses, new_learned; + ptr_addr_map cls2offset; + for (clause* c : m_clauses) c->unmark_used(); + for (clause* c : m_learned) c->unmark_used(); + + svector vars; + for (unsigned i = 0; i < num_vars(); ++i) vars.push_back(i); + std::stable_sort(vars.begin(), vars.end(), cmp_activity(*this)); + literal_vector lits; + for (bool_var v : vars) lits.push_back(to_literal(v)), lits.push_back(~to_literal(v)); + + // walk clauses, reallocate them in an order that defragments memory and creates locality. + //for (literal lit : lits) { + //watch_list& wlist = m_watches[lit.index()]; + for (watch_list& wlist : m_watches) { + for (watched& w : wlist) { + if (w.is_clause()) { + clause& c1 = get_clause(w); + clause_offset offset; + if (c1.was_used()) { + offset = cls2offset[&c1]; + } + else { + clause* c2 = alloc.copy_clause(c1); + c1.mark_used(); + if (c1.is_learned()) { + new_learned.push_back(c2); + } + else { + new_clauses.push_back(c2); + } + offset = get_offset(*c2); + cls2offset.insert(&c1, offset); + } + w = watched(w.get_blocked_literal(), offset); + } + } + } + + // reallocate ternary clauses. + for (clause* c : m_clauses) { + if (!c->was_used()) { + SASSERT(c->size() == 3); + new_clauses.push_back(alloc.copy_clause(*c)); + } + dealloc_clause(c); + } + + for (clause* c : m_learned) { + if (!c->was_used()) { + SASSERT(c->size() == 3); + new_learned.push_back(alloc.copy_clause(*c)); + } + dealloc_clause(c); + } + m_clauses.swap(new_clauses); + m_learned.swap(new_learned); + + cls_allocator().finalize(); + m_cls_allocator_idx = !m_cls_allocator_idx; + } + + void solver::set_learned(literal l1, literal l2, bool learned) { set_learned1(l1, l2, learned); set_learned1(l2, l1, learned); @@ -702,6 +782,7 @@ namespace sat { m_reasoned[v] = 0; break; } + if (m_config.m_anti_exploration) { uint64 age = m_stats.m_conflict - m_canceled[v]; if (age > 0) { @@ -712,7 +793,10 @@ namespace sat { m_case_split_queue.activity_changed_eh(v, false); } } - + + if (m_config.m_propagate_prefetch) { + _mm_prefetch((char const*)(m_watches.c_ptr() + l.index()), 0); + } SASSERT(!l.sign() || m_phase[v] == NEG_PHASE); SASSERT(l.sign() || m_phase[v] == POS_PHASE); @@ -725,9 +809,8 @@ namespace sat { lbool solver::status(clause const & c) const { bool found_undef = false; - unsigned sz = c.size(); - for (unsigned i = 0; i < sz; i++) { - switch (value(c[i])) { + for (literal lit : c) { + switch (value(lit)) { case l_true: return l_true; case l_undef: @@ -1006,7 +1089,7 @@ namespace sat { return l_undef; } - restart(); + restart(!m_config.m_restart_fast); simplify_problem(); if (check_inconsistent()) return l_false; gc(); @@ -1507,6 +1590,7 @@ namespace sat { m_min_d_tk = 1.0; m_search_lvl = 0; m_conflicts_since_gc = 0; + m_restart_next_out = 0; m_asymm_branch.init_search(); m_stopwatch.reset(); m_stopwatch.start(); @@ -1752,15 +1836,34 @@ namespace sat { return ok; } - void solver::restart() { + void solver::restart(bool to_base) { m_stats.m_restart++; m_restarts++; - IF_VERBOSE(1, - verbose_stream() << "(sat-restart :conflicts " << m_stats.m_conflict << " :decisions " << m_stats.m_decision - << " :restarts " << m_stats.m_restart << mk_stat(*this) - << " :time " << std::fixed << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";); + if (m_conflicts_since_init > m_restart_next_out + 500) { + m_restart_next_out = m_conflicts_since_init; + IF_VERBOSE(1, + verbose_stream() << "(sat-restart :conflicts " << m_stats.m_conflict << " :decisions " << m_stats.m_decision + << " :restarts " << m_stats.m_restart << mk_stat(*this) + << " :time " << std::fixed << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";); + } IF_VERBOSE(30, display_status(verbose_stream());); - pop_reinit(scope_lvl() - search_lvl()); + unsigned num_scopes = 0; + if (to_base || scope_lvl() == search_lvl()) { + num_scopes = scope_lvl() - search_lvl(); + } + else { + bool_var next = m_case_split_queue.min_var(); + do { + scope& s = m_scopes[scope_lvl() - num_scopes - 1]; + bool_var prev = m_trail[s.m_trail_lim].var(); + //IF_VERBOSE(0, verbose_stream() << "more active: " << m_case_split_queue.more_active(next, prev) << "\n"); + if (!m_case_split_queue.more_active(next, prev)) break; + ++num_scopes; + } + while (num_scopes < scope_lvl() - search_lvl()); + //IF_VERBOSE(0, verbose_stream() << "backtrack " << num_scopes << " " << scope_lvl() - search_lvl() << "\n"); + } + pop_reinit(num_scopes); m_conflicts_since_restart = 0; switch (m_config.m_restart) { case RS_GEOMETRIC: @@ -1788,6 +1891,7 @@ namespace sat { return; if (m_config.m_gc_strategy == GC_DYN_PSM && !at_base_lvl()) return; + unsigned gc = m_stats.m_gc_clause; IF_VERBOSE(10, verbose_stream() << "(sat.gc)\n";); CASSERT("sat_gc_bug", check_invariant()); switch (m_config.m_gc_strategy) { @@ -1813,6 +1917,11 @@ namespace sat { break; } if (m_ext) m_ext->gc(); + if (gc > 0 && m_config.m_gc_defrag && !memory_pressure()) { + pop(scope_lvl()); + defrag_clauses(); + reinit_assumptions(); + } m_conflicts_since_gc = 0; m_gc_threshold += m_config.m_gc_increment; CASSERT("sat_gc_bug", check_invariant()); @@ -2320,8 +2429,7 @@ namespace sat { void solver::resolve_conflict_for_unsat_core() { TRACE("sat", display(tout); unsigned level = 0; - for (unsigned i = 0; i < m_trail.size(); ++i) { - literal l = m_trail[i]; + for (literal l : m_trail) { if (level != m_level[l.var()]) { level = m_level[l.var()]; tout << level << ": "; @@ -2341,8 +2449,8 @@ namespace sat { } SASSERT(m_unmark.empty()); DEBUG_CODE({ - for (unsigned i = 0; i < m_trail.size(); ++i) { - SASSERT(!is_marked(m_trail[i].var())); + for (literal lit : m_trail) { + SASSERT(!is_marked(lit.var())); }}); unsigned old_size = m_unmark.size(); @@ -2798,8 +2906,7 @@ namespace sat { } } reset_mark(m_lemma[0].var()); - for (unsigned i = m_lemma.size(); i > sz; ) { - --i; + for (unsigned i = m_lemma.size(); i-- > sz; ) { reset_mark(m_lemma[i].var()); } m_lemma.shrink(sz); @@ -3431,7 +3538,7 @@ namespace sat { } void solver::display_watches(std::ostream & out, literal lit) const { - sat::display_watch_list(out << lit << ": ", m_cls_allocator, get_wlist(lit)) << "\n"; + display_watch_list(out << lit << ": ", get_wlist(lit)) << "\n"; } void solver::display_watches(std::ostream & out) const { @@ -3439,10 +3546,14 @@ namespace sat { for (watch_list const& wlist : m_watches) { literal l = to_literal(l_idx++); if (!wlist.empty()) - sat::display_watch_list(out << l << ": ", m_cls_allocator, wlist) << "\n"; + display_watch_list(out << l << ": ", wlist) << "\n"; } } + std::ostream& solver::display_watch_list(std::ostream& out, watch_list const& wl) const { + return sat::display_watch_list(out, cls_allocator(), wl); + } + void solver::display_assignment(std::ostream & out) const { out << m_trail << "\n"; } @@ -3774,7 +3885,7 @@ namespace sat { return l_undef; } - restart(); + restart(true); simplify_problem(); if (check_inconsistent()) { fixup_consequence_core(); @@ -3867,7 +3978,7 @@ namespace sat { else { is_sat = bounded_search(); if (is_sat == l_undef) { - restart(); + restart(true); } extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq); } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 1bf78ab8c..606907f54 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -86,7 +86,8 @@ namespace sat { scoped_ptr m_ext; parallel* m_par; random_gen m_rand; - clause_allocator m_cls_allocator; + clause_allocator m_cls_allocator[2]; + bool m_cls_allocator_idx; cleaner m_cleaner; model m_model; model_converter m_mc; @@ -217,9 +218,16 @@ namespace sat { void mk_clause(literal_vector const& lits, bool learned = false) { mk_clause(lits.size(), lits.c_ptr(), learned); } void mk_clause(unsigned num_lits, literal * lits, bool learned = false); void mk_clause(literal l1, literal l2, bool learned = false); - void mk_clause(literal l1, literal l2, literal l3, bool learned = false); + void mk_clause(literal l1, literal l2, literal l3, bool learned = false); protected: + inline clause_allocator& cls_allocator() { return m_cls_allocator[m_cls_allocator_idx]; } + inline clause_allocator const& cls_allocator() const { return m_cls_allocator[m_cls_allocator_idx]; } + inline clause * alloc_clause(unsigned num_lits, literal const * lits, bool learned) { return cls_allocator().mk_clause(num_lits, lits, learned); } + inline void dealloc_clause(clause* c) { cls_allocator().del_clause(c); } + struct cmp_activity; + void defrag_clauses(); + bool memory_pressure(); void del_clause(clause & c); clause * mk_clause_core(unsigned num_lits, literal * lits, bool learned); clause * mk_clause_core(literal_vector const& lits) { return mk_clause_core(lits.size(), lits.c_ptr()); } @@ -301,7 +309,7 @@ namespace sat { void set_conflict(justification c, literal not_l); void set_conflict(justification c) { set_conflict(c, null_literal); } lbool status(clause const & c) const; - clause_offset get_offset(clause const & c) const { return m_cls_allocator.get_offset(&c); } + clause_offset get_offset(clause const & c) const { return cls_allocator().get_offset(&c); } void checkpoint() { if (!m_checkpoint_enabled) return; if (!m_rlimit.inc()) { @@ -373,6 +381,7 @@ namespace sat { unsigned m_conflicts_since_init; unsigned m_restarts; + unsigned m_restart_next_out; unsigned m_conflicts_since_restart; unsigned m_simplifications; unsigned m_restart_threshold; @@ -405,7 +414,7 @@ namespace sat { void simplify_problem(); void mk_model(); bool check_model(model const & m) const; - void restart(); + void restart(bool to_base); void sort_watch_lits(); void exchange_par(); lbool check_par(unsigned num_lits, literal const* lits); @@ -437,7 +446,7 @@ namespace sat { if (value(l0) != l_true) return true; justification const & jst = m_justification[l0.var()]; - return !jst.is_clause() || m_cls_allocator.get_clause(jst.get_clause_offset()) != &c; + return !jst.is_clause() || cls_allocator().get_clause(jst.get_clause_offset()) != &c; } clause& get_clause(watch_list::iterator it) const { @@ -445,13 +454,18 @@ namespace sat { return get_clause(it->get_clause_offset()); } + clause& get_clause(watched const& w) const { + SASSERT(w.get_kind() == watched::CLAUSE); + return get_clause(w.get_clause_offset()); + } + clause& get_clause(justification const& j) const { SASSERT(j.is_clause()); return get_clause(j.get_clause_offset()); } clause& get_clause(clause_offset cls_off) const { - return *(m_cls_allocator.get_clause(cls_off)); + return *(cls_allocator().get_clause(cls_off)); } // ----------------------- @@ -634,6 +648,7 @@ namespace sat { void display_wcnf(std::ostream & out, unsigned sz, literal const* lits, unsigned const* weights) const; void display_assignment(std::ostream & out) const; std::ostream& display_justification(std::ostream & out, justification const& j) const; + std::ostream& display_watch_list(std::ostream& out, watch_list const& wl) const; protected: void display_binary(std::ostream & out) const; diff --git a/src/sat/sat_var_queue.h b/src/sat/sat_var_queue.h index 656e4b071..0c22766ba 100644 --- a/src/sat/sat_var_queue.h +++ b/src/sat/sat_var_queue.h @@ -72,6 +72,8 @@ namespace sat { bool_var next_var() { SASSERT(!empty()); return m_queue.erase_min(); } bool_var min_var() { SASSERT(!empty()); return m_queue.min_value(); } + + bool more_active(bool_var v1, bool_var v2) const { return m_queue.less_than(v1, v2); } }; }; diff --git a/src/util/heap.h b/src/util/heap.h index 02e30bf04..182932fd0 100644 --- a/src/util/heap.h +++ b/src/util/heap.h @@ -27,10 +27,6 @@ class heap : private LT { int_vector m_values; int_vector m_value2indices; - bool less_than(int v1, int v2) const { - return LT::operator()(v1, v2); - } - static int left(int i) { return i << 1; } @@ -126,6 +122,10 @@ public: CASSERT("heap", check_invariant()); } + bool less_than(int v1, int v2) const { + return LT::operator()(v1, v2); + } + bool empty() const { return m_values.size() == 1; } From 2f025f52c0452d299afdc6925b6ea352ec01337c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 28 Apr 2018 22:26:01 +0200 Subject: [PATCH 23/24] fix local search initialization of units, encode offset in clauses Signed-off-by: Nikolaj Bjorner --- src/sat/sat_clause.cpp | 18 +++++++++++++++++- src/sat/sat_clause.h | 2 ++ src/sat/sat_local_search.cpp | 27 +++++++++++++++++---------- src/sat/sat_solver.cpp | 8 ++++---- src/solver/parallel_params.pyg | 2 +- src/solver/parallel_tactic.cpp | 8 ++++++-- 6 files changed, 47 insertions(+), 18 deletions(-) diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp index f9caffe94..78d62bac0 100644 --- a/src/sat/sat_clause.cpp +++ b/src/sat/sat_clause.cpp @@ -95,7 +95,6 @@ namespace sat { } } - bool clause::satisfied_by(model const & m) const { for (literal l : *this) { if (l.sign()) { @@ -110,6 +109,23 @@ namespace sat { return false; } + clause_offset clause::get_new_offset() const { + unsigned o1 = m_lits[0].index(); + if (sizeof(clause_offset) == 8) { + unsigned o2 = m_lits[1].index(); + return (clause_offset)o1 + (((clause_offset)o2) << 32); + } + return (clause_offset)o1; + } + + void clause::set_new_offset(clause_offset offset) { + m_lits[0] = to_literal(static_cast(offset)); + if (sizeof(offset) == 8) { + m_lits[1] = to_literal(static_cast(offset >> 32)); + } + } + + void tmp_clause::set(unsigned num_lits, literal const * lits, bool learned) { if (m_clause && m_clause->m_capacity < num_lits) { dealloc_svect(m_clause); diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h index c42427afb..8b2d113c8 100644 --- a/src/sat/sat_clause.h +++ b/src/sat/sat_clause.h @@ -98,6 +98,8 @@ namespace sat { unsigned glue() const { return m_glue; } void set_psm(unsigned psm) { m_psm = psm > 255 ? 255 : psm; } unsigned psm() const { return m_psm; } + clause_offset get_new_offset() const; + void set_new_offset(clause_offset off); bool on_reinit_stack() const { return m_reinit_stack; } void set_reinit_stack(bool f) { m_reinit_stack = f; } diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index 35e371a9c..e02560e5f 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -79,11 +79,13 @@ namespace sat { void local_search::init_cur_solution() { for (var_info& vi : m_vars) { // use bias with a small probability - if (m_rand() % 10 < 5 || m_config.phase_sticky()) { - vi.m_value = ((unsigned)(m_rand() % 100) < vi.m_bias); - } - else { - vi.m_value = (m_rand() % 2) == 0; + if (!vi.m_unit) { + if (m_rand() % 10 < 5 || m_config.phase_sticky()) { + vi.m_value = ((unsigned)(m_rand() % 100) < vi.m_bias); + } + else { + vi.m_value = (m_rand() % 2) == 0; + } } } } @@ -149,7 +151,7 @@ namespace sat { void local_search::reinit() { - IF_VERBOSE(0, verbose_stream() << "(sat-local-search reinit)\n";); + IF_VERBOSE(1, verbose_stream() << "(sat-local-search reinit)\n";); if (true || !m_is_pb) { // // the following methods does NOT converge for pseudo-boolean @@ -216,13 +218,15 @@ namespace sat { for (unsigned i = 0; i < m_prop_queue.size() && i < m_vars.size(); ++i) { literal lit2 = m_prop_queue[i]; if (!is_true(lit2)) { - if (is_unit(lit2)) return false; + if (is_unit(lit2)) { + return false; + } flip_walksat(lit2.var()); add_propagation(lit2); } } if (m_prop_queue.size() >= m_vars.size()) { - IF_VERBOSE(0, verbose_stream() << "failed literal\n"); + IF_VERBOSE(0, verbose_stream() << "propagation loop\n"); return false; } if (unit) { @@ -328,6 +332,7 @@ namespace sat { return; } if (k == 1 && sz == 2) { + // IF_VERBOSE(0, verbose_stream() << "bin: " << ~c[0] << " + " << ~c[1] << " <= 1\n"); for (unsigned i = 0; i < 2; ++i) { literal t(c[i]), s(c[1-i]); m_vars.reserve(t.var() + 1); @@ -750,11 +755,12 @@ namespace sat { IF_VERBOSE(1, verbose_stream() << "(sat.local_search :unsat)\n"); return; } - + if (is_unit(best_var)) { + goto reflip; + } flip_walksat(best_var); literal lit(best_var, !cur_solution(best_var)); if (!propagate(lit)) { - IF_VERBOSE(0, verbose_stream() << "failed literal " << lit << "\n"); if (is_true(lit)) { flip_walksat(best_var); } @@ -774,6 +780,7 @@ namespace sat { } void local_search::flip_walksat(bool_var flipvar) { + VERIFY(!is_unit(flipvar)); m_vars[flipvar].m_value = !cur_solution(flipvar); bool flip_is_true = cur_solution(flipvar); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 792883977..90ac876d2 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -529,26 +529,26 @@ namespace sat { IF_VERBOSE(1, verbose_stream() << "(sat-defrag)\n"); clause_allocator& alloc = m_cls_allocator[!m_cls_allocator_idx]; ptr_vector new_clauses, new_learned; - ptr_addr_map cls2offset; for (clause* c : m_clauses) c->unmark_used(); for (clause* c : m_learned) c->unmark_used(); +#if 0 svector vars; for (unsigned i = 0; i < num_vars(); ++i) vars.push_back(i); std::stable_sort(vars.begin(), vars.end(), cmp_activity(*this)); literal_vector lits; for (bool_var v : vars) lits.push_back(to_literal(v)), lits.push_back(~to_literal(v)); - // walk clauses, reallocate them in an order that defragments memory and creates locality. //for (literal lit : lits) { //watch_list& wlist = m_watches[lit.index()]; +#endif for (watch_list& wlist : m_watches) { for (watched& w : wlist) { if (w.is_clause()) { clause& c1 = get_clause(w); clause_offset offset; if (c1.was_used()) { - offset = cls2offset[&c1]; + offset = c1.get_new_offset(); } else { clause* c2 = alloc.copy_clause(c1); @@ -560,7 +560,7 @@ namespace sat { new_clauses.push_back(c2); } offset = get_offset(*c2); - cls2offset.insert(&c1, offset); + c1.set_new_offset(offset); } w = watched(w.get_blocked_literal(), offset); } diff --git a/src/solver/parallel_params.pyg b/src/solver/parallel_params.pyg index 58c00aa97..2d58cbb81 100644 --- a/src/solver/parallel_params.pyg +++ b/src/solver/parallel_params.pyg @@ -5,7 +5,7 @@ def_module_params('parallel', params=( ('enable', BOOL, False, 'enable parallel solver by default on selected tactics (for QF_BV)'), ('threads.max', UINT, 10000, 'caps maximal number of threads below the number of processors'), - ('conquer.batch_size', UINT, 1000, 'number of cubes to batch together for fast conquer'), + ('conquer.batch_size', UINT, 100, 'number of cubes to batch together for fast conquer'), ('conquer.restart.max', UINT, 5, 'maximal number of restarts during conquer phase'), ('conquer.delay', UINT, 10, 'delay of cubes until applying conquer'), ('conquer.backtrack_frequency', UINT, 10, 'frequency to apply core minimization during conquer'), diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp index 748ee5d64..ac147672e 100644 --- a/src/solver/parallel_tactic.cpp +++ b/src/solver/parallel_tactic.cpp @@ -99,6 +99,8 @@ class parallel_tactic : public tactic { } } + bool in_shutdown() const { return m_shutdown; } + void add_task(solver_state* task) { std::lock_guard lock(m_mutex); m_tasks.push_back(task); @@ -285,6 +287,7 @@ class parallel_tactic : public tactic { p.set_uint("restart.max", pp.simplify_restart_max() * mult); p.set_bool("lookahead_simplify", true); p.set_bool("retain_blocked_clauses", retain_blocked); + if (m_depth > 1) p.set_uint("bce_delay", 0); get_solver().updt_params(p); } @@ -479,8 +482,8 @@ private: break; } - if (cubes.size() >= conquer_batch_size() || (!cubes.empty() && m_queue.is_idle())) { - spawn_cubes(s, std::max(2u, width), cubes); + if (cubes.size() >= conquer_batch_size()) { + spawn_cubes(s, 10*width, cubes); first = false; cubes.reset(); } @@ -575,6 +578,7 @@ private: } catch (z3_exception& ex) { IF_VERBOSE(1, verbose_stream() << ex.msg() << "\n";); + if (m_queue.in_shutdown()) return; m_queue.shutdown(); std::lock_guard lock(m_mutex); if (ex.has_error_code()) { From e940f53e9c58df2c1ca239bc3352dcf29b3a1caf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 30 Apr 2018 07:57:33 -0700 Subject: [PATCH 24/24] n/a Signed-off-by: Nikolaj Bjorner --- src/sat/sat_config.cpp | 4 ++- src/sat/sat_config.h | 3 ++- src/sat/sat_lookahead.cpp | 2 +- src/sat/sat_params.pyg | 3 ++- src/sat/sat_solver.cpp | 53 +++++++++++++++++++++------------------ src/sat/sat_solver.h | 1 + 6 files changed, 38 insertions(+), 28 deletions(-) diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index f7e2e2404..2bf20100b 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -115,9 +115,11 @@ namespace sat { m_lookahead_cube_psat_clause_base = p.lookahead_cube_psat_clause_base(); m_lookahead_cube_psat_trigger = p.lookahead_cube_psat_trigger(); m_lookahead_global_autarky = p.lookahead_global_autarky(); + m_lookahead_use_learned = p.lookahead_use_learned(); + // These parameters are not exposed - m_simplify_mult1 = _p.get_uint("simplify_mult1", 300); + m_next_simplify1 = _p.get_uint("next_simplify", 30000); m_simplify_mult2 = _p.get_double("simplify_mult2", 1.5); m_simplify_max = _p.get_uint("simplify_max", 500000); // -------------------------------- diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index f04973d13..9153f8b14 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -113,9 +113,10 @@ namespace sat { double m_lookahead_cube_psat_trigger; reward_t m_lookahead_reward; bool m_lookahead_global_autarky; + bool m_lookahead_use_learned; bool m_incremental; - unsigned m_simplify_mult1; + unsigned m_next_simplify1; double m_simplify_mult2; unsigned m_simplify_max; unsigned m_simplify_delay; diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index d4d1e615f..57ef90af9 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -2227,7 +2227,7 @@ namespace sat { void lookahead::init_search() { m_search_mode = lookahead_mode::searching; scoped_level _sl(*this, c_fixed_truth); - init(true); + init(m_s.m_config.m_lookahead_use_learned); } void lookahead::checkpoint() { diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index cf6ecc4f5..324882894 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -12,7 +12,7 @@ def_module_params('sat', ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'), ('restart.fast', BOOL, False, 'use fast restart strategy.'), ('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'), - ('variable_decay', UINT, 120, 'multiplier (divided by 100) for the VSIDS activity increement'), + ('variable_decay', UINT, 110, 'multiplier (divided by 100) for the VSIDS activity increement'), ('inprocess.max', UINT, UINT_MAX, 'maximal number of inprocessing passes'), ('branching.heuristic', SYMBOL, 'vsids', 'branching heuristic vsids, lrb or chb'), ('branching.anti_exploration', BOOL, False, 'apply anti-exploration heuristic for branch selection'), @@ -56,6 +56,7 @@ def_module_params('sat', ('lookahead_search', BOOL, False, 'use lookahead solver'), ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'), ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'), + ('lookahead.use_learned', BOOL, False, 'use learned clauses when selecting lookahead literal'), ('lookahead_simplify.bca', BOOL, True, 'add learned binary clauses as part of lookahead simplification'), ('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'), ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu'))) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 90ac876d2..f91dedeb5 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -532,17 +532,15 @@ namespace sat { for (clause* c : m_clauses) c->unmark_used(); for (clause* c : m_learned) c->unmark_used(); -#if 0 svector vars; for (unsigned i = 0; i < num_vars(); ++i) vars.push_back(i); std::stable_sort(vars.begin(), vars.end(), cmp_activity(*this)); literal_vector lits; - for (bool_var v : vars) lits.push_back(to_literal(v)), lits.push_back(~to_literal(v)); + for (bool_var v : vars) lits.push_back(literal(v, false)), lits.push_back(literal(v, true)); // walk clauses, reallocate them in an order that defragments memory and creates locality. - //for (literal lit : lits) { - //watch_list& wlist = m_watches[lit.index()]; -#endif - for (watch_list& wlist : m_watches) { + for (literal lit : lits) { + watch_list& wlist = m_watches[lit.index()]; + // for (watch_list& wlist : m_watches) { for (watched& w : wlist) { if (w.is_clause()) { clause& c1 = get_clause(w); @@ -795,7 +793,7 @@ namespace sat { } if (m_config.m_propagate_prefetch) { - _mm_prefetch((char const*)(m_watches.c_ptr() + l.index()), 0); + _mm_prefetch((const char*)(m_watches[l.index()].c_ptr()), 1); } SASSERT(!l.sign() || m_phase[v] == NEG_PHASE); @@ -1502,7 +1500,6 @@ namespace sat { SASSERT(m_search_lvl == 1); } - void solver::update_min_core() { if (!m_min_core_valid || m_core.size() < m_min_core.size()) { m_min_core.reset(); @@ -1533,8 +1530,7 @@ namespace sat { push(); reset_assumptions(); TRACE("sat", tout << "reassert: " << m_min_core << "\n";); - for (unsigned i = 0; i < m_min_core.size(); ++i) { - literal lit = m_min_core[i]; + for (literal lit : m_min_core) { SASSERT(is_external(lit.var())); add_assumption(lit); assign(lit, justification()); @@ -1554,12 +1550,12 @@ namespace sat { assign(m_assumptions[i], justification()); } TRACE("sat", - for (unsigned i = 0; i < m_assumptions.size(); ++i) { - index_set s; - if (m_antecedents.find(m_assumptions[i].var(), s)) { - tout << m_assumptions[i] << ": "; display_index_set(tout, s) << "\n"; - } - }); + for (literal a : m_assumptions) { + index_set s; + if (m_antecedents.find(a.var(), s)) { + tout << a << ": "; display_index_set(tout, s) << "\n"; + } + }); } } @@ -1602,7 +1598,6 @@ namespace sat { /** \brief Apply all simplifications. - */ void solver::simplify_problem() { if (m_conflicts_since_init < m_next_simplify) { @@ -1657,7 +1652,7 @@ namespace sat { reinit_assumptions(); if (m_next_simplify == 0) { - m_next_simplify = m_config.m_restart_initial * m_config.m_simplify_mult1; + m_next_simplify = m_config.m_next_simplify1; } else { m_next_simplify = static_cast(m_conflicts_since_init * m_config.m_simplify_mult2); @@ -1853,15 +1848,23 @@ namespace sat { } else { bool_var next = m_case_split_queue.min_var(); + + // Implementations of Marijn's idea of reusing the + // trail when the next decision literal has lower precedence. +#if 0 + // pop the trail from top do { - scope& s = m_scopes[scope_lvl() - num_scopes - 1]; - bool_var prev = m_trail[s.m_trail_lim].var(); - //IF_VERBOSE(0, verbose_stream() << "more active: " << m_case_split_queue.more_active(next, prev) << "\n"); - if (!m_case_split_queue.more_active(next, prev)) break; + bool_var prev = scope_literal(scope_lvl() - num_scopes - 1).var(); + if (m_case_split_queue.more_active(prev, next)) break; ++num_scopes; } while (num_scopes < scope_lvl() - search_lvl()); - //IF_VERBOSE(0, verbose_stream() << "backtrack " << num_scopes << " " << scope_lvl() - search_lvl() << "\n"); +#else + // pop the trail from bottom + unsigned n = search_lvl(); + for (; n < scope_lvl() && m_case_split_queue.more_active(scope_literal(n).var(), next); ++n) ; + num_scopes = n - search_lvl(); +#endif } pop_reinit(num_scopes); m_conflicts_since_restart = 0; @@ -2860,7 +2863,8 @@ namespace sat { \brief Reset the mark of the variables in the current lemma. */ void solver::reset_lemma_var_marks() { - if (m_config.m_branching_heuristic == BH_LRB) { + if (m_config.m_branching_heuristic == BH_LRB || + m_config.m_branching_heuristic == BH_VSIDS) { update_lrb_reasoned(); } literal_vector::iterator it = m_lemma.begin(); @@ -2917,6 +2921,7 @@ namespace sat { if (!is_marked(v)) { mark(v); m_reasoned[v]++; + inc_activity(v); m_lemma.push_back(lit); } } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 606907f54..15ac4df29 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -297,6 +297,7 @@ namespace sat { unsigned lvl(literal l) const { return m_level[l.var()]; } unsigned init_trail_size() const { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; } literal trail_literal(unsigned i) const { return m_trail[i]; } + literal scope_literal(unsigned n) const { return m_trail[m_scopes[n].m_trail_lim]; } void assign(literal l, justification j) { TRACE("sat_assign", tout << l << " previous value: " << value(l) << "\n";); switch (value(l)) {