From 61ade5e6cba53785f3e255f5f0d1dd22f06ad129 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 6 Feb 2017 20:57:08 -0800 Subject: [PATCH] tune cardinality solver for cache misses Signed-off-by: Nikolaj Bjorner --- src/sat/card_extension.cpp | 43 ++++++++++++++++++++++----- src/sat/card_extension.h | 9 ++++-- src/sat/sat_cleaner.cpp | 9 ++++-- src/sat/sat_par.cpp | 2 +- src/sat/sat_simplifier.cpp | 3 ++ src/sat/sat_solver.cpp | 11 ++++--- src/sat/sat_solver.h | 3 +- src/sat/sat_solver/inc_sat_solver.cpp | 2 +- src/sat/tactic/goal2sat.cpp | 25 +++++++++++----- src/sat/tactic/sat_tactic.cpp | 2 +- src/shell/dimacs_frontend.cpp | 5 ++-- src/test/sat_user_scope.cpp | 4 +-- 12 files changed, 85 insertions(+), 33 deletions(-) diff --git a/src/sat/card_extension.cpp b/src/sat/card_extension.cpp index 351c487bd..546a6905d 100644 --- a/src/sat/card_extension.cpp +++ b/src/sat/card_extension.cpp @@ -119,20 +119,37 @@ namespace sat { if (m_var_infos.size() <= static_cast(lit.var())) { return; } - ptr_vector* cards = m_var_infos[lit.var()].m_lit_watch[lit.sign()]; + ptr_vector*& cards = m_var_infos[lit.var()].m_lit_watch[lit.sign()]; if (cards) { - remove(*cards, c); + if (remove(*cards, c)) { + std::cout << "Empty: " << cards->empty() << "\n"; + cards = set_tag_empty(cards); + } } } - void card_extension::remove(ptr_vector& cards, card* c) { - for (unsigned j = 0; j < cards.size(); ++j) { + ptr_vector* card_extension::set_tag_empty(ptr_vector* c) { + return TAG(ptr_vector*, c, 1); + } + + bool card_extension::is_tag_empty(ptr_vector* c) { + return !c || GET_TAG(c) == 1; + } + + ptr_vector* card_extension::set_tag_non_empty(ptr_vector* c) { + return UNTAG(ptr_vector*, c); + } + + bool card_extension::remove(ptr_vector& cards, card* c) { + unsigned sz = cards.size(); + for (unsigned j = 0; j < sz; ++j) { if (cards[j] == c) { - std::swap(cards[j], cards[cards.size()-1]); + std::swap(cards[j], cards[sz-1]); cards.pop_back(); - break; + return sz == 1; } } + return false; } void card_extension::assign(card& c, literal lit) { @@ -171,6 +188,10 @@ namespace sat { cards = alloc(ptr_vector); m_var_infos[lit.var()].m_lit_watch[lit.sign()] = cards; } + else if (is_tag_empty(cards)) { + cards = set_tag_non_empty(cards); + m_var_infos[lit.var()].m_lit_watch[lit.sign()] = cards; + } TRACE("sat_verbose", tout << "insert: " << lit.var() << " " << lit.sign() << "\n";); cards->push_back(&c); } @@ -617,13 +638,16 @@ namespace sat { void card_extension::asserted(literal l) { bool_var v = l.var(); + if (s().inconsistent()) return; if (v >= m_var_infos.size()) return; var_info& vinfo = m_var_infos[v]; ptr_vector* cards = vinfo.m_lit_watch[!l.sign()]; //TRACE("sat", tout << "retrieve: " << v << " " << !l.sign() << "\n";); //TRACE("sat", tout << "asserted: " << l << " " << (cards ? "non-empty" : "empty") << "\n";); - if (cards != 0 && !cards->empty() && !s().inconsistent()) { - ptr_vector::iterator it = cards->begin(), it2 = it, end = cards->end(); + static unsigned is_empty = 0, non_empty = 0; + if (!is_tag_empty(cards)) { + ptr_vector::iterator begin = cards->begin(); + ptr_vector::iterator it = begin, it2 = it, end = cards->end(); for (; it != end; ++it) { card& c = *(*it); if (value(c.lit()) != l_true) { @@ -648,6 +672,9 @@ namespace sat { } } cards->set_end(it2); + if (cards->empty()) { + m_var_infos[v].m_lit_watch[!l.sign()] = set_tag_empty(cards); + } } card* crd = vinfo.m_card; diff --git a/src/sat/card_extension.h b/src/sat/card_extension.h index dbc8f7b07..4a01bc7cc 100644 --- a/src/sat/card_extension.h +++ b/src/sat/card_extension.h @@ -71,11 +71,14 @@ namespace sat { } void reset() { dealloc(m_card); - dealloc(m_lit_watch[0]); - dealloc(m_lit_watch[1]); + dealloc(card_extension::set_tag_non_empty(m_lit_watch[0])); + dealloc(card_extension::set_tag_non_empty(m_lit_watch[1])); } }; + ptr_vector* set_tag_empty(ptr_vector* c); + bool is_tag_empty(ptr_vector* c); + static ptr_vector* set_tag_non_empty(ptr_vector* c); solver* m_solver; stats m_stats; @@ -113,7 +116,7 @@ namespace sat { inline unsigned lvl(bool_var v) const { return m_solver->lvl(v); } void unwatch_literal(literal w, card* c); - void remove(ptr_vector& cards, card* c); + bool remove(ptr_vector& cards, card* c); void normalize_active_coeffs(); void inc_coeff(literal l, int offset); diff --git a/src/sat/sat_cleaner.cpp b/src/sat/sat_cleaner.cpp index 959f5e94f..10751c622 100644 --- a/src/sat/sat_cleaner.cpp +++ b/src/sat/sat_cleaner.cpp @@ -142,12 +142,17 @@ namespace sat { c.shrink(new_sz); *it2 = *it; it2++; - if (!c.frozen()) { - if (new_sz == 3) + if (!c.frozen()) { + if (new_sz == 3) s.attach_ter_clause(c); else s.attach_nary_clause(c); } + if (s.m_config.m_drat) { + // for optimization, could also report deletion + // of previous version of clause. + s.m_drat.add(c, true); + } } } } diff --git a/src/sat/sat_par.cpp b/src/sat/sat_par.cpp index cd8901e09..ec6e39822 100644 --- a/src/sat/sat_par.cpp +++ b/src/sat/sat_par.cpp @@ -117,7 +117,7 @@ namespace sat { if (i == 1 + num_threads/2) { s.m_params.set_sym("phase", symbol("random")); } - m_solvers[i] = alloc(sat::solver, s.m_params, m_limits[i], 0); + m_solvers[i] = alloc(sat::solver, s.m_params, m_limits[i]); m_solvers[i]->copy(s); m_solvers[i]->set_par(this, i); m_scoped_rlimit.push_child(&m_solvers[i]->rlimit()); diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index bd975115b..8bfa4bb69 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -304,6 +304,9 @@ namespace sat { s.attach_ter_clause(c); else s.attach_nary_clause(c); + if (s.m_config.m_drat) { + s.m_drat.add(c, true); + } } } cs.set_end(it2); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index c843fc900..9b50db8e8 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -31,10 +31,9 @@ Revision History: namespace sat { - solver::solver(params_ref const & p, reslimit& l, extension * ext): + solver::solver(params_ref const & p, reslimit& l): m_rlimit(l), m_config(p), - m_ext(ext), m_par(0), m_par_syncing_clauses(false), m_par_id(0), @@ -59,7 +58,6 @@ namespace sat { m_conflicts = 0; m_next_simplify = 0; m_num_checkpoints = 0; - if (m_ext) m_ext->set_solver(this); } solver::~solver() { @@ -77,6 +75,11 @@ namespace sat { ++m_stats.m_non_learned_generation; } + void solver::set_extension(extension* ext) { + m_ext = ext; + if (ext) ext->set_solver(this); + } + void solver::copy(solver const & src) { pop_to_base_level(); SASSERT(m_mc.empty() && src.m_mc.empty()); @@ -771,7 +774,7 @@ namespace sat { flet _searching(m_searching, true); #ifdef CLONE_BEFORE_SOLVING if (m_mc.empty()) { - m_clone = alloc(solver, m_params, 0 /* do not clone extension */); + m_clone = alloc(solver, m_params); SASSERT(m_clone); } #endif diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index af1b8f213..d5affd2d4 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -156,7 +156,7 @@ namespace sat { friend class par; friend struct mk_stat; public: - solver(params_ref const & p, reslimit& l, extension * ext); + solver(params_ref const & p, reslimit& l); ~solver(); // ----------------------- @@ -264,6 +264,7 @@ namespace sat { bool canceled() { return !m_rlimit.inc(); } config const& get_config() { return m_config; } extension* get_extension() const { return m_ext.get(); } + void set_extension(extension* e); typedef std::pair bin_clause; protected: watch_list & get_wlist(literal l) { return m_watches[l.index()]; } diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 7715c4b5d..eec734dc7 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -72,7 +72,7 @@ class inc_sat_solver : public solver { public: inc_sat_solver(ast_manager& m, params_ref const& p): m(m), - m_solver(p, m.limit(), alloc(sat::card_extension)), + m_solver(p, m.limit()), m_params(p), m_optimize_model(false), m_fmls(m), m_asmsf(m), diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 923006da2..1fcaa78b1 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -78,11 +78,6 @@ struct goal2sat::imp { m_default_external(default_external) { updt_params(p); m_true = sat::null_bool_var; - sat::extension* e = m_solver.get_extension(); - if (e) { - sat::card_extension* ce = dynamic_cast(e); - m_ext = ce; - } } void updt_params(params_ref const & p) { @@ -158,7 +153,8 @@ struct goal2sat::imp { } bool convert_app(app* t, bool root, bool sign) { - if (m_ext && t->get_family_id() == pb.get_family_id()) { + if (t->get_family_id() == pb.get_family_id()) { + ensure_extension(); m_frame_stack.push_back(frame(to_app(t), root, sign, 0)); return false; } @@ -465,6 +461,20 @@ struct goal2sat::imp { } } + void ensure_extension() { + if (!m_ext) { + sat::extension* ext = m_solver.get_extension(); + if (ext) { + m_ext = dynamic_cast(ext); + SASSERT(m_ext); + } + if (!m_ext) { + m_ext = alloc(sat::card_extension); + m_solver.set_extension(m_ext); + } + } + } + void convert(app * t, bool root, bool sign) { if (t->get_family_id() == m.get_basic_family_id()) { switch (to_app(t)->get_decl_kind()) { @@ -485,7 +495,8 @@ struct goal2sat::imp { UNREACHABLE(); } } - else if (m_ext && t->get_family_id() == pb.get_family_id()) { + else if (t->get_family_id() == pb.get_family_id()) { + ensure_extension(); switch (t->get_decl_kind()) { case OP_AT_MOST_K: convert_at_most_k(t, pb.get_k(t), root, sign); diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index f99e46851..4432d0e3c 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -34,7 +34,7 @@ class sat_tactic : public tactic { imp(ast_manager & _m, params_ref const & p): m(_m), - m_solver(p, m.limit(), 0), + m_solver(p, m.limit()), m_params(p) { SASSERT(!m.proofs_enabled()); } diff --git a/src/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp index 09645a25a..4cc9ec610 100644 --- a/src/shell/dimacs_frontend.cpp +++ b/src/shell/dimacs_frontend.cpp @@ -126,7 +126,6 @@ static void track_clauses(sat::solver const& src, } } - unsigned read_dimacs(char const * file_name) { g_start_time = clock(); register_on_timeout_proc(on_timeout); @@ -134,7 +133,7 @@ unsigned read_dimacs(char const * file_name) { params_ref p = gparams::get_module("sat"); p.set_bool("produce_models", true); reslimit limit; - sat::solver solver(p, limit, 0); + sat::solver solver(p, limit); g_solver = &solver; if (file_name) { @@ -152,7 +151,7 @@ unsigned read_dimacs(char const * file_name) { lbool r; vector tracking_clauses; - sat::solver solver2(p, limit, 0); + sat::solver solver2(p, limit); if (p.get_bool("dimacs.core", false)) { g_solver = &solver2; sat::literal_vector assumptions; diff --git a/src/test/sat_user_scope.cpp b/src/test/sat_user_scope.cpp index aa717f371..ebda383f9 100644 --- a/src/test/sat_user_scope.cpp +++ b/src/test/sat_user_scope.cpp @@ -59,7 +59,7 @@ static void init_vars(sat::solver& s) { static void check_coherence(sat::solver& s1, trail_t& t) { params_ref p; reslimit rlim; - sat::solver s2(p, rlim, 0); + sat::solver s2(p, rlim); init_vars(s2); sat::literal_vector cls; for (unsigned i = 0; i < t.size(); ++i) { @@ -85,7 +85,7 @@ void tst_sat_user_scope() { trail_t trail; params_ref p; reslimit rlim; - sat::solver s(p, rlim, 0); // incremental solver + sat::solver s(p, rlim); // incremental solver init_vars(s); while (true) { for (unsigned i = 0; i < s_num_frames; ++i) {