From d684d4fce0ab7e5521b9c0670ab7d3514cb3ca93 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 7 Feb 2018 15:57:25 -0800
Subject: [PATCH] dbl-max

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/ba_solver.cpp     | 10 +++++-----
 src/sat/sat_lookahead.cpp |  4 ++--
 src/sat/sat_lookahead.h   |  4 +++-
 3 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index f7b9e7749..517bd4593 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -1070,7 +1070,7 @@ namespace sat {
             m_overflow = true;
             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 {
@@ -1376,16 +1376,16 @@ namespace sat {
                 unsigned acoeff = get_abs_coeff(v);
                 if (lvl(lit) == m_conflict_lvl) {
                     if (m_lemma[0] == null_literal) {
-                        asserting_coeff = abs(coeff);
+                        asserting_coeff = std::abs(coeff);
                         slack -= asserting_coeff;
                         m_lemma[0] = ~lit;
                     }
                     else {
                         ++num_skipped;
-                        if (asserting_coeff < abs(coeff)) {
+                        if (asserting_coeff < std::abs(coeff)) {
                             m_lemma[0] = ~lit;
-                            slack -= (abs(coeff) - asserting_coeff);
-                            asserting_coeff = abs(coeff);
+                            slack -= (std::abs(coeff) - asserting_coeff);
+                            asserting_coeff = std::abs(coeff);
                         }
                     }
                 }
diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index 804f06341..cd3b0e19b 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -2082,7 +2082,7 @@ namespace sat {
             if (inconsistent()) {
                 TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";);
                 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();
                 if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false;                
                 continue;
@@ -2119,7 +2119,7 @@ namespace sat {
                 return l_undef;
             }
             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();
             if (inconsistent()) {
                 TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";);
diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h
index f81417d41..b86b7cb14 100644
--- a/src/sat/sat_lookahead.h
+++ b/src/sat/sat_lookahead.h
@@ -60,6 +60,8 @@ namespace sat {
         return out;
     }
 
+    const double dbl_max = 100000000.0;
+
     class lookahead {
         solver&    m_s;
         unsigned   m_num_vars;
@@ -186,7 +188,7 @@ namespace sat {
                 m_is_decision.reset(); 
                 m_cube.reset(); 
                 m_freevars_threshold = 0;
-                m_psat_threshold = 100000000.0;
+                m_psat_threshold = dbl_max;
                 reset_stats();
             }
             void reset_stats() { m_conflicts = 0; m_cutoffs = 0; }