From b3e5fade32564dd0d87095b95ec4369fd20e07f7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Dec 2017 11:22:50 -0800 Subject: [PATCH] remove cache reset that causes crash Signed-off-by: Nikolaj Bjorner --- src/ast/ast_translation.cpp | 8 ++------ src/sat/sat_asymm_branch.cpp | 37 ++++++++++++++++++++++++------------ src/sat/sat_asymm_branch.h | 2 ++ src/sat/sat_big.cpp | 30 ++++++++++++++++++++++------- src/sat/sat_big.h | 14 +++++++++++++- src/sat/sat_config.cpp | 1 + src/sat/sat_config.h | 1 + src/sat/sat_lookahead.cpp | 28 +++++++++++++++++++++++++++ src/sat/sat_lookahead.h | 2 ++ src/sat/sat_params.pyg | 1 + 10 files changed, 98 insertions(+), 26 deletions(-) diff --git a/src/ast/ast_translation.cpp b/src/ast/ast_translation.cpp index a57e5d194..b7ed86da5 100644 --- a/src/ast/ast_translation.cpp +++ b/src/ast/ast_translation.cpp @@ -48,14 +48,10 @@ void ast_translation::reset_cache() { void ast_translation::cache(ast * s, ast * t) { SASSERT(!m_cache.contains(s)); if (s->get_ref_count() > 1) { - if (m_insert_count > (1 << 17)) { - reset_cache(); - m_insert_count = 0; - } - m_cache.insert(s, t); - ++m_insert_count; m_from_manager.inc_ref(s); m_to_manager.inc_ref(t); + m_cache.insert(s, t); + ++m_insert_count; } } diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index 0d0e3a682..ee8e9db88 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -55,9 +55,11 @@ namespace sat { ~report() { m_watch.stop(); IF_VERBOSE(SAT_VB_LVL, - verbose_stream() << " (sat-asymm-branch :elim-literals " - << (m_asymm_branch.m_elim_literals - m_elim_literals) - << " :elim-learned-literals " << (m_asymm_branch.m_elim_learned_literals - m_elim_learned_literals) + unsigned num_learned = (m_asymm_branch.m_elim_learned_literals - m_elim_learned_literals); + unsigned num_total = (m_asymm_branch.m_elim_literals - m_elim_literals); + verbose_stream() + << " (sat-asymm-branch :elim-literals " << (num_total - num_learned) + << " :elim-learned-literals " << num_learned << " :hidden-tautologies " << (m_asymm_branch.m_hidden_tautologies - m_hidden_tautologies) << " :cost " << m_asymm_branch.m_counter << mem_stat() @@ -76,12 +78,15 @@ namespace sat { s.propagate(false); if (s.m_inconsistent) break; - std::cout << "elim: " << m_elim_literals - elim << "\n"; - if (m_elim_literals == elim) + unsigned num_elim = m_elim_literals - elim; + IF_VERBOSE(1, verbose_stream() << "(sat-asymm-branch-step :elim " << num_elim << ")\n";); + if (num_elim == 0) break; - } - std::cout << "elim-literals: " << m_elim_literals - elim0 << "\n"; - std::cout << "elim-learned-literals: " << m_elim_learned_literals - eliml0 << "\n"; + if (num_elim > 1000) + i = 0; + } + IF_VERBOSE(1, if (m_elim_learned_literals > eliml0) + verbose_stream() << "(sat-asymm-branch :elim " << m_elim_learned_literals - eliml0 << ")\n";); return m_elim_literals > elim0; } @@ -128,6 +133,16 @@ namespace sat { throw ex; } } + + void asymm_branch::operator()(big& big) { + s.propagate(false); + if (s.m_inconsistent) + return; + report rpt(*this); + svector saved_phase(s.m_phase); + process(&big); + s.m_phase = saved_phase; + } void asymm_branch::operator()(bool force) { ++m_calls; @@ -244,7 +259,6 @@ namespace sat { lemma[j++] = l; } } - // std::cout << lemma.size() << " -> " << j << "\n"; lemma.shrink(j); } } @@ -347,8 +361,7 @@ namespace sat { break; } } - new_sz = j; - // std::cout << "cleanup: " << c.id() << ": " << literal_vector(new_sz, c.begin()) << " delta: " << (c.size() - new_sz) << " " << skip_idx << " " << new_sz << "\n"; + new_sz = j; return re_attach(scoped_d, c, new_sz); } @@ -386,7 +399,7 @@ namespace sat { bool asymm_branch::process_sampled(big& big, clause & c) { scoped_detach scoped_d(s, c); sort(big, c); -#if 0 +#if 1 if (uhte(big, c)) { ++m_hidden_tautologies; scoped_d.del_clause(); diff --git a/src/sat/sat_asymm_branch.h b/src/sat/sat_asymm_branch.h index 6790bd963..226684c85 100644 --- a/src/sat/sat_asymm_branch.h +++ b/src/sat/sat_asymm_branch.h @@ -87,6 +87,8 @@ namespace sat { void operator()(bool force = false); + void operator()(big& big); + void updt_params(params_ref const & p); static void collect_param_descrs(param_descrs & d); diff --git a/src/sat/sat_big.cpp b/src/sat/sat_big.cpp index aa4a62745..5b32911f1 100644 --- a/src/sat/sat_big.cpp +++ b/src/sat/sat_big.cpp @@ -24,12 +24,8 @@ namespace sat { big::big() {} void big::init_big(solver& s, bool learned) { - m_num_vars = s.num_vars(); + init_adding_edges(s.num_vars()); unsigned num_lits = m_num_vars * 2; - m_dag.reset(); - m_roots.reset(); - m_dag.resize(num_lits, 0); - m_roots.resize(num_lits, true); literal_vector lits; SASSERT(num_lits == m_dag.size() && num_lits == m_roots.size()); for (unsigned l_idx = 0; l_idx < num_lits; l_idx++) { @@ -44,11 +40,31 @@ namespace sat { edges.push_back(v); } } + } + done_adding_edges(); + } + + void big::init_adding_edges(unsigned num_vars) { + m_num_vars = num_vars; + unsigned num_lits = m_num_vars * 2; + m_dag.reset(); + m_roots.reset(); + m_dag.resize(num_lits, 0); + m_roots.resize(num_lits, true); + } + + void big::add_edge(literal u, literal v) { + m_dag[u.index()].push_back(v); + } + + void big::done_adding_edges() { + for (auto& edges : m_dag) { shuffle(edges.size(), edges.c_ptr(), m_rand); } - init_dfs_num(learned); + init_dfs_num(); } + struct big::pframe { literal m_parent; literal m_child; @@ -58,7 +74,7 @@ namespace sat { literal parent() const { return m_parent; } }; - void big::init_dfs_num(bool learned) { + void big::init_dfs_num() { unsigned num_lits = m_num_vars * 2; m_left.reset(); m_right.reset(); diff --git a/src/sat/sat_big.h b/src/sat/sat_big.h index ca9f131eb..9896a3215 100644 --- a/src/sat/sat_big.h +++ b/src/sat/sat_big.h @@ -34,13 +34,24 @@ namespace sat { svector m_left, m_right; literal_vector m_root, m_parent; - void init_dfs_num(bool learned); + void init_dfs_num(); struct pframe; public: big(); + /** + \brief initialize a BIG from a solver. + */ void init_big(solver& s, bool learned); + + /** + \brief initialize a BIG externally by adding implications. + */ + void init_adding_edges(unsigned num_vars); + void add_edge(literal u, literal v); + void done_adding_edges(); + void ensure_big(solver& s, bool learned) { if (m_left.empty()) init_big(s, learned); } int get_left(literal l) const { return m_left[l.index()]; } int get_right(literal l) const { return m_right[l.index()]; } @@ -49,6 +60,7 @@ namespace sat { bool reaches(literal u, literal v) const { return m_left[u.index()] < m_left[v.index()] && m_right[v.index()] < m_right[u.index()]; } bool connected(literal u, literal v) const { return reaches(u, v) || reaches(~v, ~u); } void display(std::ostream& out) const; + }; }; diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 73bb94c7d..cf26fc09e 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -74,6 +74,7 @@ namespace sat { m_local_search_threads = p.local_search_threads(); m_lookahead_simplify = p.lookahead_simplify(); m_lookahead_simplify_bca = p.lookahead_simplify_bca(); + m_lookahead_simplify_asymm_branch = p.lookahead_simplify_asymm_branch(); if (p.lookahead_reward() == symbol("heule_schur")) m_lookahead_reward = heule_schur_reward; else if (p.lookahead_reward() == symbol("heuleu")) diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index da225c26b..c40266c93 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -92,6 +92,7 @@ namespace sat { bool m_local_search; bool m_lookahead_simplify; bool m_lookahead_simplify_bca; + bool m_lookahead_simplify_asymm_branch; cutoff_t m_lookahead_cube_cutoff; double m_lookahead_cube_fraction; unsigned m_lookahead_cube_depth; diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 9fc818014..29eaccb8e 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -2308,14 +2308,42 @@ namespace sat { elim_eqs elim(m_s); elim(roots, to_elim); + if (get_config().m_lookahead_simplify_asymm_branch) { + big_asymm_branch(); + } if (get_config().m_lookahead_simplify_bca) { add_hyper_binary(); } + } } m_lookahead.reset(); } + /** + \brief extract binary implication graph from learned binary clauses and use it + for strengthening clauses. + */ + + void lookahead::big_asymm_branch() { + unsigned num_lits = m_s.num_vars() * 2; + unsigned idx = 0; + big big; + big.init_adding_edges(m_s.num_vars()); + for (auto const& lits : m_binary) { + literal u = get_parent(to_literal(idx++)); + if (u == null_literal) continue; + for (literal v : lits) { + v = get_parent(v); + if (v != null_literal) + big.add_edge(u, v); + } + } + big.done_adding_edges(); + asymm_branch ab(m_s, m_s.m_params); + ab(big); + } + /** \brief reduction based on binary implication graph */ diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 3ebbfb7a5..75ce4fe6d 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -555,6 +555,8 @@ namespace sat { void add_hyper_binary(); + void big_asymm_branch(); + double psat_heur(); public: diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 672e22512..9d1585e7a 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -49,6 +49,7 @@ def_module_params('sat', ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'), ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'), ('lookahead_simplify.bca', BOOL, False, 'add learned binary clauses as part of lookahead simplification'), + ('lookahead_simplify.asymm_branch', BOOL, False, 'apply asymmetric branch simplification with lookahead simplifier'), ('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')))