use explanation.h for conflict explanations everywhere

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

src/smt/theory_lra.cpp

@@ -2003,7 +2003,7 @@ public:
             m_eqs.reset();
             m_core.reset();
             m_params.reset();
-            for (auto const& ev : m_lia->get_explanation().m_explanation) {
+            for (auto const& ev : ex) {
                 if (!ev.first.is_zero()) { 
                     set_evidence(ev.second);
                 }
@@ -2019,7 +2019,7 @@ public:
         case lp::lia_move::conflict:
             TRACE("arith", tout << "conflict\n";);
             // ex contains unsat core
-            m_explanation = m_lia->get_explanation().m_explanation;
+            m_explanation = ex;
             set_conflict1();
             lia_check = l_false;
             break;
@@ -2073,7 +2073,7 @@ public:
         if (!m_switcher.need_check()) return l_true;
         m_a1 = nullptr; m_a2 = nullptr;
         
-        lbool r = m_nra? m_nra->check(m_explanation): m_niil->check(m_lemma);
+        lbool r = m_nra? m_nra->check(m_explanation): m_niil->check(m_explanation, m_lemma);
         return m_nra? check_aftermath_nra(r) : check_aftermath_niil(r);
     }
 
@@ -2221,7 +2221,7 @@ public:
 
         void consume(rational const& v, lp::constraint_index j) override {
             m_imp.set_evidence(j);
-            m_imp.m_explanation.push_back(std::make_pair(v, j));
+            m_imp.m_explanation.push_justification(j, v);
         }
     };
 
@@ -3075,7 +3075,8 @@ public:
         }
     }
  
-    vector<std::pair<rational, lp::constraint_index>> m_explanation;
+    lp::explanation m_explanation;
+    
     literal_vector      m_core;
     svector<enode_pair> m_eqs;
     vector<parameter>   m_params;
@@ -3582,7 +3583,7 @@ public:
         }
     }
 
