From a4dc68766db8a07676ce3cb4f0842558d46e94a6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 29 Nov 2017 17:16:15 -0800 Subject: [PATCH] preparing for more efficient asymmetric branching Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 2 +- src/sat/sat_asymm_branch.cpp | 42 +++++++++++++++------------ src/sat/sat_asymm_branch.h | 2 ++ src/sat/sat_config.cpp | 2 ++ src/sat/sat_config.h | 2 ++ src/sat/sat_lookahead.cpp | 9 ++++++ src/sat/sat_params.pyg | 1 + src/sat/sat_solver.cpp | 2 ++ src/sat/sat_solver.h | 4 +-- src/tactic/aig/aig.cpp | 6 ++-- src/tactic/portfolio/pb2bv_solver.cpp | 2 +- 11 files changed, 47 insertions(+), 27 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 9819af47f..f15386a93 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6335,7 +6335,7 @@ class Solver(Z3PPObject): def from_string(self, s): """Parse assertions from a string""" - Z3_solver_from_string(self.ctx.ref(), self.solver, filename) + Z3_solver_from_string(self.ctx.ref(), self.solver, s) def assertions(self): """Return an AST vector containing all added constraints. diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index abf1d95be..aed29312a 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -56,25 +56,8 @@ namespace sat { << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";); } }; - - void asymm_branch::operator()(bool force) { - ++m_calls; - if (m_calls <= 1) - return; - if (!m_asymm_branch && !m_asymm_branch_all) - return; - s.propagate(false); // must propagate, since it uses s.push() - if (s.m_inconsistent) - return; - if (!force && m_counter > 0) { - m_counter /= 100; - return; - } - CASSERT("asymm_branch", s.check_invariant()); - TRACE("asymm_branch_detail", s.display(tout);); - report rpt(*this); - svector saved_phase(s.m_phase); - m_counter = 0; + + void asymm_branch::process(clause_vector& clauses) { int64 limit = -m_asymm_branch_limit; std::stable_sort(s.m_clauses.begin(), s.m_clauses.end(), clause_size_lt()); m_counter -= s.m_clauses.size(); @@ -114,6 +97,27 @@ namespace sat { m_counter = -m_counter; throw ex; } + } + + void asymm_branch::operator()(bool force) { + ++m_calls; + if (m_calls <= 1) + return; + if (!m_asymm_branch && !m_asymm_branch_all) + return; + s.propagate(false); // must propagate, since it uses s.push() + if (s.m_inconsistent) + return; + if (!force && m_counter > 0) { + m_counter /= 100; + return; + } + CASSERT("asymm_branch", s.check_invariant()); + TRACE("asymm_branch_detail", s.display(tout);); + report rpt(*this); + svector saved_phase(s.m_phase); + m_counter = 0; + process(s.m_clauses); m_counter = -m_counter; s.m_phase = saved_phase; m_asymm_branch_limit *= 2; diff --git a/src/sat/sat_asymm_branch.h b/src/sat/sat_asymm_branch.h index a6e44a4e2..0de4c8d99 100644 --- a/src/sat/sat_asymm_branch.h +++ b/src/sat/sat_asymm_branch.h @@ -44,6 +44,8 @@ namespace sat { unsigned m_elim_literals; bool process(clause & c); + + void process(clause_vector & c); bool process_all(clause & c); diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index b672fe065..24d2bca9b 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -176,6 +176,8 @@ namespace sat { m_reward_multiplier = 0.9; m_reward_offset = 1000000.0; + m_variable_decay = p.variable_decay(); + // PB parameters s = p.pb_solver(); if (s == symbol("circuit")) { diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 132b85b24..9a20bbc63 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -95,6 +95,8 @@ namespace sat { double m_simplify_mult2; unsigned m_simplify_max; + unsigned m_variable_decay; + gc_strategy m_gc_strategy; unsigned m_gc_initial; unsigned m_gc_increment; diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index fbd237339..306912b57 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -2303,7 +2303,16 @@ namespace sat { */ void lookahead::add_hyper_binary() { + + std::cout << "binary trail size: " << m_binary_trail.size() << "\n"; + std::cout << "Are windfalls still on the trail at base level?\n"; unsigned num_lits = m_s.num_vars() * 2; + unsigned_vector bin_size(num_lits); + for (unsigned idx : m_binary_trail) { + bin_size[idx]++; + } + + union_find_default_ctx ufctx; union_find uf(ufctx); for (unsigned i = 0; i < num_lits; ++i) uf.mk_var(); diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 887cea2a7..4f65b100b 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -9,6 +9,7 @@ def_module_params('sat', ('restart.initial', UINT, 100, 'initial restart (number of conflicts)'), ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'), ('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'), ('branching.heuristic', SYMBOL, 'vsids', 'branching heuristic vsids, lrb or chb'), ('branching.anti_exploration', BOOL, False, 'apply anti-exploration heuristic for branch selection'), diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index e4d239605..89acdc408 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1415,6 +1415,7 @@ namespace sat { m_next_simplify = 0; m_min_d_tk = 1.0; m_search_lvl = 0; + m_conflicts_since_gc = 0; m_asymm_branch.init_search(); m_stopwatch.reset(); m_stopwatch.start(); @@ -1660,6 +1661,7 @@ namespace sat { void solver::gc() { if (m_conflicts_since_gc <= m_gc_threshold) return; + IF_VERBOSE(1, verbose_stream() << "gc\n";); CASSERT("sat_gc_bug", check_invariant()); switch (m_config.m_gc_strategy) { case GC_GLUE: diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 45f91e7a8..0d65de1e1 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -575,8 +575,8 @@ namespace sat { } void decay_activity() { - m_activity_inc *= 11; - m_activity_inc /= 10; + m_activity_inc *= m_config.m_variable_decay; + m_activity_inc /= 100; } private: diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp index e8226e159..067e7445e 100644 --- a/src/tactic/aig/aig.cpp +++ b/src/tactic/aig/aig.cpp @@ -635,10 +635,8 @@ struct aig_manager::imp { } bool check_cache() const { - obj_map::iterator it = m_cache.begin(); - obj_map::iterator end = m_cache.end(); - for (; it != end; ++it) { - SASSERT(ref_count(it->m_value) > 0); + for (auto const& kv : m_cache) { + SASSERT(ref_count(kv.m_value) > 0); } return true; } diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp index e22a41ad3..96656ef00 100644 --- a/src/tactic/portfolio/pb2bv_solver.cpp +++ b/src/tactic/portfolio/pb2bv_solver.cpp @@ -50,7 +50,7 @@ public: virtual solver* translate(ast_manager& dst_m, params_ref const& p) { flush_assertions(); solver* result = alloc(pb2bv_solver, dst_m, p, m_solver->translate(dst_m, p)); - model_converter_ref mc = concat(mc0(), m_solver->get_model_converter().get()); + model_converter_ref mc = mc0(); if (mc) { ast_translation tr(m, dst_m); result->set_model_converter(mc->translate(tr));