mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
bug fixes in uninitialized variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
d7f9a3b37d
commit
6f273e7b8f
|
@ -29,6 +29,7 @@ namespace sat {
|
|||
m_counter(0) {
|
||||
updt_params(p);
|
||||
reset_statistics();
|
||||
m_calls = 0;
|
||||
}
|
||||
|
||||
struct clause_size_lt {
|
||||
|
@ -57,6 +58,9 @@ namespace sat {
|
|||
};
|
||||
|
||||
void asymm_branch::operator()(bool force) {
|
||||
++m_calls;
|
||||
if (m_calls <= 1)
|
||||
return;
|
||||
if (!m_asymm_branch && !m_asymm_branch_all)
|
||||
return;
|
||||
s.propagate(false); // must propagate, since it uses s.push()
|
||||
|
|
|
@ -33,7 +33,8 @@ namespace sat {
|
|||
solver & s;
|
||||
int64 m_counter;
|
||||
random_gen m_rand;
|
||||
|
||||
unsigned m_calls;
|
||||
|
||||
// config
|
||||
bool m_asymm_branch;
|
||||
bool m_asymm_branch_all;
|
||||
|
@ -63,6 +64,8 @@ namespace sat {
|
|||
void collect_statistics(statistics & st) const;
|
||||
void reset_statistics();
|
||||
|
||||
void init_search() { m_calls = 0; }
|
||||
|
||||
inline void dec(unsigned c) { m_counter -= c; }
|
||||
};
|
||||
|
||||
|
|
|
@ -104,7 +104,7 @@ namespace sat {
|
|||
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;
|
||||
return !m_incremental_mode && !s.tracking_assumptions() && !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();
|
||||
|
@ -1868,6 +1868,7 @@ namespace sat {
|
|||
m_cce = p.cce();
|
||||
m_acce = p.acce();
|
||||
m_bca = p.bca();
|
||||
m_abce = p.abce();
|
||||
m_bce_delay = p.bce_delay();
|
||||
m_elim_blocked_clauses = p.elim_blocked_clauses();
|
||||
m_elim_blocked_clauses_at = p.elim_blocked_clauses_at();
|
||||
|
|
|
@ -1422,6 +1422,7 @@ namespace sat {
|
|||
m_next_simplify = 0;
|
||||
m_min_d_tk = 1.0;
|
||||
m_search_lvl = 0;
|
||||
m_asymm_branch.init_search();
|
||||
m_stopwatch.reset();
|
||||
m_stopwatch.start();
|
||||
m_core.reset();
|
||||
|
|
Loading…
Reference in a new issue