-    void display_evidence(std::ostream& out, vector<std::pair<rational, lp::constraint_index>> const& evidence) {
+    void display_evidence(std::ostream& out, lp::explanation const& evidence) {
         for (auto const& ev : evidence) {
             expr_ref e(m);
             SASSERT(!ev.first.is_zero()); 

src/util/lp/explanation.h

@@ -19,14 +19,18 @@ Revision History:
 --*/
 #pragma once
 namespace lp {
-struct explanation {
+class explanation {
-    void clear() { m_explanation.clear(); }
     vector<std::pair<mpq, constraint_index>> m_explanation;
+public:
+    void clear() { m_explanation.clear(); }
+    vector<std::pair<mpq, constraint_index>>::const_iterator begin() const { return m_explanation.begin(); }
+    vector<std::pair<mpq, constraint_index>>::const_iterator end() const { return m_explanation.end(); }
     void push_justification(constraint_index j, const mpq& v) {
         m_explanation.push_back(std::make_pair(v, j));
     }
     void push_justification(constraint_index j) {
         m_explanation.push_back(std::make_pair(one_of_type<mpq>(), j));
     }
+    void reset() { m_explanation.reset(); }
 };
 }

src/util/lp/int_solver.cpp

@@ -601,8 +601,8 @@ bool int_solver::gcd_test_for_row(static_matrix<mpq, numeric_pair<mpq>> & A, uns
 void int_solver::add_to_explanation_from_fixed_or_boxed_column(unsigned j) {
     constraint_index lc, uc;
     m_lar_solver->get_bound_constraint_witnesses_for_column(j, lc, uc);
-    m_ex.m_explanation.push_back(std::make_pair(mpq(1), lc));
+    m_ex->push_justification(lc);
-    m_ex.m_explanation.push_back(std::make_pair(mpq(1), uc));
+    m_ex->push_justification(uc);
 }
 void int_solver::fill_explanation_from_fixed_columns(const row_strip<mpq> & row) {
     for (const auto & c : row) {

src/util/lp/lar_solver.cpp

@@ -303,12 +303,12 @@ lp_status lar_solver::solve() {
     return m_status;
 }
 
-void lar_solver::fill_explanation_from_infeasible_column(vector<std::pair<mpq, constraint_index>> & evidence) const{
+void lar_solver::fill_explanation_from_infeasible_column(explanation & evidence) const{
 
     // 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_infeasible_column_index];
-    evidence.push_back(std::make_pair(numeric_traits<mpq>::one(), ul.upper_bound_witness()));
+    evidence.push_justification(ul.upper_bound_witness(),  numeric_traits<mpq>::one());
-    evidence.push_back(std::make_pair(-numeric_traits<mpq>::one(), ul.lower_bound_witness()));
+    evidence.push_justification(ul.lower_bound_witness(), -numeric_traits<mpq>::one());
 }
 
     
@@ -1109,7 +1109,7 @@ bool lar_solver::the_right_sides_do_not_sum_to_zero(const vector<std::pair<mpq,
     return !numeric_traits<mpq>::is_zero(ret);
 }
 
-bool lar_solver::explanation_is_correct(const vector<std::pair<mpq, unsigned>>& explanation) const {
+bool lar_solver::explanation_is_correct(explanation& explanation) const {
     return true;
 #if 0
     // disabled: kind is uninitialized
@@ -1139,16 +1139,16 @@ bool lar_solver::explanation_is_correct(const vector<std::pair<mpq, unsigned>>&
 
 bool lar_solver::inf_explanation_is_correct() const {
 #ifdef Z3DEBUG
-    vector<std::pair<mpq, unsigned>> explanation;
+    explanation exp;
-    get_infeasibility_explanation(explanation);
+    get_infeasibility_explanation(exp);
-    return explanation_is_correct(explanation);
+    return explanation_is_correct(exp);
 #endif
     return true;
 }
 
-mpq lar_solver::sum_of_right_sides_of_explanation(const vector<std::pair<mpq, unsigned>> & explanation) const {
+mpq lar_solver::sum_of_right_sides_of_explanation(explanation& exp) const {
     mpq ret = numeric_traits<mpq>::zero();
-    for (auto & it : explanation) {
+    for (auto & it : exp) {
         mpq coeff = it.first;
         constraint_index con_ind = it.second;
         lp_assert(con_ind < m_constraints.size());
@@ -1214,10 +1214,10 @@ bool lar_solver::has_value(var_index var, mpq& value) const {
 }
 
 
-void lar_solver::get_infeasibility_explanation(vector<std::pair<mpq, constraint_index>> & explanation) const {
+void lar_solver::get_infeasibility_explanation(explanation& exp) const {
-    explanation.clear();
+    exp.clear();
     if (m_infeasible_column_index != -1) {
-        fill_explanation_from_infeasible_column(explanation);
+        fill_explanation_from_infeasible_column(exp);
         return;
     }
     if (m_mpq_lar_core_solver.get_infeasible_sum_sign() == 0) {
@@ -1226,14 +1226,14 @@ void lar_solver::get_infeasibility_explanation(vector<std::pair<mpq, constraint_
     // the infeasibility sign
     int inf_sign;
     auto inf_row = m_mpq_lar_core_solver.get_infeasibility_info(inf_sign);
-    get_infeasibility_explanation_for_inf_sign(explanation, inf_row, inf_sign);
+    get_infeasibility_explanation_for_inf_sign(exp, inf_row, inf_sign);
-    lp_assert(explanation_is_correct(explanation));
+    lp_assert(explanation_is_correct(exp));
 }
 
 
 
 void lar_solver::get_infeasibility_explanation_for_inf_sign(
-    vector<std::pair<mpq, constraint_index>> & explanation,
+    explanation & exp,
     const vector<std::pair<mpq, unsigned>> & inf_row,
     int inf_sign) const {
 
@@ -1246,7 +1246,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(bound_constr_i < m_constraints.size());
-        explanation.push_back(std::make_pair(coeff, bound_constr_i));
+        exp.push_justification(bound_constr_i, coeff);
     } 
 }
 

src/util/lp/lar_solver.h

@@ -307,7 +307,7 @@ public:
     
     lp_status solve();
 
-    void fill_explanation_from_infeasible_column(explanation_t & evidence) const;
+    void fill_explanation_from_infeasible_column(explanation & evidence) const;
 
     
     unsigned get_total_iterations() const;
@@ -454,11 +454,11 @@ public:
 
     bool the_right_sides_do_not_sum_to_zero(const vector<std::pair<mpq, unsigned>> & evidence);
 
-    bool explanation_is_correct(const vector<std::pair<mpq, unsigned>>& explanation) const;
+    bool explanation_is_correct(explanation&) const;
 
     bool inf_explanation_is_correct() const;
 
-    mpq sum_of_right_sides_of_explanation(const vector<std::pair<mpq, unsigned>> & explanation) const;
+    mpq sum_of_right_sides_of_explanation(explanation &) const;
 
     bool has_lower_bound(var_index var, constraint_index& ci, mpq& value, bool& is_strict) const;
     
@@ -466,10 +466,10 @@ public:
 
     bool has_value(var_index var, mpq& value) const;
 
-    void get_infeasibility_explanation(vector<std::pair<mpq, constraint_index>> & explanation) const;
+    void get_infeasibility_explanation(explanation &) const;
 
     void get_infeasibility_explanation_for_inf_sign(
-        vector<std::pair<mpq, constraint_index>> & explanation,
+        explanation & exp,
         const vector<std::pair<mpq, unsigned>> & inf_row,
         int inf_sign) const;
 

src/util/lp/lp_settings.h

@@ -32,8 +32,6 @@ typedef unsigned var_index;
 typedef unsigned constraint_index;
 typedef unsigned row_index;
 
-typedef vector<std::pair<mpq, constraint_index>> explanation_t;
-
 enum class column_type  {
     free_column = 0,
     lower_bound = 1,

src/util/lp/niil_solver.cpp

@@ -208,9 +208,7 @@ struct solver::imp {
 
     bool values_are_different(lpvar j, int sign, lpvar k) const {
         SASSERT(sign == 1 || sign == -1);
-        if (sign == 1)
+        return ! ( sign * m_lar_solver.get_column_value(j) == m_lar_solver.get_column_value(k));
-            return m_lar_solver.get_column_value(j) != m_lar_solver.get_column_value(k);        
-        return m_lar_solver.get_column_value(j) != - m_lar_solver.get_column_value(k);
     }
     
     void fill_lemma() {
@@ -342,7 +340,7 @@ void solver::add_monomial(lpvar v, unsigned sz, lpvar const* vs) {
 
 bool solver::need_check() { return true; }
 
-lbool solver::check(lemma& l) {
+lbool solver::check(lp::explanation & ex, lemma& l) {
     return m_imp->check(l);
 }
 

src/util/lp/niil_solver.h

@@ -44,6 +44,6 @@ public:
     void push();
     void pop(unsigned scopes);
     bool need_check();
-    lbool check(lemma&);
+    lbool check(lp::explanation&, lemma&);
 };
 }

src/util/lp/nra_solver.cpp

@@ -82,7 +82,7 @@ namespace nra {
            TBD: use partial model from lra_solver to prime the state of nlsat_solver.
            TBD: explore more incremental ways of applying nlsat (using assumptions)
         */
-        lbool check(lp::explanation_t& ex) {
+        lbool check(lp::explanation& ex) {
             SASSERT(need_check());
             m_nlsat = alloc(nlsat::solver, m_limit, m_params, false);
             m_zero = alloc(scoped_anum, am());
@@ -121,7 +121,7 @@ namespace nra {
                 m_nlsat->get_core(core);
                 for (auto c : core) {
                     unsigned idx = static_cast<unsigned>(static_cast<imp*>(c) - this);
-                    ex.push_back(std::pair<rational, unsigned>(rational(1), idx));
+                    ex.push_justification(idx, rational(1));
                     TRACE("arith", tout << "ex: " << idx << "\n";);
                 }
                 break;
@@ -247,7 +247,7 @@ namespace nra {
         m_imp->add(v, sz, vs);
     }
 
-    lbool solver::check(lp::explanation_t& ex) {
+    lbool solver::check(lp::explanation& ex) {
         return m_imp->check(ex);
     }
 

src/util/lp/nra_solver.h

@@ -39,7 +39,7 @@ namespace nra {
           \brief Check feasiblity of linear constraints augmented by polynomial definitions
           that are added.
          */
-        lbool check(lp::explanation_t& ex);
+        lbool check(lp::explanation& ex);
 
         /*
           \brief determine whether nra check is needed.