diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 369b3c7dd..347800d19 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -942,6 +942,7 @@ namespace sat { } literal next() { SASSERT(!empty()); return to_literal(m_queue.erase_min()); } bool empty() const { return m_queue.empty(); } + void reset() { m_queue.reset(); } }; simplifier & s; @@ -1042,7 +1043,7 @@ namespace sat { m_to_remove.reset(); clause_use_list & occs = s.m_use_list.get(l); clause_use_list::iterator it = occs.mk_iterator(); - while (!it.at_end()) { + for (; !it.at_end(); it.next()) { clause & c = it.curr(); if (c.is_blocked()) continue; m_counter -= c.size(); @@ -1052,8 +1053,7 @@ namespace sat { block_clause(c, l, new_entry); s.m_num_blocked_clauses++; } - s.unmark_all(c); - it.next(); + s.unmark_all(c); } for (clause* c : m_to_remove) s.block_clause(*c); @@ -1083,7 +1083,7 @@ namespace sat { } clause_use_list & neg_occs = s.m_use_list.get(~l); clause_use_list::iterator it = neg_occs.mk_iterator(); - while (!it.at_end()) { + for (; !it.at_end(); it.next()) { bool tautology = false; clause & c = it.curr(); if (c.is_blocked()) continue; @@ -1110,7 +1110,6 @@ namespace sat { if (j == 0) return false; } } - it.next(); } return first; } @@ -1204,12 +1203,12 @@ namespace sat { } void cce() { + insert_queue(); cce_clauses(); cce_binary(); } void cce_binary() { - insert_queue(); while (!m_queue.empty() && m_counter >= 0) { s.checkpoint(); process_cce_binary(m_queue.next()); @@ -1309,6 +1308,7 @@ namespace sat { } void bca() { + m_queue.reset(); insert_queue(); while (!m_queue.empty() && m_counter >= 0) { s.checkpoint(); @@ -1360,7 +1360,7 @@ namespace sat { clause_use_list & neg_occs = s.m_use_list.get(~l); clause_use_list::iterator it = neg_occs.mk_iterator(); - while (!it.at_end()) { + for (; !it.at_end(); it.next()) { clause & c = it.curr(); if (c.is_blocked()) continue; m_counter -= c.size(); @@ -1372,7 +1372,6 @@ namespace sat { } if (i == sz) return false; - it.next(); } if (s.s.m_ext) { diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 53383a7c2..144b6b86c 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -69,10 +69,11 @@ class inc_sat_solver : public solver { bool m_internalized; // are formulas internalized? bool m_internalized_converted; // have internalized formulas been converted back expr_ref_vector m_internalized_fmls; // formulas in internalized format + bool m_incremental_mode; typedef obj_map dep2asm_t; public: - inc_sat_solver(ast_manager& m, params_ref const& p): + inc_sat_solver(ast_manager& m, params_ref const& p, bool incremental_mode): m(m), m_solver(p, m.limit()), m_params(p), @@ -86,7 +87,8 @@ public: m_unknown("no reason given"), m_internalized(false), m_internalized_converted(false), - m_internalized_fmls(m) { + m_internalized_fmls(m), + m_incremental_mode(incremental_mode) { updt_params(p); init_preprocess(); } @@ -99,7 +101,7 @@ public: } ast_translation tr(m, dst_m); m_solver.pop_to_base_level(); - inc_sat_solver* result = alloc(inc_sat_solver, dst_m, p); + inc_sat_solver* result = alloc(inc_sat_solver, dst_m, p, m_incremental_mode); result->m_solver.copy(m_solver); result->m_fmls_head = m_fmls_head; for (expr* f : m_fmls) result->m_fmls.push_back(tr(f)); @@ -271,7 +273,10 @@ public: virtual void updt_params(params_ref const & p) { m_params.append(p); sat_params p1(p); - m_params.set_bool("elim_vars", false); + if (m_incremental_mode) { + m_params.set_bool("elim_vars", false); + m_params.set_uint("elim_blocked_clauses_at", UINT_MAX); + } m_params.set_bool("keep_cardinality_constraints", p1.cardinality_solver()); m_params.set_bool("keep_pb_constraints", m_solver.get_config().m_pb_solver == sat::PB_SOLVER); m_params.set_bool("pb_num_system", m_solver.get_config().m_pb_solver == sat::PB_SORTING); @@ -848,8 +853,8 @@ private: }; -solver* mk_inc_sat_solver(ast_manager& m, params_ref const& p) { - return alloc(inc_sat_solver, m, p); +solver* mk_inc_sat_solver(ast_manager& m, params_ref const& p, bool incremental_mode) { + return alloc(inc_sat_solver, m, p, incremental_mode); } diff --git a/src/sat/sat_solver/inc_sat_solver.h b/src/sat/sat_solver/inc_sat_solver.h index 658c0583d..fb4b05b91 100644 --- a/src/sat/sat_solver/inc_sat_solver.h +++ b/src/sat/sat_solver/inc_sat_solver.h @@ -22,7 +22,7 @@ Notes: #include "solver/solver.h" -solver* mk_inc_sat_solver(ast_manager& m, params_ref const& p); +solver* mk_inc_sat_solver(ast_manager& m, params_ref const& p, bool incremental_mode = true); void inc_sat_display(std::ostream& out, solver& s, unsigned sz, expr*const* soft, rational const* _weights); diff --git a/src/tactic/portfolio/fd_solver.cpp b/src/tactic/portfolio/fd_solver.cpp index daecb6c9c..946b3b30c 100644 --- a/src/tactic/portfolio/fd_solver.cpp +++ b/src/tactic/portfolio/fd_solver.cpp @@ -25,8 +25,8 @@ Notes: #include "tactic/portfolio/bounded_int2bv_solver.h" #include "solver/solver2tactic.h" -solver * mk_fd_solver(ast_manager & m, params_ref const & p) { - solver* s = mk_inc_sat_solver(m, p); +solver * mk_fd_solver(ast_manager & m, params_ref const & p, bool incremental_mode) { + solver* s = mk_inc_sat_solver(m, p, incremental_mode); s = mk_enum2bv_solver(m, p, s); s = mk_pb2bv_solver(m, p, s); s = mk_bounded_int2bv_solver(m, p, s); @@ -34,5 +34,5 @@ solver * mk_fd_solver(ast_manager & m, params_ref const & p) { } tactic * mk_fd_tactic(ast_manager & m, params_ref const& p) { - return mk_solver2tactic(mk_fd_solver(m, p)); + return mk_solver2tactic(mk_fd_solver(m, p, false)); } diff --git a/src/tactic/portfolio/fd_solver.h b/src/tactic/portfolio/fd_solver.h index b54ba74f4..1e107ac20 100644 --- a/src/tactic/portfolio/fd_solver.h +++ b/src/tactic/portfolio/fd_solver.h @@ -25,7 +25,7 @@ Notes: class solver; class tactic; -solver * mk_fd_solver(ast_manager & m, params_ref const & p); +solver * mk_fd_solver(ast_manager & m, params_ref const & p, bool incremental_mode = true); tactic * mk_fd_tactic(ast_manager & m, params_ref const & p); /*