From f84a06b4c5d3028050ef1e7a2fa792453e463a4c Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 27 Jun 2019 14:58:44 -0700 Subject: [PATCH] starting the horner heuristic Signed-off-by: Lev Nachmanson --- src/math/lp/CMakeLists.txt | 1 + src/math/lp/horner.cpp | 46 ++++++++++++++++++++++++++++++++++++++ src/math/lp/horner.h | 35 +++++++++++++++++++++++++++++ src/math/lp/nla_core.cpp | 24 ++++++++++++-------- src/math/lp/nla_core.h | 10 ++++++--- src/math/lp/nla_settings.h | 15 ++++++++++++- 6 files changed, 118 insertions(+), 13 deletions(-) create mode 100644 src/math/lp/horner.cpp create mode 100644 src/math/lp/horner.h diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt index 77c7422e5..35d6d8703 100644 --- a/src/math/lp/CMakeLists.txt +++ b/src/math/lp/CMakeLists.txt @@ -10,6 +10,7 @@ z3_add_component(lp factorization.cpp factorization_factory_imp.cpp gomory.cpp + horner.cpp indexed_vector.cpp int_solver.cpp lar_solver.cpp diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp new file mode 100644 index 000000000..0bb6d7400 --- /dev/null +++ b/src/math/lp/horner.cpp @@ -0,0 +1,46 @@ +/*++ + Copyright (c) 2017 Microsoft Corporation + + Module Name: + + + + Abstract: + + + + Author: + Nikolaj Bjorner (nbjorner) + Lev Nachmanson (levnach) + + Revision History: + + + --*/ + +#include "math/lp/horner.h" +#include "math/lp/nla_core.h" + +namespace nla { + +horner::horner(core * c) : common(c) {} + +void horner::lemma_on_row(const lp::row_strip&) {} + +void horner::horner_lemmas() { + if (!c().m_settings.run_horner()) { + TRACE("nla_solver", tout << "not generating horner lemmas\n";); + return; + } + + const auto& m = c().m_lar_solver.A_r(); + unsigned r = random(); + unsigned s = m.row_count(); + for (unsigned i = 0; i < s && !done(); i++) { + lemma_on_row(m.m_rows[(i%s)]); + } + + SASSERT(false); +} + +} diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h new file mode 100644 index 000000000..16b51a9e0 --- /dev/null +++ b/src/math/lp/horner.h @@ -0,0 +1,35 @@ +/*++ + 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" + +namespace nla { +class core; + + +class horner : common { +public: + horner(core *core); + void horner_lemmas(); + void lemma_on_row(const lp::row_strip&); +private: +}; // end of horner +} diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 8c700fe59..cb9fac56d 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -29,8 +29,8 @@ core::core(lp::lar_solver& s, reslimit & lim) : m_basics(this), m_order(this), m_monotone(this), - m_emons(m_evars) { -} + m_horner(this), + m_emons(m_evars) {} bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const { switch(cmp) { @@ -182,7 +182,7 @@ std::ostream& core::print_product(const T & m, std::ostream& out) const { bool first = true; for (lpvar v : m) { if (!first) out << "*"; else first = false; - if (settings().m_print_external_var_name) + if (lp_settings().m_print_external_var_name) out << "(" << m_lar_solver.get_variable_name(v) << "=" << val(v) << ")"; else out << "(v" << v << " =" << val(v) << ")"; @@ -229,7 +229,7 @@ std::ostream & core::print_factor_with_vars(const factor& f, std::ostream& out) } std::ostream& core::print_monomial(const monomial& m, std::ostream& out) const { - if (settings().m_print_external_var_name) + if (lp_settings().m_print_external_var_name) out << "([" << m.var() << "] = " << m_lar_solver.get_variable_name(m.var()) << " = " << val(m.var()) << " = "; else out << "(v" << m.var() << " = " << val(m.var()) << " = "; @@ -805,14 +805,14 @@ bool core:: mon_has_zero(const T& product) const { template bool core::mon_has_zero(const unsigned_vector& product) const; -lp::lp_settings& core::settings() { +lp::lp_settings& core::lp_settings() { return m_lar_solver.settings(); } -const lp::lp_settings& core::settings() const { +const lp::lp_settings& core::lp_settings() const { return m_lar_solver.settings(); } -unsigned core::random() { return settings().random_next(); } +unsigned core::random() { return lp_settings().random_next(); } // we look for octagon constraints here, with a left part +-x +- y @@ -1268,6 +1268,12 @@ bool core:: done() const { } 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; + } + TRACE("nla_cn", print_terms(tout);); for (int search_level = 0; search_level < 3 && !done(); search_level++) { TRACE("nla_solver", tout << "derived = " << derived << ", search_level = " << search_level << "\n";); @@ -1318,8 +1324,8 @@ bool core::elists_are_consistent(bool check_in_model) const { } lbool core::check(vector& l_vec) { - settings().st().m_nla_calls++; - TRACE("nla_solver", tout << "calls = " << settings().st().m_nla_calls << "\n";); + lp_settings().st().m_nla_calls++; + TRACE("nla_solver", tout << "calls = " << lp_settings().st().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 04ccfbca2..1a651df69 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -28,6 +28,7 @@ #include "math/lp/emonomials.h" #include "math/lp/nla_settings.h" #include "math/lp/nla_expr.h" +#include "math/lp/horner.h" namespace nla { template @@ -86,8 +87,11 @@ public: basics m_basics; order m_order; monotone m_monotone; + horner m_horner; + nla_settings m_settings; +private: emonomials m_emons; - svector m_add_buffer; + svector m_add_buffer; public: emonomials& emons() { return m_emons; } const emonomials& emons() const { return m_emons; } @@ -277,8 +281,8 @@ public: template bool mon_has_zero(const T& product) const; - lp::lp_settings& settings(); - const lp::lp_settings& settings() const; + lp::lp_settings& lp_settings(); + const lp::lp_settings& lp_settings() const; unsigned random(); void map_monomial_vars_to_monomial_indices(unsigned i); diff --git a/src/math/lp/nla_settings.h b/src/math/lp/nla_settings.h index bc9de779f..c26d17e0c 100644 --- a/src/math/lp/nla_settings.h +++ b/src/math/lp/nla_settings.h @@ -23,12 +23,25 @@ namespace nla { class nla_settings { bool m_run_order; bool m_run_tangents; + bool m_run_horner; + // how often to call the horner heuristic + unsigned m_horner_frequency; public: - nla_settings() : m_run_order(true), m_run_tangents(true) {} + nla_settings() : m_run_order(true), + m_run_tangents(true), + m_run_horner(true), + m_horner_frequency(4) {} + bool run_order() const { return m_run_order; } bool& run_order() { return m_run_order; } bool run_tangents() const { return m_run_tangents; } bool& run_tangents() { return m_run_tangents; } + + bool run_horner() const { return m_run_horner; } + bool& run_horner() { return m_run_horner; } + + unsigned horner_frequency() const { return m_horner_frequency; } + unsigned& horner_frequency() { return m_horner_frequency; } }; }