From 885d640301b9687d30c7e569cd8dd9d64eb9762b Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 19 Mar 2019 14:58:23 -0700
Subject: [PATCH] make explicit rational(double)constructor

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/util/lp/lp_core_solver_base.h |  2 +-
 src/util/lp/lp_solver_def.h       |  2 +-
 src/util/lp/scaler_def.h          | 16 ++++++++--------
 src/util/rational.h               |  2 +-
 4 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/util/lp/lp_core_solver_base.h b/src/util/lp/lp_core_solver_base.h
index c1b8aa987..46f683c91 100644
--- a/src/util/lp/lp_core_solver_base.h
+++ b/src/util/lp/lp_core_solver_base.h
@@ -214,7 +214,7 @@ public:
             if (m_A.m_columns[bj].size() > 1)
                 return true;
             for (const auto & c : m_A.m_columns[bj]) {
-                if (m_A.get_val(c) != one_of_type<mpq>())
+                if (m_A.get_val(c) != one_of_type<T>())
                     return true;
                 else
                     break;
diff --git a/src/util/lp/lp_solver_def.h b/src/util/lp/lp_solver_def.h
index 21a86efba..d18333161 100644
--- a/src/util/lp/lp_solver_def.h
+++ b/src/util/lp/lp_solver_def.h
@@ -561,7 +561,7 @@ template <typename T, typename X> void lp_solver<T, X>::set_scaled_cost(unsigned
     column_info<T> * ci = this->m_map_from_var_index_to_column_info[this->m_core_solver_columns_to_external_columns[j]];
     T cost = ci->get_cost();
     if (ci->is_flipped()){
-        cost *= -1;
+        cost *= T(-1);
     }
     lp_assert(ci->is_fixed() == false);
     this->m_costs[j] = cost * this->m_column_scale[j];
diff --git a/src/util/lp/scaler_def.h b/src/util/lp/scaler_def.h
index 4c9784a43..489f42c56 100644
--- a/src/util/lp/scaler_def.h
+++ b/src/util/lp/scaler_def.h
@@ -221,15 +221,15 @@ template <typename T, typename X>    void scaler<T, X>::scale_row(unsigned i) {
     }
     if (row_max < m_scaling_minimum) {
         do {
-            alpha *= 2;
-            row_max *= 2;
+            alpha *= T(2);
+            row_max *= T(2);
         } while (row_max < m_scaling_minimum);
         m_A.multiply_row(i, alpha);
         m_b[i] *= alpha;
     } else if (row_max > m_scaling_maximum) {
         do {
-            alpha /= 2;
-            row_max /= 2;
+            alpha /= T(2);
+            row_max /= T(2);
         } while (row_max > m_scaling_maximum);
         m_A.multiply_row(i, alpha);
         m_b[i] *= alpha;
@@ -245,13 +245,13 @@ template <typename T, typename X>    void scaler<T, X>::scale_column(unsigned i)
     }
     if (column_max < m_scaling_minimum) {
         do {
-            alpha *= 2;
-            column_max *= 2;
+            alpha *= T(2);
+            column_max *= T(2);
         } while (column_max < m_scaling_minimum);
     } else if (column_max > m_scaling_maximum) {
         do {
-            alpha /= 2;
-            column_max /= 2;
+            alpha /= T(2);
+            column_max /= T(2);
         } while (column_max > m_scaling_maximum);
     } else {
         return;
diff --git a/src/util/rational.h b/src/util/rational.h
index bf68c0bf6..f343ee019 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -53,7 +53,7 @@ public:
 
     rational(mpz const & z) { m().set(m_val, z); }
 
-    rational(double  z) { UNREACHABLE(); }
+    explicit rational(double  z) { UNREACHABLE(); }
     
     explicit rational(char const * v) { m().set(m_val, v); }