From d301a9c403291e3faf8be3451c0d02bad5ad869b Mon Sep 17 00:00:00 2001
From: Lev <levnach@hotmail.com>
Date: Mon, 24 Sep 2018 13:42:20 -0700
Subject: [PATCH] rebase with z3prover

Signed-off-by: Lev <levnach@hotmail.com>
---
 src/ast/ast.cpp            |  2 +-
 src/smt/theory_lra.cpp     | 75 ++++++++++++--------------------------
 src/test/lp/gomory_test.h  | 10 ++---
 src/test/lp/lp.cpp         | 16 +++++++-
 src/util/lp/gomory.cpp     |  8 ++--
 src/util/lp/int_solver.cpp | 37 ++++++-------------
 src/util/lp/nla_solver.cpp | 20 +++++++---
 src/util/lp/nla_solver.h   |  1 +
 8 files changed, 77 insertions(+), 92 deletions(-)

diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index fa461aca5..c02ba2400 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1928,7 +1928,7 @@ void ast_manager::delete_node(ast * n) {
         CTRACE("del_quantifier", is_quantifier(n), tout << "deleting quantifier " << n->m_id << " " << n << "\n";);
         TRACE("mk_var_bug", tout << "del_ast: " << " " << n->m_ref_count << "\n";);
         TRACE("ast_delete_node", tout << mk_bounded_pp(n, *this) << "\n";);
-        TRACE("ast", tout << mk_pp(n, *this) << "\n";);
+
         SASSERT(m_ast_table.contains(n));
         m_ast_table.erase(n);
         SASSERT(!m_ast_table.contains(n));
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 832cddc06..05a64aabc 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -159,6 +159,7 @@ class theory_lra::imp {
     ast_manager&         m;
     theory_arith_params& m_arith_params;
     arith_util           a;
+    bool                 m_has_int;
     arith_eq_adapter     m_arith_eq_adapter;
     vector<rational>     m_columns;
       
@@ -225,10 +226,10 @@ class theory_lra::imp {
     lp::var_index m_rzero_var;
 
     enum constraint_source {
-        inequality_source,
-        equality_source,
-        definition_source,
-        null_source
+                            inequality_source,
+                            equality_source,
+                            definition_source,
+                            null_source
     };
     svector<constraint_source>                    m_constraint_sources;
     svector<literal>                              m_inequalities;    // asserted rows corresponding to inequality literals.
@@ -363,7 +364,6 @@ class theory_lra::imp {
     enode* get_enode(expr* e) const { return ctx().get_enode(e); }
     expr*  get_owner(theory_var v) const { return get_enode(v)->get_owner(); }        
 
-    
     void init_solver() {
         if (m_solver) return;
 
@@ -427,10 +427,6 @@ class theory_lra::imp {
         add_const(0, m_zero_var);
         return m_zero_var;
     }
-    void ensure_niil() {
-        if (!m_niil) {
-            m_niil = alloc(niil::solver, *m_solver.get(), m.limit(), ctx().get_params());
-            m_switcher.m_niil = &m_niil;
 
     void ensure_nla() {
         if (!m_nla) {
@@ -724,6 +720,7 @@ class theory_lra::imp {
         }
         if (result == UINT_MAX) {
             result = m_solver->add_var(v, is_int(v));
+            m_has_int |= is_int(v);
             m_theory_var2var_index.setx(v, result, UINT_MAX);
             m_var_index2theory_var.setx(result, v, UINT_MAX);
             m_var_trail.push_back(v);
@@ -916,6 +913,7 @@ public:
         th(th), m(m), 
         m_arith_params(ap), 
         a(m), 
+        m_has_int(false),
         m_arith_eq_adapter(th, ap, a),            
         m_internalize_head(0),
         m_one_var(UINT_MAX),
@@ -1512,6 +1510,7 @@ public:
     }
 
     void init_variable_values() {
+        reset_variable_values();
         if (!m.canceled() && m_solver.get() && th.get_num_vars() > 0) {
             TRACE("arith", tout << "update variable values\n";);
             m_solver->get_model(m_variable_values);
@@ -1537,9 +1536,9 @@ public:
         init_variable_values();
         TRACE("arith", 
               for (theory_var v = 0; v < sz; ++v) {
-                  if (th.is_relevant_and_shared(get_enode(v))) { 
-                      tout << "v" << v << " ";
-                  }
+                                                   if (th.is_relevant_and_shared(get_enode(v))) { 
+                                                                                                 tout << "v" << v << " ";
+                                                   }
               }
               tout << "\n"; );
         if (!m_use_nra_model) {
@@ -1752,7 +1751,7 @@ public:
         return atom;
     }
 
-    /*    bool make_sure_all_vars_have_bounds() {
+    bool make_sure_all_vars_have_bounds() {
         if (!m_has_int) {
             return true;
         }
@@ -1764,7 +1763,7 @@ public:
                 continue;
             if (!m_solver->is_term(vi) && !var_has_bound(vi, true) && !var_has_bound(vi, false)) {
                 lp::lar_term term;
-                term.add_monomial(rational::one(), vi);
+                term.add_coeff_var(rational::one(), vi);
                 app_ref b = mk_bound(term, rational::zero(), true);
                 TRACE("arith", tout << "added bound " << b << "\n";);
                 IF_VERBOSE(2, verbose_stream() << "bound: " << b << "\n");
@@ -1772,7 +1771,7 @@ public:
             }
         }
         return all_bounded;
-        }*/
+    }
 
     /**
      * n = (div p q)
@@ -1973,28 +1972,6 @@ public:
         visitor.display_asserts(out, fmls, true);
         out << "(check-sat)\n";            
     }
-    
-    bool all_variables_have_bounds() {
-        if (!m_has_int) {
-            return true;
-        }
-        unsigned nv = th.get_num_vars();
-        bool added_bound = false;
-        for (unsigned v = 0; v < nv; ++v) {
-            lp::constraint_index ci;
-            rational bound;
-            lp::var_index vi = m_theory_var2var_index[v];
-            if (!has_upper_bound(vi, ci, bound) && !has_lower_bound(vi, ci, bound)) {
-                lp::lar_term term;
-                term.add_coeff_var(rational::one(), vi);
-                app_ref b = mk_bound(term, rational::zero(), false);
-                TRACE("arith", tout << "added bound " << b << "\n";);
-                added_bound = true;
-            }
-        }
-        return !added_bound;
-    }
-
 
     lbool check_lia() {
         if (m.canceled()) {
@@ -2005,11 +1982,6 @@ public:
         if (!check_idiv_bounds()) {
             return l_false;
         }
-
-        lp::lar_term term;
-        lp::mpq k;
-        lp::explanation ex; // TBD, this should be streamlined accross different explanations
-        bool upper;
         m_explanation.reset();
         switch (m_lia->check()) {
         case lp::lia_move::sat:
@@ -2048,7 +2020,7 @@ public:
             m_eqs.reset();
             m_core.reset();
             m_params.reset();
-            for (auto const& ev : ex) {
+            for (auto const& ev : m_explanation) {
                 if (!ev.first.is_zero()) { 
                     set_evidence(ev.second);
                 }
@@ -2064,7 +2036,6 @@ public:
         case lp::lia_move::conflict:
             TRACE("arith", tout << "conflict\n";);
             // ex contains unsat core
-            m_explanation = ex;
             set_conflict1();
             lia_check = l_false;
             break;
@@ -2365,7 +2336,7 @@ public:
                   );
             DEBUG_CODE(
                 for (auto& lit : m_core) {
-                    SASSERT(ctx().get_assignment(lit) == l_true);
+                                          SASSERT(ctx().get_assignment(lit) == l_true);
                 });
             ++m_stats.m_bound_propagations1;
             assign(lit);
@@ -2569,7 +2540,7 @@ public:
             }            
             CTRACE("arith_verbose", !atoms.empty(),  
                    for (unsigned i = 0; i < atoms.size(); ++i) {
-                       atoms[i]->display(tout); tout << "\n";
+                                                                atoms[i]->display(tout); tout << "\n";
                    });
             lp_bounds occs(m_bounds[v]);
                 
@@ -3212,6 +3183,12 @@ public:
             m_core.push_back(lit);
         }
         // m_solver->shrink_explanation_to_minimum(m_explanation); // todo, enable when perf is fixed
+        /*
+          static unsigned cn = 0;
+          static unsigned num_l = 0;
+          num_l+=m_explanation.size();
+          std::cout << num_l / (++cn) << "\n";
+        */
         ++m_num_conflicts;
         ++m_stats.m_conflicts;
         TRACE("arith", tout << "scope: " << ctx().get_scope_level() << "\n"; display_evidence(tout, m_explanation); );
@@ -3266,10 +3243,6 @@ public:
 
     void init_model(model_generator & mg) {
         init_variable_values();
-        DEBUG_CODE(            
-            for (auto const& kv : m_variable_values) {
-                SASSERT(!m_solver->var_is_int(kv.first) || kv.second.is_int() || m.canceled());
-            });
         m_factory = alloc(arith_factory, m);
         mg.register_factory(m_factory);
         TRACE("arith", display(tout););
@@ -3572,7 +3545,7 @@ public:
 
     app_ref coeffs2app(u_map<rational> const& coeffs, rational const& offset, bool is_int) {
         expr_ref_vector args(m);
-         for (auto const& kv : coeffs) {
+        for (auto const& kv : coeffs) {
             theory_var w = kv.m_key;
             expr* o = get_enode(w)->get_owner();
             if (kv.m_value.is_zero()) {
diff --git a/src/test/lp/gomory_test.h b/src/test/lp/gomory_test.h
index 37817d0c7..304ef52f1 100644
--- a/src/test/lp/gomory_test.h
+++ b/src/test/lp/gomory_test.h
@@ -82,7 +82,7 @@ struct gomory_test {
             expl.push_justification(column_upper_bound_constraint(x_j), new_a);
         }
         TRACE("gomory_cut_detail_real", tout << a << "*v" << x_j << " k: " << k << "\n";);
-        pol.add_monomial(new_a, x_j);
+        pol.add_coeff_var(new_a, x_j);
     }
     
     void int_case_in_gomory_cut(const mpq & a, unsigned x_j, mpq & k, lar_term & t, explanation& expl, mpq & lcm_den, const mpq& f_0, const mpq& one_minus_f_0) {
@@ -122,7 +122,7 @@ struct gomory_test {
             expl.push_justification(column_upper_bound_constraint(x_j), new_a);
         }
         TRACE("gomory_cut_detail", tout << "new_a: " << new_a << " k: " << k << "\n";);
-        t.add_monomial(new_a, x_j);
+        t.add_coeff_var(new_a, x_j);
         lcm_den = lcm(lcm_den, denominator(new_a));
     }
 
@@ -145,12 +145,12 @@ struct gomory_test {
                 if (!k.is_int())
                     k = ceil(k);
                 // switch size
-                t.add_monomial(- mpq(1), v);
+                t.add_coeff_var(- mpq(1), v);
                 k.neg();
             } else {
                 if (!k.is_int())
                     k = floor(k);
-                t.add_monomial(mpq(1), v);
+                t.add_coeff_var(mpq(1), v);
             }
         } else {
             TRACE("gomory_cut_detail", tout << "pol.size() > 1" << std::endl;);
@@ -177,7 +177,7 @@ struct gomory_test {
             
             // negate everything to return -pol <= -k
             for (const auto & pi: pol)
-                t.add_monomial(-pi.first, pi.second);
+                t.add_coeff_var(-pi.first, pi.second);
             k.neg();
         }
         TRACE("gomory_cut_detail", tout << "k = " << k << std::endl;);
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index e764a985c..fe3128159 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -54,6 +54,7 @@
 #include "util/lp/lu_def.h"
 #include "util/lp/general_matrix.h"
 #include "util/lp/bound_propagator.h"
+#include "util/lp/nla_solver.h"
 namespace lp {
 unsigned seed = 1;
 
@@ -1895,6 +1896,7 @@ void test_replace_column() {
 
 
 void setup_args_parser(argument_parser & parser) {
+    parser.add_option_with_help_string("-nla", "test nla_solver");
     parser.add_option_with_help_string("-hnf", "test hermite normal form");
     parser.add_option_with_help_string("-gomory", "gomory");
     parser.add_option_with_help_string("-intd", "test integer_domain");
@@ -2405,7 +2407,7 @@ void run_lar_solver(argument_parser & args_parser, lar_solver * solver, mps_read
     lp_status status = solver->solve();
     std::cout << "status is " <<  lp_status_to_string(status) << ", processed for " << sw.get_current_seconds() <<" seconds, and " << solver->get_total_iterations() << " iterations" << std::endl;
     if (solver->get_status() == lp_status::INFEASIBLE) {
-        vector<std::pair<lp::mpq, constraint_index>> evidence;
+        explanation evidence;
         solver->get_infeasibility_explanation(evidence);
     }
     if (args_parser.option_is_used("--randomize_lar")) {
@@ -3546,6 +3548,10 @@ void test_gomory_cut() {
     test_gomory_cut_1();
 }
 
+void test_nla() {
+    nla::solver::test();
+}
+
 void test_lp_local(int argn, char**argv) {
     
     // initialize_util_module();
@@ -3561,7 +3567,15 @@ void test_lp_local(int argn, char**argv) {
     }
 
     args_parser.print();
+    
+    if (args_parser.option_is_used("-nla")) {
+#ifdef Z3DEBUG
+        test_nla();
+#endif
+        return finalize(0);
+    }
 
+    
     if (args_parser.option_is_used("-hnf")) {
 #ifdef Z3DEBUG
         test_hnf();
diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp
index 15453f1e5..b0ae395bd 100644
--- a/src/util/lp/gomory.cpp
+++ b/src/util/lp/gomory.cpp
@@ -69,8 +69,8 @@ class gomory::imp {
             m_ex.push_justification(column_upper_bound_constraint(j));
         }
         m_t.add_coeff_var(new_a, j);
-        lcm_den = lcm(lcm_den, denominator(new_a));
-        TRACE("gomory_cut_detail", tout << "new_a = " << new_a << ", k = " << m_k << ", lcm_den = " << lcm_den << "\n";);
+        m_lcm_den = lcm(m_lcm_den, denominator(new_a));
+        TRACE("gomory_cut_detail", tout << "new_a = " << new_a << ", k = " << m_k << ", lcm_den = " << m_lcm_den << "\n";);
     }
 
     void real_case_in_gomory_cut(const mpq & a, unsigned j) {
@@ -98,8 +98,8 @@ class gomory::imp {
             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));
         }
-        TRACE("gomory_cut_detail_real", tout << a << "*v" << x_j << " k: " << m_k << "\n";);
-        m_t.add_coeff_var(new_a, x_j);
+        TRACE("gomory_cut_detail_real", tout << a << "*v" << j << " k: " << m_k << "\n";);
+        m_t.add_coeff_var(new_a, j);
     }
 
     lia_move report_conflict_from_gomory_cut() {
diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp
index f86a2f3e8..e2670fad7 100644
--- a/src/util/lp/int_solver.cpp
+++ b/src/util/lp/int_solver.cpp
@@ -118,21 +118,6 @@ constraint_index int_solver::column_upper_bound_constraint(unsigned j) const {
     return m_lar_solver->get_column_upper_bound_witness(j);
 }
 
-bool int_solver::current_solution_is_inf_on_cut() const {
-    const auto & x = m_lar_solver->m_mpq_lar_core_solver.m_r_x;
-    impq v = m_t->apply(x);
-    mpq sign = *m_upper ? one_of_type<mpq>()  : -one_of_type<mpq>();
-    CTRACE("current_solution_is_inf_on_cut", v * sign <= (*m_k) * sign,
-           tout << "m_upper = " << *m_upper << std::endl;
-           tout << "v = " << v << ", k = " << (*m_k) << std::endl;
-          );
-    return v * sign > (*m_k) * sign;
-}
-
-constraint_index int_solver::column_lower_bound_constraint(unsigned j) const {
-    return m_lar_solver->get_column_lower_bound_witness(j);
-}
-
 bool int_solver::current_solution_is_inf_on_cut() const {
     const auto & x = m_lar_solver->m_mpq_lar_core_solver.m_r_x;
     impq v = m_t.apply(x);
@@ -144,6 +129,10 @@ bool int_solver::current_solution_is_inf_on_cut() const {
     return v * sign > m_k * sign;
 }
 
+constraint_index int_solver::column_lower_bound_constraint(unsigned j) const {
+    return m_lar_solver->get_column_lower_bound_witness(j);
+}
+
 lia_move int_solver::mk_gomory_cut( unsigned inf_col, const row_strip<mpq> & row) {
 
     lp_assert(column_is_int_inf(inf_col));
@@ -186,11 +175,9 @@ typedef monomial mono;
 // this will allow to enable and disable tracking of the pivot rows
 struct check_return_helper {
     lar_solver *     m_lar_solver;
-    const lia_move & m_r;
     bool             m_track_pivoted_rows;
-    check_return_helper(lar_solver* ls, const lia_move& r) :
+    check_return_helper(lar_solver* ls) :
         m_lar_solver(ls),
-        m_r(r),
         m_track_pivoted_rows(ls->get_track_pivoted_rows())
     {
         TRACE("pivoted_rows", tout << "pivoted rows = " << ls->m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows->size() << std::endl;);
@@ -389,8 +376,8 @@ lia_move int_solver::make_hnf_cut() {
 
     if (r == lia_move::cut) {      
         TRACE("hnf_cut",
-              m_lar_solver->print_term(*m_t, tout << "cut:"); 
-              tout << " <= " << *m_k << std::endl;
+              m_lar_solver->print_term(m_t, tout << "cut:"); 
+              tout << " <= " << m_k << std::endl;
               for (unsigned i : m_hnf_cutter.constraints_for_explanation()) {
                   m_lar_solver->print_constraint(i, tout);
               }              
@@ -433,7 +420,7 @@ lia_move int_solver::check() {
 
     CHECK_RET(run_gcd_test());
 
-    check_return_helper pc(m_lar_solver, r);
+    check_return_helper pc(m_lar_solver);
 
     if (settings().m_int_pivot_fixed_vars_from_basis)
         m_lar_solver->pivot_fixed_vars_from_basis();
@@ -611,8 +598,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(uc);
+    m_ex.push_justification(lc);
+    m_ex.push_justification(uc);
 }
 void int_solver::fill_explanation_from_fixed_columns(const row_strip<mpq> & row) {
     for (const auto & c : row) {
@@ -1009,13 +996,13 @@ lia_move int_solver::create_branch_on_column(int j) {
     TRACE("check_main_int", tout << "branching" << std::endl;);
     lp_assert(m_t.is_empty());
     lp_assert(j != -1);
-    m_t->add_coeff_var(mpq(1), m_lar_solver->adjust_column_index_to_term_index(j));
+    m_t.add_coeff_var(mpq(1), m_lar_solver->adjust_column_index_to_term_index(j));
     if (is_free(j)) {
         m_upper = true;
         m_k = mpq(0);
     } else {
         m_upper = left_branch_is_more_narrow_than_right(j);
-        m_k = *m_upper? floor(get_value(j)) : ceil(get_value(j));        
+        m_k = m_upper? floor(get_value(j)) : ceil(get_value(j));        
     }
 
     TRACE("int_solver", tout << "branching v" << j << " = " << get_value(j) << "\n";
diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index 58abeb208..534bba720 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -77,7 +77,8 @@ struct vars_equivalence {
     unsigned size() const { return m_map.size(); }
 
     void add_equivalence_maybe(const lp::lar_term *t, lpci c0, lpci c1) {
-        if (t->size() != 2 || ! t->m_v.is_zero())
+        SASSERT(false); // check for new terms
+        if (t->size() != 2 || t->size() != 3)
             return;
         bool seen_minus = false;
         bool seen_plus = false;
@@ -489,7 +490,8 @@ struct solver::imp {
         }
         lp::lar_term t;
         t.add_coeff_var(rational(1), m_monomials[i_mon].var());
-        t.m_v = -rs;
+        SASSERT(false); // figure out the change!!!!!! 
+        //  t.m_v = -rs;
         ineq in(kind, t);
         m_lemma->push_back(in);
         TRACE("nla_solver", print_explanation_and_lemma(tout););
@@ -1274,6 +1276,9 @@ struct solver::imp {
         
         return l_undef;
     }
+    void test() {
+        std::cout << "test called\n";
+    }
 }; // end of imp
 
 void solver::add_monomial(lpvar v, unsigned sz, lpvar const* vs) {
@@ -1286,9 +1291,6 @@ lbool solver::check(lp::explanation & ex, lemma& l) {
     return m_imp->check(ex, l);
 }
 
-
-}; // end of imp
-
 void solver::add_monomial(lpvar v, unsigned sz, lpvar const* vs) {
     m_imp->add(v, sz, vs);
 }
@@ -1315,4 +1317,12 @@ solver::~solver() {
     dealloc(m_imp);
 }
 
+void solver::test() {
+    lp::lar_solver s;
+    reslimit l;
+    params_ref p;
+    imp i(s, l, p);
+    i.test();
+}
+
 }
diff --git a/src/util/lp/nla_solver.h b/src/util/lp/nla_solver.h
index c8cf074b9..eb45957de 100644
--- a/src/util/lp/nla_solver.h
+++ b/src/util/lp/nla_solver.h
@@ -45,5 +45,6 @@ public:
     void pop(unsigned scopes);
     bool need_check();
     lbool check(lp::explanation&, lemma&);
+    static void test();
 };
 }