toward fetching existing terms intervals from lar_solver

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

src/math/lp/horner.cpp

@@ -242,7 +242,7 @@ void horner::add_linear_to_vector(const nex& e, vector<std::pair<rational, lpvar
     }
 }
 // e = a * can_t + b, but we do not calculate the offset here
-lp::lar_term horner::expression_to_canonical_form(nex& e, rational& a, rational& b) {
+lp::lar_term horner::expression_to_normalized_term(nex& e, rational& a, rational& b) {
     TRACE("nla_horner_details", tout << e << "\n";);
     lpvar smallest_j;
     vector<std::pair<rational, lpvar>> v;
@@ -281,12 +281,10 @@ lp::lar_term horner::expression_to_canonical_form(nex& e, rational& a, rational&
     return t;
 }
 
-bool horner::find_term_expr(const nex& e, rational& a, const lp::lar_term* &t, rational& b) const {
+lpvar horner::find_term_column(const nex& e, rational& a, rational& b) const {
     nex n = e;
-    lp::lar_term can_t = expression_to_canonical_form(n, a, b);
+    lp::lar_term norm_t = expression_to_normalized_term(n, a, b);
-    TRACE("nla_horner_details", tout << "term = "; c().m_lar_solver.print_term(can_t, tout) << "\n";);
+    return c().m_lar_solver.fetch_normalized_term_column(norm_t);
-    SASSERT(false);
-    return false;
 }
 
 interv horner::interval_of_sum_no_terms(const nex& e) {
@@ -326,10 +324,21 @@ interv horner::interval_of_sum_no_terms(const nex& e) {
 bool horner::interval_from_term(const nex& e, interv & i) const {
     rational a, b;
     nex n = e;
-    lp::lar_term canonical_t = expression_to_canonical_form(n, a, b);
+    lpvar j = find_term_column(n, a, b);
-    // TRACE("nla_horner_details",     
+    if (j + 1 == 0)
-    SASSERT(false);
+        return false;
-    return false;
+
+    set_var_interval(j, i);
+    interv bi;
+    m_intervals.mul(a, i, bi);
+    m_intervals.add(b, bi);
+    m_intervals.set(i, bi);
+    
+    TRACE("nla_horner",
+          c().m_lar_solver.print_column_info(j, tout) << "\n";
+          tout << "a=" << a << ", b=" << b << "\n"; 
+          tout << e << ", interval = "; m_intervals.display(tout, i););
+    return true;
 }
 
 
@@ -349,7 +358,7 @@ interv horner::interval_of_sum(const nex& e) {
 }
 
 // sets the dependencies also
-void horner::set_var_interval(lpvar v, interv& b) {
+void horner::set_var_interval(lpvar v, interv& b) const{
     m_intervals.set_var_interval_with_deps(v, b);    
     TRACE("nla_horner_details_var", tout << "v = "; print_var(v, tout) << "\n"; m_intervals.display(tout, b););    
 }

src/math/lp/horner.h

@@ -46,13 +46,13 @@ public:
     intervals::interval interval_of_sum_no_terms(const nex&);
     intervals::interval interval_of_mul(const nex&);
     void set_interval_for_scalar(intervals::interval&, const rational&);
-    void set_var_interval(lpvar j, intervals::interval&);
+    void set_var_interval(lpvar j, intervals::interval&) const;
     bool lemmas_on_expr(nex &);
     
     template <typename T> // T has an iterator of (coeff(), var())
     bool row_has_monomial_to_refine(const T&) const;
-    bool find_term_expr(const nex& e, rational& a, const lp::lar_term * & t, rational& b) const;
+    lpvar find_term_column(const nex& e, rational& a, rational& b) const;
-    static lp::lar_term expression_to_canonical_form(nex&, rational& a, rational & b);
+    static lp::lar_term expression_to_normalized_term(nex&, rational& a, rational & b);
     static void add_linear_to_vector(const nex&, vector<std::pair<rational, lpvar>> &);
     static void add_mul_to_vector(const nex&, vector<std::pair<rational, lpvar>> &);
     bool is_tighter(const interv&, const interv&) const;

src/math/lp/lar_solver.cpp

@@ -34,7 +34,7 @@ lar_solver::lar_solver() : m_status(lp_status::UNKNOWN),
                            m_terms_start_index(1000000),
                            m_var_register(0),
                            m_term_register(m_terms_start_index),
-                           m_need_register_terms(true) // change to false
+                           m_need_register_terms(false)
 {}
     
 void lar_solver::set_track_pivoted_rows(bool v) {
@@ -387,9 +387,8 @@ void lar_solver::pop(unsigned k) {
     m_constraints.resize(m_constraint_count);
     m_term_count.pop(k);
     for (unsigned i = m_term_count; i < m_terms.size(); i++) {
-#if Z3DEBUG_CHECK_UNIQUE_TERMS
+        if (m_need_register_terms)
-        m_set_of_terms.erase(m_terms[i]);
+            deregister_normalized_term(*m_terms[i]);
-#endif
         delete m_terms[i];
     }
     m_term_register.shrink(m_term_count);
@@ -1822,6 +1821,8 @@ bool lar_solver::all_vars_are_registered(const vector<std::pair<mpq, var_index>>
 }
 
 var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & coeffs, unsigned ext_i) {
+    TRACE("lar_solver_terms", print_linear_combination_of_column_indices_only(coeffs, tout) << ", ext_i =" << ext_i << "\n";); 
+          
     m_term_register.add_var(ext_i);
     lp_assert(all_vars_are_registered(coeffs));
     if (strategy_is_undecided())
@@ -1838,8 +1839,7 @@ var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & coeffs,
     }
     lp_assert(m_var_register.size() == A_r().column_count());
     if (m_need_register_terms) {
-        lar_term normalized_t = t->get_normalized_by_min_var();
+        register_normalized_term(*t, A_r().column_count() - 1); 
-        m_normalized_terms_to_columns[normalized_t] = A_r().column_count() - 1;        
     }
     return ret;
 }
@@ -2371,14 +2371,35 @@ void lar_solver::set_cut_strategy(unsigned cut_frequency) {
         settings().set_hnf_cut_period(100000000);
     } 
 }
+
+void lar_solver::register_normalized_term(const lar_term& t, lpvar j) {
+    lar_term normalized_t = t.get_normalized_by_min_var();
+    TRACE("lar_solver_terms", tout << "t="; print_term_as_indices(t, tout);
+          tout << ", normalized_t="; print_term_as_indices(normalized_t, tout) << "\n";);
+    lp_assert(m_normalized_terms_to_columns.find(normalized_t) == m_normalized_terms_to_columns.end());
+    m_normalized_terms_to_columns[normalized_t] = j;            
+}
+
+void lar_solver::deregister_normalized_term(const lar_term& t) {
+    lar_term normalized_t = t.get_normalized_by_min_var();
+    lp_assert(m_normalized_terms_to_columns.find(normalized_t) != m_normalized_terms_to_columns.end());
+    m_normalized_terms_to_columns.erase(normalized_t);
+}
+
 void lar_solver::register_existing_terms() {
+    TRACE("nla_solver", tout << "registering " << m_terms.size() << " terms\n";);
     for (unsigned k = 0; k < m_terms.size(); k++) {
-        lar_term * t = m_terms[k];
-        lar_term normalized_t = t->get_normalized_by_min_var();
         lpvar j = m_var_register.external_to_local(k + m_terms_start_index);
-        m_normalized_terms_to_columns[normalized_t] = j;        
+        register_normalized_term(*m_terms[k], j);
     }
 }
+
+unsigned lar_solver::fetch_normalized_term_column(const lar_term& c) const {
+    auto it = m_normalized_terms_to_columns.find(c);
+    if (it != m_normalized_terms_to_columns.end())
+        return it->second;
+    return -1;
+}
 } // namespace lp
 
 

src/math/lp/lar_solver.h

@@ -644,5 +644,8 @@ public:
     void fix_Ax_b_on_rounded_row(unsigned);
     void collect_rounded_rows_to_fix();
     void register_existing_terms();
+    void register_normalized_term(const lar_term&, lpvar);
+    void deregister_normalized_term(const lar_term&);
+    lpvar fetch_normalized_term_column(const lar_term& t) const;
 };
 }

src/math/lp/nla_intervals.cpp

@@ -4,7 +4,7 @@
 #include "util/mpq.h"
 
 namespace nla {
-void intervals::set_var_interval_with_deps(lpvar v, interval& b) {
+void intervals::set_var_interval_with_deps(lpvar v, interval& b) const {
     lp::constraint_index ci;
     rational val;
     bool is_strict;

src/math/lp/nla_intervals.h

@@ -171,10 +171,31 @@ public:
     void set_upper_is_open(interval & a, bool strict) { m_config.set_upper_is_open(a, strict); }
     void set_upper_is_inf(interval & a, bool inf) { m_config.set_upper_is_inf(a, inf); }
     bool is_zero(const interval& a) const { return m_config.is_zero(a); }
+    void mul(const rational& r, const interval& a, interval& b) const {       
+        m_imanager.mul(r.to_mpq(), a, b);
+        if (r.is_pos()) {
+            b.m_lower_dep = a.m_lower_dep;
+            b.m_upper_dep = a.m_upper_dep;
+        } else {
+            SASSERT(r.is_neg());
+            b.m_upper_dep = a.m_lower_dep;
+            b.m_lower_dep = a.m_upper_dep;
+        }
+    }
+
+    void add(const rational& r, interval& a) const {
+        if (!a.m_lower_inf) {
+            m_config.set_lower(a, a.m_lower + r);
+        }
+        if (!a.m_upper_inf) {
+            m_config.set_upper(a, a.m_upper + r);
+        }
+    }
+
     void mul(const interval& a, const interval& b, interval& c) { m_imanager.mul(a, b, c); }
     void add(const interval& a, const interval& b, interval& c) { m_imanager.add(a, b, c); }
     void add(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.add(a, b, c, deps); }
-    void set(interval& a, const interval& b) {
+    void set(interval& a, const interval& b) const {
         m_imanager.set(a, b);
         a.m_lower_dep = b.m_lower_dep;
         a.m_upper_dep = b.m_upper_dep;
@@ -228,7 +249,7 @@ public:
     
     bool upper_is_inf(const interval& a) const { return m_config.upper_is_inf(a); }
     bool lower_is_inf(const interval& a) const { return m_config.lower_is_inf(a); }    
-    void set_var_interval_with_deps(lpvar, interval &);
+    void set_var_interval_with_deps(lpvar, interval &) const;
     void set_zero_interval_deps_for_mult(interval&);
     bool is_inf(const interval& i) const { return m_config.is_inf(i); }
     bool check_interval_for_conflict_on_zero(const interval & i);