going over the binary factor for basic lemmas

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

src/test/lp/lp.cpp

@@ -69,7 +69,7 @@ static unsigned my_random() {
 }
 struct simple_column_namer:public column_namer
 {
-    std::string get_column_name(unsigned j) const override {
+    std::string get_variable_name(unsigned j) const override {
         return std::string("x") + T_to_string(j); 
     }
 };

src/util/lp/column_namer.h

@@ -23,7 +23,7 @@ Revision History:
 namespace lp {
 class column_namer {
 public:
-    virtual std::string get_column_name(unsigned j) const = 0;
+    virtual std::string get_variable_name(unsigned j) const = 0;
     template <typename T>
     void print_row(const row_strip<T> & row, std::ostream & out) const {
         vector<std::pair<T, unsigned>> coeff;
@@ -55,7 +55,7 @@ public:
             else if (val != numeric_traits<T>::one())
                 out << val;
         
-            out << get_column_name(it.second);
+            out << get_variable_name(it.second);
         }
     }
     template <typename T>
@@ -78,7 +78,7 @@ public:
             else if (val != numeric_traits<T>::one())
                 out << val;
         
-            out << get_column_name(it.second);
+            out << get_variable_name(it.second);
         }
     }
 

src/util/lp/int_solver.cpp

@@ -797,7 +797,7 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
 
     TRACE("freedom_interval",
           tout << "freedom variable for:\n";
-          tout << m_lar_solver->get_column_name(j);
+          tout << m_lar_solver->get_variable_name(j);
           tout << "[";
           if (inf_l) tout << "-oo"; else tout << l;
           tout << "; ";

src/util/lp/lar_solver.cpp

@@ -79,7 +79,7 @@ std::ostream& lar_solver::print_implied_bound(const implied_bound& be, std::ostr
         print_term(*m_terms[be.m_j - m_terms_start_index],  out);
     }
     else {
-        out << get_column_name(v);
+        out << get_variable_name(v);
     }
     out << " " << lconstraint_kind_string(be.kind()) << " "  << be.m_bound << std::endl;
     out << "end of implied bound" << std::endl;
@@ -999,15 +999,6 @@ column_type lar_solver::get_column_type(unsigned j) const{
     return m_mpq_lar_core_solver.m_column_types[j];
 }
 
-std::string lar_solver::get_column_name(unsigned j) const {
-    if (j >= m_terms_start_index) 
-        return std::string("_t") + T_to_string(j);
-    if (j >= m_var_register.size())
-        return std::string("_s") + T_to_string(j);
-
-    return std::string("v") + T_to_string(m_var_register.local_to_external(j));
-}
-
 bool lar_solver::all_constrained_variables_are_registered(const vector<std::pair<mpq, var_index>>& left_side) {
     for (auto it : left_side) {
         if (! var_is_registered(it.second))
@@ -1290,8 +1281,13 @@ void lar_solver::get_model_do_not_care_about_diff_vars(std::unordered_map<var_in
 }
 
 
-std::string lar_solver::get_variable_name(var_index vi) const {
+std::string lar_solver::get_variable_name(var_index j) const {
-    return get_column_name(vi);
+    if (j >= m_terms_start_index) 
+        return std::string("_t") + T_to_string(j);
+    if (j >= m_var_register.size())
+        return std::string("_s") + T_to_string(j);
+
+    return std::string("v") + T_to_string(m_var_register.local_to_external(j));
 }
 
 // ********** print region start
@@ -1344,7 +1340,7 @@ std::ostream& lar_solver::print_term(lar_term const& term, std::ostream & out) c
             out << " - ";
         else if (val != numeric_traits<mpq>::one())
             out << T_to_string(val);
-        out << this->get_column_name(p.var());
+        out << this->get_variable_name(p.var());
     }
     return out;
 }

src/util/lp/lar_solver.h

@@ -438,8 +438,6 @@ public:
 
     column_type get_column_type(unsigned j) const;
 
-    std::string get_column_name(unsigned j) const override;
-
     bool all_constrained_variables_are_registered(const vector<std::pair<mpq, var_index>>& left_side);
 
     constraint_index add_constraint(const vector<std::pair<mpq, var_index>>& left_side_with_terms, lconstraint_kind kind_par, const mpq& right_side_parm);

src/util/lp/lp_core_solver_base_def.h

@@ -780,7 +780,7 @@ copy_rs_to_xB(vector<X> & rs) {
 
 template <typename T, typename X> std::string lp_core_solver_base<T, X>::
 column_name(unsigned column) const {
-    return m_column_names.get_column_name(column);
+    return m_column_names.get_variable_name(column);
 }
 
 template <typename T, typename X> void lp_core_solver_base<T, X>::

src/util/lp/lp_solver.h

@@ -96,7 +96,7 @@ public:
     void set_cost_for_column(unsigned column, T  column_cost) {
         get_or_create_column_info(column)->set_cost(column_cost);
     }
-    std::string get_column_name(unsigned j) const override;
+    std::string get_variable_name(unsigned j) const override;
 
     void set_row_column_coefficient(unsigned row, unsigned column, T const & val) {
         m_A_values[row][column] = val;

src/util/lp/lp_solver_def.h

@@ -28,7 +28,7 @@ template <typename T, typename X> column_info<T> * lp_solver<T, X>::get_or_creat
 }
 
 template <typename T, typename X>
-std::string lp_solver<T, X>::get_column_name(unsigned j) const { // j here is the core solver index
+std::string lp_solver<T, X>::get_variable_name(unsigned j) const { // j here is the core solver index
     auto it = this->m_core_solver_columns_to_external_columns.find(j);
     if (it == this->m_core_solver_columns_to_external_columns.end())
         return std::string("x")+T_to_string(j);

src/util/lp/mon_eq.h

@@ -7,12 +7,14 @@
 #include "util/lp/lar_solver.h"
 namespace nra {
 struct mon_eq {
+    // fields
+    lp::var_index          m_v;
+    svector<lp::var_index> m_vs;
+    // constructors
     mon_eq(lp::var_index v, unsigned sz, lp::var_index const* vs):
         m_v(v), m_vs(sz, vs) {}
     mon_eq(lp::var_index v, const svector<lp::var_index> &vs):
         m_v(v), m_vs(vs) {}
-        lp::var_index          m_v;
-        svector<lp::var_index> m_vs;
     unsigned var() const { return m_v; }
     unsigned size() const { return m_vs.size(); }
     svector<lp::var_index>::const_iterator begin() const { return m_vs.begin(); }

src/util/lp/nla_solver.cpp

@@ -193,7 +193,7 @@ struct solver::imp {
     
     vars_equivalence                                       m_vars_equivalence;
     vector<mon_eq>                                         m_monomials;
-    // maps the vector of the minimized monomial vars to the list of monomial indices having the same vector
+    // maps the vector of the minimized monomial vars to the list of the indices of monomials having the same minimized monomial
     std::unordered_map<svector<lpvar>, vector<mono_index_with_sign>, hash_svector>
     m_minimal_monomials;
     unsigned_vector                                        m_monomials_lim;
@@ -271,9 +271,9 @@ struct solver::imp {
     }
 
     std::ostream& print_monomial(const mon_eq& m, std::ostream& out) const {
-        out << m_lar_solver.get_column_name(m.var()) << " = ";
+        out << m_lar_solver.get_variable_name(m.var()) << " = ";
         for (unsigned k = 0; k < m.size(); k++) {
-            out << m_lar_solver.get_column_name(m.m_vs[k]);
+            out << m_lar_solver.get_variable_name(m.m_vs[k]);
             if (k + 1 < m.m_vs.size()) out << "*";
         }
         return out;
@@ -328,7 +328,7 @@ struct solver::imp {
 
     // Replaces each variable index by a smaller index and flips the sing if the var comes with a minus.
     // 
-    svector<lpvar> reduce_monomial_to_minimal(const svector<lpvar> & vars, int & sign)  {
+    svector<lpvar> reduce_monomial_to_minimal(const svector<lpvar> & vars, int & sign) const {
         svector<lpvar> ret;
         sign = 1;
         for (unsigned i = 0; i < vars.size(); i++) {
@@ -543,7 +543,7 @@ struct solver::imp {
             }
         }
         if (!monomial)
-            out << m_lar_solver.get_column_name(j) << " = " << m_lar_solver.get_column_value(j);
+            out << m_lar_solver.get_variable_name(j) << " = " << m_lar_solver.get_column_value(j);
         out <<";";
         return out;
     }    
@@ -656,7 +656,7 @@ struct solver::imp {
             return false;
         }
         if (m_minimal_monomials.empty() && m.size() > 2)
-            create_min_map();
+            create_min_mon_map();
         
         return process_ones_of_mon(m, ones_of_mon, vars, v);
     }
@@ -674,8 +674,7 @@ struct solver::imp {
     }
 
     // returns the variable m_i, of a monomial if found and sets the sign,
-    // if the 
+    bool find_monomial_of_vars(const svector<lpvar>& vars, unsigned &j, int & sign) const {
-    bool find_monomial_of_vars(const svector<lpvar>& vars, unsigned &j, int & sign) {
         if (vars.size() == 1) {
             j = vars[0];
             sign = 1;
@@ -967,7 +966,7 @@ struct solver::imp {
             return false;
         
         if (m_minimal_monomials.empty())
-            create_min_map();
+            create_min_mon_map();
 
         if (!large.empty() && large_basic_lemma_for_mon_proportionality(i_mon, large))
             return true;
@@ -978,6 +977,10 @@ struct solver::imp {
         return false;
     }
 
+    // Using the following theorems
+    // |ab| >= |b| iff |a| >= 1 or b = 0
+    // |ab| <= |b| iff |a| <= 1 or b = 0
+    // and their commutative variants
     bool generate_basic_lemma_for_mon_proportionality(unsigned i_mon) {
         TRACE("nla_solver", tout << "generate_basic_lemma_for_mon_proportionality";);
         if (basic_lemma_for_mon_proportionality_from_factors_to_product(i_mon))
@@ -986,21 +989,35 @@ struct solver::imp {
         return basic_lemma_for_mon_proportionality_from_product_to_factors(i_mon);
     }
 
-    struct signed_two_factorization {
+    struct signed_binary_factorization {
-        unsigned m_i; // monomial index
         unsigned m_k; // monomial index
-        int      m_sign;  // 
+        bool     m_k_is_var;
+        unsigned m_j; // monomial index
+        bool     m_j_is_var;
+        int      m_sign;
+        // the default constructor
+        signed_binary_factorization() :m_k(-1) {}
+        signed_binary_factorization(unsigned k, bool k_is_var, unsigned j, bool j_is_var, int sign) : m_k(k),
+                                                                                                      m_k_is_var(k_is_var),
+                                                                                                      m_j(j),
+                                                                                                      m_j_is_var(j_is_var),
+                                                                                                      m_sign(sign) {}
+
+        bool k_is_var() const { return m_k_is_var; }
+        bool j_is_var() const { return m_j_is_var; }
     };
     
-    struct factors_of_monomial {
+    struct binary_factorizations_of_monomial {
         unsigned         m_i_mon;
         const imp&       m_imp;
         const mon_eq&    m_mon;
         unsigned_vector  m_minimized_vars;
-        int              m_sign;
+        int              m_sign; // the sign appears after reducing the monomial "mm_mon" to the minimal one
-        factors_of_monomial(unsigned i_mon, const imp& s) : m_i_mon(i_mon), m_imp(s),
+        
+        binary_factorizations_of_monomial(unsigned i_mon, const imp& s) : m_i_mon(i_mon), m_imp(s),
                                                             m_mon(m_imp.m_monomials[i_mon]) {
-            // m_minimized_vars = reduce_monomial_to_minimal(i_mon, m_sign);
+            m_minimized_vars = m_imp.reduce_monomial_to_minimal(
+                m_imp.m_monomials[m_i_mon].m_vs, m_sign);
         }
 
         
@@ -1008,61 +1025,60 @@ struct solver::imp {
         struct const_iterator {
             // fields
             unsigned_vector        m_mask;
-            //            factors_of_monomial&   m_fm;
+            const binary_factorizations_of_monomial&   m_binary_factorizations;
+
             //typedefs
-            
-            
             typedef const_iterator self_type;
-            typedef signed_two_factorization value_type;
+            typedef signed_binary_factorization value_type;
-            typedef const signed_two_factorization reference;
+            typedef const signed_binary_factorization reference;
-            //        typedef const column_cell* pointer;
             typedef int difference_type;
             typedef std::forward_iterator_tag iterator_category;
 
-            bool get_factors(unsigned& k, unsigned& j) {
+            void init_vars_by_the_mask(unsigned_vector & k_vars, unsigned_vector & j_vars) const {
-                /*
-                unsigned_vector a;
-                unsigned_vector b;
                 for (unsigned j = 0; j < m_mask.size(); j++) {
                     if (m_mask[j] == 1) {
-                        a.push_back(m_fm.m_minimized_vars[j]);
+                        k_vars.push_back(m_binary_factorizations.m_minimized_vars[j]);
                     } else {
-                        b.push_back(m_fm.m_minimized_vars[j]);
+                        j_vars.push_back(m_binary_factorizations.m_minimized_vars[j]);
                     }
                 }
-                SASSERT(!a.empty() && !b.empty());
-                std::sort(a.begin(), a.end());
-                std::sort(b.begin(), b.end());
-                int a_sign, b_sign;
-                if (a.size() == 1) {
-                    k = a[0];
-                    a_sign = 1;
-                } else if (!m_imp.find_monomial_of_vars(a, k, a_sign)) {
-                    return false;
-                } else {
-                    return false;
             }
-                if (b.size() == 1) {
-                    j = b[0];
-                    b_sign = 1;
-                } else  if (!m_imp.find_monomial_of_vars(b, j, b_sign)) {
-                        return false;
-                } else {
-                    return false;
-                }
-                */
-                SASSERT(false); // not implemented
-                return false;
             
+            bool get_factors(unsigned& k, bool& k_is_var, unsigned& j, bool& j_is_var, int& sign) const {
+                unsigned_vector k_vars;
+                unsigned_vector j_vars;
+                init_vars_by_the_mask(k_vars, j_vars);
+                SASSERT(!k_vars.empty() && !j_vars.empty());
+                std::sort(k_vars.begin(), k_vars.end());
+                std::sort(j_vars.begin(), j_vars.end());
+
+                int k_sign, j_sign;
+                if (k_vars.size() == 1) {
+                    k = k_vars[0];
+                    k_sign = 1;
+                    k_is_var = true;
+                } else if (m_binary_factorizations.m_imp.find_monomial_of_vars(k_vars, k, k_sign)) {
+                    k_is_var = false;
+                } else {
+                    return false;
+                }
+                if (j_vars.size() == 1) {
+                    j = j_vars[0];
+                    j_sign = 1;
+                    j_is_var = true;
+                } else if (m_binary_factorizations.m_imp.find_monomial_of_vars(j_vars, j, j_sign)) {
+                    j_is_var = false;
+                } else return false;
+                sign = j_sign * k_sign;
+                return true;
             }
             
             reference operator*() const {
-                SASSERT(false); // not implemented
+                unsigned k,j; int sign;
-                // unsigned k, j; // the factors
+                bool k_is_var, j_is_var;
-                //if (!get_factors(k, j))
+                if (!get_factors(k, k_is_var, j, j_is_var, sign))
-                //  return std::pair<lpvar, lpvar>(static_cast<unsigned>(-1), 0);
+                    return signed_binary_factorization();
-                return signed_two_factorization();
+                return signed_binary_factorization(k, k_is_var, j, j_is_var, m_binary_factorizations.m_sign * sign);
-                //                return std::pair<lpvar, lpvar>(k, j);
             }
             void advance_mask() {
                 SASSERT(false);// not implemented
@@ -1079,8 +1095,7 @@ struct solver::imp {
             self_type operator++() {  self_type i = *this; operator++(1); return i;  }
             self_type operator++(int) { advance_mask(); return *this; }
 
-            const_iterator(const unsigned_vector& mask) :
+            const_iterator(const unsigned_vector& mask, const binary_factorizations_of_monomial & f) : m_mask(mask), m_binary_factorizations(f) {
-                m_mask(mask) {
                 //   SASSERT(false);
             }
             bool operator==(const self_type &other) const {
@@ -1092,21 +1107,37 @@ struct solver::imp {
         const_iterator begin() const {
             unsigned_vector mask(m_mon.m_vs.size(), static_cast<lpvar>(0));
             mask[0] = 1; 
-            return const_iterator(mask);
+            return const_iterator(mask, *this);
         }
         
         const_iterator end() const {
             unsigned_vector mask(m_mon.m_vs.size(), 1);
-            return const_iterator(mask);
+            return const_iterator(mask, *this);
         }
     };
-    bool lemma_for_proportional_factors(unsigned i_mon, lpvar a, lpvar b) {
+    bool lemma_for_proportional_factors(unsigned i_mon, const signed_binary_factorization& f) {
-        return false;
+        TRACE("nla_solver", print_monomial(m_monomials[i_mon], tout);
+              tout << " is factorized as ";
+              if (f.m_sign == -1) { tout << "-";}
+              if (f.k_is_var()) {
+                  tout <<  m_lar_solver.get_variable_name(f.m_k);
+              } else {
+                  print_monomial(m_monomials[f.m_k], tout);
               }
-    // we derive a lemma from |xy| > |y| => |x| >= 1 || |y| = 0
+              tout << "*";
+              if (f.j_is_var()) {
+                  tout << m_lar_solver.get_variable_name(f.m_j);
+              } else {
+                  print_monomial(m_monomials[f.m_j], tout);
+              });
+             SASSERT(false);
+        return false; // not implemented
+    }
+    // we derive a lemma from |xy| >= |y| => |x| >= 1 || |y| = 0
     bool basic_lemma_for_mon_proportionality_from_product_to_factors(unsigned i_mon) {
-        for (auto factors : factors_of_monomial(i_mon, *this)) {
+        for (auto factorization : binary_factorizations_of_monomial(i_mon, *this)) {
-            // if (lemma_for_proportional_factors(i_mon, factors.first, factors.second))
+            if (lemma_for_proportional_factors(i_mon, factorization))
+                return true;
         }
         //  return true;
         SASSERT(false);
@@ -1132,7 +1163,7 @@ struct solver::imp {
         return false;
     }
 
-    void map_monomials_var_to_monomial_indices(unsigned i) {
+    void map_monomial_vars_to_monomial_indices(unsigned i) {
         const mon_eq& m = m_monomials[i];
         for (lpvar j : m.m_vs) {
             auto it = m_var_lists.find(j);
@@ -1149,35 +1180,37 @@ struct solver::imp {
 
     void map_vars_to_monomials_and_constraints() {
         for (unsigned i = 0; i < m_monomials.size(); i++)
-            map_monomials_var_to_monomial_indices(i);
+            map_monomial_vars_to_monomial_indices(i);
     }
 
+    // x is equivalent to y if x = +- y
     void init_vars_equivalence() {
         m_vars_equivalence.init(m_lar_solver);
     }
 
-    void add_pair_to_min_monomials(const svector<lpvar>& key, unsigned i, int sign) {
+    void register_key_mono_in_min_monomials(const svector<lpvar>& key, unsigned i, int sign) {
         mono_index_with_sign ms(i, sign);
         auto it = m_minimal_monomials.find(key);
         if (it == m_minimal_monomials.end()) {
             vector<mono_index_with_sign> v;
             v.push_back(ms);
+            // v is a vector containing a single mono_index_with_sign
             m_minimal_monomials.emplace(key, v);
         } else {
             it->second.push_back(ms);
         }
     }
     
-    void add_monomial_to_min_map(unsigned i) {
+    void register_monomial_in_min_map(unsigned i) {
         const mon_eq& m = m_monomials[i];
         int sign;
         svector<lpvar> key = reduce_monomial_to_minimal(m.m_vs, sign);
-        add_pair_to_min_monomials(key, i, sign);
+        register_key_mono_in_min_monomials(key, i, sign);
     }
     
-    void create_min_map() {
+    void create_min_mon_map() {
         for (unsigned i = 0; i < m_monomials.size(); i++)
-            add_monomial_to_min_map(i);
+            register_monomial_in_min_map(i);
     }
     
     void init_search() {