rebase

Signed-off-by: Lev <levnach@hotmail.com>

src/smt/theory_lra.cpp

@@ -54,17 +54,6 @@ std::ostream& operator<<(std::ostream& out, bound_kind const& k) {
     return out;
 }
 
-struct term_info {
-    rational m_offset;
-    lp::var_index m_var;
-
-    rational const& offset() const { return m_offset; }
-    lp::var_index var() const { return m_var; }
-
-    term_info(): m_var(-1) {}
-    term_info(lp:var_index vi, rational const& offset): m_offset(offset), m_var(vi) {}
-};
-
 class bound { 
     smt::bool_var     m_bv;
     smt::theory_var  m_var;
@@ -788,8 +777,8 @@ class theory_lra::imp {
             lp::var_index vi = m_theory_var2var_index.get(v, UINT_MAX);
             TRACE("arith", tout << mk_pp(term, m) << " " << v << " " << vi << "\n";);
             if (vi == UINT_MAX) {
-                vi = m_solver->add_term(m_left_side);
+                vi = m_solver->add_term(m_left_side, st.coeff());
-                m_theory_var2var_index.setx(v, term_info(vi, st.coeff()), term_info(0, rational::zero()));
+                m_theory_var2var_index.setx(v, vi, UINT_MAX);
                 if (m_solver->is_term(vi)) {
                     m_term_index2theory_var.setx(m_solver->adjust_term_index(vi), v, UINT_MAX);
                 }
@@ -1198,19 +1187,17 @@ public:
     lp::impq get_ivalue(theory_var v) const {
         SASSERT(can_get_ivalue(v));
         lp::var_index vi = m_theory_var2var_index[v];
-        term_info ti = m_theory_var2var_index[v];
+        if (!m_solver->is_term(vi))
-        if (!m_solver->is_term(ti.var()))
+            return m_solver->get_column_value(vi);
-            return m_solver->get_column_value(ti.var()) + ti.offset();
+        m_todo_terms.push_back(std::make_pair(vi, rational::one()));
-        m_todo_terms.push_back(std::make_pair(ti, rational::one())); 
+        lp::impq result(0);
-        lp::impq result(ti);
         while (!m_todo_terms.empty()) {
-            ti = m_todo_terms.back().first;
+            vi = m_todo_terms.back().first;
-            vi = ti.var();
             rational coeff = m_todo_terms.back().second;
             m_todo_terms.pop_back();
-            result += ti.offset() * coeff;            
             if (m_solver->is_term(vi)) {
                 const lp::lar_term& term = m_solver->get_term(vi);
+                result += term.m_v * coeff;
                 for (const auto & i:  term) {
                     m_todo_terms.push_back(std::make_pair(i.var(), coeff * i.coeff()));
                 }                    

src/util/lp/bound_propagator.cpp

@@ -17,6 +17,10 @@ const impq & bound_propagator::get_upper_bound(unsigned j) const {
 }
 void bound_propagator::try_add_bound(mpq  v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) {
     j = m_lar_solver.adjust_column_index_to_term_index(j);    
+    if (m_lar_solver.is_term(j)) {
+        // lp treats terms as not having a free coefficient, restoring it below for the outside consumption
+        v += m_lar_solver.get_term(j).m_v;
+    }
 
     lconstraint_kind kind = is_low? GE : LE;
     if (strict)

src/util/lp/lar_constraints.h

@@ -75,7 +75,7 @@ struct lar_term_constraint: public lar_base_constraint {
     }
     unsigned size() const override { return m_term->size();}
     lar_term_constraint(const lar_term *t, lconstraint_kind kind, const mpq& right_side) : lar_base_constraint(kind, right_side), m_term(t) { }
-    mpq get_free_coeff_of_left_side() const override { return zero_of_type<mpq>();}
+    mpq get_free_coeff_of_left_side() const override { return m_term->m_v;}
 
 };
 

src/util/lp/lar_solver.cpp

@@ -137,6 +137,7 @@ bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be,
             kind = static_cast<lconstraint_kind>(-kind);
         }
         rs_of_evidence /= ratio;
+        rs_of_evidence += t->m_v * ratio;
     }
 
     return kind == be.kind() && rs_of_evidence == be.m_bound;
@@ -612,6 +613,7 @@ void lar_solver::substitute_terms_in_linear_expression(const vector<std::pair<mp
             for (auto & p : term.coeffs()){
                 register_monoid_in_map(coeffs, t.first * p.second , p.first);
             }
+            free_coeff += t.first * term.m_v;
         }
     }
 
@@ -1115,7 +1117,7 @@ bool lar_solver::has_upper_bound(var_index var, constraint_index& ci, mpq& value
 bool lar_solver::has_value(var_index var, mpq& value) const {
     if (is_term(var)) {
         lar_term const& t = get_term(var);
-        value = zero_of_type<mpq>();
+        value = t.m_v;
         for (auto const& cv : t) {
             impq const& r = get_column_value(cv.var());
             if (!numeric_traits<mpq>::is_zero(r.y)) return false;
@@ -1495,7 +1497,7 @@ bool lar_solver::term_is_int(const lar_term * t) const {
     for (auto const & p :  t->m_coeffs)
         if (! (column_is_int(p.first)  && p.second.is_int()))
             return false;
-    return true;
+    return t->m_v.is_int();
 }
 
 bool lar_solver::var_is_int(var_index v) const {
@@ -1596,8 +1598,9 @@ void lar_solver::add_new_var_to_core_fields_for_mpq(bool register_in_basis) {
 }
 
 
-var_index lar_solver::add_term_undecided(const vector<std::pair<mpq, var_index>> & coeffs) {
+var_index lar_solver::add_term_undecided(const vector<std::pair<mpq, var_index>> & coeffs,
-    push_and_register_term(new lar_term(coeffs));
+                                         const mpq &m_v) {
+    push_and_register_term(new lar_term(coeffs, m_v));
     return m_terms_start_index + m_terms.size() - 1;
 }
 
@@ -1640,11 +1643,12 @@ void lar_solver::push_and_register_term(lar_term* t) {
 }
 
 // terms
-var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & coeffs) {
+var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & coeffs,
+                               const mpq &m_v) {
     if (strategy_is_undecided())
-        return add_term_undecided(coeffs);
+        return add_term_undecided(coeffs, m_v);
 
-    push_and_register_term(new lar_term(coeffs));
+    push_and_register_term(new lar_term(coeffs, m_v));
     unsigned adjusted_term_index = m_terms.size() - 1;
     var_index ret = m_terms_start_index + adjusted_term_index;
     if (use_tableau() && !coeffs.empty()) {
@@ -1739,8 +1743,9 @@ void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_k
     //    lp_assert(!term_is_int(m_terms[adjusted_term_index]) || right_side.is_int());
     unsigned term_j;
     if (m_var_register.external_is_used(j, term_j)) {
+        mpq rs = right_side - m_terms[adjusted_term_index]->m_v;
         m_constraints.push_back(new lar_term_constraint(m_terms[adjusted_term_index], kind, right_side));
-        update_column_type_and_bound(term_j, kind, right_side, ci);
+        update_column_type_and_bound(term_j, kind, rs, ci);
     }
     else {
         add_constraint_from_term_and_create_new_column_row(j, m_terms[adjusted_term_index], kind, right_side);
@@ -1751,7 +1756,7 @@ constraint_index lar_solver::add_constraint(const vector<std::pair<mpq, var_inde
     vector<std::pair<mpq, var_index>> left_side;
     mpq rs = -right_side_parm;
     substitute_terms_in_linear_expression(left_side_with_terms, left_side, rs);
-    unsigned term_index = add_term(left_side);
+    unsigned term_index = add_term(left_side, zero_of_type<mpq>());
     constraint_index ci = m_constraints.size();
     add_var_bound_on_constraint_for_term(term_index, kind_par, -rs, ci);
     return ci;
@@ -1762,7 +1767,7 @@ void lar_solver::add_constraint_from_term_and_create_new_column_row(unsigned ter
 
     add_row_from_term_no_constraint(term, term_j);
     unsigned j = A_r().column_count() - 1;
-    update_column_type_and_bound(j, kind, right_side, m_constraints.size());
+    update_column_type_and_bound(j, kind, right_side - term->m_v, m_constraints.size());
     m_constraints.push_back(new lar_term_constraint(term, kind, right_side));
     lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size());
 }

src/util/lp/lar_solver.h

@@ -164,11 +164,13 @@ public:
 
 
     // terms
-    var_index add_term(const vector<std::pair<mpq, var_index>> & coeffs);
+    var_index add_term(const vector<std::pair<mpq, var_index>> & coeffs,
+                       const mpq &m_v);
 
-    var_index add_term_undecided(const vector<std::pair<mpq, var_index>> & coeffs);
+    var_index add_term_undecided(const vector<std::pair<mpq, var_index>> & coeffs,
+                                 const mpq &m_v);
 
-    bool term_coeffs_are_ok(const vector<std::pair<mpq, var_index>> & coeffs);
+    bool term_coeffs_are_ok(const vector<std::pair<mpq, var_index>> & coeffs, const mpq& v);
     void push_and_register_term(lar_term* t);
 
     void add_row_for_term(const lar_term * term, unsigned term_ext_index);

src/util/lp/lar_term.h

@@ -23,6 +23,7 @@ namespace lp {
 struct lar_term {
     // the term evaluates to sum of m_coeffs + m_v
     std::unordered_map<unsigned, mpq> m_coeffs;
+    mpq m_v;
     lar_term() {}
     void add_monomial(const mpq& c, unsigned j) {
         auto it = m_coeffs.find(j);
@@ -36,7 +37,7 @@ struct lar_term {
     }
 
     bool is_empty() const {
-        return m_coeffs.size() == 0;
+        return m_coeffs.size() == 0 && is_zero(m_v);
     }
     
     unsigned size() const { return static_cast<unsigned>(m_coeffs.size()); }
@@ -45,7 +46,8 @@ struct lar_term {
         return m_coeffs;
     }
     
-    lar_term(const vector<std::pair<mpq, unsigned>>& coeffs) {
+    lar_term(const vector<std::pair<mpq, unsigned>>& coeffs,
+             const mpq & v) : m_v(v) {
         for (const auto & p : coeffs) {
             add_monomial(p.first, p.second);
         }
@@ -85,7 +87,7 @@ struct lar_term {
 
     template <typename T>
     T apply(const vector<T>& x) const {
-        T ret = zero_of_type<T>();
+        T ret = T(m_v);
         for (const auto & t : m_coeffs) {
             ret += t.second * x[t.first];
         }
@@ -94,6 +96,7 @@ struct lar_term {
    
     void clear() {
         m_coeffs.clear();
+        m_v = zero_of_type<mpq>();
     }
 
     struct ival {