From 7afbf8165ed403dd23e6510fa0c44feaad20158f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 12 Dec 2017 01:36:44 -0800 Subject: [PATCH] snapshot Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 9 - src/api/dotnet/Solver.cs | 24 +-- src/api/z3_api.h | 10 -- src/ast/rewriter/pb2bv_rewriter.cpp | 5 +- src/sat/sat_asymm_branch.cpp | 161 ++++++++++++------ src/sat/sat_asymm_branch.h | 10 ++ src/sat/sat_asymm_branch_params.pyg | 1 + src/sat/sat_config.cpp | 118 +++++-------- src/sat/sat_config.h | 14 +- src/sat/sat_elim_vars.cpp | 3 +- src/sat/sat_local_search.cpp | 38 ++--- src/sat/sat_lookahead.cpp | 73 ++------ src/sat/sat_params.pyg | 3 +- src/sat/sat_scc.h | 5 +- src/sat/sat_simplifier.cpp | 27 +-- src/sat/sat_simplifier.h | 1 + src/sat/sat_solver.cpp | 13 +- src/sat/sat_solver.h | 2 + src/sat/sat_solver/inc_sat_solver.cpp | 11 +- src/smt/smt_solver.cpp | 4 - src/solver/combined_solver.cpp | 6 - src/solver/solver.h | 6 - .../portfolio/bounded_int2bv_solver.cpp | 4 - src/tactic/portfolio/enum2bv_solver.cpp | 10 -- src/tactic/portfolio/pb2bv_solver.cpp | 4 - 25 files changed, 230 insertions(+), 332 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 8c2cbf25e..2805e7e2d 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -323,15 +323,6 @@ extern "C" { Z3_CATCH; } - void Z3_API Z3_solver_assert_lemma(Z3_context c, Z3_solver s, Z3_ast a) { - Z3_TRY; - LOG_Z3_solver_assert_lemma(c, s, a); - RESET_ERROR_CODE(); - init_solver(c, s); - CHECK_FORMULA(a,); - to_solver_ref(s)->assert_lemma(to_expr(a)); - Z3_CATCH; - } Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s) { Z3_TRY; diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index af5f8e47e..e136516e4 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -239,29 +239,6 @@ namespace Microsoft.Z3 Native.Z3_solver_from_string(Context.nCtx, NativeObject, str); } - /// - /// Assert a lemma (or multiple) into the solver. - /// - public void AssertLemma(params BoolExpr[] constraints) - { - Contract.Requires(constraints != null); - Contract.Requires(Contract.ForAll(constraints, c => c != null)); - - Context.CheckContextMatch(constraints); - foreach (BoolExpr a in constraints) - { - Native.Z3_solver_assert_lemma(Context.nCtx, NativeObject, a.NativeObject); - } - } - - /// - /// Assert a lemma (or multiple) into the solver. - /// - public void AddLemma(IEnumerable constraints) - { - AssertLemma(constraints.ToArray()); - } - /// /// The number of assertions in the solver. /// @@ -325,6 +302,7 @@ namespace Microsoft.Z3 return lboolToStatus(r); } + /// /// Retrieve fixed assignments to the set of variables in the form of consequences. /// Each consequence is an implication of the form diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 7f92501ec..b212912b9 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -6135,16 +6135,6 @@ extern "C" { */ void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p); - /** - \brief add a lemma. A lemma is a assumed to be a consequence of the current assertions. - Adding a lemma should therefore be a logical no-op. Solvers are free to ignore lemmas. - - \pre \c a must be a Boolean expression - - def_API('Z3_solver_assert_lemma', VOID, (_in(CONTEXT), _in(SOLVER), _in(AST))) - */ - void Z3_API Z3_solver_assert_lemma(Z3_context c, Z3_solver s, Z3_ast a); - /** \brief load solver assertions from a file. diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index 1e8cd7182..0a0fed292 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -319,9 +319,8 @@ struct pb2bv_rewriter::imp { sums.insert(sum); } } - uint_set::iterator it = sums.begin(), end = sums.end(); - for (; it != end; ++it) { - oc.push_back(*it); + for (unsigned u : sums) { + oc.push_back(u); } std::sort(oc.begin(), oc.end()); DEBUG_CODE( diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index 8e5e556e3..eb7be411a 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -42,9 +42,13 @@ namespace sat { asymm_branch & m_asymm_branch; stopwatch m_watch; unsigned m_elim_literals; + unsigned m_elim_learned_literals; + unsigned m_hidden_tautologies; report(asymm_branch & a): m_asymm_branch(a), - m_elim_literals(a.m_elim_literals) { + m_elim_literals(a.m_elim_literals), + m_elim_learned_literals(a.m_elim_learned_literals), + m_hidden_tautologies(a.m_hidden_tautologies) { m_watch.start(); } @@ -53,12 +57,35 @@ namespace sat { 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) + << " :hidden-tautologies " << (m_asymm_branch.m_hidden_tautologies - m_hidden_tautologies) << " :cost " << m_asymm_branch.m_counter << mem_stat() << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";); } }; + bool asymm_branch::process(scc* scc) { + unsigned elim0 = m_elim_literals; + unsigned eliml0 = m_elim_learned_literals; + for (unsigned i = 0; i < m_asymm_branch_rounds; ++i) { + unsigned elim = m_elim_literals; + if (scc) scc->init_big(true); + process(scc, s.m_clauses); + process(scc, s.m_learned); + s.propagate(false); + if (s.m_inconsistent) + break; + std::cout << "elim: " << m_elim_literals - elim << "\n"; + if (m_elim_literals == elim) + break; + } + std::cout << "elim-literals: " << m_elim_literals - elim0 << "\n"; + std::cout << "elim-learned-literals: " << m_elim_learned_literals - eliml0 << "\n"; + return m_elim_literals > elim0; + } + + void asymm_branch::process(scc* scc, clause_vector& clauses) { int64 limit = -m_asymm_branch_limit; std::stable_sort(clauses.begin(), clauses.end(), clause_size_lt()); @@ -119,26 +146,23 @@ namespace sat { TRACE("asymm_branch_detail", s.display(tout);); report rpt(*this); svector saved_phase(s.m_phase); - if (m_asymm_branch) { - m_counter = 0; - process(nullptr, s.m_clauses); - m_counter = -m_counter; - } - if (m_asymm_branch_sampled) { - scc scc(s, m_params); - while (true) { - unsigned elim = m_elim_literals; - scc.init_big(true); - process(&scc, s.m_clauses); - process(&scc, s.m_learned); - s.propagate(false); - if (s.m_inconsistent) - break; - std::cout << m_elim_literals - elim << "\n"; - if (m_elim_literals == elim) - break; + + bool change = true; + unsigned counter = 0; + while (change && counter < 2) { + ++counter; + change = false; + if (m_asymm_branch_sampled) { + scc sc(s, m_params); + if (process(&sc)) change = true; + } + if (m_asymm_branch) { + m_counter = 0; + if (process(nullptr)) change = true; + m_counter = -m_counter; } } + s.m_phase = saved_phase; m_asymm_branch_limit *= 2; if (m_asymm_branch_limit > UINT_MAX) @@ -172,8 +196,13 @@ namespace sat { }; void asymm_branch::sort(scc& scc, clause const& c) { + sort(scc, c.begin(), c.end()); + } + + void asymm_branch::sort(scc& scc, literal const* begin, literal const* end) { m_pos.reset(); m_neg.reset(); - for (literal l : c) { + for (; begin != end; ++begin) { + literal l = *begin; m_pos.push_back(l); m_neg.push_back(~l); } @@ -203,23 +232,42 @@ namespace sat { return false; } - bool asymm_branch::uhle(scoped_detach& scoped_d, scc& scc, clause & c) { - int right = scc.get_right(m_pos.back()); - m_to_delete.reset(); - for (unsigned i = m_pos.size() - 1; i-- > 0; ) { - literal lit = m_pos[i]; - SASSERT(scc.get_left(lit) < scc.get_left(last)); - int right2 = scc.get_right(lit); - if (right2 > right) { - // lit => last, so lit can be deleted - m_to_delete.push_back(lit); + void asymm_branch::minimize(scc& scc, literal_vector& lemma) { + scc.ensure_big(true); + sort(scc, lemma.begin(), lemma.end()); + uhle(scc); + if (!m_to_delete.empty()) { + unsigned j = 0; + for (unsigned i = 0; i < lemma.size(); ++i) { + literal l = lemma[i]; + if (!m_to_delete.contains(l)) { + lemma[j++] = l; + } } - else { - right = right2; + // std::cout << lemma.size() << " -> " << j << "\n"; + lemma.shrink(j); + } + } + + void asymm_branch::uhle(scc& scc) { + m_to_delete.reset(); + if (m_to_delete.empty()) { + int right = scc.get_right(m_pos.back()); + for (unsigned i = m_pos.size() - 1; i-- > 0; ) { + literal lit = m_pos[i]; + SASSERT(scc.get_left(lit) < scc.get_left(last)); + int right2 = scc.get_right(lit); + if (right2 > right) { + // lit => last, so lit can be deleted + m_to_delete.push_back(lit); + } + else { + right = right2; + } } } if (m_to_delete.empty()) { - right = scc.get_right(m_neg[0]); + int right = scc.get_right(m_neg[0]); for (unsigned i = 1; i < m_neg.size(); ++i) { literal lit = m_neg[i]; int right2 = scc.get_right(lit); @@ -232,20 +280,11 @@ namespace sat { } } } - if (!m_to_delete.empty()) { -#if 0 - std::cout << "delete " << m_to_delete << "\n"; + } - std::cout << "pos\n"; - for (literal l : m_pos) { - std::cout << l << ": " << scc.get_left(l) << " " << scc.get_right(l) << "\n"; - } - std::cout << "neg\n"; - for (literal l : m_neg) { - std::cout << l << ": " << scc.get_left(l) << " " << scc.get_right(l) << "\n"; - } - std::cout << "\n"; -#endif + bool asymm_branch::uhle(scoped_detach& scoped_d, scc& scc, clause & c) { + uhle(scc); + if (!m_to_delete.empty()) { unsigned j = 0; for (unsigned i = 0; i < c.size(); ++i) { if (!m_to_delete.contains(c[i])) { @@ -314,10 +353,13 @@ namespace sat { return re_attach(scoped_d, c, new_sz); } - bool asymm_branch::re_attach(scoped_detach& scoped_d, clause& c, unsigned new_sz) { - m_elim_literals += c.size() - new_sz; - switch(new_sz) { - case 0: + bool asymm_branch::re_attach(scoped_detach& scoped_d, clause& c, unsigned new_sz) { + m_elim_literals += c.size() - new_sz; + if (c.is_learned()) { + m_elim_learned_literals += c.size() - new_sz; + } + switch(new_sz) { + case 0: s.set_conflict(justification()); return false; case 1: @@ -329,7 +371,7 @@ namespace sat { return false; // check_missed_propagation() may fail, since m_clauses is not in a consistent state. case 2: SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef); - s.mk_bin_clause(c[0], c[1], false); + s.mk_bin_clause(c[0], c[1], c.is_learned()); scoped_d.del_clause(); SASSERT(s.m_qhead == s.m_trail.size()); return false; @@ -345,10 +387,13 @@ namespace sat { bool asymm_branch::process_sampled(scc& scc, clause & c) { scoped_detach scoped_d(s, c); sort(scc, c); +#if 0 if (uhte(scc, c)) { + ++m_hidden_tautologies; scoped_d.del_clause(); return false; } +#endif return uhle(scoped_d, scc, c); } @@ -381,7 +426,7 @@ namespace sat { // clause must not be used for propagation scoped_detach scoped_d(s, c); unsigned new_sz = c.size(); - unsigned flip_position = 2 + m_rand(c.size() - 2); // don't flip on the watch literals. + unsigned flip_position = m_rand(c.size()); bool found_conflict = flip_literal_at(c, flip_position, new_sz); SASSERT(!s.inconsistent()); SASSERT(s.scope_lvl() == 0); @@ -399,11 +444,12 @@ namespace sat { void asymm_branch::updt_params(params_ref const & _p) { sat_asymm_branch_params p(_p); - m_asymm_branch = p.asymm_branch(); - m_asymm_branch_delay = p.asymm_branch_delay(); + m_asymm_branch = p.asymm_branch(); + m_asymm_branch_rounds = p.asymm_branch_rounds(); + m_asymm_branch_delay = p.asymm_branch_delay(); m_asymm_branch_sampled = p.asymm_branch_sampled(); - m_asymm_branch_limit = p.asymm_branch_limit(); - m_asymm_branch_all = p.asymm_branch_all(); + m_asymm_branch_limit = p.asymm_branch_limit(); + m_asymm_branch_all = p.asymm_branch_all(); if (m_asymm_branch_limit > UINT_MAX) m_asymm_branch_limit = UINT_MAX; } @@ -414,10 +460,13 @@ namespace sat { void asymm_branch::collect_statistics(statistics & st) const { st.update("elim literals", m_elim_literals); + st.update("hidden tautologies", m_hidden_tautologies); } void asymm_branch::reset_statistics() { m_elim_literals = 0; + m_elim_learned_literals = 0; + m_hidden_tautologies = 0; } }; diff --git a/src/sat/sat_asymm_branch.h b/src/sat/sat_asymm_branch.h index 4510aaddf..14c37427e 100644 --- a/src/sat/sat_asymm_branch.h +++ b/src/sat/sat_asymm_branch.h @@ -39,6 +39,7 @@ namespace sat { // config bool m_asymm_branch; + unsigned m_asymm_branch_rounds; unsigned m_asymm_branch_delay; bool m_asymm_branch_sampled; bool m_asymm_branch_propagate; @@ -47,20 +48,27 @@ namespace sat { // stats unsigned m_elim_literals; + unsigned m_elim_learned_literals; + unsigned m_hidden_tautologies; literal_vector m_pos, m_neg; // literals (complements of literals) in clauses sorted by discovery time (m_left in scc). literal_vector m_to_delete; struct compare_left; + void sort(scc& scc, literal const* begin, literal const* end); void sort(scc & scc, clause const& c); bool uhle(scoped_detach& scoped_d, scc & scc, clause & c); + void uhle(scc & scc); + bool uhte(scc & scc, clause & c); bool re_attach(scoped_detach& scoped_d, clause& c, unsigned new_sz); + bool process(scc* scc); + bool process(clause & c); bool process_sampled(scc& scc, clause & c); @@ -86,6 +94,8 @@ namespace sat { void collect_statistics(statistics & st) const; void reset_statistics(); + void minimize(scc& scc, literal_vector& lemma); + void init_search() { m_calls = 0; } inline void dec(unsigned c) { m_counter -= c; } diff --git a/src/sat/sat_asymm_branch_params.pyg b/src/sat/sat_asymm_branch_params.pyg index a457220be..0fd19d500 100644 --- a/src/sat/sat_asymm_branch_params.pyg +++ b/src/sat/sat_asymm_branch_params.pyg @@ -2,6 +2,7 @@ def_module_params(module_name='sat', class_name='sat_asymm_branch_params', export=True, params=(('asymm_branch', BOOL, True, 'asymmetric branching'), + ('asymm_branch.rounds', UINT, 10, 'maximal number of rounds to run asymmetric branch simplifications if progress is made'), ('asymm_branch.delay', UINT, 1, 'number of simplification rounds to wait until invoking asymmetric branch simplification'), ('asymm_branch.sampled', BOOL, False, 'use sampling based asymmetric branching based on binary implication graph'), ('asymm_branch.limit', UINT, 100000000, 'approx. maximum number of literals visited during asymmetric branching'), diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index ed951fd93..940dc4e43 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -24,24 +24,8 @@ Revision History: namespace sat { - config::config(params_ref const & p): - m_restart_max(0), - m_always_true("always_true"), - m_always_false("always_false"), - m_caching("caching"), - m_random("random"), - m_geometric("geometric"), - m_luby("luby"), - m_dyn_psm("dyn_psm"), - m_psm("psm"), - m_glue("glue"), - m_glue_psm("glue_psm"), - m_psm_glue("psm_glue") { - m_num_threads = 1; - m_lookahead_simplify = false; - m_lookahead_simplify_bca = false; - m_elim_vars = false; - m_incremental = false; + config::config(params_ref const & p) { + m_incremental = false; // ad-hoc parameter updt_params(p); } @@ -50,21 +34,21 @@ namespace sat { m_max_memory = megabytes_to_bytes(p.max_memory()); symbol s = p.restart(); - if (s == m_luby) + if (s == symbol("luby")) m_restart = RS_LUBY; - else if (s == m_geometric) + else if (s == symbol("geometric")) m_restart = RS_GEOMETRIC; else throw sat_param_exception("invalid restart strategy"); s = p.phase(); - if (s == m_always_false) + if (s == symbol("always_false")) m_phase = PS_ALWAYS_FALSE; - else if (s == m_always_true) + else if (s == symbol("always_true")) m_phase = PS_ALWAYS_TRUE; - else if (s == m_caching) + else if (s == symbol("caching")) m_phase = PS_CACHING; - else if (s == m_random) + else if (s == symbol("random")) m_phase = PS_RANDOM; else throw sat_param_exception("invalid phase selection strategy"); @@ -90,24 +74,18 @@ namespace sat { m_local_search_threads = p.local_search_threads(); m_lookahead_simplify = p.lookahead_simplify(); m_lookahead_simplify_bca = p.lookahead_simplify_bca(); - if (p.lookahead_reward() == symbol("heule_schur")) { + if (p.lookahead_reward() == symbol("heule_schur")) m_lookahead_reward = heule_schur_reward; - } - else if (p.lookahead_reward() == symbol("heuleu")) { + else if (p.lookahead_reward() == symbol("heuleu")) m_lookahead_reward = heule_unit_reward; - } - else if (p.lookahead_reward() == symbol("ternary")) { + else if (p.lookahead_reward() == symbol("ternary")) m_lookahead_reward = ternary_reward; - } - else if (p.lookahead_reward() == symbol("unit")) { + else if (p.lookahead_reward() == symbol("unit")) m_lookahead_reward = unit_literal_reward; - } - else if (p.lookahead_reward() == symbol("march_cu")) { + else if (p.lookahead_reward() == symbol("march_cu")) m_lookahead_reward = march_cu_reward; - } - else { + else throw sat_param_exception("invalid reward type supplied: accepted heuristics are 'ternary', 'heuleu', 'unit' or 'heule_schur'"); - } m_lookahead_cube_fraction = p.lookahead_cube_fraction(); m_lookahead_cube_cutoff = p.lookahead_cube_cutoff(); @@ -120,29 +98,23 @@ namespace sat { // -------------------------------- s = p.gc(); - if (s == m_dyn_psm) { - m_gc_strategy = GC_DYN_PSM; - m_gc_initial = p.gc_initial(); - m_gc_increment = p.gc_increment(); - m_gc_small_lbd = p.gc_small_lbd(); - m_gc_k = p.gc_k(); - if (m_gc_k > 255) - m_gc_k = 255; - } - else { - if (s == m_glue_psm) - m_gc_strategy = GC_GLUE_PSM; - else if (s == m_glue) - m_gc_strategy = GC_GLUE; - else if (s == m_psm) - m_gc_strategy = GC_PSM; - else if (s == m_psm_glue) - m_gc_strategy = GC_PSM_GLUE; - else - throw sat_param_exception("invalid gc strategy"); - m_gc_initial = p.gc_initial(); - m_gc_increment = p.gc_increment(); - } + if (s == symbol("dyn_psm")) + m_gc_strategy = GC_DYN_PSM; + else if (s == symbol("glue_psm")) + m_gc_strategy = GC_GLUE_PSM; + else if (s == symbol("glue")) + m_gc_strategy = GC_GLUE; + else if (s == symbol("psm")) + m_gc_strategy = GC_PSM; + else if (s == symbol("psm_glue")) + m_gc_strategy = GC_PSM_GLUE; + else + throw sat_param_exception("invalid gc strategy"); + m_gc_initial = p.gc_initial(); + m_gc_increment = p.gc_increment(); + m_gc_small_lbd = p.gc_small_lbd(); + m_gc_k = std::min(255u, p.gc_k()); + m_minimize_lemmas = p.minimize_lemmas(); m_core_minimize = p.core_minimize(); m_core_minimize_partial = p.core_minimize_partial(); @@ -154,18 +126,15 @@ namespace sat { // Parameters used in Liang, Ganesh, Poupart, Czarnecki AAAI 2016. m_branching_heuristic = BH_VSIDS; - if (p.branching_heuristic() == symbol("vsids")) { + if (p.branching_heuristic() == symbol("vsids")) m_branching_heuristic = BH_VSIDS; - } - else if (p.branching_heuristic() == symbol("chb")) { + else if (p.branching_heuristic() == symbol("chb")) m_branching_heuristic = BH_CHB; - } - else if (p.branching_heuristic() == symbol("lrb")) { + else if (p.branching_heuristic() == symbol("lrb")) m_branching_heuristic = BH_LRB; - } - else { + else throw sat_param_exception("invalid branching heuristic: accepted heuristics are 'vsids', 'lrb' or 'chb'"); - } + m_anti_exploration = p.branching_anti_exploration(); m_step_size_init = 0.40; m_step_size_dec = 0.000001; @@ -177,21 +146,16 @@ namespace sat { // PB parameters s = p.pb_solver(); - if (s == symbol("circuit")) { + if (s == symbol("circuit")) m_pb_solver = PB_CIRCUIT; - } - else if (s == symbol("sorting")) { + else if (s == symbol("sorting")) m_pb_solver = PB_SORTING; - } - else if (s == symbol("totalizer")) { + else if (s == symbol("totalizer")) m_pb_solver = PB_TOTALIZER; - } - else if (s == symbol("solver")) { + else if (s == symbol("solver")) m_pb_solver = PB_SOLVER; - } - else { + else throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting"); - } sat_simplifier_params sp(_p); m_elim_vars = sp.elim_vars(); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index c3018ef29..b2ccb8a1f 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -101,6 +101,7 @@ namespace sat { unsigned m_gc_increment; unsigned m_gc_small_lbd; unsigned m_gc_k; + bool m_gc_burst; bool m_minimize_lemmas; bool m_dyn_sub_res; @@ -110,20 +111,7 @@ namespace sat { symbol m_drat_file; bool m_drat_check_unsat; bool m_drat_check_sat; - - symbol m_always_true; - symbol m_always_false; - symbol m_caching; - symbol m_random; - symbol m_geometric; - symbol m_luby; - symbol m_dyn_psm; - symbol m_psm; - symbol m_glue; - symbol m_glue_psm; - symbol m_psm_glue; - pb_solver m_pb_solver; // branching heuristic settings. diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp index 5dd3ed1f7..7e803eaa5 100644 --- a/src/sat/sat_elim_vars.cpp +++ b/src/sat/sat_elim_vars.cpp @@ -87,6 +87,7 @@ namespace sat{ simp.m_neg_cls.reset(); simp.collect_clauses(pos_l, simp.m_pos_cls, false); simp.collect_clauses(neg_l, simp.m_neg_cls, false); + VERIFY(!s.is_external(v)); model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v); simp.save_clauses(mc_entry, simp.m_pos_cls); simp.save_clauses(mc_entry, simp.m_neg_cls); @@ -99,7 +100,7 @@ namespace sat{ pos_occs.reset(); neg_occs.reset(); literal_vector lits; - add_clauses(b, lits); + add_clauses(b, lits); return true; } diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index 3a9e48182..726fda7f4 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -301,12 +301,10 @@ namespace sat { for (unsigned l_idx = 0; l_idx < sz; ++l_idx) { literal l1 = ~to_literal(l_idx); watch_list const & wlist = s.m_watches[l_idx]; - watch_list::const_iterator it = wlist.begin(); - watch_list::const_iterator end = wlist.end(); - for (; it != end; ++it) { - if (!it->is_binary_unblocked_clause()) + for (watched const& w : wlist) { + if (!w.is_binary_unblocked_clause()) continue; - literal l2 = it->get_literal(); + literal l2 = w.get_literal(); if (l1.index() > l2.index()) continue; literal ls[2] = { l1, l2 }; @@ -316,11 +314,8 @@ namespace sat { } // copy clauses - clause_vector::const_iterator it = s.m_clauses.begin(); - clause_vector::const_iterator end = s.m_clauses.end(); - for (; it != end; ++it) { - clause& c = *(*it); - add_clause(c.size(), c.begin()); + for (clause* c : s.m_clauses) { + add_clause(c->size(), c->begin()); } m_num_non_binary_clauses = s.m_clauses.size(); @@ -568,12 +563,11 @@ namespace sat { best_var = v = l.var(); bool tt = cur_solution(v); coeff_vector const& falsep = m_vars[v].m_watch[!tt]; - coeff_vector::const_iterator it = falsep.begin(), end = falsep.end(); - for (; it != end; ++it) { - int slack = constraint_slack(it->m_constraint_id); + for (pbcoeff const& pbc : falsep) { + int slack = constraint_slack(pbc.m_constraint_id); if (slack < 0) ++best_bsb; - else if (slack < static_cast(it->m_coeff)) + else if (slack < static_cast(pbc.m_coeff)) best_bsb += num_unsat; } ++cit; @@ -583,7 +577,7 @@ namespace sat { v = l.var(); unsigned bsb = 0; coeff_vector const& falsep = m_vars[v].m_watch[!cur_solution(v)]; - coeff_vector::const_iterator it = falsep.begin(), end = falsep.end(); + auto it = falsep.begin(), end = falsep.end(); for (; it != end; ++it) { int slack = constraint_slack(it->m_constraint_id); if (slack < 0) { @@ -637,22 +631,20 @@ namespace sat { coeff_vector const& truep = m_vars[flipvar].m_watch[flip_is_true]; coeff_vector const& falsep = m_vars[flipvar].m_watch[!flip_is_true]; - coeff_vector::const_iterator it = truep.begin(), end = truep.end(); - for (; it != end; ++it) { - unsigned ci = it->m_constraint_id; + for (auto const& pbc : truep) { + unsigned ci = pbc.m_constraint_id; constraint& c = m_constraints[ci]; int old_slack = c.m_slack; - c.m_slack -= it->m_coeff; + c.m_slack -= pbc.m_coeff; if (c.m_slack < 0 && old_slack >= 0) { // from non-negative to negative: sat -> unsat unsat(ci); } } - it = falsep.begin(), end = falsep.end(); - for (; it != end; ++it) { - unsigned ci = it->m_constraint_id; + for (auto const& pbc : falsep) { + unsigned ci = pbc.m_constraint_id; constraint& c = m_constraints[ci]; int old_slack = c.m_slack; - c.m_slack += it->m_coeff; + c.m_slack += pbc.m_coeff; if (c.m_slack >= 0 && old_slack < 0) { // from negative to non-negative: unsat -> sat sat(ci); } diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 843c70fd8..ef9c0aedf 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -2254,7 +2254,7 @@ namespace sat { init(); if (inconsistent()) return; inc_istamp(); - literal l = choose(); + literal l = choose(); if (inconsistent()) return; SASSERT(m_trail_lim.empty()); unsigned num_units = 0; @@ -2266,7 +2266,7 @@ namespace sat { ++num_units; } } - IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :units " << num_units << ")\n";); + IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :units " << num_units << " :propagations " << m_stats.m_propagations << ")\n";); if (m_s.inconsistent()) return; @@ -2315,16 +2315,8 @@ namespace sat { void lookahead::add_hyper_binary() { unsigned num_lits = m_s.num_vars() * 2; + unsigned num_bins = 0; -#if 0 - std::cout << "binary trail size: " << m_binary_trail.size() << "\n"; - std::cout << "Are windfalls still on the trail at base level?\n"; -#endif - - unsigned disconnected1 = 0; - unsigned disconnected2 = 0; - -#if 1 typedef std::pair u_pair; hashtable, default_eq > imp; for (unsigned idx = 0; idx < num_lits; ++idx) { @@ -2355,14 +2347,16 @@ namespace sat { literal_vector const& lits = m_binary[idx]; for (unsigned sz = bin_size[idx]; sz > 0; --sz) { literal v = lits[lits.size() - sz]; - if (v != get_parent(v)) continue; - if (m_s.was_eliminated(v.var())) continue; - if (imp.contains(std::make_pair(u.index(), v.index()))) continue; - if (scc.reaches(u, v)) continue; - candidates.push_back(std::make_pair(u, v)); + if (v == get_parent(v) && + !m_s.was_eliminated(v.var()) && + !imp.contains(std::make_pair(u.index(), v.index())) && + !scc.reaches(u, v)) { + candidates.push_back(std::make_pair(u, v)); + } } } - for (unsigned i = 0; i < 5; ++i) { + + for (unsigned count = 0; count < 5; ++count) { scc.init_big(true); unsigned k = 0; union_find_default_ctx ufctx; @@ -2373,7 +2367,7 @@ namespace sat { literal v = candidates[j].second; if (!scc.reaches(u, v)) { if (uf.find(u.index()) != uf.find(v.index())) { - ++disconnected1; + ++num_bins; uf.merge(u.index(), v.index()); uf.merge((~u).index(), (~v).index()); VERIFY(!m_s.was_eliminated(u.var())); @@ -2389,48 +2383,11 @@ namespace sat { std::cout << candidates.size() << " -> " << k << "\n"; if (k == candidates.size()) break; candidates.shrink(k); + if (k == 0) break; } - - std::cout << "candidates: " << candidates.size() << "\n"; - -#endif - -#if 0 - union_find_default_ctx ufctx; - union_find uf(ufctx); - for (unsigned i = 0; i < num_lits; ++i) uf.mk_var(); - for (unsigned idx = 0; idx < num_lits; ++idx) { - literal u = get_parent(to_literal(idx)); - if (null_literal != u) { - for (watched const& w : m_s.m_watches[idx]) { - if (!w.is_binary_clause()) continue; - literal v = get_parent(w.get_literal()); - if (null_literal != v) { - uf.merge(u.index(), v.index()); - } - } - } - } - - for (unsigned i = 0; i < m_binary.size(); ++i) { - literal u = to_literal(i); - if (u == get_parent(u) && !m_s.was_eliminated(u.var())) { - for (literal v : m_binary[i]) { - if (v == get_parent(v) && - !m_s.was_eliminated(v.var()) && - uf.find(u.index()) != uf.find(v.index())) { - ++disconnected2; - uf.merge(u.index(), v.index()); - // m_s.mk_clause(~u, v, true); - } - } - } - } -#endif - IF_VERBOSE(10, verbose_stream() << "(sat-lookahead :bca " << disconnected1 << " " << disconnected2 << ")\n";); - //IF_VERBOSE(10, verbose_stream() << "(sat-lookahead :bca " << disconnected << ")\n";); - //m_stats.m_bca += disconnected; + IF_VERBOSE(10, verbose_stream() << "(sat-lookahead :bca " << num_bins << ")\n";); + m_stats.m_bca += num_bins; } void lookahead::normalize_parents() { diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index e8ae53dca..fde5f1272 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -18,10 +18,11 @@ def_module_params('sat', ('burst_search', UINT, 100, 'number of conflicts before first global simplification'), ('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts'), ('gc', SYMBOL, 'glue_psm', 'garbage collection strategy: psm, glue, glue_psm, dyn_psm'), - ('gc.initial', UINT, 20000, 'learned clauses garbage collection frequence'), + ('gc.initial', UINT, 20000, 'learned clauses garbage collection frequency'), ('gc.increment', UINT, 500, 'increment to the garbage collection threshold'), ('gc.small_lbd', UINT, 3, 'learned clauses with small LBD are never deleted (only used in dyn_psm)'), ('gc.k', UINT, 7, 'learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm)'), + ('gc.burst', BOOL, True, 'perform eager garbage collection during initialization'), ('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'), diff --git a/src/sat/sat_scc.h b/src/sat/sat_scc.h index 2973245a3..84858ca27 100644 --- a/src/sat/sat_scc.h +++ b/src/sat/sat_scc.h @@ -51,6 +51,8 @@ namespace sat { struct pframe; + bool reaches_aux(literal u, literal v) const { return m_left[u.index()] < m_left[v.index()] && m_right[v.index()] < m_right[u.index()]; } + public: scc(solver & s, params_ref const & p); @@ -66,11 +68,12 @@ namespace sat { \brief create binary implication graph and associated data-structures to check transitivity. */ void init_big(bool learned); + void ensure_big(bool learned) { if (m_left.empty()) init_big(learned); } int get_left(literal l) const { return m_left[l.index()]; } int get_right(literal l) const { return m_right[l.index()]; } literal get_parent(literal l) const { return m_parent[l.index()]; } literal get_root(literal l) const { return m_root[l.index()]; } - 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 reaches(literal u, literal v) const { return reaches_aux(u, v) || reaches_aux(~v, ~u); } }; }; diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 283083237..87218b735 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -77,6 +77,7 @@ namespace sat { inline bool simplifier::is_external(bool_var v) const { return s.is_assumption(v) || + (s.is_external(v) && s.is_incremental()) || (s.is_external(v) && s.m_ext && (!m_ext_use_list.get(literal(v, false)).empty() || !m_ext_use_list.get(literal(v, true)).empty())); @@ -154,6 +155,7 @@ namespace sat { else { remove_clause(c); } + } inline void simplifier::unblock_clause(clause & c) { @@ -1354,6 +1356,7 @@ namespace sat { void prepare_block_clause(clause& c, literal l, model_converter::entry*& new_entry, model_converter::kind k) { TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";); + VERIFY(!s.is_external(l)); if (new_entry == 0 && !s.m_retain_blocked_clauses) new_entry = &(mc.mk(k, l.var())); m_to_remove.push_back(&c); @@ -1365,20 +1368,22 @@ namespace sat { } void block_clause(clause& c, literal l, model_converter::entry *& new_entry) { + SASSERT(!s.is_external(l.var())); prepare_block_clause(c, l, new_entry, model_converter::BLOCK_LIT); - if (!s.m_retain_blocked_clauses) - mc.insert(*new_entry, c); + mc.insert(*new_entry, c); } void block_covered_clause(clause& c, literal l, model_converter::kind k) { + SASSERT(!s.is_external(l.var())); model_converter::entry * new_entry = 0; prepare_block_clause(c, l, new_entry, k); - if (!s.m_retain_blocked_clauses) - mc.insert(*new_entry, m_covered_clause, m_elim_stack); + mc.insert(*new_entry, m_covered_clause, m_elim_stack); } void prepare_block_binary(watch_list::iterator it, literal l1, literal blocked, model_converter::entry*& new_entry, model_converter::kind k) { - if (new_entry == 0 && !s.m_retain_blocked_clauses) + SASSERT(!s.is_external(blocked)); + VERIFY(!s.is_external(blocked)); + if (new_entry == 0) new_entry = &(mc.mk(k, blocked.var())); literal l2 = it->get_literal(); TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l1 << "\n";); @@ -1394,15 +1399,13 @@ namespace sat { void block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) { prepare_block_binary(it, l, l, new_entry, model_converter::BLOCK_LIT); - if (!s.m_retain_blocked_clauses) - mc.insert(*new_entry, l, it->get_literal()); + mc.insert(*new_entry, l, it->get_literal()); } void block_covered_binary(watch_list::iterator it, literal l, literal blocked, model_converter::kind k) { model_converter::entry * new_entry = 0; prepare_block_binary(it, l, blocked, new_entry, k); - if (!s.m_retain_blocked_clauses) - mc.insert(*new_entry, m_covered_clause, m_elim_stack); + mc.insert(*new_entry, m_covered_clause, m_elim_stack); } void bca() { @@ -1779,6 +1782,7 @@ namespace sat { // eliminate variable ++s.m_stats.m_elim_var_res; + VERIFY(!s.is_external(v)); model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v); save_clauses(mc_entry, m_pos_cls); save_clauses(mc_entry, m_neg_cls); @@ -1867,7 +1871,10 @@ namespace sat { checkpoint(); if (m_elim_counter < 0) break; - if (try_eliminate(v)) { + if (is_external(v)) { + // skip + } + else if (try_eliminate(v)) { m_num_elim_vars++; } else if (elim_vars_bdd_enabled() && elim_bdd(v)) { diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index 0acb78ce1..75703e34b 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -163,6 +163,7 @@ namespace sat { void cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists); bool is_external(bool_var v) const; + bool is_external(literal l) const { return is_external(l.var()); } bool was_eliminated(bool_var v) const; lbool value(bool_var v) const; lbool value(literal l) const; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index b3fc95f47..d4a57a9b1 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -904,6 +904,11 @@ namespace sat { propagate(false); if (check_inconsistent()) return l_false; cleanup(); + if (m_config.m_gc_burst) { + // force gc + m_conflicts_since_gc = m_gc_threshold + 1; + gc(); + } if (m_config.m_max_conflicts > 0 && m_config.m_burst_search > 0) { m_restart_threshold = m_config.m_burst_search; lbool r = bounded_search(); @@ -1326,6 +1331,7 @@ namespace sat { void solver::add_assumption(literal lit) { m_assumption_set.insert(lit); m_assumptions.push_back(lit); + VERIFY(is_external(lit.var())); } void solver::pop_assumption() { @@ -1438,14 +1444,12 @@ namespace sat { CASSERT("sat_simplify_bug", check_invariant()); } - if (m_config.m_lookahead_simplify) { lookahead lh(*this); lh.simplify(); lh.collect_statistics(m_aux_stats); } - sort_watch_lits(); CASSERT("sat_simplify_bug", check_invariant()); @@ -1585,6 +1589,8 @@ namespace sat { } for (literal l : m_assumptions) { if (value_at(l, m) != l_true) { + VERIFY(is_external(l.var())); + IF_VERBOSE(0, verbose_stream() << l << " does not model check " << value_at(l, m) << "\n";); TRACE("sat", tout << l << " does not model check\n"; tout << "trail: " << m_trail << "\n"; @@ -1641,7 +1647,7 @@ namespace sat { void solver::gc() { if (m_conflicts_since_gc <= m_gc_threshold) return; - IF_VERBOSE(1, verbose_stream() << "gc\n";); + IF_VERBOSE(10, verbose_stream() << "(sat.gc)\n";); CASSERT("sat_gc_bug", check_invariant()); switch (m_config.m_gc_strategy) { case GC_GLUE: @@ -2099,6 +2105,7 @@ namespace sat { pop_reinit(m_scope_lvl - new_scope_lvl); TRACE("sat_conflict_detail", tout << new_scope_lvl << "\n"; display(tout);); + // unsound: m_asymm_branch.minimize(m_scc, m_lemma); clause * lemma = mk_clause_core(m_lemma.size(), m_lemma.c_ptr(), true); if (lemma) { lemma->set_glue(glue); diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 135d9e067..37290940d 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -263,6 +263,7 @@ namespace sat { unsigned num_clauses() const; unsigned num_restarts() const { return m_restarts; } bool is_external(bool_var v) const { return m_external[v] != 0; } + bool is_external(literal l) const { return is_external(l.var()); } void set_external(bool_var v); void set_non_external(bool_var v); bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; } @@ -305,6 +306,7 @@ namespace sat { bool canceled() { return !m_rlimit.inc(); } config const& get_config() const { return m_config; } void set_incremental(bool b) { m_config.m_incremental = b; } + bool is_incremental() const { return m_config.m_incremental; } extension* get_extension() const { return m_ext.get(); } void set_extension(extension* e); bool set_root(literal l, literal r); diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 1eee15893..9e185e6fa 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -251,15 +251,6 @@ public: } } - virtual void assert_lemma(expr* e) { - dep2asm_t dep2asm; - goal_ref g = alloc(goal, m, true, false); // models, maybe cores are enabled - for (unsigned i = m_fmls_head ; i < m_fmls.size(); ++i) { - g->assert_expr(m_fmls[i].get()); - } - VERIFY(l_undef != internalize_goal(g, dep2asm, true)); - } - virtual ast_manager& get_manager() const { return m; } virtual void assert_expr_core(expr * t) { m_internalized = false; @@ -526,7 +517,7 @@ private: m_pc = g->pc(); m_mc = g->mc(); TRACE("sat", g->display_with_dependencies(tout);); - m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, false, is_lemma); + m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, m_solver.get_config().m_incremental, is_lemma); m_goal2sat.get_interpreted_atoms(atoms); if (!atoms.empty()) { std::stringstream strm; diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 68312c6a9..01ea61fd9 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -114,10 +114,6 @@ namespace smt { m_name2assertion.insert(a, t); } - virtual void assert_lemma(expr* t) { - // no-op - } - virtual void push_core() { m_context.push(); } diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index 90a6cb7c8..29f6a32f1 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -180,12 +180,6 @@ public: m_solver2->assert_expr(t, a); } - virtual void assert_lemma(expr* t) { - m_solver1->assert_lemma(t); - if (m_solver2_initialized) - m_solver2->assert_lemma(t); - } - virtual void push() { switch_inc_mode(); m_solver1->push(); diff --git a/src/solver/solver.h b/src/solver/solver.h index 2b1824cd3..7a51725a2 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -104,12 +104,6 @@ public: virtual void assert_expr_core(expr * t, expr * a) = 0; - /** - \brief Add a lemma to the assertion stack. A lemma is assumed to be a consequence of already - asserted formulas. The solver is free to ignore lemmas. - */ - virtual void assert_lemma(expr * t) {} - /** \brief Create a backtracking point. */ diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp index 0eb5cef18..b8a8f6704 100644 --- a/src/tactic/portfolio/bounded_int2bv_solver.cpp +++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp @@ -105,10 +105,6 @@ public: } } - virtual void assert_lemma(expr * t) { - m_solver->assert_lemma(t); - } - virtual void push_core() { flush_assertions(); m_solver->push(); diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp index 9c522a714..ffb51fe2e 100644 --- a/src/tactic/portfolio/enum2bv_solver.cpp +++ b/src/tactic/portfolio/enum2bv_solver.cpp @@ -68,16 +68,6 @@ public: m_solver->assert_expr(bounds); } - virtual void assert_lemma(expr* t) { - expr_ref tmp(t, m); - expr_ref_vector bounds(m); - proof_ref tmp_proof(m); - m_rewriter(t, tmp, tmp_proof); - m_solver->assert_lemma(tmp); - m_rewriter.flush_side_constraints(bounds); - m_solver->assert_expr(bounds); - } - virtual void push_core() { m_rewriter.push(); m_solver->push(); diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp index 96656ef00..cb5327443 100644 --- a/src/tactic/portfolio/pb2bv_solver.cpp +++ b/src/tactic/portfolio/pb2bv_solver.cpp @@ -62,10 +62,6 @@ public: m_assertions.push_back(t); } - virtual void assert_lemma(expr * t) { - m_solver->assert_lemma(t); - } - virtual void push_core() { flush_assertions(); m_rewriter.push();