From 683eed0c1e29dc79a3a0dca7ea76f6491d93013a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 21 Jan 2020 11:15:13 -0600
Subject: [PATCH] use get_sign

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/nlsat/nlsat_evaluator.cpp | 14 +++++++-------
 src/util/lp/int_solver.cpp    | 28 +++++++++++++++-------------
 2 files changed, 22 insertions(+), 20 deletions(-)

diff --git a/src/nlsat/nlsat_evaluator.cpp b/src/nlsat/nlsat_evaluator.cpp
index 25013f6db..980701aef 100644
--- a/src/nlsat/nlsat_evaluator.cpp
+++ b/src/nlsat/nlsat_evaluator.cpp
@@ -226,7 +226,7 @@ namespace nlsat {
             }
             
             // Return the sign idx of pinfo
-            ::sign sign(poly_info const & pinfo, unsigned i) const {
+            ::sign get_sign(poly_info const & pinfo, unsigned i) const {
                 return m_poly_signs[pinfo.m_first_sign + i];
             }
             
@@ -243,19 +243,19 @@ namespace nlsat {
                         else if (section_cell_id > c)
                             break;
                     }
-                    return sign(pinfo, i);
+                    return get_sign(pinfo, i);
                 }
                 else {
                     if (num_roots == 0)
-                        return sign(pinfo, 0);
+                        return get_sign(pinfo, 0);
                     unsigned root_1_cell_id = cell_id(pinfo, 0);
                     unsigned root_n_cell_id = cell_id(pinfo, num_roots - 1);
                     if (c < root_1_cell_id)
-                        return sign(pinfo, 0);
+                        return get_sign(pinfo, 0);
                     else if (c == root_1_cell_id || c == root_n_cell_id)
                         return sign_zero;
                     else if (c > root_n_cell_id)
-                        return sign(pinfo, num_roots);
+                        return get_sign(pinfo, num_roots);
                     int low  = 0;
                     int high = num_roots-1;
                     while (true) {
@@ -265,7 +265,7 @@ namespace nlsat {
                         if (high == low + 1) {
                             SASSERT(cell_id(pinfo, low) < c);
                             SASSERT(c < cell_id(pinfo, low+1));
-                            return sign(pinfo, low+1);
+                            return get_sign(pinfo, low+1);
                         }
                         SASSERT(high > low + 1);
                         int mid   = low + ((high - low)/2);
@@ -381,7 +381,7 @@ namespace nlsat {
            
            \pre All variables of p are assigned in the current interpretation.
         */
-        sign eval_sign(poly * p) {
+        ::sign eval_sign(poly * p) {
             // TODO: check if it is useful to cache results
             SASSERT(m_assignment.is_assigned(max_var(p)));
             return m_am.eval_sign_at(polynomial_ref(p, m_pm), m_assignment);
diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp
index 0d25a9d11..e5a28182e 100644
--- a/src/util/lp/int_solver.cpp
+++ b/src/util/lp/int_solver.cpp
@@ -285,6 +285,7 @@ lia_move int_solver::run_gcd_test() {
         TRACE("int_solver", tout << "gcd-test " << settings().st().m_gcd_calls << "\n";);
         if (!gcd_test()) {
             settings().st().m_gcd_conflicts++;
+            TRACE("gcd_test", tout << "gcd conflict\n";);
             return lia_move::conflict;
         }
     }
@@ -404,29 +405,30 @@ lia_move int_solver::hnf_cut() {
 lia_move int_solver::check() {
     if (!has_inf_int()) return lia_move::sat;
 
+#define CHECK_RET(fn)                                                   \
+    r = fn;                                                             \
+    if (r != lia_move::undef) { TRACE("int_solver", tout << #fn << "\n";); return r; }
+
     m_t.clear();
     m_k.reset();
     m_ex.clear();
     m_upper = false;
-    lia_move r = run_gcd_test();
-    if (r != lia_move::undef) return r;
+    lia_move r;
+
+    CHECK_RET(run_gcd_test());
 
     check_return_helper pc(m_lar_solver, r);
 
-    if(settings().m_int_pivot_fixed_vars_from_basis)
+    if (settings().m_int_pivot_fixed_vars_from_basis)
         m_lar_solver->pivot_fixed_vars_from_basis();
 
-    r = patch_nbasic_columns();
-    if (r != lia_move::undef) return r;
+    CHECK_RET(patch_nbasic_columns());
     ++m_number_of_calls;
-    r = find_cube();
-    if (r != lia_move::undef) return r;
-    
-    r = hnf_cut();
-    if (r != lia_move::undef) return r;
-    
-    r = gomory_cut();
-    return (r == lia_move::undef)? branch_or_sat() : r;
+    CHECK_RET(find_cube());        
+    CHECK_RET(hnf_cut());    
+    CHECK_RET(gomory_cut());
+    CHECK_RET(branch_or_sat());
+    return r;
 }
 
 lia_move int_solver::branch_or_sat() {