mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

dbl-max

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-02-07 15:57:25 -08:00
parent 42cc7c7f87
commit d684d4fce0
3 changed files with 10 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/sat/ba_solver.cpp
View file

@ -1070,7 +1070,7 @@ namespace sat {
m_overflow = true; m_overflow = true;
return UINT_MAX; return UINT_MAX;
} }
return static_cast<unsigned>(abs(c)); return static_cast<unsigned>(std::abs(c));
} }
int ba_solver::get_int_coeff(bool_var v) const { int ba_solver::get_int_coeff(bool_var v) const {
@ -1376,16 +1376,16 @@ namespace sat {
unsigned acoeff = get_abs_coeff(v); unsigned acoeff = get_abs_coeff(v);
if (lvl(lit) == m_conflict_lvl) { if (lvl(lit) == m_conflict_lvl) {
if (m_lemma[0] == null_literal) { if (m_lemma[0] == null_literal) {
asserting_coeff = abs(coeff); asserting_coeff = std::abs(coeff);
slack -= asserting_coeff; slack -= asserting_coeff;
m_lemma[0] = ~lit; m_lemma[0] = ~lit;
} }
else { else {
++num_skipped; ++num_skipped;
if (asserting_coeff < abs(coeff)) { if (asserting_coeff < std::abs(coeff)) {
m_lemma[0] = ~lit; m_lemma[0] = ~lit;
slack -= (abs(coeff) - asserting_coeff); slack -= (std::abs(coeff) - asserting_coeff);
asserting_coeff = abs(coeff); asserting_coeff = std::abs(coeff);
} }
} }
} }

4
src/sat/sat_lookahead.cpp
View file

@ -2082,7 +2082,7 @@ namespace sat {
if (inconsistent()) { if (inconsistent()) {
TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";); TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";);
m_cube_state.m_freevars_threshold = m_freevars.size(); m_cube_state.m_freevars_threshold = m_freevars.size();
m_cube_state.m_psat_threshold = m_config.m_cube_cutoff == adaptive_psat_cutoff ? psat_heur() : DBL_MAX; // MN. only compute PSAT if enabled m_cube_state.m_psat_threshold = m_config.m_cube_cutoff == adaptive_psat_cutoff ? psat_heur() : dbl_max; // MN. only compute PSAT if enabled
m_cube_state.inc_conflict(); m_cube_state.inc_conflict();
if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false; if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false;
continue; continue;
@ -2119,7 +2119,7 @@ namespace sat {
return l_undef; return l_undef;
} }
int prev_nfreevars = m_freevars.size(); int prev_nfreevars = m_freevars.size();
double prev_psat = m_config.m_cube_cutoff == adaptive_psat_cutoff ? psat_heur() : DBL_MAX; // MN. only compute PSAT if enabled double prev_psat = m_config.m_cube_cutoff == adaptive_psat_cutoff ? psat_heur() : dbl_max; // MN. only compute PSAT if enabled
literal lit = choose(); literal lit = choose();
if (inconsistent()) { if (inconsistent()) {
TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";); TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";);

4
src/sat/sat_lookahead.h
View file

@ -60,6 +60,8 @@ namespace sat {
return out; return out;
} }
const double dbl_max = 100000000.0;
class lookahead { class lookahead {
solver& m_s; solver& m_s;
unsigned m_num_vars; unsigned m_num_vars;
@ -186,7 +188,7 @@ namespace sat {
m_is_decision.reset(); m_is_decision.reset();
m_cube.reset(); m_cube.reset();
m_freevars_threshold = 0; m_freevars_threshold = 0;
m_psat_threshold = 100000000.0; m_psat_threshold = dbl_max;
reset_stats(); reset_stats();
} }
void reset_stats() { m_conflicts = 0; m_cutoffs = 0; } void reset_stats() { m_conflicts = 0; m_cutoffs = 0; }