change the signature of int_solver::check by adding explanation* parameter

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

src/smt/theory_lra.cpp

@@ -415,7 +415,6 @@ class theory_lra::imp {
             return var;
         }
         app_ref cnst(a.mk_numeral(rational(c), is_int), m);
-        TRACE("arith", tout << "add " << cnst << "\n";);
         mk_enode(cnst);
         theory_var v = mk_var(cnst);
         var = m_solver->add_var(v, true);
@@ -424,6 +423,7 @@ class theory_lra::imp {
         m_var_trail.push_back(v);
         add_def_constraint(m_solver->add_var_bound(var, lp::GE, rational(c)));
         add_def_constraint(m_solver->add_var_bound(var, lp::LE, rational(c)));
+        TRACE("arith", tout << "add " << cnst << ", var = " << var << "\n";);
         return var;
     }
 
@@ -785,7 +785,7 @@ class theory_lra::imp {
         m_constraint_sources.setx(index, inequality_source, null_source);
         m_inequalities.setx(index, lit, null_literal);
         ++m_stats.m_add_rows;
-        TRACE("arith", m_solver->print_constraint(index, tout) << "\n";);
+        TRACE("arith", m_solver->print_constraint(index, tout) << " m_stats.m_add_rows = " << m_stats.m_add_rows << "\n";);
     }
 
     void add_def_constraint(lp::constraint_index index) {
@@ -1709,7 +1709,7 @@ public:
                 
             return st;
         case l_false:
-            set_conflict();
+            get_infeasibility_explanation_and_set_conflict();
             return FC_CONTINUE;
         case l_undef:
             TRACE("arith", tout << "check feasiable is undef\n";);
@@ -2023,8 +2023,7 @@ public:
         if (!check_idiv_bounds()) {
             return l_false;
         }
-        m_explanation.clear();
+        switch (m_lia->check(&m_explanation)) {
-        switch (m_lia->check()) {
         case lp::lia_move::sat:
             lia_check = l_true;
             break;
@@ -2057,11 +2056,11 @@ public:
                 m.trace_stream() << "[end-of-instance]\n";
             }
             IF_VERBOSE(2, verbose_stream() << "cut " << b << "\n");
-            TRACE("arith", dump_cut_lemma(tout, m_lia->get_term(), m_lia->get_offset(), m_lia->get_explanation(), m_lia->is_upper()););
+            TRACE("arith", dump_cut_lemma(tout, m_lia->get_term(), m_lia->get_offset(), m_explanation, m_lia->is_upper()););
             m_eqs.reset();
             m_core.reset();
             m_params.reset();
-            for (auto const& ev : m_lia->get_explanation()) {
+            for (auto const& ev : m_explanation) {
                 if (!ev.first.is_zero()) { 
                     set_evidence(ev.second);
                 }
@@ -2077,9 +2076,8 @@ public:
         case lp::lia_move::conflict:
             TRACE("arith", tout << "conflict\n";);
             // ex contains unsat core
-            set_conflict1();
+            set_conflict();
-            lia_check = l_false;
+            return l_false;
-            break;
         case lp::lia_move::undef:
             TRACE("arith", tout << "lia undef\n";);
             lia_check = l_undef;
@@ -2098,7 +2096,7 @@ public:
         m_a2 = alloc(scoped_anum, m_nra->am());
         switch (r) {
         case l_false:
-            set_conflict1();
+            set_conflict();
             break;
         case l_true:
             m_use_nra_model = true;
@@ -2271,7 +2269,7 @@ public:
         switch(lbl) {
         case l_false:
             TRACE("arith", tout << "propagation conflict\n";);
-            set_conflict();
+            get_infeasibility_explanation_and_set_conflict();
             break;
         case l_true:
             propagate_basic_bounds();
@@ -2298,7 +2296,7 @@ public:
         (void)new_num_of_p;
         CTRACE("arith", new_num_of_p > num_of_p, tout << "found " << new_num_of_p << " implied bounds\n";);
         if (is_infeasible()) {
-            set_conflict();
+            get_infeasibility_explanation_and_set_conflict();
         }
         else {
             for (unsigned i = 0; !m.canceled() && !ctx().inconsistent() && i < bp.m_ibounds.size(); ++i) {
@@ -3237,13 +3235,13 @@ public:
         }
     }
 
-    void set_conflict() {
+    void get_infeasibility_explanation_and_set_conflict() {
         m_explanation.clear();
         m_solver->get_infeasibility_explanation(m_explanation);
-        set_conflict1();
+        set_conflict();
     }
 
-    void set_conflict1() {
+    void set_conflict() {
         literal_vector core;
         set_conflict_or_lemma(core, true);
     }

src/test/lp/lp.cpp

@@ -3521,7 +3521,8 @@ void test_maximize_term() {
         std::cout<< "v[" << p.first << "] = " << p.second << std::endl;
     }
     std::cout << "calling int_solver\n";
-    lia_move lm = i_solver.check();
+    explanation ex;
+    lia_move lm = i_solver.check(&ex);
     VERIFY(lm == lia_move::sat);
     impq term_max;
     lp_status st = solver.maximize_term(term_2x_pl_2y, term_max);

src/util/lp/gomory.cpp

@@ -26,7 +26,7 @@ namespace lp {
 class gomory::imp {
     lar_term   &          m_t; // the term to return in the cut
     mpq        &          m_k; // the right side of the cut
-    explanation&          m_ex; // the conflict explanation
+    explanation*          m_ex; // the conflict explanation
     unsigned              m_inf_col; // a basis column which has to be an integer but has a non integral value
     const row_strip<mpq>& m_row;
     const int_solver&     m_int_solver;
@@ -58,7 +58,7 @@ class gomory::imp {
             new_a = m_fj <= m_one_minus_f ? m_fj / m_one_minus_f : ((1 - m_fj) / m_f);
             lp_assert(new_a.is_pos());
             m_k.addmul(new_a, lower_bound(j).x);
-            m_ex.push_justification(column_lower_bound_constraint(j));            
+            m_ex->push_justification(column_lower_bound_constraint(j));            
         }
         else {
             lp_assert(at_upper(j));
@@ -66,7 +66,7 @@ class gomory::imp {
             new_a = - (m_fj <= m_f ? m_fj / m_f  : ((1 - m_fj) / m_one_minus_f));
             lp_assert(new_a.is_neg());
             m_k.addmul(new_a, upper_bound(j).x);
-            m_ex.push_justification(column_upper_bound_constraint(j));
+            m_ex->push_justification(column_upper_bound_constraint(j));
         }
         m_t.add_coeff_var(new_a, j);
         m_lcm_den = lcm(m_lcm_den, denominator(new_a));
@@ -85,7 +85,7 @@ class gomory::imp {
             }
             m_k.addmul(new_a, lower_bound(j).x); // is it a faster operation than
             // k += lower_bound(j).x * new_a;  
-            m_ex.push_justification(column_lower_bound_constraint(j));
+            m_ex->push_justification(column_lower_bound_constraint(j));
         }
         else {
             lp_assert(at_upper(j));
@@ -96,7 +96,7 @@ class gomory::imp {
                 new_a =   a / m_one_minus_f; 
             }
             m_k.addmul(new_a, upper_bound(j).x); //  k += upper_bound(j).x * new_a; 
-            m_ex.push_justification(column_upper_bound_constraint(j));
+            m_ex->push_justification(column_upper_bound_constraint(j));
         }
         TRACE("gomory_cut_detail_real", tout << a << "*v" << j << " k: " << m_k << "\n";);
         m_t.add_coeff_var(new_a, j);
@@ -314,7 +314,7 @@ public:
         return lia_move::cut;
     }
 
-    imp(lar_term & t, mpq & k, explanation& ex, unsigned basic_inf_int_j, const row_strip<mpq>& row, const int_solver& int_slv ) :
+    imp(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_int_j, const row_strip<mpq>& row, const int_solver& int_slv ) :
         m_t(t),
         m_k(k),
         m_ex(ex),
@@ -331,7 +331,7 @@ lia_move gomory::create_cut() {
     return m_imp->create_cut();
 }
 
-gomory::gomory(lar_term & t, mpq & k, explanation& ex, unsigned basic_inf_int_j, const row_strip<mpq>& row, const int_solver& s) {
+gomory::gomory(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_int_j, const row_strip<mpq>& row, const int_solver& s) {
     m_imp = alloc(imp, t, k, ex, basic_inf_int_j, row, s);
 }
 

src/util/lp/gomory.h

@@ -27,7 +27,7 @@ class gomory {
     class imp;
     imp                  *m_imp;
 public :
-    gomory(lar_term & t, mpq & k, explanation& ex, unsigned basic_inf_int_j, const row_strip<mpq>& row, const int_solver& s);
+    gomory(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_int_j, const row_strip<mpq>& row, const int_solver& s);
     lia_move create_cut();
     ~gomory();
 };

src/util/lp/hnf_cutter.h

@@ -186,7 +186,7 @@ public:
 
     bool overflow() const { return m_overflow; }
     
-    lia_move create_cut(lar_term& t, mpq& k, explanation& ex, bool & upper, const vector<mpq> & x0) {
+    lia_move create_cut(lar_term& t, mpq& k, explanation* ex, bool & upper, const vector<mpq> & x0) {
         // we suppose that x0 has at least one non integer element 
         (void)x0;
 

src/util/lp/int_solver.cpp

@@ -382,9 +382,9 @@ lia_move int_solver::make_hnf_cut() {
               );
         lp_assert(current_solution_is_inf_on_cut());
         settings().st().m_hnf_cuts++;
-        m_ex.clear();        
+        m_ex->clear();        
         for (unsigned i : m_hnf_cutter.constraints_for_explanation()) {
-             m_ex.push_justification(i);
+             m_ex->push_justification(i);
         }
     } 
     return r;
@@ -412,7 +412,8 @@ lia_move int_solver::check() {
 
     m_t.clear();
     m_k.reset();
-    m_ex.clear();
+    m_ex = e;
+    m_ex->clear();
     m_upper = false;
     lia_move r;
 
@@ -596,8 +597,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.push_justification(lc);
+    m_ex->push_justification(lc);
-    m_ex.push_justification(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/int_solver.h

@@ -41,7 +41,7 @@ public:
     unsigned            m_number_of_calls;
     lar_term            m_t; // the term to return in the cut
     mpq                 m_k; // the right side of the cut
-    explanation         m_ex; // the conflict explanation
+    explanation         *m_ex; // the conflict explanation
     bool                m_upper; // we have a cut m_t*x <= k if m_upper is true nad m_t*x >= k otherwise
     hnf_cutter          m_hnf_cutter;
     // methods
@@ -49,10 +49,9 @@ public:
 
     // main function to check that the solution provided by lar_solver is valid for integral values,
     // or provide a way of how it can be adjusted.
-    lia_move check();
+    lia_move check(explanation *);
     lar_term const& get_term() const { return m_t; }
     mpq const& get_offset() const { return m_k; }
-    explanation const& get_explanation() const { return m_ex; }
     bool is_upper() const { return m_upper; }
     lia_move check_wrapper(lar_term& t, mpq& k, explanation& ex);    
     bool is_base(unsigned j) const;

src/util/lp/nla_solver.cpp

@@ -831,12 +831,36 @@ struct solver::imp {
         m_expl->clear();
         m_lemma->clear();
     }
+
+    bool order_lemma_on_factor_equiv_and_other_mon_factor(unsigned i_f,
+                                                   unsigned o_i_mon, unsigned e_j, unsigned i_mon, const factorization& f, unsigned k, const rational& sign) {
+        return false;
+    }    
+    
     bool order_lemma_on_factor_equiv_and_other_mon(unsigned o_i_mon, unsigned e_j, unsigned i_mon, const factorization& f, unsigned k, const rational& sign) {
-        NOT_IMPLEMENTED_YET();
+        if (o_i_mon == i_mon) return false;
+        const monomial & o_m = m_monomials[o_i_mon];
+        svector<lpvar> o_key;
+        for (unsigned j : o_m) {
+            if (j != e_j) {
+                o_key.push_back(j);
+            }
+        }
+
+        rational o_sign(1);
+        o_key = reduce_monomial_to_rooted(o_key, o_sign);
+        auto it = m_rooted_monomials.find(o_key);
+        if (it == m_rooted_monomials.end())
+            return false;
+        for (const index_with_sign& i_s : it->second) {
+            if (order_lemma_on_factor_equiv_and_other_mon_factor(i_s.var(), o_i_mon, e_j, i_mon, f, k, sign * o_sign * i_s.sign()))
+                return true;
+        }
         return false;
     }
-    // here e_j is equivalent to f[k],
+
     // f is a factorization of m_monomials[i_mon]
+    // here e_j is equivalent to f[k],
     bool order_lemma_on_factor_and_equiv(unsigned e_j, unsigned i_mon, const factorization& f, unsigned k, const rational& sign) {
         lpvar j = f[k];
         for (unsigned i : m_monomials_containing_var[j]) {

src/util/lp/vars_equivalence.h

@@ -36,6 +36,8 @@ struct index_with_sign {
     bool operator==(const index_with_sign& b) {
         return m_i == b.m_i && m_sign == b.m_sign;
     }
+    unsigned var() const { return m_i; }
+    const rational& sign() const { return m_sign; }
 };
 
 struct rat_hash {