From 921423ec8032eeacba091b82f0e3e3b13ae7d616 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 12 Dec 2017 10:43:23 -0800 Subject: [PATCH] fix model conversions for incremental SAT, fix lookahead with ba_solver 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_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 | 78 +++--------- src/sat/sat_params.pyg | 13 +- 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 - .../portfolio/bounded_int2bv_solver.cpp | 4 - src/tactic/portfolio/enum2bv_solver.cpp | 10 -- src/tactic/portfolio/pb2bv_solver.cpp | 4 - 20 files changed, 119 insertions(+), 274 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_config.cpp b/src/sat/sat_config.cpp index 660337071..361e15d91 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'"); - } if (p.lookahead_cube_cutoff() == symbol("depth")) { m_lookahead_cube_cutoff = depth_cutoff; @@ -142,29 +120,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(); @@ -176,18 +148,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; @@ -199,21 +168,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 f66c0dbdf..da225c26b 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -114,6 +114,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; @@ -123,20 +124,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 ec1bf23f2..f58339922 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -683,7 +683,7 @@ namespace sat { // NB. u.index() > l.index() iff u.index() > (~l).index(). // since indices for the same boolean variables occupy // two adjacent numbers. - if (u.index() > l.index() && is_stamped(u)) { + if (u.index() > l.index() && is_stamped(u) && ~l != u) { add_arc(~l, ~u); add_arc( u, l); } @@ -692,7 +692,8 @@ namespace sat { lits.reset(); if (w.is_ext_constraint() && m_s.m_ext->is_extended_binary(w.get_ext_constraint_idx(), lits)) { for (literal u : lits) { - if (u.index() > l.index() && is_stamped(u)) { + // u is positive in lits, l is negative: + if (~l != u && u.index() > l.index() && is_stamped(u)) { add_arc(~l, ~u); add_arc( u, l); } @@ -2291,7 +2292,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; @@ -2303,7 +2304,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; @@ -2352,16 +2353,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) { @@ -2392,14 +2385,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; @@ -2410,7 +2405,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())); @@ -2426,48 +2421,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 4432c0b16..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'), @@ -37,14 +38,8 @@ def_module_params('sat', ('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'), ('local_search', BOOL, False, 'use local search instead of CDCL'), ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'), - ('lookahead.cube.cutoff', SYMBOL, 'adaptive_freevars', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'), - ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive_freevars or adaptive_psat'), - ('lookahead.cube.depth', UINT, 10, 'cut-off depth to create cubes. Used when lookahead.cube.cutoff is depth.'), - ('lookahead.cube.freevars', DOUBLE, 0.8, 'cube free fariable fraction. Used when lookahead.cube.cutoff is freevars'), - ('lookahead.cube.psat.var_exp', DOUBLE, 1, 'free variable exponent for PSAT cutoff'), - ('lookahead.cube.psat.clause_base', DOUBLE, 2, 'clause base for PSAT cutoff'), - ('lookahead.cube.psat.trigger', DOUBLE, 5, 'trigger value to create lookahead cubes for PSAT cutoff. Used when lookahead.cube.cutoff is psat'), - ('lookahead_search', BOOL, False, 'use lookahead solver'), + ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead_cube is true'), + ('lookahead.cube.cutoff', UINT, 10, 'cut-off depth to create cubes. Only enabled when non-zero. Used when lookahead_cube is true.'), ('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'), 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/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();