diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 9dd0011d1..1085b5a2a 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -22,19 +22,25 @@ #include "math/lp/nla_core.h" namespace nla { - +typedef nla_expr nex; horner::horner(core * c) : common(c) {} template -bool horner::row_is_interesting(const T&) const { - return true; +bool horner::row_is_interesting(const T& row) const { + for (const auto& p : row) { + if (c().m_to_refine.contains(p.var())) + return true; + } + return false; } template void horner::lemma_on_row(const T& row) { if (!row_is_interesting(row)) return; - SASSERT(false); + nex e = create_expr_from_row(row); + intervals::interval inter = interval_of_expr(e); + check_interval_for_conflict(inter); } void horner::horner_lemmas() { @@ -53,4 +59,105 @@ void horner::horner_lemmas() { SASSERT(false); } +nex horner::nexvar(lpvar j) const { + if (!c().is_monomial_var(j)) + return nex::var(j); + const monomial& m = c().emons()[j]; + nex e(expr_type::MUL); + for (lpvar k : m.vars()) { + e.add_child(nex::var(k)); + } + return e; +} + +void process_var_occurences(lpvar j, std::unordered_set& seen, std::unordered_map& occurences) { + if (seen.find(j) != seen.end()) return; + seen.insert(j); + auto it = occurences.find(j); + if (it == occurences.end()) + occurences[j] = 1; + else + it->second ++; +} + +void process_mul_occurences(const nex& e, std::unordered_set& seen, std::unordered_map& occurences) { + SASSERT(e.type() == expr_type::MUL); + for (const auto & ce : e.children()) { + if (ce.type() == expr_type::SCALAR) { + } else if (ce.type() == expr_type::VAR) { + process_var_occurences(ce.var(), seen, occurences); + } else if (ce.type() == expr_type::MUL){ + process_mul_occurences(ce, seen, occurences); + } else { + SASSERT(false); // unexpected type + } + } +} + + + +// j -> the number of expressions j appears in +void horner::get_occurences_map(const nla_expr& e, std::unordered_map& occurences) const { + SASSERT(e.type() == expr_type::SUM); + for (const auto & ce : e.children()) { + std::unordered_set seen; + if (ce.type() == expr_type::MUL) { + for (const auto & cce : ce.children()) { + if (cce.type() == expr_type::SCALAR) { + } else if (cce.type() == expr_type::VAR) { + process_var_occurences(cce.var(), seen, occurences); + } else if (cce.type() == expr_type::MUL) { + process_mul_occurences(cce, seen, occurences); + } else { + TRACE("nla_cn", tout << "e = " << e << "\nce = " << ce << std::endl << + "ce type = " << ce.type() << std::endl;); + + SASSERT(false); // unexpected type + } + } + } else if (ce.type() == expr_type::VAR) { + process_var_occurences(ce.var(), seen, occurences); + } else { + SASSERT(false); + } + } +} + + +nex horner::cross_nested_of_sum(const nla_expr& e) const { + SASSERT(e.type() == expr_type::SUM); + std::unordered_map occurences; + get_occurences_map(e, occurences); + TRACE("nla_cn", + tout << "e = " << e << "\noccurences "; + for (auto p : occurences){ + tout << "(v"< nex horner::create_expr_from_row(const T& row) { + nex e; + if (row.size() > 1) { + e.type() = expr_type::SUM; + for (const auto &p : row) { + e.add_child(nex::mul(p.coeff(), nexvar(p.var()))); + } + return cross_nested_of_sum(e); + } + if (row.size() == 1) { + const auto &p = *row.begin(); + return nex::mul(p.coeff(), nexvar(p.var())); + } + + SASSERT(false); +} +intervals::interval horner::interval_of_expr(const nex& e) { + + SASSERT(false); +} +void horner::check_interval_for_conflict(const intervals::interval&) { + SASSERT(false); +} } diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h index ff6d67dbe..4a6c53730 100644 --- a/src/math/lp/horner.h +++ b/src/math/lp/horner.h @@ -20,6 +20,8 @@ #pragma once #include "math/lp/nla_common.h" +#include "math/lp/nla_intervals.h" +#include "math/lp/nla_expr.h" namespace nla { class core; @@ -33,6 +35,12 @@ public: void lemma_on_row(const T&); template bool row_is_interesting(const T&) const; -private: + template nla_expr create_expr_from_row(const T&); + intervals::interval interval_of_expr(const nla_expr& e); + void check_interval_for_conflict(const intervals::interval&); + nla_expr nexvar(lpvar j) const; + nla_expr cross_nested_of_sum(const nla_expr&) const; + void get_occurences_map(const nla_expr& e, std::unordered_map& ) const; + }; // end of horner } diff --git a/src/math/lp/int_set.h b/src/math/lp/int_set.h index 3b749b93c..eab6aefe1 100644 --- a/src/math/lp/int_set.h +++ b/src/math/lp/int_set.h @@ -54,6 +54,8 @@ public: m_data[j] = -1; } + int operator[](unsigned j) const { return m_index[j]; } + void resize(unsigned size) { m_data.resize(size, -1); } @@ -61,7 +63,7 @@ public: void increase_size_by_one() { resize(m_data.size() + 1); } - + unsigned data_size() const { return m_data.size(); } unsigned size() const { return m_index.size();} bool is_empty() const { return size() == 0; } @@ -76,6 +78,7 @@ public: } out << std::endl; } - + const int * begin() const { return m_index.begin(); } + const int * end() const { return m_index.end(); } }; } diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp index bbb5bce12..7eeec02ea 100644 --- a/src/math/lp/nla_basics_lemmas.cpp +++ b/src/math/lp/nla_basics_lemmas.cpp @@ -149,8 +149,8 @@ bool basics::basic_sign_lemma(bool derived) { return basic_sign_lemma_model_based(); std::unordered_set explored; - for (lpvar i : c().m_to_refine){ - if (basic_sign_lemma_on_mon(i, explored)) + for (lpvar j : c().m_to_refine){ + if (basic_sign_lemma_on_mon(j, explored)) return true; } return false; diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index cb9fac56d..ac91066eb 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -831,37 +831,6 @@ void core::collect_equivs() { } } -void core::collect_equivs_of_fixed_vars() { - std::unordered_map > abs_map; - for (lpvar j = 0; j < m_lar_solver.number_of_vars(); j++) { - if (!var_is_fixed(j)) - continue; - rational v = abs(val(j)); - auto it = abs_map.find(v); - if (it == abs_map.end()) { - abs_map[v] = svector(); - abs_map[v].push_back(j); - } else { - it->second.push_back(j); - } - } - for (auto p : abs_map) { - svector& v = p.second; - lpvar head = v[0]; - auto c0 = m_lar_solver.get_column_upper_bound_witness(head); - auto c1 = m_lar_solver.get_column_lower_bound_witness(head); - for (unsigned k = 1; k < v.size(); k++) { - auto c2 = m_lar_solver.get_column_upper_bound_witness(v[k]); - auto c3 = m_lar_solver.get_column_lower_bound_witness(v[k]); - if (val(head) == val(v[k])) { - m_evars.merge_plus(head, v[k], eq_justification({c0, c1, c2, c3})); - } else { - SASSERT(val(head) == -val(v[k])); - m_evars.merge_minus(head, v[k], eq_justification({c0, c1, c2, c3})); - } - } - } -} // returns true iff the term is in a form +-x-+y. // the sign is true iff the term is x+y, -x-y. @@ -975,11 +944,12 @@ void core::init_search() { void core::init_to_refine() { TRACE("nla_solver", tout << "emons:" << pp_emons(*this, m_emons);); m_to_refine.clear(); + m_to_refine.resize(m_lar_solver.number_of_vars()); unsigned r = random(), sz = m_emons.number_of_monomials(); for (unsigned k = 0; k < sz; k++) { auto const & m = *(m_emons.begin() + (k + r)% sz); if (!check_monomial(m)) - m_to_refine.push_back(m.var()); + m_to_refine.insert(m.var()); } TRACE("nla_solver", @@ -1333,7 +1303,7 @@ lbool core::check(vector& l_vec) { } init_to_refine(); - if (m_to_refine.empty()) { + if (m_to_refine.is_empty()) { return l_true; } init_search(); diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 1a651df69..306e9818f 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -82,7 +82,7 @@ public: var_eqs m_evars; lp::lar_solver& m_lar_solver; vector * m_lemma_vec; - svector m_to_refine; + lp::int_set m_to_refine; tangents m_tangents; basics m_basics; order m_order; @@ -291,8 +291,6 @@ public: // we look for octagon constraints here, with a left part +-x +- y void collect_equivs(); - void collect_equivs_of_fixed_vars(); - bool is_octagon_term(const lp::lar_term& t, bool & sign, lpvar& i, lpvar &j) const; void add_equivalence_maybe(const lp::lar_term *t, lpci c0, lpci c1); diff --git a/src/math/lp/nla_expr.h b/src/math/lp/nla_expr.h index 31b04873b..ca6848943 100644 --- a/src/math/lp/nla_expr.h +++ b/src/math/lp/nla_expr.h @@ -19,15 +19,45 @@ Revision History: #pragma once #include "math/lp/nla_defs.h" namespace nla { -enum class expr_type { SUM, MUL, VAR, SCALAR }; +enum class expr_type { SUM, MUL, VAR, SCALAR, UNDEF }; +inline std::ostream & operator<<(std::ostream& out, expr_type t) { + switch (t) { + case expr_type::SUM: + out << "SUM"; + break; + case expr_type::MUL: + out << "MUL"; + break; + case expr_type::VAR: + out << "VAR"; + break; + case expr_type::SCALAR: + out << "SCALAR"; + break; + case expr_type::UNDEF: + out << "UNDEF"; + break; + default: + out << "NN"; + break; + } + return out; +} // This class is needed in horner calculation with intervals template class nla_expr { + // todo: use union expr_type m_type; lpvar m_j; T m_v; // for the scalar vector m_children; public: + lpvar var() const { SASSERT(m_type == expr_type::VAR); return m_j; } + expr_type type() const { return m_type; } + expr_type& type() { return m_type; } + const vector& children() const { return m_children; } + vector& children() { return m_children; } + std::string str() const { std::stringstream ss; ss << *this; return ss.str(); } std::ostream & print_sum(std::ostream& out) const { bool first = true; @@ -90,6 +120,7 @@ public: out << m_v; return out; default: + out << "undef"; return out; } } @@ -106,6 +137,11 @@ public: } nla_expr(expr_type t): m_type(t) {} + nla_expr() { +#if Z3DEBUG + m_type = expr_type::UNDEF; +#endif + } void add_child(const nla_expr& e) { SASSERT(m_type == expr_type::SUM || m_type == expr_type::MUL); @@ -126,6 +162,21 @@ public: return r; } + static nla_expr mul(const T& v, const nla_expr & w) { + if (v == 1) + return w; + nla_expr r(expr_type::MUL); + r.add_child(scalar(v)); + r.add_child(w); + return r; + } + + static nla_expr mul(const T& v, lpvar j) { + if (v == 1) + return var(j); + return mul(scalar(v), var(j)); + } + static nla_expr scalar(const T& v) { nla_expr r(expr_type::SCALAR); r.m_v = v;