From 06dbc623c7bcbf0818763e9ee83eb60faefe72dd Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 4 Sep 2019 18:33:54 -0700 Subject: [PATCH] start porting grobner basis functionality Signed-off-by: Lev Nachmanson --- src/math/lp/horner.cpp | 8 +-- src/math/lp/horner.h | 1 - src/math/lp/lar_solver.h | 1 + src/math/lp/lp_settings.h | 2 + src/math/lp/nla_core.h | 21 +++++++- src/math/lp/nla_grobner.cpp | 104 ++++++++++++++++++++++++++++++++++++ src/math/lp/nla_grobner.h | 38 +++++++++++++ src/smt/theory_lra.cpp | 2 + 8 files changed, 170 insertions(+), 7 deletions(-) create mode 100644 src/math/lp/nla_grobner.cpp create mode 100644 src/math/lp/nla_grobner.h diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index e6c57b63c..c16317f80 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -45,7 +45,7 @@ bool horner::row_is_interesting(const T& row) const { return false; } SASSERT(row_has_monomial_to_refine(row)); - m_row_var_set.clear(); + c().clear_row_var_set(); for (const auto& p : row) { lpvar j = p.var(); if (!c().is_monomial_var(j)) @@ -53,11 +53,11 @@ bool horner::row_is_interesting(const T& row) const { auto & m = c().emons()[j]; for (lpvar k : m.vars()) { - if (m_row_var_set.contains(k)) + if (c().row_var_set_contains(k)) return true; } for (lpvar k : m.vars()) { - m_row_var_set.insert(k); + c().insert_to_row_var_set(k); } } return false; @@ -113,7 +113,7 @@ void horner::horner_lemmas() { for (auto & s : matrix.m_columns[j]) rows_to_check.insert(s.var()); } - m_row_var_set.resize(c().m_lar_solver.number_of_vars()); + c().prepare_row_var_set(); svector rows; for (unsigned i : rows_to_check) { if (row_is_interesting(matrix.m_rows[i])) diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h index 957169e2c..7b3130159 100644 --- a/src/math/lp/horner.h +++ b/src/math/lp/horner.h @@ -32,7 +32,6 @@ class core; class horner : common { intervals m_intervals; nex_sum m_row_sum; - mutable lp::int_set m_row_var_set; public: typedef intervals::interval interv; horner(core *core); diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 0e19140fb..a14ba59f6 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -636,6 +636,7 @@ public: void update_delta_for_terms(const impq & delta, unsigned j, const vector&); void fill_vars_to_terms(vector> & vars_to_terms); unsigned column_count() const { return A_r().column_count(); } + unsigned row_count() const { return A_r().row_count(); } const vector & r_basis() const { return m_mpq_lar_core_solver.r_basis(); } const vector & r_nbasis() const { return m_mpq_lar_core_solver.r_nbasis(); } bool get_equality_and_right_side_for_term_on_current_x(unsigned i, mpq &rs, constraint_index& ci, bool &upper_bound) const; diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 9a10b7731..a9faeb7f9 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -110,6 +110,8 @@ struct stats { unsigned m_horner_calls; unsigned m_horner_conflicts; unsigned m_cross_nested_forms; + unsigned m_grobner_calls; + unsigned m_grobner_conflicts; stats() { reset(); } void reset() { memset(this, 0, sizeof(*this)); } }; diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index b5cbc74c2..d14f06dd9 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -93,14 +93,31 @@ public: private: emonomials m_emons; svector m_add_buffer; + mutable lp::int_set m_row_var_set; public: - reslimit m_reslim; + reslimit m_reslim; + + + const lp::int_set& row_var_set () const { return m_row_var_set;} + bool row_var_set_contains(unsigned j) const { return m_row_var_set.contains(j); } + + void insert_to_row_var_set(unsigned j) const { m_row_var_set.insert(j); } + + void clear_row_var_set() const { + m_row_var_set.clear(); + } + + void prepare_row_var_set() const { + m_row_var_set.clear(); + m_row_var_set.resize(m_lar_solver.number_of_vars()); + } + reslimit & reslim() { return m_reslim; } emonomials& emons() { return m_emons; } const emonomials& emons() const { return m_emons; } // constructor core(lp::lar_solver& s, reslimit &); - + bool compare_holds(const rational& ls, llc cmp, const rational& rs) const; rational value(const lp::lar_term& r) const; diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp new file mode 100644 index 000000000..29673340e --- /dev/null +++ b/src/math/lp/nla_grobner.cpp @@ -0,0 +1,104 @@ +/*++ + Copyright (c) 2017 Microsoft Corporation + + Module Name: + + + + Abstract: + + + + Author: + Nikolaj Bjorner (nbjorner) + Lev Nachmanson (levnach) + + Revision History: + + + --*/ +#include "math/lp/nla_grobner.h" +#include "math/lp/nla_core.h" +#include "math/lp/factorization_factory_imp.h" +namespace nla { +nla_grobner::nla_grobner(core *c) : common(c) {} + +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); + const auto& matrix = c().m_lar_solver.A_r(); + m_active_vars.insert(j); + for (auto & s : matrix.m_columns[j]) { + unsigned row = s.var(); + if (m_rows.contains(row)) continue; + m_rows.insert(row); + for (auto& rc : matrix.m_rows[row]) { + if (m_active_vars.contains(rc.var())) + continue; + q.push(rc.var()); + } + } + + if (!c().is_monomial_var(j)) + return; + + const monomial& m = c().emons()[j]; + for (auto fcn : factorization_factory_imp(m, c())) { + for (const factor& fc: fcn) { + lpvar j = var(fc); + if (! m_active_vars.contains(j)) + add_var_and_its_factors_to_q_and_collect_new_rows(j, q); + } + } +} + + +void nla_grobner::find_rows() { + prepare_rows_and_active_vars(); + std::queue q; + for (lpvar j : c().m_to_refine) { + TRACE("nla_grobner", c().print_monomial(c().emons()[j], tout) << "\n";); + q.push(j); + } + + while (!q.empty()) { + unsigned j = q.front(); + q.pop(); + if (m_active_vars.contains(j)) + continue; + add_var_and_its_factors_to_q_and_collect_new_rows(j, q); + } + + +} + +void nla_grobner::prepare_rows_and_active_vars() { + m_rows.clear(); + m_rows.resize(c().m_lar_solver.row_count()); + m_active_vars.clear(); + m_active_vars.resize(c().m_lar_solver.column_count()); +} + +void nla_grobner::grobner_lemmas() { + c().lp_settings().st().m_grobner_calls++; + if (c().lp_settings().st().m_grobner_calls == 2) + SASSERT(false); + + + find_rows(); + + TRACE("nla_grobner", + { + const auto& matrix = c().m_lar_solver.A_r(); + tout << "rows = " << m_rows.size() << "\n"; + for (unsigned k : m_rows) { + c().print_term(matrix.m_rows[k], tout) << "\n"; + } + tout << "the matrix =\n"; + + for (const auto & r : matrix.m_rows) { + c().print_term(r, tout) << "\n"; + } + } + ); +} +} // end of nla namespace diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h new file mode 100644 index 000000000..23e20aaf9 --- /dev/null +++ b/src/math/lp/nla_grobner.h @@ -0,0 +1,38 @@ +/*++ + Copyright (c) 2017 Microsoft Corporation + + Module Name: + + + + Abstract: + + + + Author: + Nikolaj Bjorner (nbjorner) + Lev Nachmanson (levnach) + + Revision History: + + + --*/ +#pragma once + +#include "math/lp/nla_common.h" +#include "math/lp/nex.h" +namespace nla { +class core; + +class nla_grobner : common { + lp::int_set m_rows; + lp::int_set m_active_vars; +public: + nla_grobner(core *core); + void grobner_lemmas(); +private: + void find_rows(); + void prepare_rows_and_active_vars(); + void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::queue& q); +}; // end of grobner +} diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 26ce5702f..eae4d1311 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -3791,6 +3791,8 @@ public: 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("nla-explanations", m_stats.m_nla_explanations); st.update("nla-lemmas", m_stats.m_nla_lemmas); }