python for accessing lambda, switch to theory branching for QF_LRA

Signed-off-by: Nikolaj Bjorner <[email protected]>

Author: NikolajBjorner

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();
     }
 

src/smt/theory_lra.cpp

@@ -944,10 +944,6 @@ class theory_lra::imp {
         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 @@ class theory_lra::imp {
         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) {

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);
             }

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 @@ template < typename B> class stacked_vector {
     }
 
     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);
     }