From 490672a5baa5af64b7e3e61b7939f2af377adfd8 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 7 Sep 2019 11:54:36 -0700 Subject: [PATCH] start porting grobner basis functionality Signed-off-by: Lev Nachmanson --- src/math/lp/horner.cpp | 6 ++--- src/math/lp/int_solver.cpp | 19 +++++++------ src/math/lp/lar_core_solver_def.h | 2 +- src/math/lp/lp_core_solver_base.h | 2 +- src/math/lp/lp_settings.h | 11 ++++---- src/math/lp/lu_def.h | 2 +- src/math/lp/nla_core.cpp | 4 +-- src/math/lp/nla_core.h | 4 +-- src/math/lp/nla_grobner.cpp | 44 ++++++++++++++++++++++++++++--- src/math/lp/nla_grobner.h | 8 ++++++ src/smt/theory_lra.cpp | 38 +++++++++++++------------- 11 files changed, 93 insertions(+), 47 deletions(-) diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index c16317f80..8fb662ae3 100644 --- a/src/math/lp/horner.cpp +++ b/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 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; } } diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index b63af29c0..77bb9aae9 100644 --- a/src/math/lp/int_solver.cpp +++ b/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; diff --git a/src/math/lp/lar_core_solver_def.h b/src/math/lp/lar_core_solver_def.h index 56fe669c4..425812db9 100644 --- a/src/math/lp/lar_core_solver_def.h +++ b/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()) { diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h index db7fd70ce..ad0478757 100644 --- a/src/math/lp/lp_core_solver_base.h +++ b/src/math/lp/lp_core_solver_base.h @@ -35,7 +35,7 @@ template // 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: diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index a9faeb7f9..818f13794 100644 --- a/src/math/lp/lp_settings.h +++ b/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 static bool is_eps_small_general(const T & t, const double & eps) { return (!numeric_traits::precise())? is_epsilon_small(t, eps) : numeric_traits::is_zero(t); diff --git a/src/math/lp/lu_def.h b/src/math/lp/lu_def.h index c4bf648c8..0dcb2ba1b 100644 --- a/src/math/lp/lu_def.h +++ b/src/math/lp/lu_def.h @@ -119,7 +119,7 @@ lu::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()); diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index b185d4d3c..b80d1379c 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1316,8 +1316,8 @@ bool core::elists_are_consistent(bool check_in_model) const { } lbool core::check(vector& 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";); diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index d14f06dd9..c1582df9a 100644 --- a/src/math/lp/nla_core.h +++ b/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); diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 3b9260620..7b0a326c7 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/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 diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index d6cb74e36..92550e1d5 100644 --- a/src/math/lp/nla_grobner.h +++ b/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 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 } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index eae4d1311..aae426531 100644 --- a/src/smt/theory_lra.cpp +++ b/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); }