From 9ebe980b440a09fdaa3efea8c25a395d25856c1d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 22 Jun 2017 07:42:44 -0700 Subject: [PATCH] cleaning up lookahead Signed-off-by: Nikolaj Bjorner --- src/sat/sat_lookahead.cpp | 7 +------ src/sat/sat_params.pyg | 3 ++- src/sat/sat_simplifier.cpp | 1 - src/sat/sat_solver.cpp | 24 ++++++++++++------------ src/sat/sat_solver.h | 2 +- src/sat/sat_solver/inc_sat_solver.cpp | 4 +--- 6 files changed, 17 insertions(+), 24 deletions(-) diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 955b3766c..95b11fa15 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -299,7 +299,6 @@ namespace sat { bool_var x = *it; if (!m_select_lookahead_vars.empty()) { if (m_select_lookahead_vars.contains(x)) { - // IF_VERBOSE(1, verbose_stream() << x << " " << m_rating[x] << "\n";); m_candidates.push_back(candidate(x, m_rating[x])); sum += m_rating[x]; } @@ -309,7 +308,6 @@ namespace sat { sum += m_rating[x]; } } - IF_VERBOSE(1, verbose_stream() << " " << sum << " " << m_candidates.size() << "\n";); TRACE("sat", display_candidates(tout << "sum: " << sum << "\n");); return sum; } @@ -424,12 +422,9 @@ namespace sat { literal_vector::iterator it = m_binary[l.index()].begin(), end = m_binary[l.index()].end(); for (; it != end; ++it) { bool_var v = it->var(); - if (it->index() >= h.size()) - IF_VERBOSE(0, verbose_stream() << l << " " << *it << " " << h.size() << "\n";); if (is_undef(*it)) sum += h[it->index()]; // if (m_freevars.contains(it->var())) sum += h[it->index()]; } - // std::cout << "sum: " << sum << "\n"; watch_list& wlist = m_watches[l.index()]; watch_list::iterator wit = wlist.begin(), wend = wlist.end(); for (; wit != wend; ++wit) { @@ -930,7 +925,7 @@ namespace sat { } void lookahead::pop() { - if (m_assumptions.empty()) IF_VERBOSE(0, verbose_stream() << "empty pop\n";); + SASSERT(!m_assumptions.empty()); m_assumptions.pop_back(); m_inconsistent = false; SASSERT(m_search_mode == lookahead_mode::searching); diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 211b3b2bd..58873f517 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -23,7 +23,8 @@ def_module_params('sat', ('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'), - ('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'), ('threads', UINT, 1, 'number of parallel threads to use'), + ('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'), + ('threads', UINT, 1, 'number of parallel threads to use'), ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'), ('drat.file', SYMBOL, '', 'file to dump DRAT proofs'), ('drat.check', BOOL, False, 'build up internal proof and check'), diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 366e994ae..5e218f278 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -21,7 +21,6 @@ Revision History: #include"sat_simplifier.h" #include"sat_simplifier_params.hpp" #include"sat_solver.h" -#include"sat_lookahead.h" #include"stopwatch.h" #include"trace.h" diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 078acfb6e..c3b464716 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -60,7 +60,7 @@ namespace sat { init_reason_unknown(); updt_params(p); m_conflicts_since_gc = 0; - m_conflicts = 0; + m_conflicts_since_init = 0; m_next_simplify = 0; m_num_checkpoints = 0; } @@ -881,9 +881,9 @@ namespace sat { if (r != l_undef) return r; - if (m_conflicts > m_config.m_max_conflicts) { + if (m_conflicts_since_init > m_config.m_max_conflicts) { m_reason_unknown = "sat.max.conflicts"; - IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = " << m_conflicts << "\")\n";); + IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = " << m_conflicts_since_init << "\")\n";); return l_undef; } @@ -1194,7 +1194,7 @@ namespace sat { return l_true; if (!resolve_conflict()) return l_false; - if (m_conflicts > m_config.m_max_conflicts) + if (m_conflicts_since_init > m_config.m_max_conflicts) return l_undef; if (m_conflicts_since_restart > m_restart_threshold) return l_undef; @@ -1355,7 +1355,7 @@ namespace sat { m_luby_idx = 1; m_gc_threshold = m_config.m_gc_initial; m_restarts = 0; - m_conflicts = 0; + m_conflicts_since_init = 0; m_min_d_tk = 1.0; m_search_lvl = 0; m_stopwatch.reset(); @@ -1371,7 +1371,7 @@ namespace sat { */ void solver::simplify_problem() { - if (m_conflicts < m_next_simplify) { + if (m_conflicts_since_init < m_next_simplify) { return; } IF_VERBOSE(2, verbose_stream() << "(sat.simplify)\n";); @@ -1429,9 +1429,9 @@ namespace sat { m_next_simplify = m_config.m_restart_initial * m_config.m_simplify_mult1; } else { - m_next_simplify = static_cast(m_conflicts * m_config.m_simplify_mult2); - if (m_next_simplify > m_conflicts + m_config.m_simplify_max) - m_next_simplify = m_conflicts + m_config.m_simplify_max; + m_next_simplify = static_cast(m_conflicts_since_init * m_config.m_simplify_mult2); + if (m_next_simplify > m_conflicts_since_init + m_config.m_simplify_max) + m_next_simplify = m_conflicts_since_init + m_config.m_simplify_max; } } @@ -1882,7 +1882,7 @@ namespace sat { bool solver::resolve_conflict_core() { - m_conflicts++; + m_conflicts_since_init++; m_conflicts_since_restart++; m_conflicts_since_gc++; m_stats.m_conflict++; @@ -3551,8 +3551,8 @@ namespace sat { extract_fixed_consequences(num_units, asms, unfixed_vars, conseq); - if (m_conflicts > m_config.m_max_conflicts) { - IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = " << m_conflicts << "\")\n";); + if (m_conflicts_since_init > m_config.m_max_conflicts) { + IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = " << m_conflicts_since_init << "\")\n";); return l_undef; } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 9da445cad..0dcd9837f 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -358,7 +358,7 @@ namespace sat { literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars); protected: - unsigned m_conflicts; + unsigned m_conflicts_since_init; unsigned m_restarts; unsigned m_conflicts_since_restart; unsigned m_restart_threshold; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 4cff85510..5ba1fa136 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -323,7 +323,6 @@ public: IF_VERBOSE(0, verbose_stream() << "WARNING: could not handle " << mk_pp(c, m) << "\n";); } } - IF_VERBOSE(1, verbose_stream() << "vars: " << vars.size() << "\n";); if (vars.empty()) { return expr_ref(m.mk_true(), m); } @@ -336,15 +335,14 @@ public: return expr_ref(m.mk_true(), m); } expr_ref result(lit2expr[l.index()].get(), m); - IF_VERBOSE(1, verbose_stream() << "solution: " << l << " " << result << "\n";); return result; } virtual void get_lemmas(expr_ref_vector & lemmas) { - IF_VERBOSE(1, verbose_stream() << "(sat-get-lemmas " << lemmas.size() << ")\n";); if (!m_internalized) return; sat2goal s2g; goal g(m, false, false, false); s2g.get_learned(m_solver, m_map, m_params, lemmas); + IF_VERBOSE(1, verbose_stream() << "(sat :lemmas " << lemmas.size() << ")\n";); // TBD: handle externals properly. }