mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-08 17:01:55 +00:00
Code Activity

allow incremental mode override

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-06 15:00:52 -08:00
parent 5813e22032
commit 303157d3b7
9 changed files with 34 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

31
src/sat/sat_simplifier.cpp
View file

@ -93,17 +93,28 @@ namespace sat {
bool simplifier::single_threaded() const { return s.m_config.m_num_threads == 1; }
bool simplifier::bce_enabled() const {
return !s.tracking_assumptions() &&
!m_learned_in_use_lists &&
m_num_calls >= m_bce_delay &&
return
!m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay &&
(m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls || cce_enabled());
}
bool simplifier::acce_enabled() const { return !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && m_acce; }
bool simplifier::cce_enabled() const { return !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && (m_cce || acce_enabled()); }
bool simplifier::abce_enabled() const { return !m_learned_in_use_lists && m_num_calls >= m_bce_delay && m_abce; }
bool simplifier::bca_enabled() const { return !s.tracking_assumptions() && m_bca && m_learned_in_use_lists && single_threaded(); }
bool simplifier::elim_vars_bdd_enabled() const { return !s.tracking_assumptions() && m_elim_vars_bdd && m_num_calls >= m_elim_vars_bdd_delay && single_threaded(); }
bool simplifier::elim_vars_enabled() const { return !s.tracking_assumptions() && m_elim_vars && single_threaded(); }
bool simplifier::acce_enabled() const {
return !m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && m_acce;
}
bool simplifier::cce_enabled() const {
return !m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && (m_cce || acce_enabled());
}
bool simplifier::abce_enabled() const {
return !m_incremental_mode && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && m_abce;
}
bool simplifier::bca_enabled() const {
return !m_incremental_mode && !s.tracking_assumptions() && m_bca && m_learned_in_use_lists && single_threaded();
}
bool simplifier::elim_vars_bdd_enabled() const {
return !m_incremental_mode && !s.tracking_assumptions() && m_elim_vars_bdd && m_num_calls >= m_elim_vars_bdd_delay && single_threaded();
}
bool simplifier::elim_vars_enabled() const {
return !m_incremental_mode && !s.tracking_assumptions() && m_elim_vars && single_threaded();
}
void simplifier::register_clauses(clause_vector & cs) {
std::stable_sort(cs.begin(), cs.end(), size_lt());
@ -199,6 +210,7 @@ namespace sat {
}
void simplifier::operator()(bool learned) {
if (s.inconsistent())
return;
if (!m_subsumption && !bce_enabled() && !bca_enabled() && !elim_vars_enabled())
@ -1883,6 +1895,7 @@ namespace sat {
m_elim_vars = p.elim_vars();
m_elim_vars_bdd = p.elim_vars_bdd();
m_elim_vars_bdd_delay = p.elim_vars_bdd_delay();
m_incremental_mode = s.get_config().m_incremental && !p.override_incremental();
}
void simplifier::collect_param_descrs(param_descrs & r) {