From cc5a12c5c7c9b533f403ed486e574512b6eabe95 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 17 Sep 2019 13:54:18 -0700 Subject: [PATCH] port grobner basis Signed-off-by: Lev Nachmanson --- src/math/lp/horner.cpp | 4 +-- src/math/lp/nla_core.h | 6 ++-- src/math/lp/nla_grobner.cpp | 57 ++++++++++++++++++++++++++++-- src/math/lp/nla_grobner.h | 47 +++++++++++++++++++++++- src/math/lp/nla_order_lemmas.cpp | 2 +- src/math/lp/nla_params.pyg | 3 +- src/math/lp/nla_settings.h | 8 ++++- src/math/lp/nla_tangent_lemmas.cpp | 2 +- src/smt/theory_lra.cpp | 15 ++++---- 9 files changed, 125 insertions(+), 19 deletions(-) diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 8fb662ae3..49d1e14b4 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -40,7 +40,7 @@ bool horner::row_has_monomial_to_refine(const T& row) const { template bool horner::row_is_interesting(const T& row) const { TRACE("nla_solver_details", m_core->print_term(row, tout);); - if (row.size() > m_core->m_settings.horner_row_length_limit()) { + if (row.size() > m_core->m_nla_settings.horner_row_length_limit()) { TRACE("nla_solver_details", tout << "disregard\n";); return false; } @@ -101,7 +101,7 @@ bool horner::lemmas_on_row(const T& row) { } void horner::horner_lemmas() { - if (!c().m_settings.run_horner()) { + if (!c().m_nla_settings.run_horner()) { TRACE("nla_solver", tout << "not generating horner lemmas\n";); return; } diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index c1582df9a..497c9e6ec 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -88,7 +88,7 @@ public: order m_order; monotone m_monotone; horner m_horner; - nla_settings m_settings; + nla_settings m_nla_settings; nla_grobner m_grobner; private: emonomials m_emons; @@ -142,9 +142,9 @@ public: lpvar var(const factor& f) const { return f.var(); } - bool need_to_call_horner() const { return lp_settings().stats().m_nla_calls % m_settings.horner_frequency() == 0; } + bool need_to_call_horner() const { return lp_settings().stats().m_nla_calls % m_nla_settings.horner_frequency() == 0; } - bool need_to_call_grobner() const { return lp_settings().stats().m_nla_calls % m_settings.grobner_frequency() == 0; } + bool need_to_call_grobner() const { return lp_settings().stats().m_nla_calls % m_nla_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 7b0a326c7..e4c7b66ae 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -127,6 +127,56 @@ void nla_grobner::init() { find_nl_cluster(); } +equation* nla_grobner::pick_next() { + SASSERT(false); + return nullptr; +} + +equation* nla_grobner::simplify_using_processed(equation* eq) { + SASSERT(false); + return nullptr; +} + +equation* nla_grobner::simplify_processed(equation* eq) { + SASSERT(false); + return nullptr; +} + +equation* nla_grobner::simplify_to_process(equation*) { + SASSERT(false); + return nullptr; +} + + +void nla_grobner::superpose(equation * eq1, equation * eq2) { + SASSERT(false); +} + +void nla_grobner::superpose(equation * eq){ + SASSERT(false); +} + + +bool nla_grobner::compute_basis_step() { + equation * eq = pick_next(); + if (!eq) + return true; + m_stats.m_num_processed++; + equation * new_eq = simplify_using_processed(eq); + if (new_eq != nullptr && eq != new_eq) { + // equation was updated using non destructive updates + m_equations_to_unfreeze.push_back(eq); + eq = new_eq; + } + if (canceled()) return false; + if (!simplify_processed(eq)) return false; + superpose(eq); + m_processed.insert(eq); + simplify_to_process(eq); + TRACE("grobner", tout << "end of iteration:\n"; display(tout);); + return false; +} + void nla_grobner::compute_basis(){ compute_basis_init(); if (!compute_basis_loop()) { @@ -135,12 +185,15 @@ void nla_grobner::compute_basis(){ } void nla_grobner::compute_basis_init(){ c().lp_settings().stats().m_grobner_basis_computatins++; - m_num_new_equations = 0; + m_num_of_equations = 0; } bool nla_grobner::compute_basis_loop(){ - SASSERT(false); + while (m_num_of_equations < c().m_nla_settings.grobner_eqs_threshold()) { + if (compute_basis_step()) + return true; + } return false; } diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index 92550e1d5..aa294357a 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -21,9 +21,38 @@ #include "math/lp/nla_common.h" #include "math/lp/nex.h" +#include "util/dependency.h" + namespace nla { class core; +struct grobner_stats { + long m_simplify; + long m_superpose; + long m_compute_basis; + long m_num_processed; + void reset() { memset(this, 0, sizeof(grobner_stats)); } + grobner_stats() { reset(); } +}; + + +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 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, @@ -37,10 +66,18 @@ enum class var_weight { }; class nla_grobner : common { + typedef obj_hashtable equation_set; + typedef ptr_vector equation_vector; + equation_vector m_equations_to_unfreeze; + equation_vector m_equations_to_delete; + lp::int_set m_rows; lp::int_set m_active_vars; svector m_active_vars_weights; - unsigned m_num_new_equations; + unsigned m_num_of_equations; + grobner_stats m_stats; + equation_set m_processed; + equation_set m_to_process; public: nla_grobner(core *core); void grobner_lemmas(); @@ -58,6 +95,14 @@ private: bool push_calculation_forward(); void compute_basis_init(); bool compute_basis_loop(); + bool compute_basis_step(); + equation* simplify_using_processed(equation*); + equation* simplify_processed(equation*); + equation* simplify_to_process(equation*); + equation* pick_next(); void set_gb_exhausted(); + bool canceled() { return false; } // todo, implement + void superpose(equation * eq1, equation * eq2); + void superpose(equation * eq); }; // end of grobner } diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index cdfab0367..aaa214979 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -28,7 +28,7 @@ namespace nla { // a > b && c > 0 => ac > bc void order::order_lemma() { TRACE("nla_solver", ); - if (!c().m_settings.run_order()) { + if (!c().m_nla_settings.run_order()) { TRACE("nla_solver", tout << "not generating order lemmas\n";); return; } diff --git a/src/math/lp/nla_params.pyg b/src/math/lp/nla_params.pyg index 9614a86b0..a17f44482 100644 --- a/src/math/lp/nla_params.pyg +++ b/src/math/lp/nla_params.pyg @@ -7,7 +7,8 @@ def_module_params('nla', ('horner_frequency', UINT, 4, 'horner\'s call frequency'), ('horner_row_length_limit', UINT, 10, 'row is disregarded by the heuristic if its length is longer than the value'), ('grobner', BOOL, True, 'run grobner\'s heuristic'), - ('grobner_frequency', UINT, 5, 'grobner\'s call frequency') + ('grobner_frequency', UINT, 5, 'grobner\'s call frequency'), + ('grobner_eqs_threshold', UINT, 512, 'grobner\'s maximum number of equalities') )) diff --git a/src/math/lp/nla_settings.h b/src/math/lp/nla_settings.h index 278b972b4..799ce53d2 100644 --- a/src/math/lp/nla_settings.h +++ b/src/math/lp/nla_settings.h @@ -27,8 +27,10 @@ class nla_settings { // how often to call the horner heuristic unsigned m_horner_frequency; unsigned m_horner_row_length_limit; + // grobner fields bool m_run_grobner; unsigned m_grobner_frequency; + unsigned m_grobner_eqs_threshold; public: nla_settings() : m_run_order(true), @@ -37,9 +39,13 @@ public: m_horner_frequency(4), m_horner_row_length_limit(10), m_run_grobner(true), - m_grobner_frequency(5) + m_grobner_frequency(5), + m_grobner_eqs_threshold(512) {} + unsigned grobner_eqs_threshold() const { return m_grobner_eqs_threshold; } + unsigned& grobner_eqs_threshold() { return m_grobner_eqs_threshold; } + bool run_order() const { return m_run_order; } bool& run_order() { return m_run_order; } diff --git a/src/math/lp/nla_tangent_lemmas.cpp b/src/math/lp/nla_tangent_lemmas.cpp index 6d32da442..430054f6a 100644 --- a/src/math/lp/nla_tangent_lemmas.cpp +++ b/src/math/lp/nla_tangent_lemmas.cpp @@ -30,7 +30,7 @@ std::ostream& tangents::print_tangent_domain(const point &a, const point &b, std return out << "(" << a << ", " << b << ")"; } void tangents::tangent_lemma() { - if (!c().m_settings.run_tangents()) { + if (!c().m_nla_settings.run_tangents()) { TRACE("nla_solver", tout << "not generating tangent lemmas\n";); return; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index aae426531..8e25a46d4 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -448,13 +448,14 @@ class theory_lra::imp { m_nla->push(); } nla_params nla(ctx().get_params()); - m_nla->get_core()->m_settings.run_order() = nla.order(); - m_nla->get_core()->m_settings.run_tangents() = nla.tangents(); - m_nla->get_core()->m_settings.run_horner() = nla.horner(); - m_nla->get_core()->m_settings.horner_frequency() = nla.horner_frequency(); - m_nla->get_core()->m_settings.horner_row_length_limit() = nla.horner_row_length_limit(); - m_nla->get_core()->m_settings.grobner_frequency() = nla.grobner_frequency(); - m_nla->get_core()->m_settings.run_grobner() = nla.grobner(); + m_nla->get_core()->m_nla_settings.run_order() = nla.order(); + m_nla->get_core()->m_nla_settings.run_tangents() = nla.tangents(); + m_nla->get_core()->m_nla_settings.run_horner() = nla.horner(); + m_nla->get_core()->m_nla_settings.horner_frequency() = nla.horner_frequency(); + m_nla->get_core()->m_nla_settings.horner_row_length_limit() = nla.horner_row_length_limit(); + m_nla->get_core()->m_nla_settings.grobner_frequency() = nla.grobner_frequency(); + m_nla->get_core()->m_nla_settings.run_grobner() = nla.grobner(); + m_nla->get_core()->m_nla_settings.grobner_eqs_threshold() = nla.grobner_eqs_threshold(); } }