diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h index bf2a26ef2..1cd530944 100644 --- a/src/math/lp/cross_nested.h +++ b/src/math/lp/cross_nested.h @@ -26,15 +26,17 @@ namespace nla { class cross_nested { // fields - nex * m_e; - std::function m_call_on_result; - std::function m_var_is_fixed; - std::function m_random; - bool m_done; - ptr_vector m_b_split_vec; - int m_reported; - bool m_random_bit; - nex_creator m_nex_creator; + nex * m_e; + std::function m_call_on_result; + std::function m_var_is_fixed; + std::function m_random; + bool m_done; + ptr_vector m_b_split_vec; + int m_reported; + bool m_random_bit; + nex_creator m_nex_creator; + std::function m_lt; + #ifdef Z3DEBUG nex* m_e_clone; #endif @@ -44,13 +46,14 @@ public: cross_nested(std::function call_on_result, std::function var_is_fixed, - std::function random): + std::function random, + std::function lt): m_call_on_result(call_on_result), m_var_is_fixed(var_is_fixed), m_random(random), m_done(false), - m_reported(0) - {} + m_reported(0), + m_nex_creator(lt) {} void run(nex *e) { @@ -124,7 +127,7 @@ public: } nex* c_over_f = m_nex_creator.mk_div(*c, f); - to_sum(c_over_f)->simplify(&c_over_f); + to_sum(c_over_f)->simplify(&c_over_f, m_lt); nex_mul* cm; *c = cm = m_nex_creator.mk_mul(f, c_over_f); TRACE("nla_cn", tout << "common factor=" << *f << ", c=" << **c << "\ne = " << *m_e << "\n";); @@ -389,7 +392,7 @@ public: TRACE("nla_cn_details", tout << "a = " << *a << "\n";); SASSERT(a->children().size() >= 2 && m_b_split_vec.size()); nex* f; - a->simplify(&f); + a->simplify(&f, m_lt); if (m_b_split_vec.size() == 1) { b = m_b_split_vec[0]; @@ -518,7 +521,7 @@ public: a->children()[j] = normalize(a->children()[j]); } nex *r; - a->simplify(&r); + a->simplify(&r, m_lt); return r; } diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 0119db847..41aadb94d 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -92,7 +92,9 @@ bool horner::lemmas_on_row(const T& row) { cross_nested cn( [this](const nex* n) { return check_cross_nested_expr(n); }, [this](unsigned j) { return c().var_is_fixed(j); }, - [this]() { return c().random(); } + [this]() { return c().random(); }, + [](const nex* a, const nex* b) { return + less_than_nex(a, b, [](lpvar j, lpvar k) { return j < k;}); } ); SASSERT (row_is_interesting(row)); diff --git a/src/math/lp/nex.cpp b/src/math/lp/nex.cpp new file mode 100644 index 000000000..ac7e51ed3 --- /dev/null +++ b/src/math/lp/nex.cpp @@ -0,0 +1,98 @@ +/*++ + Copyright (c) 2017 Microsoft Corporation + + Module Name: + + + + Abstract: + + + + Author: + Lev Nachmanson (levnach) + + Revision History: + + + --*/ + +#include "math/lp/nex.h" +namespace nla { + + +bool ignored_child(nex* e, expr_type t) { + switch(t) { + case expr_type::MUL: + return e->is_scalar() && to_scalar(e)->value().is_one(); + case expr_type::SUM: + return e->is_scalar() && to_scalar(e)->value().is_zero(); + default: return false; + } + return false; +} + + + +void promote_children_of_sum(ptr_vector & children,std::function lt ) { + ptr_vector to_promote; + int skipped = 0; + for(unsigned j = 0; j < children.size(); j++) { + nex** e = &(children[j]); + (*e)->simplify(e, lt); + if ((*e)->is_sum()) { + to_promote.push_back(*e); + } else if (ignored_child(*e, expr_type::SUM)) { + skipped ++; + continue; + } else { + unsigned offset = to_promote.size() + skipped; + if (offset) { + children[j - offset] = *e; + } + } + } + + children.shrink(children.size() - to_promote.size() - skipped); + + for (nex *e : to_promote) { + for (nex *ee : *(to_sum(e)->children_ptr())) { + if (!ignored_child(ee, expr_type::SUM)) + children.push_back(ee); + } + } +} + +void promote_children_of_mul(vector & children, std::function lt) { + TRACE("nla_cn_details", print_vector(children, tout);); + vector to_promote; + int skipped = 0; + for(unsigned j = 0; j < children.size(); j++) { + nex_pow& p = children[j]; + (p.e())->simplify(p.ee(), lt); + if ((p.e())->is_mul()) { + to_promote.push_back(p); + } else if (ignored_child(p.e(), expr_type::MUL)) { + skipped ++; + continue; + } else { + unsigned offset = to_promote.size() + skipped; + if (offset) { + children[j - offset] = p; + } + } + } + + children.shrink(children.size() - to_promote.size() - skipped); + + for (nex_pow & p : to_promote) { + for (nex_pow& pp : to_mul(p.e())->children()) { + SASSERT(!ignored_child(pp.e(), expr_type::MUL)); + children.push_back(nex_pow(pp.e(), pp.pow() * p.pow())); + } + } + + TRACE("nla_cn_details", print_vector(children, tout);); + +} +} diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h index f3d29f9d0..b6e32667b 100644 --- a/src/math/lp/nex.h +++ b/src/math/lp/nex.h @@ -19,6 +19,7 @@ #pragma once #include #include "math/lp/nla_defs.h" +#include namespace nla { enum class expr_type { VAR, SUM, MUL, SCALAR, UNDEF }; inline std::ostream & operator<<(std::ostream& out, expr_type t) { @@ -42,6 +43,8 @@ inline std::ostream & operator<<(std::ostream& out, expr_type t) { return out; } +class nex; +bool less_than_nex_standard(const nex* a, const nex* b); // This is the class of non-linear expressions class nex { @@ -68,7 +71,9 @@ public: virtual ~nex() {} virtual bool contains(lpvar j) const { return false; } virtual int get_degree() const = 0; - virtual void simplify(nex** ) = 0; + // simplifies the expression and also assigns the address of "this" to *e + virtual void simplify(nex** e, std::function lt) { *e = this; } + void simplify(nex** e) { return simplify(e, less_than_nex_standard); } virtual bool is_simplified() const { return true; } @@ -100,7 +105,6 @@ public: bool contains(lpvar j) const { return j == m_j; } int get_degree() const { return 1; } - virtual void simplify(nex** e) { *e = this; } bool virtual is_linear() const { return true; } }; @@ -118,7 +122,6 @@ public: } int get_degree() const { return 0; } - virtual void simplify(nex** e) { *e = this; } bool is_linear() const { return true; } }; @@ -126,20 +129,10 @@ public: const nex_scalar * to_scalar(const nex* a); class nex_sum; const nex_sum* to_sum(const nex*a); -static bool ignored_child(nex* e, expr_type t) { - switch(t) { - case expr_type::MUL: - return e->is_scalar() && to_scalar(e)->value().is_one(); - case expr_type::SUM: - return e->is_scalar() && to_scalar(e)->value().is_zero(); - default: return false; - } - return false; -} -void promote_children_of_sum(ptr_vector & children); +void promote_children_of_sum(ptr_vector & children, std::function); class nex_pow; -void promote_children_of_mul(vector & children); +void promote_children_of_mul(vector & children, std::function lt); class nex_pow { nex* m_e; @@ -202,6 +195,7 @@ public: } void get_powers_from_mul(std::unordered_map & r) const { + TRACE("nla_cn_details", tout << "powers of " << *this << "\n";); r.clear(); for (const auto & c : children()) { if (!c.e()->is_var()) { @@ -221,13 +215,13 @@ public: } return degree; } - - void simplify(nex **e) { + // the second argument is the comparison less than operator + void simplify(nex **e, std::function lt) { TRACE("nla_cn_details", tout << *this << "\n";); TRACE("nla_cn_details", tout << "**e = " << **e << "\n";); *e = this; TRACE("nla_cn_details", tout << *this << "\n";); - promote_children_of_mul(m_children); + promote_children_of_mul(m_children, lt); if (size() == 1 && m_children[0].pow() == 1) *e = m_children[0].e(); TRACE("nla_cn_details", tout << *this << "\n";); @@ -326,12 +320,13 @@ public: return out; } - void simplify(nex **e) { + void simplify(nex **e, std::function lt ) { *e = this; - promote_children_of_sum(m_children); + promote_children_of_sum(m_children, lt); if (size() == 1) *e = m_children[0]; } + virtual bool is_simplified() const { if (size() < 2) return false; for (nex * e : children()) { @@ -402,6 +397,16 @@ inline std::ostream& operator<<(std::ostream& out, const nex& e ) { return e.print(out); } + +inline bool less_than_nex(const nex* a, const nex* b, std::function lt) { + NOT_IMPLEMENTED_YET(); + return false; +} + +inline bool less_than_nex_standard(const nex* a, const nex* b) { + return less_than_nex(a, b, [](lpvar j, lpvar k) { return j < k; }); +} + #if Z3DEBUG inline bool operator<(const ptr_vector&a , const ptr_vector& b) { @@ -420,5 +425,6 @@ inline bool operator<(const ptr_vector&a , const ptr_vector& b) { } #endif + } diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h index f2c6ebbf7..0f38c31b2 100644 --- a/src/math/lp/nex_creator.h +++ b/src/math/lp/nex_creator.h @@ -38,10 +38,13 @@ struct occ { class nex_creator { - ptr_vector m_allocated; - std::unordered_map m_occurences_map; - std::unordered_map m_powers; + ptr_vector m_allocated; + std::unordered_map m_occurences_map; + std::unordered_map m_powers; + // the "less than" operator on expressions + std::function m_lt; public: + nex_creator(std::function lt) {} const std::unordered_map& occurences_map() const { return m_occurences_map; } std::unordered_map& occurences_map() { return m_occurences_map; } const std::unordered_map & powers() const { return m_powers; } diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index fa7670ca4..9c36c96d7 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -21,7 +21,13 @@ #include "math/lp/nla_core.h" #include "math/lp/factorization_factory_imp.h" namespace nla { -nla_grobner::nla_grobner(core *c) : common(c), m_nl_gb_exhausted(false), m_dep_manager(m_val_manager, m_alloc) {} +nla_grobner::nla_grobner(core *c + ) : + common(c), + m_nl_gb_exhausted(false), + m_dep_manager(m_val_manager, m_alloc), + m_nex_creator([this](const nex* a, const nex* b) { return + this->less_than_on_expr(a, b); }) {} // Scan the grobner basis eqs for equations of the form x - k = 0 or x = 0 is found, and x is not fixed, // then assert bounds for x, and continue diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index 8e9431e4c..784b2efe9 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -37,7 +37,7 @@ struct grobner_stats { }; enum class var_weight { - FIXED = 0, + FIXED = 0, QUOTED_FIXED = 1, BOUNDED = 2, QUOTED_BOUNDED = 3, @@ -86,22 +86,23 @@ class nla_grobner : common { typedef ptr_vector equation_vector; // fields - 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_of_equations; - grobner_stats m_stats; - equation_set m_processed; - equation_set m_to_process; - bool m_nl_gb_exhausted; - ptr_vector m_allocated; - lp::int_set m_tmp_var_set; - region m_alloc; - ci_value_manager m_val_manager; - ci_dependency_manager m_dep_manager; - nex_creator m_nex_creator; + 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_of_equations; + grobner_stats m_stats; + equation_set m_processed; + equation_set m_to_process; + bool m_nl_gb_exhausted; + ptr_vector m_allocated; + lp::int_set m_tmp_var_set; + region m_alloc; + ci_value_manager m_val_manager; + ci_dependency_manager m_dep_manager; + nex_creator m_nex_creator; + std::function m_lt; public: nla_grobner(core *core); void grobner_lemmas(); @@ -156,5 +157,22 @@ private: return static_cast(a)->value(); return rational(1); } + + bool less_than_on_vars(lpvar a, lpvar b) const { + const auto &aw = m_active_vars_weights[a]; + const auto &ab = m_active_vars_weights[b]; + if (aw < ab) + return true; + if (aw > ab) + return false; + // aw == ab + return a < b; + } + + bool less_than_on_expr(const nex* a, const nex* b) const { + return less_than_nex(a, b, [this](lpvar j, lpvar k) {return less_than_on_vars(j, k);}); + } + + }; // end of grobner } diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index 44514dafc..6a669d39f 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -96,7 +96,8 @@ void test_cn() { return false; } , [](unsigned) { return false; }, - []{ return 1; } + []{ return 1; }, + less_than_nex_standard ); enable_trace("nla_cn"); enable_trace("nla_cn_details");