start porting grobner basis functionality

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

src/math/lp/horner.cpp

@@ -72,7 +72,7 @@ bool horner::lemmas_on_expr(cross_nested& cn) {
 
 bool horner::check_cross_nested_expr(const nex* n) {
     TRACE("nla_horner", tout << "cross-nested n = " << *n << "\n";);
-    c().lp_settings().st().m_cross_nested_forms++;
+    c().lp_settings().stats().m_cross_nested_forms++;
 
     auto i = interval_of_expr(n);
     TRACE("nla_horner", tout << "callback n = " << *n << "\ni="; m_intervals.display(tout, i) << "\n";);
@@ -105,7 +105,7 @@ void horner::horner_lemmas() {
         TRACE("nla_solver", tout << "not generating horner lemmas\n";);
         return;
     }
-    c().lp_settings().st().m_horner_calls++;
+    c().lp_settings().stats().m_horner_calls++;
     const auto& matrix = c().m_lar_solver.A_r();
     // choose only rows that depend on m_to_refine variables
     std::set<unsigned> rows_to_check; // we need it to be determenistic: cannot work with the unordered_set
@@ -125,7 +125,7 @@ void horner::horner_lemmas() {
     for (unsigned i = 0; i < sz; i++) {
         unsigned row_index = rows[(i + r) % sz];
         if (lemmas_on_row(matrix.m_rows[row_index])) {
-            c().lp_settings().st().m_horner_conflicts++;
+            c().lp_settings().stats().m_horner_conflicts++;
             break;
         }
     }

src/math/lp/int_solver.cpp

@@ -244,7 +244,7 @@ lia_move int_solver::find_cube() {
     if (m_number_of_calls % settings().m_int_find_cube_period != 0)
         return lia_move::undef;
     
-    settings().st().m_cube_calls++;
+    settings().stats().m_cube_calls++;
     TRACE("cube",
           for (unsigned j = 0; j < m_lar_solver->A_r().column_count(); j++)
               display_column(tout, j);
@@ -271,8 +271,7 @@ lia_move int_solver::find_cube() {
     m_lar_solver->set_status(lp_status::FEASIBLE);
     lp_assert(settings().get_cancel_flag() || is_feasible());
     TRACE("cube", tout << "success";);
-    settings().st().m_cube_success++;
-    TRACE("cube", tout << "sat with cube\n";);
+    settings().stats().m_cube_success++;
     return lia_move::sat;
 }
 
@@ -283,8 +282,8 @@ void int_solver::find_feasible_solution() {
 
 lia_move int_solver::run_gcd_test() {
     if (settings().m_int_run_gcd_test) {
-        settings().st().m_gcd_calls++;
-        TRACE("int_solver", tout << "gcd-test " << settings().st().m_gcd_calls << "\n";);
+        settings().stats().m_gcd_calls++;
+        TRACE("int_solver", tout << "gcd-test " << settings().stats().m_gcd_calls << "\n";);
         if (!gcd_test()) {
             settings().st().m_gcd_conflicts++;
             TRACE("gcd_test", tout << "gcd conflict\n";);
@@ -362,8 +361,8 @@ lia_move int_solver::make_hnf_cut() {
     if (!init_terms_for_hnf_cut()) {
         return lia_move::undef;
     }
-    settings().st().m_hnf_cutter_calls++;
-    TRACE("hnf_cut", tout << "settings().st().m_hnf_cutter_calls = " << settings().st().m_hnf_cutter_calls << "\n";
+    settings().stats().m_hnf_cutter_calls++;
+    TRACE("hnf_cut", tout << "settings().stats().m_hnf_cutter_calls = " << settings().stats().m_hnf_cutter_calls << "\n";
           for (unsigned i : m_hnf_cutter.constraints_for_explanation()) {
               m_lar_solver->print_constraint(i, tout);
           }              
@@ -385,7 +384,7 @@ lia_move int_solver::make_hnf_cut() {
               }              
               );
         lp_assert(current_solution_is_inf_on_cut());
-        settings().st().m_hnf_cuts++;
+        settings().stats().m_hnf_cuts++;
         m_ex->clear();        
         for (unsigned i : m_hnf_cutter.constraints_for_explanation()) {
              m_ex->push_justification(i);
@@ -512,14 +511,14 @@ void int_solver::patch_nbasic_column(unsigned j, bool patch_only_int_vals) {
 }
 
 lia_move int_solver::patch_nbasic_columns() {
-    settings().st().m_patches++;
+    settings().stats().m_patches++;
     lp_assert(is_feasible());
     for (unsigned j : m_lar_solver->m_mpq_lar_core_solver.m_r_nbasis) {
         patch_nbasic_column(j, settings().m_int_patch_only_integer_values);
     }
     lp_assert(is_feasible());
     if (!has_inf_int()) {
-        settings().st().m_patches_success++;
+        settings().stats().m_patches_success++;
         return lia_move::sat;
     }
     return lia_move::undef;

src/math/lp/lar_core_solver_def.h

@@ -274,7 +274,7 @@ void lar_core_solver::solve() {
             TRACE("lar_solver", tout << m_r_solver.get_status() << "\n";);
             return;
 	}
-    ++settings().st().m_need_to_solve_inf;
+    ++settings().stats().m_need_to_solve_inf;
     CASSERT("A_off", !m_r_solver.A_mult_x_is_off());
     lp_assert((!settings().use_tableau()) || r_basis_is_OK());
     if (need_to_presolve_with_double_solver()) {

src/math/lp/lp_core_solver_base.h

@@ -35,7 +35,7 @@ template <typename T, typename X> // X represents the type of the x variable and
 class lp_core_solver_base {    
     unsigned m_total_iterations;
     unsigned m_iters_with_no_cost_growing;
-    unsigned inc_total_iterations() { ++m_settings.st().m_total_iterations; return m_total_iterations++; }
+    unsigned inc_total_iterations() { ++m_settings.stats().m_total_iterations; return m_total_iterations++; }
 private:
     lp_status m_status;
 public:

src/math/lp/lp_settings.h

@@ -89,7 +89,7 @@ public:
     virtual bool get_cancel_flag() = 0;
 };
 
-struct stats {
+struct statistics {
     unsigned m_make_feasible;
     unsigned m_total_iterations;
     unsigned m_iters_with_no_cost_growing;
@@ -111,8 +111,9 @@ struct stats {
     unsigned m_horner_conflicts;
     unsigned m_cross_nested_forms;
     unsigned m_grobner_calls;
+    unsigned m_grobner_basis_computatins;
     unsigned m_grobner_conflicts;
-    stats() { reset(); }
+    statistics() { reset(); }
     void reset() { memset(this, 0, sizeof(*this)); }
 };
 
@@ -137,7 +138,7 @@ private:
     // used for messages, for example, the computation progress messages
     std::ostream*             m_message_out;
 
-    stats                     m_stats;
+    statistics                     m_stats;
     random_gen                m_rand;
 
 public:
@@ -286,8 +287,8 @@ public:
     
     std::ostream* get_debug_ostream() { return m_debug_out; }
     std::ostream* get_message_ostream() { return m_message_out; }
-    stats& st() { return m_stats; }
-    stats const& st() const { return m_stats; }
+    statistics& stats() { return m_stats; }
+    statistics const& stats() const { return m_stats; }
 
     template <typename T> static bool is_eps_small_general(const T & t, const double & eps) {
         return (!numeric_traits<T>::precise())? is_epsilon_small<T>(t, eps) : numeric_traits<T>::is_zero(t);

src/math/lp/lu_def.h

@@ -119,7 +119,7 @@ lu<M>::lu(const M& A,
 #ifdef Z3DEBUG
     debug_test_of_basis(A, basis);
 #endif
-    ++m_settings.st().m_num_factorizations;
+    ++m_settings.stats().m_num_factorizations;
     create_initial_factorization();
 #ifdef Z3DEBUG
     // lp_assert(check_correctness());

src/math/lp/nla_core.cpp

@@ -1316,8 +1316,8 @@ bool core::elists_are_consistent(bool check_in_model) const {
 }
 
 lbool core::check(vector<lemma>& l_vec) {
-    lp_settings().st().m_nla_calls++;
-    TRACE("nla_solver", tout << "calls = " << lp_settings().st().m_nla_calls << "\n";);
+    lp_settings().stats().m_nla_calls++;
+    TRACE("nla_solver", tout << "calls = " << lp_settings().stats().m_nla_calls << "\n";);
     m_lemma_vec =  &l_vec;
     if (!(m_lar_solver.get_status() == lp::lp_status::OPTIMAL || m_lar_solver.get_status() == lp::lp_status::FEASIBLE )) {
         TRACE("nla_solver", tout << "unknown because of the m_lar_solver.m_status = " << m_lar_solver.get_status() << "\n";);

src/math/lp/nla_core.h

@@ -142,9 +142,9 @@ public:
     
     lpvar var(const factor& f) const { return f.var(); }
 
-    bool need_to_call_horner() const { return lp_settings().st().m_nla_calls % m_settings.horner_frequency() == 0; }
+    bool need_to_call_horner() const { return lp_settings().stats().m_nla_calls % m_settings.horner_frequency() == 0; }
 
-    bool need_to_call_grobner() const { return lp_settings().st().m_nla_calls % m_settings.grobner_frequency() == 0; }
+    bool need_to_call_grobner() const { return lp_settings().stats().m_nla_calls % m_settings.grobner_frequency() == 0; }
 
     lbool incremental_linearization(bool);
     

src/math/lp/nla_grobner.cpp

@@ -127,10 +127,48 @@ void nla_grobner::init() {
     find_nl_cluster();
 }
 
-void nla_grobner::grobner_lemmas() {
-    c().lp_settings().st().m_grobner_calls++;    
-    init();
+void nla_grobner::compute_basis(){
+    compute_basis_init();        
+    if (!compute_basis_loop()) {
+        set_gb_exhausted();
+    }
+}
+void nla_grobner::compute_basis_init(){
+    c().lp_settings().stats().m_grobner_basis_computatins++;    
+    m_num_new_equations = 0;
+    
+}        
 
+bool nla_grobner::compute_basis_loop(){
+    SASSERT(false);
+    return false;
+}
+
+void nla_grobner::set_gb_exhausted(){ SASSERT(false); }
+
+void nla_grobner::update_statistics(){
     SASSERT(false);
 }
+
+bool nla_grobner::find_conflict(){ SASSERT(false);
+    return false;
+}
+
+bool nla_grobner::push_calculation_forward(){ SASSERT(false);
+    return false;
+}
+
+void nla_grobner::grobner_lemmas() {
+    c().lp_settings().stats().m_grobner_calls++;    
+    init();
+    do {
+        TRACE("nla_gb", tout << "before:\n"; display(tout););
+        compute_basis();
+        update_statistics();
+        TRACE("nla_gb", tout << "after:\n"; display(tout););
+        if (find_conflict())
+            return;
+    }
+    while(push_calculation_forward());
+}
 } // end of nla namespace

src/math/lp/nla_grobner.h

@@ -40,6 +40,7 @@ class nla_grobner : common {
     lp::int_set         m_rows;
     lp::int_set         m_active_vars;
     svector<var_weight> m_active_vars_weights;
+    unsigned            m_num_new_equations;
 public:
     nla_grobner(core *core);
     void grobner_lemmas();
@@ -51,5 +52,12 @@ private:
     void set_active_vars_weights();
     void init();
     var_weight get_var_weight(lpvar) const;
+    void compute_basis();
+    void update_statistics();
+    bool find_conflict();
+    bool push_calculation_forward();
+    void compute_basis_init();        
+    bool compute_basis_loop();
+    void set_gb_exhausted();
 }; // end of grobner
 }

src/smt/theory_lra.cpp

@@ -2291,14 +2291,14 @@ public:
         if (BP_NONE == propagation_mode()) {
             return;
         }
-        int num_of_p = lp().settings().st().m_num_of_implied_bounds;
+        int num_of_p = lp().settings().stats().m_num_of_implied_bounds;
         (void)num_of_p;
         local_bound_propagator bp(*this);
         lp().propagate_bounds_for_touched_rows(bp);
         if (m.canceled()) {
             return;
         }
-        int new_num_of_p = lp().settings().st().m_num_of_implied_bounds;
+        int new_num_of_p = lp().settings().stats().m_num_of_implied_bounds;
         (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()) {
@@ -2379,7 +2379,7 @@ public:
             }
             TRACE("arith", tout << lit << " bound: " << *b << " first: " << first << "\n";);
 
-            lp().settings().st().m_num_of_implied_bounds ++;
+            lp().settings().stats().m_num_of_implied_bounds ++;
             if (first) {
                 first = false;
                 m_core.reset();
@@ -3770,7 +3770,7 @@ public:
         st.update("arith-rows", m_stats.m_add_rows);
         st.update("arith-propagations", m_stats.m_bounds_propagations);
         st.update("arith-iterations", m_stats.m_num_iterations);
-        st.update("arith-factorizations", lp().settings().st().m_num_factorizations);
+        st.update("arith-factorizations", lp().settings().stats().m_num_factorizations);
         st.update("arith-pivots", m_stats.m_need_to_solve_inf);
         st.update("arith-plateau-iterations", m_stats.m_num_iterations_with_no_progress);
         st.update("arith-fixed-eqs", m_stats.m_fixed_eqs);
@@ -3778,21 +3778,21 @@ public:
         st.update("arith-bound-propagations-lp", m_stats.m_bound_propagations1);
         st.update("arith-bound-propagations-cheap", m_stats.m_bound_propagations2);
         st.update("arith-diseq", m_stats.m_assert_diseq);
-        st.update("arith-make-feasible", lp().settings().st().m_make_feasible);
-        st.update("arith-max-columns", lp().settings().st().m_max_cols);
-        st.update("arith-max-rows", lp().settings().st().m_max_rows);
-        st.update("gcd-calls", lp().settings().st().m_gcd_calls);
-        st.update("gcd-conflict", lp().settings().st().m_gcd_conflicts);
-        st.update("cube-calls", lp().settings().st().m_cube_calls);
-        st.update("cube-success", lp().settings().st().m_cube_success);
-        st.update("arith-patches", lp().settings().st().m_patches);
-        st.update("arith-patches-success", lp().settings().st().m_patches_success);
-        st.update("arith-hnf-calls", lp().settings().st().m_hnf_cutter_calls);
-        st.update("horner-calls", lp().settings().st().m_horner_calls);
-        st.update("horner-conflicts", lp().settings().st().m_horner_conflicts);
-        st.update("horner-cross-nested-forms", lp().settings().st().m_cross_nested_forms);
-        st.update("grobner-calls", lp().settings().st().m_grobner_calls);
-        st.update("grobner-conflicts", lp().settings().st().m_grobner_conflicts);
+        st.update("arith-make-feasible", lp().settings().stats().m_make_feasible);
+        st.update("arith-max-columns", lp().settings().stats().m_max_cols);
+        st.update("arith-max-rows", lp().settings().stats().m_max_rows);
+        st.update("gcd-calls", lp().settings().stats().m_gcd_calls);
+        st.update("gcd-conflict", lp().settings().stats().m_gcd_conflicts);
+        st.update("cube-calls", lp().settings().stats().m_cube_calls);
+        st.update("cube-success", lp().settings().stats().m_cube_success);
+        st.update("arith-patches", lp().settings().stats().m_patches);
+        st.update("arith-patches-success", lp().settings().stats().m_patches_success);
+        st.update("arith-hnf-calls", lp().settings().stats().m_hnf_cutter_calls);
+        st.update("horner-calls", lp().settings().stats().m_horner_calls);
+        st.update("horner-conflicts", lp().settings().stats().m_horner_conflicts);
+        st.update("horner-cross-nested-forms", lp().settings().stats().m_cross_nested_forms);
+        st.update("grobner-calls", lp().settings().stats().m_grobner_calls);
+        st.update("grobner-conflicts", lp().settings().stats().m_grobner_conflicts);
         st.update("nla-explanations", m_stats.m_nla_explanations);
         st.update("nla-lemmas", m_stats.m_nla_lemmas);
     }