From bfcfc517fe0fad1396c6879a6fc7a0a729397e2e Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 4 Sep 2019 12:27:05 -0700 Subject: [PATCH] add stubs to the nla_grobner Signed-off-by: Lev Nachmanson --- src/math/lp/CMakeLists.txt | 1 + src/math/lp/nex.h | 2 +- src/math/lp/nla_core.cpp | 33 +++++++++++++++++++++------------ src/math/lp/nla_core.h | 11 +++++++++-- src/math/lp/nla_params.pyg | 4 +++- src/math/lp/nla_settings.h | 19 +++++++++++++++---- src/smt/theory_lra.cpp | 4 +++- 7 files changed, 53 insertions(+), 21 deletions(-) diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt index 454dd5a30..db6e98102 100644 --- a/src/math/lp/CMakeLists.txt +++ b/src/math/lp/CMakeLists.txt @@ -29,6 +29,7 @@ z3_add_component(lp nla_basics_lemmas.cpp nla_common.cpp nla_core.cpp + nla_grobner.cpp nla_intervals.cpp nla_monotone_lemmas.cpp nla_order_lemmas.cpp diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h index 2124c2081..35278c2cd 100644 --- a/src/math/lp/nex.h +++ b/src/math/lp/nex.h @@ -56,7 +56,7 @@ public: return false; default: return true; - } + } } bool is_sum() const { return type() == expr_type::SUM; } diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 9b3d73788..b185d4d3c 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -30,6 +30,7 @@ core::core(lp::lar_solver& s, reslimit & lim) : m_order(this), m_monotone(this), m_horner(this), + m_grobner(this), m_emons(m_evars), m_reslim(lim) {} @@ -1249,24 +1250,18 @@ bool core::conflict_found() const { bool core::done() const { return m_lemma_vec->size() >= 10 || conflict_found(); } - -lbool core::inner_check(bool derived) { - if (derived && (lp_settings().st().m_nla_calls % m_settings.horner_frequency() == 0)) - m_horner.horner_lemmas(); - if (done()) { - return l_false; - } - + +lbool core::incremental_linearization(bool constraint_derived) { TRACE("nla_solver", print_terms(tout); m_lar_solver.print_constraints(tout);); for (int search_level = 0; search_level < 3 && !done(); search_level++) { - TRACE("nla_solver", tout << "derived = " << derived << ", search_level = " << search_level << "\n";); + TRACE("nla_solver", tout << "constraint_derived = " << constraint_derived << ", search_level = " << search_level << "\n";); if (search_level == 0) { - m_basics.basic_lemma(derived); + m_basics.basic_lemma(constraint_derived); if (!m_lemma_vec->empty()) return l_false; } - if (derived) continue; - TRACE("nla_solver", tout << "passed derived and basic lemmas\n";); + if (constraint_derived) continue; + TRACE("nla_solver", tout << "passed constraint_derived and basic lemmas\n";); SASSERT(elists_are_consistent(true)); if (search_level == 1) { m_order.order_lemma(); @@ -1277,6 +1272,20 @@ lbool core::inner_check(bool derived) { } return m_lemma_vec->empty()? l_undef : l_false; } +// constraint_derived is set to true when we do not use the model values to +// obtain the lemmas +lbool core::inner_check(bool constraint_derived) { + if (constraint_derived) { + if (need_to_call_horner()) + m_horner.horner_lemmas(); + else if (need_to_call_grobner()) + m_grobner.grobner_lemmas(); + if (done()) { + return l_false; + } + } + return incremental_linearization(constraint_derived); +} bool core::elist_is_consistent(const std::unordered_set & list) const { bool first = true; diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 56999669e..b5cbc74c2 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -29,6 +29,7 @@ #include "math/lp/nla_settings.h" #include "math/lp/nex.h" #include "math/lp/horner.h" +#include "math/lp/nla_grobner.h" namespace nla { template @@ -76,19 +77,19 @@ public: bool is_conflict() const { return m_ineqs.empty() && !m_expl.empty(); } }; - class core { public: var_eqs m_evars; lp::lar_solver& m_lar_solver; vector * m_lemma_vec; - lp::int_set m_to_refine; + lp::int_set m_to_refine; tangents m_tangents; basics m_basics; order m_order; monotone m_monotone; horner m_horner; nla_settings m_settings; + nla_grobner m_grobner; private: emonomials m_emons; svector m_add_buffer; @@ -124,6 +125,12 @@ 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_grobner() const { return lp_settings().st().m_nla_calls % m_settings.grobner_frequency() == 0; } + + lbool incremental_linearization(bool); + svector sorted_rvars(const factor& f) const; bool done() const; diff --git a/src/math/lp/nla_params.pyg b/src/math/lp/nla_params.pyg index 859c600a8..9614a86b0 100644 --- a/src/math/lp/nla_params.pyg +++ b/src/math/lp/nla_params.pyg @@ -5,7 +5,9 @@ def_module_params('nla', ('tangents', BOOL, True, 'run tangent lemmas'), ('horner', BOOL, True, 'run horner\'s heuristic'), ('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') + ('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') )) diff --git a/src/math/lp/nla_settings.h b/src/math/lp/nla_settings.h index b68f96542..278b972b4 100644 --- a/src/math/lp/nla_settings.h +++ b/src/math/lp/nla_settings.h @@ -21,18 +21,23 @@ Revision History: #pragma once namespace nla { class nla_settings { - bool m_run_order; - bool m_run_tangents; - bool m_run_horner; + bool m_run_order; + bool m_run_tangents; + bool m_run_horner; // how often to call the horner heuristic unsigned m_horner_frequency; unsigned m_horner_row_length_limit; + bool m_run_grobner; + unsigned m_grobner_frequency; + public: nla_settings() : m_run_order(true), m_run_tangents(true), m_run_horner(true), m_horner_frequency(4), - m_horner_row_length_limit(10) + m_horner_row_length_limit(10), + m_run_grobner(true), + m_grobner_frequency(5) {} bool run_order() const { return m_run_order; } @@ -48,5 +53,11 @@ public: unsigned& horner_frequency() { return m_horner_frequency; } unsigned horner_row_length_limit() const { return m_horner_row_length_limit; } unsigned& horner_row_length_limit() { return m_horner_row_length_limit; } + + bool run_grobner() const { return m_run_grobner; } + bool& run_grobner() { return m_run_grobner; } + + unsigned grobner_frequency() const { return m_grobner_frequency; } + unsigned& grobner_frequency() { return m_grobner_frequency; } }; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 990f200d6..26ce5702f 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -452,7 +452,9 @@ class theory_lra::imp { 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.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(); } }