From e8b6b870ac1736305f4053cae43a28a814422298 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 18 Sep 2019 11:53:17 -0700 Subject: [PATCH] port grobner basis functionality Signed-off-by: Lev Nachmanson --- src/math/lp/nla_grobner.cpp | 66 +++++++++++++++++++++++++++++-------- src/math/lp/nla_grobner.h | 43 ++++++++++++++---------- src/smt/theory_arith.h | 2 +- src/smt/theory_arith_nl.h | 4 +-- 4 files changed, 81 insertions(+), 34 deletions(-) diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index d32fc8be1..da3684414 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -21,7 +21,27 @@ #include "math/lp/nla_core.h" #include "math/lp/factorization_factory_imp.h" namespace nla { -nla_grobner::nla_grobner(core *c) : common(c) {} +nla_grobner::nla_grobner(core *c) : common(c), m_nl_gb_exhausted(false) {} + +// Scan the grobner basis eqs for equations of the form x - k = 0 or x = 0 is found, and x is not fixed, +// then assert bounds for x, and continue +bool nla_grobner::scan_for_linear(ptr_vector& eqs) { + bool result = false; + for (nla_grobner::equation* eq : eqs) { + if (!eq->is_linear_combination()) { + TRACE("non_linear", tout << "processing new equality:\n"; display_equation(tout, *eq);); + TRACE("non_linear_bug", tout << "processing new equality:\n"; display_equation(tout, *eq);); + if (internalize_gb_eq(eq)) + result = true; + } + } + return result; +} + +bool nla_grobner::internalize_gb_eq(equation* ) { + NOT_IMPLEMENTED_YET(); + return false; +} void nla_grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::queue & q) { SASSERT(m_active_vars.contains(j) == false); @@ -122,9 +142,20 @@ void nla_grobner::display(std::ostream & out) { c().print_term(r, out) << std::endl; } } - +void nla_grobner::add_row_to_gb(unsigned) { + NOT_IMPLEMENTED_YET(); +} +void nla_grobner::add_monomial_def(lpvar) { + NOT_IMPLEMENTED_YET(); +} void nla_grobner::init() { find_nl_cluster(); + for (unsigned i : m_rows) { + add_row_to_gb(i); + } + for (lpvar j : m_active_vars) { + add_monomial_def(j); + } } bool nla_grobner::is_trivial(equation* eq) const { @@ -158,7 +189,7 @@ void nla_grobner::del_equation(equation * eq) { */ } -equation* nla_grobner::pick_next() { +nla_grobner::equation* nla_grobner::pick_next() { equation * r = nullptr; ptr_buffer to_delete; for (equation * curr : m_to_process) { @@ -175,18 +206,18 @@ equation* nla_grobner::pick_next() { return r; } -equation* nla_grobner::simplify_using_processed(equation* eq) { - SASSERT(false); +nla_grobner::equation* nla_grobner::simplify_using_processed(equation* eq) { + NOT_IMPLEMENTED_YET(); return nullptr; } -equation* nla_grobner::simplify_processed(equation* eq) { - SASSERT(false); +nla_grobner::equation* nla_grobner::simplify_processed(equation* eq) { + NOT_IMPLEMENTED_YET(); return nullptr; } -equation* nla_grobner::simplify_to_process(equation*) { - SASSERT(false); +nla_grobner::equation* nla_grobner::simplify_to_process(equation*) { + NOT_IMPLEMENTED_YET(); return nullptr; } @@ -241,7 +272,7 @@ bool nla_grobner::compute_basis_loop(){ } void nla_grobner::set_gb_exhausted(){ - NOT_IMPLEMENTED_YET(); + m_nl_gb_exhausted = true; } void nla_grobner::update_statistics(){ @@ -288,17 +319,26 @@ void nla_grobner::get_equations(ptr_vector& result) { } -bool nla_grobner::push_calculation_forward(){ +bool nla_grobner::push_calculation_forward(ptr_vector& eqs, unsigned & next_weight) { + return scan_for_linear(eqs) + && + (!m_nl_gb_exhausted) && + try_to_modify_eqs(eqs, next_weight); +} + +bool nla_grobner::try_to_modify_eqs(ptr_vector& eqs, unsigned& next_weight) { NOT_IMPLEMENTED_YET(); return false; } + void nla_grobner::grobner_lemmas() { c().lp_settings().stats().m_grobner_calls++; init(); ptr_vector eqs; - + unsigned next_weight = + (unsigned)(var_weight::MAX_DEFAULT_WEIGHT) + 1; // next weight using during perturbation phase. do { TRACE("nla_gb", tout << "before:\n"; display(tout);); compute_basis(); @@ -307,7 +347,7 @@ void nla_grobner::grobner_lemmas() { if (find_conflict(eqs)) return; } - while(push_calculation_forward()); + while(push_calculation_forward(eqs, next_weight)); } void nla_grobner:: del_equations(unsigned old_size) { SASSERT(m_equations_to_delete.size() >= old_size); diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index c0b60d824..93f7aa591 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -50,23 +50,6 @@ public: lpvar get_var(unsigned idx) const { return m_vars[idx]; } }; -class equation { - unsigned m_scope_lvl; //!< scope level when this equation was created. - unsigned m_bidx:31; //!< position at m_equations_to_delete - unsigned m_lc:1; //!< true if equation if a linear combination of the input equations. - ptr_vector m_monomials; //!< sorted monomials - v_dependency * m_dep; //!< justification for the equality - friend class nla_grobner; - equation() {} -public: - unsigned get_num_monomials() const { return m_monomials.size(); } - monomial const * get_monomial(unsigned idx) const { return m_monomials[idx]; } - monomial * const * get_monomials() const { return m_monomials.c_ptr(); } - v_dependency * get_dependency() const { return m_dep; } - unsigned hash() const { return m_bidx; } - bool is_linear_combination() const { return m_lc; } -}; - enum class var_weight { FIXED = 0, QUOTED_FIXED = 1, @@ -80,6 +63,24 @@ enum class var_weight { }; class nla_grobner : common { + + class equation { + unsigned m_scope_lvl; //!< scope level when this equation was created. + unsigned m_bidx:31; //!< position at m_equations_to_delete + unsigned m_lc:1; //!< true if equation if a linear combination of the input equations. + ptr_vector m_monomials; //!< sorted monomials + v_dependency * m_dep; //!< justification for the equality + friend class nla_grobner; + equation() {} + public: + unsigned get_num_monomials() const { return m_monomials.size(); } + monomial const * get_monomial(unsigned idx) const { return m_monomials[idx]; } + monomial * const * get_monomials() const { return m_monomials.c_ptr(); } + v_dependency * get_dependency() const { return m_dep; } + unsigned hash() const { return m_bidx; } + bool is_linear_combination() const { return m_lc; } + }; + typedef obj_hashtable equation_set; typedef ptr_vector equation_vector; @@ -93,10 +94,12 @@ class nla_grobner : common { grobner_stats m_stats; equation_set m_processed; equation_set m_to_process; + bool m_nl_gb_exhausted; public: nla_grobner(core *core); void grobner_lemmas(); private: + bool scan_for_linear(ptr_vector& eqs); void find_nl_cluster(); void prepare_rows_and_active_vars(); void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::queue& q); @@ -109,7 +112,7 @@ private: bool find_conflict(ptr_vector& eqs); bool is_inconsistent(equation*); bool is_inconsistent2(equation*); - bool push_calculation_forward(); + bool push_calculation_forward(ptr_vector& eqs, unsigned&); void compute_basis_init(); bool compute_basis_loop(); bool compute_basis_step(); @@ -132,5 +135,9 @@ private: void display(std::ostream & out) const; void get_equations(ptr_vector& eqs); + bool try_to_modify_eqs(ptr_vector& eqs, unsigned& next_weight); + bool internalize_gb_eq(equation*); + void add_row_to_gb(unsigned); + void add_monomial_def(lpvar); }; // end of grobner } diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 3c7fe26be..3a4739e01 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -1043,7 +1043,7 @@ namespace smt { void compute_basis(grobner&, bool&); void update_statistics(grobner&); void set_gb_exhausted(); - bool pass_over_gb_eqs_for_conflict(ptr_vector& eqs, grobner&); + bool get_gb_eqs_and_look_for_conflict(ptr_vector& eqs, grobner&); bool scan_for_linear(ptr_vector& eqs, grobner&); bool try_to_modify_eqs(ptr_vector& eqs, grobner&, unsigned &); bool max_min_nl_vars(); diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 2c42bcc33..7c5abcf3d 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -2241,7 +2241,7 @@ void theory_arith::set_gb_exhausted() { // Scan the grobner basis eqs, and look for inconsistencies. template -bool theory_arith::pass_over_gb_eqs_for_conflict(ptr_vector& eqs, grobner& gb) { +bool theory_arith::get_gb_eqs_and_look_for_conflict(ptr_vector& eqs, grobner& gb) { eqs.reset(); gb.get_equations(eqs); TRACE("grobner_bug", tout << "after gb\n";); @@ -2346,7 +2346,7 @@ typename theory_arith::gb_result theory_arith::compute_grobner(svector TRACE("non_linear_gb", tout << "after:\n"; gb.display(tout);); if (get_context().get_cancel_flag()) return GB_FAIL; - if (pass_over_gb_eqs_for_conflict(eqs, gb)) + if (get_gb_eqs_and_look_for_conflict(eqs, gb)) return GB_PROGRESS; } while(scan_for_linear(eqs, gb) && m_params.m_nl_arith_gb_perturbate &&