diff --git a/contrib/cmake/src/sat/CMakeLists.txt b/contrib/cmake/src/sat/CMakeLists.txt index 5494049d7..fcfe53e02 100644 --- a/contrib/cmake/src/sat/CMakeLists.txt +++ b/contrib/cmake/src/sat/CMakeLists.txt @@ -3,6 +3,7 @@ z3_add_component(sat card_extension.cpp dimacs.cpp sat_asymm_branch.cpp + sat_ccc.cpp sat_clause.cpp sat_clause_set.cpp sat_clause_use_list.cpp diff --git a/src/sat/card_extension.cpp b/src/sat/card_extension.cpp index cb05e5d61..7d1c27abb 100644 --- a/src/sat/card_extension.cpp +++ b/src/sat/card_extension.cpp @@ -26,8 +26,7 @@ namespace sat { m_index(index), m_lit(lit), m_k(k), - m_size(lits.size()) - { + m_size(lits.size()) { for (unsigned i = 0; i < lits.size(); ++i) { m_lits[i] = lits[i]; } @@ -42,6 +41,27 @@ namespace sat { SASSERT(m_size >= m_k && m_k > 0); } + card_extension::pb::pb(unsigned index, literal lit, svector const& wlits, unsigned k): + m_index(index), + m_lit(lit), + m_k(k), + m_size(wlits.size()) { + for (unsigned i = 0; i < wlits.size(); ++i) { + m_wlits[i] = wlits[i]; + } + } + + void card_extension::pb::negate() { + m_lit.neg(); + unsigned w = 0; + for (unsigned i = 0; i < m_size; ++i) { + m_wlits[i].second.neg(); + w += m_wlits[i].first; + } + m_k = w - m_k + 1; + SASSERT(w >= m_k && m_k > 0); + } + card_extension::xor::xor(unsigned index, literal lit, literal_vector const& lits): m_index(index), m_lit(lit), @@ -191,6 +211,15 @@ namespace sat { SASSERT(s().inconsistent()); } + // pb: + void card_extension::init_watch(pb& p, bool is_true) { + NOT_IMPLEMENTED_YET(); + } + + + + + // xor: void card_extension::clear_watch(xor& x) { unwatch_literal(x[0], &x); unwatch_literal(x[1], &x); @@ -510,7 +539,7 @@ namespace sat { process_card(c, offset); ++m_stats.m_num_card_resolves; } - else { + else if (is_xor_index(index)) { // jus.push_back(js); m_lemma.reset(); m_bound += offset; @@ -521,6 +550,12 @@ namespace sat { } ++m_stats.m_num_xor_resolves; } + else if (is_pb_index(index)) { + NOT_IMPLEMENTED_YET(); + } + else { + UNREACHABLE(); + } break; } default: @@ -758,7 +793,7 @@ namespace sat { } void card_extension::add_at_least(bool_var v, literal_vector const& lits, unsigned k) { - unsigned index = 2*m_cards.size(); + unsigned index = 4*m_cards.size(); literal lit = v == null_bool_var ? null_literal : literal(v, false); card* c = new (memory::allocate(card::get_obj_size(lits.size()))) card(index, lit, lits, k); m_cards.push_back(c); @@ -774,9 +809,26 @@ namespace sat { } } + void card_extension::add_pb_ge(bool_var v, svector const& wlits, unsigned k) { + unsigned index = 4*m_pb.size() + 0x11; + literal lit = v == null_bool_var ? null_literal : literal(v, false); + pb* p = new (memory::allocate(pb::get_obj_size(wlits.size()))) pb(index, lit, wlits, k); + m_pb.push_back(p); + if (v == null_bool_var) { + init_watch(*p, true); + m_pb_axioms.push_back(p); + } + else { + init_watch(v); + m_var_infos[v].m_pb = p; + m_var_trail.push_back(v); + } + } + + void card_extension::add_xor(bool_var v, literal_vector const& lits) { m_has_xor = true; - unsigned index = 2*m_xors.size()+1; + unsigned index = 4*m_xors.size() + 0x01; xor* x = new (memory::allocate(xor::get_obj_size(lits.size()))) xor(index, literal(v, false), lits); m_xors.push_back(x); init_watch(v); @@ -819,7 +871,7 @@ namespace sat { unsigned level = lvl(l); bool_var v = l.var(); SASSERT(js.get_kind() == justification::EXT_JUSTIFICATION); - SASSERT(!is_card_index(js.get_ext_justification_idx())); + SASSERT(is_xor_index(js.get_ext_justification_idx())); TRACE("sat", tout << l << ": " << js << "\n"; tout << s().m_trail << "\n";); unsigned num_marks = 0; @@ -828,7 +880,7 @@ namespace sat { ++count; if (js.get_kind() == justification::EXT_JUSTIFICATION) { unsigned idx = js.get_ext_justification_idx(); - if (is_card_index(idx)) { + if (!is_xor_index(idx)) { r.push_back(l); } else { @@ -912,7 +964,7 @@ namespace sat { r.push_back(~c[i]); } } - else { + else if (is_xor_index(idx)) { xor& x = index2xor(idx); if (x.lit() != null_literal) r.push_back(x.lit()); TRACE("sat", display(tout << l << " ", x, true);); @@ -931,6 +983,12 @@ namespace sat { r.push_back(value(x[i]) == l_true ? x[i] : ~x[i]); } } + else if (is_pb_index(idx)) { + NOT_IMPLEMENTED_YET(); + } + else { + UNREACHABLE(); + } } @@ -1281,13 +1339,19 @@ namespace sat { } out << ">= " << c.k(); } - else { + else if (is_xor_index(idx)) { xor& x = index2xor(idx); out << "xor " << x.lit() << ": "; for (unsigned i = 0; i < x.size(); ++i) { out << x[i] << " "; } } + else if (is_pb_index(idx)) { + NOT_IMPLEMENTED_YET(); + } + else { + UNREACHABLE(); + } return out; } @@ -1382,7 +1446,7 @@ namespace sat { } if (c.lit() != null_literal) p.push(~c.lit(), offset*c.k()); } - else { + else if (is_xor_index(index)) { literal_vector ls; get_antecedents(lit, index, ls); p.reset(offset); @@ -1392,6 +1456,12 @@ namespace sat { literal lxor = index2xor(index).lit(); if (lxor != null_literal) p.push(~lxor, offset); } + else if (is_pb_index(index)) { + NOT_IMPLEMENTED_YET(); + } + else { + UNREACHABLE(); + } break; } default: diff --git a/src/sat/card_extension.h b/src/sat/card_extension.h index 0d649a97c..6f8b6d120 100644 --- a/src/sat/card_extension.h +++ b/src/sat/card_extension.h @@ -58,6 +58,26 @@ namespace sat { void swap(unsigned i, unsigned j) { std::swap(m_lits[i], m_lits[j]); } void negate(); }; + + typedef std::pair wliteral; + + class pb { + unsigned m_index; + literal m_lit; + unsigned m_k; + unsigned m_size; + wliteral m_wlits[0]; + public: + static size_t get_obj_size(unsigned num_lits) { return sizeof(card) + num_lits * sizeof(wliteral); } + pb(unsigned index, literal lit, svector const& wlits, unsigned k); + unsigned index() const { return m_index; } + literal lit() const { return m_lit; } + wliteral operator[](unsigned i) const { return m_wlits[i]; } + unsigned k() const { return m_k; } + unsigned size() const { return m_size; } + void swap(unsigned i, unsigned j) { std::swap(m_wlits[i], m_wlits[j]); } + void negate(); + }; class xor { unsigned m_index; @@ -85,20 +105,28 @@ namespace sat { typedef ptr_vector card_watch; typedef ptr_vector xor_watch; + typedef ptr_vector pb_watch; struct var_info { card_watch* m_card_watch[2]; + pb_watch* m_pb_watch[2]; xor_watch* m_xor_watch; card* m_card; + pb* m_pb; xor* m_xor; - var_info(): m_xor_watch(0), m_card(0), m_xor(0) { + var_info(): m_xor_watch(0), m_card(0), m_xor(0), m_pb(0) { m_card_watch[0] = 0; m_card_watch[1] = 0; + m_pb_watch[0] = 0; + m_pb_watch[1] = 0; } void reset() { dealloc(m_card); dealloc(m_xor); + dealloc(m_pb); dealloc(card_extension::set_tag_non_empty(m_card_watch[0])); dealloc(card_extension::set_tag_non_empty(m_card_watch[1])); + dealloc(card_extension::set_tag_non_empty(m_pb_watch[0])); + dealloc(card_extension::set_tag_non_empty(m_pb_watch[1])); dealloc(card_extension::set_tag_non_empty(m_xor_watch)); } }; @@ -125,8 +153,10 @@ namespace sat { ptr_vector m_cards; ptr_vector m_xors; + ptr_vector m_pb; scoped_ptr_vector m_card_axioms; + scoped_ptr_vector m_pb_axioms; // watch literals svector m_var_infos; @@ -173,11 +203,17 @@ namespace sat { lbool add_assign(xor& x, literal alit); void asserted_xor(literal l, ptr_vector* xors, xor* x); - bool is_card_index(unsigned idx) const { return 0 == (idx & 0x1); } - card& index2card(unsigned idx) const { SASSERT(is_card_index(idx)); return *m_cards[idx >> 1]; } - xor& index2xor(unsigned idx) const { SASSERT(!is_card_index(idx)); return *m_xors[idx >> 1]; } + bool is_card_index(unsigned idx) const { return 0x00 == (idx & 0x11); } + bool is_xor_index(unsigned idx) const { return 0x01 == (idx & 0x11); } + bool is_pb_index(unsigned idx) const { return 0x11 == (idx & 0x11); } + card& index2card(unsigned idx) const { SASSERT(is_card_index(idx)); return *m_cards[idx >> 2]; } + xor& index2xor(unsigned idx) const { SASSERT(!is_card_index(idx)); return *m_xors[idx >> 2]; } + pb& index2pb(unsigned idx) const { SASSERT(is_pb_index(idx)); return *m_pb[idx >> 2]; } + void get_xor_antecedents(literal l, unsigned inddex, justification js, literal_vector& r); + void init_watch(pb& p, bool is_true); + template bool remove(ptr_vector& ts, T* t) { @@ -233,6 +269,7 @@ namespace sat { virtual ~card_extension(); virtual void set_solver(solver* s) { m_solver = s; } void add_at_least(bool_var v, literal_vector const& lits, unsigned k); + void add_pb_ge(bool_var v, svector const& wlits, unsigned k); void add_xor(bool_var v, literal_vector const& lits); virtual void propagate(literal l, ext_constraint_idx idx, bool & keep); virtual bool resolve_conflict(); diff --git a/src/sat/sat_ccc.cpp b/src/sat/sat_ccc.cpp new file mode 100644 index 000000000..70defb17d --- /dev/null +++ b/src/sat/sat_ccc.cpp @@ -0,0 +1,271 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + sat_ccc.cpp + +Abstract: + + A variant of Concurrent Cube and Conquer + +Author: + + Nikolaj Bjorner (nbjorner) 2017-4-17 + +Notes: + +--*/ + +#include "sat_solver.h" +#include "sat_lookahead.h" +#include "sat_ccc.h" + +using namespace sat; + +lbool ccc::cube() { + unsigned branch_id = 0; + unsigned_vector id_trail; + + lookahead lh(s); + lh.init_search(); + lh.m_model.reset(); + + lookahead::scoped_level _sl(lh, lh.c_fixed_truth); + literal_vector trail; + lh.m_search_mode = lookahead_mode::searching; + while (!m_cancel) { + // remove old branch ids from id_trail. + while (id_trail.size() > trail.size()) { + id_trail.pop_back(); + } + TRACE("sat", lh.display(tout);); + lh.inc_istamp(); + s.checkpoint(); + if (lh.inconsistent()) { + if (!lh.backtrack(trail)) return l_false; + continue; + } + + // check if CDCL solver got ahead. + bool repeat = false; + #pragma omp critical (ccc_solved) + { + if (!m_solved.empty()) { + unsigned solved_id = m_solved.top(); + if (id_trail.contains(solved_id)) { + lh.set_conflict(); + } + else { + m_solved.pop(); + } + repeat = true; + } + } + if (repeat) continue; + + ++branch_id; + if (!trail.empty()) { + #pragma omp critical (ccc_decisions) + { + m_decisions.push(decision(branch_id, trail.size()-1, trail.back())); + } + } + + literal l = lh.choose(); + if (lh.inconsistent()) { + if (!lh.backtrack(trail)) return l_false; + continue; + } + if (l == null_literal) { + m_model = lh.get_model(); + return l_true; + } + + // update trail and set of ids + id_trail.push_back(branch_id); + trail.push_back(l); + SASSERT(id_trail.size() == trail.size()); + + TRACE("sat", tout << "choose: " << l << " " << trail << "\n";); + ++lh.m_stats.m_decisions; + IF_VERBOSE(1, verbose_stream() << "select " << pp_prefix(lh.m_prefix, lh.m_trail_lim.size()) << ": " << l << " " << lh.m_trail.size() << "\n";); + lh.push(l, lh.c_fixed_truth); + SASSERT(lh.inconsistent() || !lh.is_unsat()); + } + return l_undef; +} + +lbool ccc::conquer(solver& s) { + try { + if (s.inconsistent()) return l_false; + s.init_search(); + s.propagate(false); + if (s.inconsistent()) return l_false; + s.init_assumptions(0, 0); + s.propagate(false); + if (s.check_inconsistent()) return l_false; + s.cleanup(); + s.simplify_problem(); + if (s.check_inconsistent()) return l_false; + + unsigned_vector ids; + + while (true) { + SASSERT(!s.inconsistent()); + + lbool r = bounded_search(s, ids); + if (r != l_undef) + return r; + + if (s.m_conflicts > s.m_config.m_max_conflicts) { + IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = " << s.m_conflicts << "\")\n";); + return l_undef; + } + + s.restart(); + s.simplify_problem(); + if (s.check_inconsistent()) return l_false; + s.gc(); + } + } + catch (solver::abort_solver) { + return l_undef; + } +} + +lbool ccc::bounded_search(solver& s, unsigned_vector& ids) { + decision d; + + while (true) { + s.checkpoint(); + bool done = false; + while (!done) { + lbool is_sat = s.propagate_and_backjump_step(done); + if (is_sat != l_true) return is_sat; + } + + if (s.m_scope_lvl < ids.size()) { + while (ids.size() > s.m_scope_lvl + 1) ids.pop_back(); + unsigned id = ids.back(); + ids.pop_back(); + #pragma omp critical (ccc_solved) + { + m_solved.push(id); + } + } + + s.gc(); + + bool cube_decision = false; + #pragma omp critical (ccc_decisions) + { + if (!m_decisions.empty()) { + d = m_decisions.pop(); + cube_decision = true; + } + } + if (cube_decision) { + if (d.m_depth > ids.size()) continue; + ids.push_back(d.m_id); + s.pop_reinit(s.m_scope_lvl - d.m_depth); // TBD: check alignment of scopes + s.push(); + s.assign(d.m_last, justification()); + } + else if (!s.decide()) { + lbool is_sat = s.final_check(); + if (is_sat != l_undef) { + return is_sat; + } + } + } +} + + +lbool ccc::search() { + enum par_exception_kind { + DEFAULT_EX, + ERROR_EX + }; + + m_cancel = false; + + scoped_limits scoped_rlimit(s.rlimit()); + vector limits; + ptr_vector solvers; + int finished_id = -1; + std::string ex_msg; + par_exception_kind ex_kind; + unsigned error_code = 0; + lbool result = l_undef; + bool canceled = false; + + int num_threads = s.m_config.m_num_threads + 1; + for (int i = 1; i < num_threads; ++i) { + limits.push_back(reslimit()); + } + + for (int i = 1; i < num_threads; ++i) { + s.m_params.set_uint("random_seed", s.m_rand()); + solvers[i] = alloc(sat::solver, s.m_params, limits[i]); + solvers[i]->copy(s); + scoped_rlimit.push_child(&solvers[i]->rlimit()); + } + + #pragma omp parallel for + for (int i = 0; i < num_threads; ++i) { + try { + lbool r = l_undef; + if (i == 0) { + r = cube(); + } + else { + r = conquer(*solvers[i-1]); + } + bool first = false; + #pragma omp critical (par_solver) + { + if (finished_id == -1) { + finished_id = i; + first = true; + result = r; + } + } + if (first) { + for (unsigned j = 0; j < solvers.size(); ++j) { + solvers[j]->rlimit().cancel(); + } + // cancel lookahead solver: + m_cancel = true; + } + } + catch (z3_error & err) { + error_code = err.error_code(); + ex_kind = ERROR_EX; + } + catch (z3_exception & ex) { + ex_msg = ex.msg(); + ex_kind = DEFAULT_EX; + } + } + + if (finished_id > 0 && result == l_true) { + // set model from auxiliary solver + m_model = solvers[finished_id - 1]->get_model(); + } + + for (unsigned i = 0; i < solvers.size(); ++i) { + dealloc(solvers[i]); + } + + if (finished_id == -1) { + switch (ex_kind) { + case ERROR_EX: throw z3_error(error_code); + default: throw default_exception(ex_msg.c_str()); + } + } + + + return result; +} + diff --git a/src/sat/sat_ccc.h b/src/sat/sat_ccc.h new file mode 100644 index 000000000..d5357090a --- /dev/null +++ b/src/sat/sat_ccc.h @@ -0,0 +1,66 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + sat_ccc.h + +Abstract: + + A variant of Concurrent Cube and Conquer + +Author: + + Nikolaj Bjorner (nbjorner) 2017-4-17 + +Notes: + +--*/ +#ifndef _SAT_CCC_H_ +#define _SAT_CCC_H_ + +#include "queue.h" + +namespace sat { + + class ccc { + struct decision { + unsigned m_id; + unsigned m_depth; + literal m_last; + decision(unsigned id, unsigned d, literal last): + m_id(id), m_depth(d), m_last(last) {} + decision(): m_id(0), m_depth(0), m_last(null_literal) {} + }; + + solver& s; + queue m_solved; + queue m_decisions; + model m_model; + volatile bool m_cancel; + + struct config { + config() { + } + }; + + struct stats { + stats() { reset(); } + void reset() { memset(this, 0, sizeof(*this)); } + }; + + lbool conquer(solver& s); + lbool bounded_search(solver& s, unsigned_vector& ids); + + lbool cube(); + + public: + ccc(solver& s): s(s) {} + + lbool search(); + + }; +} + +#endif + diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 42c185ee1..175c34690 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -82,6 +82,7 @@ namespace sat { m_max_conflicts = p.max_conflicts(); m_num_threads = p.threads(); m_local_search = p.local_search(); + m_local_search_threads = p.local_search_threads(); m_lookahead_search = p.lookahead_search(); // These parameters are not exposed diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 8c10983d2..fb125c529 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -58,7 +58,8 @@ namespace sat { unsigned m_burst_search; unsigned m_max_conflicts; unsigned m_num_threads; - unsigned m_local_search; + unsigned m_local_search_threads; + bool m_local_search; bool m_lookahead_search; unsigned m_simplify_mult1; diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 6bc528220..a801cdad7 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -61,6 +61,8 @@ namespace sat { class lookahead { solver& s; + friend class ccc; + struct config { double m_dl_success; float m_alpha; @@ -70,6 +72,7 @@ namespace sat { unsigned m_level_cand; float m_delta_rho; unsigned m_dl_max_iterations; + unsigned m_tc1_limit; config() { m_max_hlevel = 50; @@ -79,6 +82,7 @@ namespace sat { m_level_cand = 600; m_delta_rho = (float)0.9995; m_dl_max_iterations = 32; + m_tc1_limit = 10000000; } }; @@ -126,6 +130,8 @@ namespace sat { vector m_binary; // literal: binary clauses unsigned_vector m_binary_trail; // trail of added binary clauses unsigned_vector m_binary_trail_lim; + unsigned m_num_tc1; + unsigned_vector m_num_tc1_lim; unsigned m_qhead; // propagation queue head unsigned_vector m_qhead_lim; clause_vector m_clauses; // non-binary clauses @@ -314,8 +320,11 @@ namespace sat { assign(u); return false; } - IF_VERBOSE(3, verbose_stream() << "tc1: " << u << " " << w << "\n";); - add_binary(u, w); + if (m_num_tc1 < m_config.m_tc1_limit) { + ++m_num_tc1; + IF_VERBOSE(3, verbose_stream() << "tc1: " << u << " " << w << "\n";); + add_binary(u, w); + } } } return true; @@ -1055,11 +1064,10 @@ namespace sat { unsigned trail_sz = s.init_trail_size(); for (unsigned i = 0; i < trail_sz; ++i) { literal l = s.m_trail[i]; - if (!s.was_eliminated(l.var())) - { - if (s.m_config.m_drat) m_drat.add(l, false); - assign(l); - } + if (!s.was_eliminated(l.var())) { + if (s.m_config.m_drat) m_drat.add(l, false); + assign(l); + } } propagate(); m_qhead = m_trail.size(); @@ -1090,6 +1098,7 @@ namespace sat { SASSERT(m_search_mode == lookahead_mode::searching); m_binary_trail_lim.push_back(m_binary_trail.size()); m_trail_lim.push_back(m_trail.size()); + m_num_tc1_lim.push_back(m_num_tc1); m_retired_clause_lim.push_back(m_retired_clauses.size()); m_retired_ternary_lim.push_back(m_retired_ternary.size()); m_qhead_lim.push_back(m_qhead); @@ -1116,6 +1125,9 @@ namespace sat { } m_trail.shrink(old_sz); // reset assignment. m_trail_lim.pop_back(); + + m_num_tc1 = m_num_tc1_lim.back(); + m_num_tc1_lim.pop_back(); // unretire clauses old_sz = m_retired_clause_lim.back(); @@ -1792,11 +1804,17 @@ namespace sat { return out; } + void init_search() { + m_search_mode = lookahead_mode::searching; + scoped_level _sl(*this, c_fixed_truth); + init(); + } public: lookahead(solver& s) : s(s), m_drat(s), + m_num_tc1(0), m_level(2), m_prefix(0) { } @@ -1806,11 +1824,7 @@ namespace sat { } lbool check() { - { - m_search_mode = lookahead_mode::searching; - scoped_level _sl(*this, c_fixed_truth); - init(); - } + init_search(); return search(); } diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index ffc699d02..a69de0772 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -28,6 +28,7 @@ def_module_params('sat', ('drat.check', BOOL, False, 'build up internal proof and check'), ('cardinality.solver', BOOL, False, 'use cardinality solver'), ('xor.solver', BOOL, False, 'use xor solver'), - ('local_search', UINT, 0, 'number of local search threads to find satisfiable solution'), + ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'), + ('local_search', BOOL, False, 'use local search instead of CDCL'), ('lookahead_search', BOOL, False, 'use lookahead solver') )) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 5ebd661ee..8eaba2734 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -787,7 +787,10 @@ namespace sat { if (m_config.m_lookahead_search && num_lits == 0) { return lookahead_search(); } - if ((m_config.m_num_threads > 1 || m_config.m_local_search > 0) && !m_par) { + if (m_config.m_local_search) { + return do_local_search(num_lits, lits); + } + if ((m_config.m_num_threads > 1 || m_config.m_local_search_threads > 0) && !m_par) { return check_par(num_lits, lits); } flet _searching(m_searching, true); @@ -859,6 +862,18 @@ namespace sat { ERROR_EX }; + lbool solver::do_local_search(unsigned num_lits, literal const* lits) { + scoped_limits scoped_rl(rlimit()); + local_search srch; + srch.config().set_seed(m_config.m_random_seed); + srch.import(*this, false); + scoped_rl.push_child(&srch.rlimit()); + lbool r = srch.check(num_lits, lits, 0); + m_model = srch.get_model(); + // srch.collect_statistics(m_lookahead_stats); + return r; + } + lbool solver::lookahead_search() { lookahead lh(*this); lbool r = l_undef; @@ -876,9 +891,9 @@ namespace sat { lbool solver::check_par(unsigned num_lits, literal const* lits) { scoped_ptr_vector ls; - int num_threads = static_cast(m_config.m_num_threads + m_config.m_local_search); + int num_threads = static_cast(m_config.m_num_threads + m_config.m_local_search_threads); int num_extra_solvers = m_config.m_num_threads - 1; - int num_local_search = static_cast(m_config.m_local_search); + int num_local_search = static_cast(m_config.m_local_search_threads); for (int i = 0; i < num_local_search; ++i) { local_search* l = alloc(local_search); l->config().set_seed(m_config.m_random_seed + i); diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 1bf393696..b4b7f82fe 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -160,6 +160,7 @@ namespace sat { friend class lookahead; friend class local_search; friend struct mk_stat; + friend class ccc; public: solver(params_ref const & p, reslimit& l); ~solver(); @@ -349,6 +350,7 @@ namespace sat { void exchange_par(); lbool check_par(unsigned num_lits, literal const* lits); lbool lookahead_search(); + lbool do_local_search(unsigned num_lits, literal const* lits); // ----------------------- // @@ -465,7 +467,7 @@ namespace sat { lbool get_consequences(literal_vector const& assms, bool_var_vector const& vars, vector& conseq); // initialize and retrieve local search. - local_search& init_local_search(); + // local_search& init_local_search(); private: diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index 6bd4ec64f..c727a8af3 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -57,6 +57,7 @@ static void throw_out_of_memory() { { g_memory_out_of_memory = true; } + if (g_exit_when_out_of_memory) { std::cerr << g_out_of_memory_msg << "\n"; exit(ERR_MEMOUT); diff --git a/src/util/queue.h b/src/util/queue.h new file mode 100644 index 000000000..4b85f53f0 --- /dev/null +++ b/src/util/queue.h @@ -0,0 +1,61 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + queue.h + +Abstract: + + Generic queue. + +Author: + + Nikolaj Bjorner (nbjorner) 2017-4-17 + +Notes: + +--*/ +#ifndef _QUEUE_H_ +#define _QUEUE_H_ + +#include "vector.h" + +template +class queue { + vector m_elems; + unsigned m_head; + unsigned m_capacity; + +public: + + queue(): m_head(0), m_capacity(0) {} + + void push(T const& t) { m_elems.push_back(t); } + + bool empty() const { + return m_head == m_elems.size(); + } + + T top() const { + return m_elems[m_head]; + } + + T pop() { + SASSERT(!empty()); + m_capacity = std::max(m_capacity, m_elems.size()); + SASSERT(m_head < m_elems.size()); + if (2 * m_head > m_capacity && m_capacity > 10) { + for (unsigned i = 0; i < m_elems.size() - m_head; ++i) { + m_elems[i] = m_elems[i + m_head]; + } + m_elems.shrink(m_elems.size() - m_head); + m_head = 0; + } + return m_elems[m_head++]; + } + +}; + +#endif +