Expl (#4462)

* cleaner API for explanation

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

* remove an unnecessery check

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

* expl

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

src/math/lp/explanation.h

@@ -20,68 +20,93 @@ Revision History:
 #pragma once
 #include "math/lp/lp_utils.h"
 #include "util/map.h"
-#include "util/optional.h"
+#include "util/hashtable.h"
 namespace lp {
 class explanation {
-    u_map<optional<mpq>> m_j_to_mpq;   
+    typedef vector<std::pair<unsigned, mpq>> pair_vec;
+    typedef    hashtable<unsigned, u_hash, u_eq>  ci_set;
+    // Only one of the fields below is used. The first call adding an entry decides which one it is.
+    vector<std::pair<constraint_index, mpq>> m_vector;
+    ci_set  m_set;   
 public:
     explanation() {}
+    
     template <typename T>
     explanation(const T& t) {
-        for ( unsigned c : t)
+        for (unsigned c : t)
             push_back(c);
     }
     
-    void clear() { m_j_to_mpq.reset(); }
-    void add_with_coeff(constraint_index j, const mpq& v) {
-        SASSERT(m_j_to_mpq.contains(j) == false); // if we hit the assert then we
-                                                  // might start using summation
-        m_j_to_mpq.insert(j, optional<mpq>(v));
+    void clear() { m_vector.clear(); m_set.reset(); }
+    void add_pair(constraint_index j, const mpq& v) {
+        SASSERT(m_set.empty()); 
+        m_vector.push_back(std::make_pair(j, v));
     }
 
     // this signature is needed to use it in a template that also works for the vector type
     void push_back(constraint_index j) {
-        if (m_j_to_mpq.contains(j))
-            return;
-        m_j_to_mpq.insert(j, optional<mpq>());
+        SASSERT(m_vector.empty());
+        m_set.insert(j);
     }
     
     void add_expl(const explanation& e) {
-        for (const auto& p: e.m_j_to_mpq) {
-            m_j_to_mpq.insert(p.m_key, p.m_value);
+        if (e.m_vector.empty()) {
+            for (constraint_index j : e.m_set)
+                push_back(j);
+        } else {
+            for (const auto & p : e.m_vector) {
+                add_pair(p.first, p.second);
+            }
         }
     }
 
-    void add_pair(const std::pair<mpq, constraint_index>& j) {
-        add_with_coeff(j.second, j.first);
-    }
-
-    bool empty() const {  return m_j_to_mpq.empty();  }
-    size_t size() const { return m_j_to_mpq.size(); }
+    bool empty() const {  return m_vector.empty() || m_set.empty();  }
+    size_t size() const { return std::max(m_vector.size(), m_set.size()); }
 
     class cimpq {
         constraint_index m_var;
-        const optional<mpq> & m_coeff;
+        const mpq&  m_coeff;
     public:
-        cimpq(constraint_index var, const optional<mpq> & val) : m_var(var), m_coeff(val) { }
+        cimpq(constraint_index var, const mpq & val) : m_var(var), m_coeff(val) { }
         constraint_index ci() const { return m_var; }
-        mpq coeff() const { return m_coeff.initialized()? *m_coeff: one_of_type<mpq>(); }
+        const mpq &coeff() const { return m_coeff; }
     };
     class iterator {
-        u_map<optional<mpq>>::iterator m_it; 
+        bool      m_run_on_vector;
+        pair_vec::const_iterator    m_vi;
+        ci_set::iterator            m_ci;
     public:
         cimpq operator*() const {
-            return cimpq(m_it->m_key, m_it->m_value);
+            return m_run_on_vector?
+                cimpq( m_vi->first, m_vi->second) :
+                cimpq( *m_ci, one_of_type<mpq>()); 
         }        
-        iterator operator++() { iterator i = *this; m_it++; return i;  }
-        iterator operator++(int) { m_it++; return *this; }
-        iterator(u_map<optional<mpq>>::iterator it) : m_it(it) {}
-        bool operator==(const iterator &other) const { return m_it == other.m_it; }
+        iterator operator++() {
+            if (m_run_on_vector)
+                m_vi++;
+            else
+                m_ci++;                    
+            return *this;
+        }
+        iterator operator++(int) {
+            iterator i = *this; ++(*this); return i;
+        }
+        iterator(bool run_on_vector, pair_vec::const_iterator vi, ci_set::iterator cii) :
+            m_run_on_vector(run_on_vector), m_vi(vi), m_ci(cii)
+        {}
+        bool operator==(const iterator &other) const {
+            SASSERT(m_run_on_vector == other.m_run_on_vector);
+            return  m_run_on_vector? m_vi == other.m_vi : m_ci == other.m_ci;
+        }
         bool operator!=(const iterator &other) const { return !(*this == other); }
     };
 
-    iterator begin() const { return iterator(m_j_to_mpq.begin()); }
-    iterator end() const { return iterator(m_j_to_mpq.end()); }
+    iterator begin() const {
+        return iterator( !m_vector.empty(), m_vector.begin(), m_set.begin());
+    }
+    iterator end() const {
+        return iterator(!m_vector.empty(), m_vector.end(), m_set.end());
+    }
 
 };
 }

src/math/lp/lar_solver.cpp

@@ -307,8 +307,8 @@ void lar_solver::fill_explanation_from_crossed_bounds_column(explanation & evide
     
     // this is the case when the lower bound is in conflict with the upper one
     const ul_pair & ul =  m_columns_to_ul_pairs[m_crossed_bounds_column];
-    evidence.add_with_coeff(ul.upper_bound_witness(),  numeric_traits<mpq>::one());
-    evidence.add_with_coeff(ul.lower_bound_witness(), -numeric_traits<mpq>::one());
+    evidence.add_pair(ul.upper_bound_witness(),  numeric_traits<mpq>::one());
+    evidence.add_pair(ul.lower_bound_witness(), -numeric_traits<mpq>::one());
 }
 
     
@@ -1195,7 +1195,7 @@ void lar_solver::get_infeasibility_explanation_for_inf_sign(
 
         constraint_index bound_constr_i = adj_sign < 0 ? ul.upper_bound_witness() : ul.lower_bound_witness();
         lp_assert(m_constraints.valid_index(bound_constr_i));
-        exp.add_with_coeff(bound_constr_i, coeff);
+        exp.add_pair(bound_constr_i, coeff);
     } 
 }