From 2b2f016f968e449392bb98632d28c0276619f0d1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 14 Aug 2019 15:44:25 -0700
Subject: [PATCH] python for accessing lambda, switch to theory branching for
 QF_LRA

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_setup.cpp               | 7 ++++---
 src/smt/theory_lra.cpp              | 9 +++------
 src/util/lp/bound_analyzer_on_row.h | 5 ++++-
 src/util/lp/stacked_vector.h        | 6 +++---
 4 files changed, 14 insertions(+), 13 deletions(-)

diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 54038ce64..96e6f6552 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -409,7 +409,7 @@ namespace smt {
         m_params.m_nnf_cnf          = false;
         m_params.m_arith_eq_bounds  = true;
         m_params.m_arith_eq2ineq    = true;
-        m_params.m_phase_selection  = PS_ALWAYS_FALSE;
+        // m_params.m_phase_selection  = PS_THEORY;
         m_params.m_restart_strategy = RS_GEOMETRIC;
         m_params.m_restart_factor   = 1.5;
         m_params.m_restart_adaptive = false;
@@ -442,7 +442,7 @@ namespace smt {
             }
         }
         m_params.m_arith_eq_bounds  = true;
-        m_params.m_phase_selection  = PS_ALWAYS_FALSE;
+        // m_params.m_phase_selection  = PS_THEORY;
         m_params.m_restart_strategy = RS_GEOMETRIC;
         m_params.m_restart_factor   = 1.5;
         m_params.m_restart_adaptive = false;
@@ -456,13 +456,14 @@ namespace smt {
     }
 
     void setup::setup_QF_LRA() {
-        TRACE("setup", tout << "setup_QF_LRA(st)\n";);
+        TRACE("setup", tout << "setup_QF_LRA()\n";);
         m_params.m_relevancy_lvl       = 0;
         m_params.m_arith_eq2ineq       = true;
         m_params.m_arith_reflect       = false;
         m_params.m_arith_propagate_eqs = false;
         m_params.m_eliminate_term_ite  = true;
         m_params.m_nnf_cnf             = false;
+        m_params.m_phase_selection       = PS_THEORY;
         setup_lra_arith();
     }
 
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 6fc9d9497..6011436b2 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -944,10 +944,6 @@ public:
         if (!m_bool_var2bound.find(v, b)) {
             return l_undef;
         }
-        scoped_internalize_state st(*this);
-        st.vars().push_back(b->get_var());
-        st.coeffs().push_back(rational::one());
-        init_left_side(st);
         lp::lconstraint_kind k = lp::EQ;
         switch (b->get_bound_kind()) {
         case lp_api::lower_t:
@@ -956,10 +952,11 @@ public:
         case lp_api::upper_t:
             k = lp::LE;
             break;
+        default:
+            break;
         }         
         auto vi = get_var_index(b->get_var());
-        rational bound = b->get_value();
-        return m_solver->compare_values(vi, k, bound) ? l_true : l_false;
+        return m_solver->compare_values(vi, k, b->get_value()) ? l_true : l_false;
     }
 
     void new_eq_eh(theory_var v1, theory_var v2) {
diff --git a/src/util/lp/bound_analyzer_on_row.h b/src/util/lp/bound_analyzer_on_row.h
index a20b4850a..59d386fee 100644
--- a/src/util/lp/bound_analyzer_on_row.h
+++ b/src/util/lp/bound_analyzer_on_row.h
@@ -175,10 +175,13 @@ public :
         }
 
         
+        mpq bound;
         for (const auto &p : m_row) {
             bool str;
             bool a_is_pos = is_pos(p.coeff());
-            mpq bound = total / p.coeff() + monoid_min_no_mult(a_is_pos, p.var(), str);
+            bound = total;
+            bound /= p.coeff();
+            bound += monoid_min_no_mult(a_is_pos, p.var(), str);
             if (a_is_pos) {
                 limit_j(p.var(), bound, true, false, strict - static_cast<int>(str) > 0);
             }
diff --git a/src/util/lp/stacked_vector.h b/src/util/lp/stacked_vector.h
index 539e932b2..ad83b3d87 100644
--- a/src/util/lp/stacked_vector.h
+++ b/src/util/lp/stacked_vector.h
@@ -25,8 +25,8 @@ Revision History:
 #include "util/vector.h"
 namespace lp {
 template < typename B> class stacked_vector {
-    vector<unsigned> m_stack_of_vector_sizes;
-    vector<unsigned> m_stack_of_change_sizes;
+    svector<unsigned> m_stack_of_vector_sizes;
+    svector<unsigned> m_stack_of_change_sizes;
     vector<std::pair<unsigned, B>> m_changes;
     vector<B> m_vector;
 public:
@@ -114,7 +114,7 @@ public:
     }
 
     template <typename T>  
-    void pop_tail(vector<T> & v, unsigned k) {
+    void pop_tail(svector<T> & v, unsigned k) {
         lp_assert(v.size() >= k);
         v.resize(v.size() - k);
     }