mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

improve incremental use of sat solver: carry over simplification threshold

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-08-24 12:47:57 -07:00
parent d67a73820d
commit aa695f6a6c
1 changed files with 16 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/sat/sat_solver.cpp
View file

@ -50,6 +50,7 @@ namespace sat {
m_params(p) { m_params(p) {
m_config.updt_params(p); m_config.updt_params(p);
m_conflicts_since_gc = 0; m_conflicts_since_gc = 0;
m_conflicts = 0;
m_next_simplify = 0; m_next_simplify = 0;
m_num_checkpoints = 0; m_num_checkpoints = 0;
} }
@ -742,8 +743,7 @@ namespace sat {
// iff3_finder(*this)(); // iff3_finder(*this)();
simplify_problem(); simplify_problem();
if (check_inconsistent()) return l_false; if (check_inconsistent()) return l_false;
m_next_simplify = m_config.m_restart_initial * m_config.m_simplify_mult1;
if (m_config.m_max_conflicts == 0) { if (m_config.m_max_conflicts == 0) {
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"abort: max-conflicts = 0\"\n";); IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"abort: max-conflicts = 0\"\n";);
@ -763,13 +763,8 @@ namespace sat {
} }
restart(); restart();
if (m_conflicts >= m_next_simplify) { simplify_problem();
simplify_problem(); if (check_inconsistent()) return l_false;
if (check_inconsistent()) return l_false;
m_next_simplify = static_cast<unsigned>(m_conflicts * m_config.m_simplify_mult2);
if (m_next_simplify > m_conflicts + m_config.m_simplify_max)
m_next_simplify = m_conflicts + m_config.m_simplify_max;
}
gc(); gc();
} }
} }
@ -955,7 +950,6 @@ namespace sat {
void solver::init_search() { void solver::init_search() {
m_phase_counter = 0; m_phase_counter = 0;
m_phase_cache_on = false; m_phase_cache_on = false;
m_conflicts = 0;
m_conflicts_since_restart = 0; m_conflicts_since_restart = 0;
m_restart_threshold = m_config.m_restart_initial; m_restart_threshold = m_config.m_restart_initial;
m_luby_idx = 1; m_luby_idx = 1;
@ -972,6 +966,9 @@ namespace sat {
*/ */
void solver::simplify_problem() { void solver::simplify_problem() {
if (m_conflicts < m_next_simplify) {
return;
}
// Disable simplification during MUS computation. // Disable simplification during MUS computation.
// if (m_mus.is_active()) return; // if (m_mus.is_active()) return;
@ -1016,6 +1013,15 @@ namespace sat {
TRACE("sat", display(tout << "consistent: " << (!inconsistent()) << "\n");); TRACE("sat", display(tout << "consistent: " << (!inconsistent()) << "\n"););
reinit_assumptions(); reinit_assumptions();
if (m_next_simplify == 0) {
m_next_simplify = m_config.m_restart_initial * m_config.m_simplify_mult1;
}
else {
m_next_simplify = static_cast<unsigned>(m_conflicts * m_config.m_simplify_mult2);
if (m_next_simplify > m_conflicts + m_config.m_simplify_max)
m_next_simplify = m_conflicts + m_config.m_simplify_max;
}
} }
void solver::sort_watch_lits() { void solver::sort_watch_lits() {