From a085edceff4f31e42fd77b4cf11ed6ae20ff9637 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 19 Sep 2019 15:51:01 -0700 Subject: [PATCH] port grobner basis functionality, prepare create nex objects to the grobner basis calculation Signed-off-by: Lev Nachmanson --- src/math/lp/cross_nested.h | 257 ++++++------------------------ src/math/lp/horner.cpp | 14 +- src/math/lp/horner.h | 6 +- src/math/lp/lp_core_solver_base.h | 5 +- src/math/lp/nex.h | 4 +- src/math/lp/nex_creator.h | 215 +++++++++++++++++++++++++ src/math/lp/nla_common.h | 23 +++ src/math/lp/nla_core.cpp | 14 +- src/math/lp/nla_grobner.cpp | 86 +++++++++- src/math/lp/nla_grobner.h | 49 ++++-- src/math/lp/nla_intervals.cpp | 4 +- src/math/lp/nla_intervals.h | 21 +-- 12 files changed, 424 insertions(+), 274 deletions(-) create mode 100644 src/math/lp/nex_creator.h diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h index 09d3706ee..500e909b9 100644 --- a/src/math/lp/cross_nested.h +++ b/src/math/lp/cross_nested.h @@ -20,19 +20,10 @@ #pragma once #include #include "math/lp/nex.h" +#include "math/lp/nex_creator.h" + namespace nla { class cross_nested { - struct occ { - unsigned m_occs; - unsigned m_power; - occ() : m_occs(0), m_power(0) {} - occ(unsigned k, unsigned p) : m_occs(k), m_power(p) {} - // use the "name injection rule here" - friend std::ostream& operator<<(std::ostream& out, const occ& c) { - out << "(occs:" << c.m_occs <<", pow:" << c.m_power << ")"; - return out; - } - }; // fields nex * m_e; @@ -40,20 +31,17 @@ class cross_nested { std::function m_var_is_fixed; std::function m_random; bool m_done; - std::unordered_map m_occurences_map; - std::unordered_map m_powers; - ptr_vector m_allocated; ptr_vector m_b_split_vec; int m_reported; bool m_random_bit; - + nex_creator m_nex_creator; #ifdef Z3DEBUG nex* m_e_clone; #endif - void add_to_allocated(nex* r) { - m_allocated.push_back(r); - } public: + + nex_creator& get_nex_creator() { return m_nex_creator; } + cross_nested(std::function call_on_result, std::function var_is_fixed, std::function random): @@ -84,172 +72,25 @@ public: return c; } - nex_sum* mk_sum() { - auto r = new nex_sum(); - add_to_allocated(r); - return r; - } - template - void add_children(T) { } - - template - void add_children(T r, K e, Args ... es) { - r->add_child(e); - add_children(r, es ...); - } - - nex_sum* mk_sum(const ptr_vector& v) { - auto r = new nex_sum(); - add_to_allocated(r); - r->children() = v; - return r; - } - - nex_mul* mk_mul(const ptr_vector& v) { - auto r = new nex_mul(); - add_to_allocated(r); - r->children() = v; - return r; - } - - - template - nex_sum* mk_sum(K e, Args... es) { - auto r = new nex_sum(); - add_to_allocated(r); - r->add_child(e); - add_children(r, es...); - return r; - } - nex_var* mk_var(lpvar j) { - auto r = new nex_var(j); - add_to_allocated(r); - return r; - } - - nex_mul* mk_mul() { - auto r = new nex_mul(); - add_to_allocated(r); - return r; - } - - template - nex_mul* mk_mul(K e, Args... es) { - auto r = new nex_mul(); - add_to_allocated(r); - add_children(r, e, es...); - return r; - } - - nex_scalar* mk_scalar(const rational& v) { - auto r = new nex_scalar(v); - add_to_allocated(r); - return r; - } - - - nex * mk_div(const nex* a, lpvar j) { - TRACE("nla_cn_details", tout << "a=" << *a << ", v" << j << "\n";); - SASSERT((a->is_mul() && a->contains(j)) || (a->is_var() && to_var(a)->var() == j)); - if (a->is_var()) - return mk_scalar(rational(1)); - ptr_vector bv; - bool seenj = false; - for (nex* c : to_mul(a)->children()) { - if (!seenj) { - if (c->contains(j)) { - if (!c->is_var()) - bv.push_back(mk_div(c, j)); - seenj = true; - continue; - } - } - bv.push_back(c); - } - if (bv.size() > 1) { - return mk_mul(bv); - } - if (bv.size() == 1) { - return bv[0]; - } - - SASSERT(bv.size() == 0); - return mk_scalar(rational(1)); - } - - nex * mk_div(const nex* a, const nex* b) { - TRACE("nla_cn_details", tout << *a <<" / " << *b << "\n";); - if (b->is_var()) { - return mk_div(a, to_var(b)->var()); - } - SASSERT(b->is_mul()); - const nex_mul *bm = to_mul(b); - if (a->is_sum()) { - nex_sum * r = mk_sum(); - const nex_sum * m = to_sum(a); - for (auto e : m->children()) { - r->add_child(mk_div(e, bm)); - } - TRACE("nla_cn_details", tout << *r << "\n";); - return r; - } - if (a->is_var() || (a->is_mul() && to_mul(a)->children().size() == 1)) { - return mk_scalar(rational(1)); - } - SASSERT(a->is_mul()); - const nex_mul* am = to_mul(a); - bm->get_powers_from_mul(m_powers); - nex_mul* ret = new nex_mul(); - for (auto e : am->children()) { - TRACE("nla_cn_details", tout << "e=" << *e << "\n";); - - if (!e->is_var()) { - SASSERT(e->is_scalar()); - ret->add_child(e); - TRACE("nla_cn_details", tout << "continue\n";); - continue; - } - SASSERT(e->is_var()); - lpvar j = to_var(e)->var(); - auto it = m_powers.find(j); - if (it == m_powers.end()) { - ret->add_child(e); - } else { - it->second --; - if (it->second == 0) - m_powers.erase(it); - } - TRACE("nla_cn_details", tout << *ret << "\n";); - } - SASSERT(m_powers.size() == 0); - if (ret->children().size() == 0) { - delete ret; - TRACE("nla_cn_details", tout << "return 1\n";); - return mk_scalar(rational(1)); - } - add_to_allocated(ret); - TRACE("nla_cn_details", tout << *ret << "\n";); - return ret; - } nex* extract_common_factor(nex* e) { nex_sum* c = to_sum(e); - TRACE("nla_cn", tout << "c=" << *c << "\n"; tout << "occs:"; dump_occurences(tout, m_occurences_map) << "\n";); + TRACE("nla_cn", tout << "c=" << *c << "\n"; tout << "occs:"; dump_occurences(tout, m_nex_creator.occurences_map()) << "\n";); unsigned size = c->children().size(); bool have_factor = false; - for(const auto & p : m_occurences_map) { + for(const auto & p : m_nex_creator.occurences_map()) { if (p.second.m_occs == size) { have_factor = true; break; } } if (have_factor == false) return nullptr; - nex_mul* f = mk_mul(); - for(const auto & p : m_occurences_map) { // randomize here: todo + nex_mul* f = m_nex_creator.mk_mul(); + for(const auto & p : m_nex_creator.occurences_map()) { // randomize here: todo if (p.second.m_occs == size) { unsigned pow = p.second.m_power; while (pow --) { - f->add_child(mk_var(p.first)); + f->add_child(m_nex_creator.mk_var(p.first)); } } } @@ -282,9 +123,9 @@ public: return false; } - nex* c_over_f = mk_div(*c, f); + nex* c_over_f = m_nex_creator.mk_div(*c, f); to_sum(c_over_f)->simplify(&c_over_f); - *c = mk_mul(f, c_over_f); + *c = m_nex_creator.mk_mul(f, c_over_f); TRACE("nla_cn", tout << "common factor=" << *f << ", c=" << **c << "\ne = " << *m_e << "\n";); explore_expr_on_front_elem(&(*((*c)->children_ptr()))[1], front); @@ -310,16 +151,14 @@ public: } void pop_allocated(unsigned sz) { - for (unsigned j = sz; j < m_allocated.size(); j ++) - delete m_allocated[j]; - m_allocated.resize(sz); + m_nex_creator.pop(sz); } void explore_expr_on_front_elem_vars(nex** c, vector& front, const svector & vars) { TRACE("nla_cn", tout << "save c=" << **c << "; front:"; print_front(front, tout) << "\n";); nex* copy_of_c = *c; auto copy_of_front = copy_front(front); - int alloc_size = m_allocated.size(); + int alloc_size = m_nex_creator.size(); for(lpvar j : vars) { if (m_var_is_fixed(j)) { // it does not make sense to explore fixed multupliers @@ -353,26 +192,26 @@ public: clear_maps(); for (const auto * ce : e->children()) { if (ce->is_mul()) { - to_mul(ce)->get_powers_from_mul(m_powers); + to_mul(ce)->get_powers_from_mul(m_nex_creator.powers()); update_occurences_with_powers(); } else if (ce->is_var()) { add_var_occs(to_var(ce)->var()); } } remove_singular_occurences(); - TRACE("nla_cn_details", tout << "e=" << *e << "\noccs="; dump_occurences(tout, m_occurences_map) << "\n";); + TRACE("nla_cn_details", tout << "e=" << *e << "\noccs="; dump_occurences(tout, m_nex_creator.occurences_map()) << "\n";); } void fill_vars_from_occurences_map(svector& vars) { - for (auto & p : m_occurences_map) + for (auto & p : m_nex_creator.occurences_map()) vars.push_back(p.first); m_random_bit = m_random() % 2; TRACE("nla_cn", tout << "m_random_bit = " << m_random_bit << "\n";); std::sort(vars.begin(), vars.end(), [this](lpvar j, lpvar k) { - auto it_j = m_occurences_map.find(j); - auto it_k = m_occurences_map.find(k); + auto it_j = m_nex_creator.occurences_map().find(j); + auto it_k = m_nex_creator.occurences_map().find(k); const occ& a = it_j->second; @@ -456,46 +295,46 @@ public: } void add_var_occs(lpvar j) { - auto it = m_occurences_map.find(j); - if (it != m_occurences_map.end()) { + auto it = m_nex_creator.occurences_map().find(j); + if (it != m_nex_creator.occurences_map().end()) { it->second.m_occs++; it->second.m_power = 1; } else { - m_occurences_map.insert(std::make_pair(j, occ(1, 1))); + m_nex_creator.occurences_map().insert(std::make_pair(j, occ(1, 1))); } } void update_occurences_with_powers() { - for (auto & p : m_powers) { + for (auto & p : m_nex_creator.powers()) { lpvar j = p.first; unsigned jp = p.second; - auto it = m_occurences_map.find(j); - if (it == m_occurences_map.end()) { - m_occurences_map[j] = occ(1, jp); + auto it = m_nex_creator.occurences_map().find(j); + if (it == m_nex_creator.occurences_map().end()) { + m_nex_creator.occurences_map()[j] = occ(1, jp); } else { it->second.m_occs++; it->second.m_power = std::min(it->second.m_power, jp); } } - TRACE("nla_cn_details", tout << "occs="; dump_occurences(tout, m_occurences_map) << "\n";); + TRACE("nla_cn_details", tout << "occs="; dump_occurences(tout, m_nex_creator.occurences_map()) << "\n";); } void remove_singular_occurences() { svector r; - for (const auto & p : m_occurences_map) { + for (const auto & p : m_nex_creator.occurences_map()) { if (p.second.m_occs <= 1) { r.push_back(p.first); } } for (lpvar j : r) - m_occurences_map.erase(j); + m_nex_creator.occurences_map().erase(j); } void clear_maps() { - m_occurences_map.clear(); - m_powers.clear(); + m_nex_creator.occurences_map().clear(); + m_nex_creator.powers().clear(); } // j -> the number of expressions j appears in as a multiplier @@ -504,16 +343,16 @@ public: clear_maps(); for (const auto * ce : e->children()) { if (ce->is_mul()) { - to_mul(ce)->get_powers_from_mul(m_powers); + to_mul(ce)->get_powers_from_mul(m_nex_creator.powers()); update_occurences_with_powers(); } else if (ce->is_var()) { add_var_occs(to_var(ce)->var()); } } remove_singular_occurences(); - TRACE("nla_cn_details", tout << "e=" << *e << "\noccs="; dump_occurences(tout, m_occurences_map) << "\n";); + TRACE("nla_cn_details", tout << "e=" << *e << "\noccs="; dump_occurences(tout, m_nex_creator.occurences_map()) << "\n";); vector> ret; - for (auto & p : m_occurences_map) + for (auto & p : m_nex_creator.occurences_map()) ret.push_back(p); std::sort(ret.begin(), ret.end(), [](const std::pair& a, const std::pair& b) { if (a.second.m_occs > b.second.m_occs) @@ -536,11 +375,11 @@ public: } // all factors of j go to a, the rest to b void pre_split(nex_sum * e, lpvar j, nex_sum*& a, nex*& b) { - a = mk_sum(); + a = m_nex_creator.mk_sum(); m_b_split_vec.clear(); for (nex * ce: e->children()) { if (is_divisible_by_var(ce, j)) { - a->add_child(mk_div(ce , j)); + a->add_child(m_nex_creator.mk_div(ce , j)); } else { m_b_split_vec.push_back(ce); TRACE("nla_cn_details", tout << "ce = " << *ce << "\n";); @@ -557,14 +396,14 @@ public: TRACE("nla_cn_details", tout << "b = " << *b << "\n";); } else { SASSERT(m_b_split_vec.size() > 1); - b = mk_sum(m_b_split_vec); + b = m_nex_creator.mk_sum(m_b_split_vec); TRACE("nla_cn_details", tout << "b = " << *b << "\n";); } } void update_front_with_split_with_non_empty_b(nex* &e, lpvar j, vector & front, nex_sum* a, nex* b) { TRACE("nla_cn_details", tout << "b = " << *b << "\n";); - e = mk_sum(mk_mul(mk_var(j), a), b); // e = j*a + b + e = m_nex_creator.mk_sum(m_nex_creator.mk_mul(m_nex_creator.mk_var(j), a), b); // e = j*a + b if (!a->is_linear()) { nex **ptr_to_a = &(to_mul(to_sum(e)->children()[0]))->children()[1]; push_to_front(front, ptr_to_a); @@ -578,7 +417,7 @@ public: void update_front_with_split(nex* & e, lpvar j, vector & front, nex_sum* a, nex* b) { if (b == nullptr) { - e = mk_mul(mk_var(j), a); + e = m_nex_creator.mk_mul(m_nex_creator.mk_var(j), a); if (!to_sum(a)->is_linear()) push_to_front(front, &(to_mul(e)->children()[1])); } else { @@ -635,9 +474,7 @@ public: } ~cross_nested() { - for (auto e: m_allocated) - delete e; - m_allocated.clear(); + m_nex_creator.clear(); } bool done() const { return m_done; } @@ -646,16 +483,16 @@ public: switch (a->type()) { case expr_type::VAR: { auto v = to_var(a); - return mk_var(v->var()); + return m_nex_creator.mk_var(v->var()); } case expr_type::SCALAR: { auto v = to_scalar(a); - return mk_scalar(v->value()); + return m_nex_creator.mk_scalar(v->value()); } case expr_type::MUL: { auto m = to_mul(a); - auto r = mk_mul(); + auto r = m_nex_creator.mk_mul(); for (nex * e : m->children()) { r->add_child(clone(e)); } @@ -663,7 +500,7 @@ public: } case expr_type::SUM: { auto m = to_sum(a); - auto r = mk_sum(); + auto r = m_nex_creator.mk_sum(); for (nex * e : m->children()) { r->add_child(clone(e)); } @@ -701,10 +538,10 @@ public: return r; } - nex_sum *r = mk_sum(); + nex_sum *r = m_nex_creator.mk_sum(); nex_sum *as = to_sum(a->children()[sum_j]); for (unsigned k = 0; k < as->size(); k++) { - nex_mul *b = mk_mul(as->children()[k]); + nex_mul *b = m_nex_creator.mk_mul(as->children()[k]); for (unsigned j = 0; j < a->size(); j ++) { if ((int)j != sum_j) b->add_child(a->children()[j]); diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 7c3c22830..7433b687d 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -96,7 +96,7 @@ bool horner::lemmas_on_row(const T& row) { ); SASSERT (row_is_interesting(row)); - create_sum_from_row(row, cn); + create_sum_from_row(row, cn.get_nex_creator(), m_row_sum); return lemmas_on_expr(cn); } @@ -131,7 +131,7 @@ void horner::horner_lemmas() { } } -nex * horner::nexvar(lpvar j, cross_nested& cn) const { +nex * horner::nexvar(lpvar j, nex_creator& cn) const { // todo: consider deepen the recursion if (!c().is_monic_var(j)) return cn.mk_var(j); @@ -144,7 +144,7 @@ nex * horner::nexvar(lpvar j, cross_nested& cn) const { return e; } -nex * horner::nexvar(const rational & coeff, lpvar j, cross_nested& cn) const { +nex * horner::nexvar(const rational & coeff, lpvar j, nex_creator& cn) const { // todo: consider deepen the recursion if (!c().is_monic_var(j)) return cn.mk_mul(cn.mk_scalar(coeff), cn.mk_var(j)); @@ -158,15 +158,15 @@ nex * horner::nexvar(const rational & coeff, lpvar j, cross_nested& cn) const { } -template void horner::create_sum_from_row(const T& row, cross_nested& cn) { +template void horner::create_sum_from_row(const T& row, nex_creator& cn, nex_sum& sum) { TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";); SASSERT(row.size() > 1); - m_row_sum.children().clear(); + sum.children().clear(); for (const auto &p : row) { if (p.coeff().is_one()) - m_row_sum.add_child(nexvar(p.var(), cn)); + sum.add_child(nexvar(p.var(), cn)); else { - m_row_sum.add_child(nexvar(p.coeff(), p.var(), cn)); + sum.add_child(nexvar(p.coeff(), p.var(), cn)); } } } diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h index 7b3130159..a38a41801 100644 --- a/src/math/lp/horner.h +++ b/src/math/lp/horner.h @@ -40,7 +40,7 @@ public: bool lemmas_on_row(const T&); template bool row_is_interesting(const T&) const; template - void create_sum_from_row(const T&, cross_nested&); + void create_sum_from_row(const T&, nex_creator&, nex_sum&); intervals::interval interval_of_expr_with_deps(const nex* e); intervals::interval interval_of_expr(const nex* e); intervals::interval interval_of_sum(const nex_sum*); @@ -51,8 +51,8 @@ public: bool interval_from_term(const nex* e, interv&) const; - nex* nexvar(lpvar j, cross_nested& cn) const; - nex* nexvar(const rational& coeff, lpvar j, cross_nested& cn) const; + nex* nexvar(lpvar j, nex_creator& ) const; + nex* nexvar(const rational& coeff, lpvar j, nex_creator&) const; intervals::interval interval_of_sum_with_deps(const nex_sum*); intervals::interval interval_of_sum_no_term_with_deps(const nex_sum*); intervals::interval interval_of_mul_with_deps(const nex_mul*); diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h index ad0478757..09531f820 100644 --- a/src/math/lp/lp_core_solver_base.h +++ b/src/math/lp/lp_core_solver_base.h @@ -610,8 +610,11 @@ public: return out; } - bool column_is_free(unsigned j) const { return this->m_column_type[j] == free; } + bool column_is_free(unsigned j) const { return this->m_column_type[j] == column_type::free_column; } + bool column_is_fixed(unsigned j) const { return this->m_column_type[j] == column_type::fixed; } + + bool column_has_upper_bound(unsigned j) const { switch(m_column_types[j]) { case column_type::free_column: diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h index 35278c2cd..7aa5c9c46 100644 --- a/src/math/lp/nex.h +++ b/src/math/lp/nex.h @@ -63,6 +63,7 @@ public: bool is_mul() const { return type() == expr_type::MUL; } bool is_var() const { return type() == expr_type::VAR; } bool is_scalar() const { return type() == expr_type::SCALAR; } + virtual bool is_pure_monomial() const { return false; } std::string str() const { std::stringstream ss; print(ss); return ss.str(); } virtual ~nex() {} virtual bool contains(lpvar j) const { return false; } @@ -182,7 +183,8 @@ public: const ptr_vector& children() const { return m_children;} const ptr_vector* children_ptr() const { return &m_children;} ptr_vector* children_ptr() { return &m_children;} - + // A monomial is 'pure' if does not have a numeric coefficient. + bool is_pure_monomial() { return size() == 0 || (!m_children[0]->is_scalar()); } std::ostream & print(std::ostream& out) const { bool first = true; for (const nex* v : m_children) { diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h new file mode 100644 index 000000000..4a2ec04d1 --- /dev/null +++ b/src/math/lp/nex_creator.h @@ -0,0 +1,215 @@ +/*++ + Copyright (c) 2017 Microsoft Corporation + + Module Name: + + + + Abstract: + + + + Author: + Nikolaj Bjorner (nbjorner) + Lev Nachmanson (levnach) + + Revision History: + + + --*/ +#pragma once + +namespace nla { + +struct occ { + unsigned m_occs; // number of occurences + unsigned m_power; // min power in occurences + occ() : m_occs(0), m_power(0) {} + occ(unsigned k, unsigned p) : m_occs(k), m_power(p) {} + // use the "name injection rule here" + friend std::ostream& operator<<(std::ostream& out, const occ& c) { + out << "(occs:" << c.m_occs <<", pow:" << c.m_power << ")"; + return out; + } +}; + + +// the purpose of this class is to create nex objects, keep them, and delete them + +class nex_creator { + + ptr_vector m_allocated; + std::unordered_map m_occurences_map; + std::unordered_map m_powers; +public: + 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; } + std::unordered_map & powers() { return m_powers; } + + void add_to_allocated(nex* r) { m_allocated.push_back(r); } + + void pop(unsigned sz) { + for (unsigned j = sz; j < m_allocated.size(); j ++) + delete m_allocated[j]; + m_allocated.resize(sz); + } + + void clear() { + for (auto e: m_allocated) + delete e; + m_allocated.clear(); + } + + unsigned size() const { return m_allocated.size(); } + + nex_sum* mk_sum() { + auto r = new nex_sum(); + add_to_allocated(r); + return r; + } + template + void add_children(T) { } + + template + void add_children(T r, K e, Args ... es) { + r->add_child(e); + add_children(r, es ...); + } + + nex_sum* mk_sum(const ptr_vector& v) { + auto r = new nex_sum(); + add_to_allocated(r); + r->children() = v; + return r; + } + + nex_mul* mk_mul(const ptr_vector& v) { + auto r = new nex_mul(); + add_to_allocated(r); + r->children() = v; + return r; + } + + + template + nex_sum* mk_sum(K e, Args... es) { + auto r = new nex_sum(); + add_to_allocated(r); + r->add_child(e); + add_children(r, es...); + return r; + } + nex_var* mk_var(lpvar j) { + auto r = new nex_var(j); + add_to_allocated(r); + return r; + } + + nex_mul* mk_mul() { + auto r = new nex_mul(); + add_to_allocated(r); + return r; + } + + template + nex_mul* mk_mul(K e, Args... es) { + auto r = new nex_mul(); + add_to_allocated(r); + add_children(r, e, es...); + return r; + } + + nex_scalar* mk_scalar(const rational& v) { + auto r = new nex_scalar(v); + add_to_allocated(r); + return r; + } + + + nex * mk_div(const nex* a, lpvar j) { + TRACE("nla_cn_details", tout << "a=" << *a << ", v" << j << "\n";); + SASSERT((a->is_mul() && a->contains(j)) || (a->is_var() && to_var(a)->var() == j)); + if (a->is_var()) + return mk_scalar(rational(1)); + ptr_vector bv; + bool seenj = false; + for (nex* c : to_mul(a)->children()) { + if (!seenj) { + if (c->contains(j)) { + if (!c->is_var()) + bv.push_back(mk_div(c, j)); + seenj = true; + continue; + } + } + bv.push_back(c); + } + if (bv.size() > 1) { + return mk_mul(bv); + } + if (bv.size() == 1) { + return bv[0]; + } + + SASSERT(bv.size() == 0); + return mk_scalar(rational(1)); + } + + nex * mk_div(const nex* a, const nex* b) { + TRACE("nla_cn_details", tout << *a <<" / " << *b << "\n";); + if (b->is_var()) { + return mk_div(a, to_var(b)->var()); + } + SASSERT(b->is_mul()); + const nex_mul *bm = to_mul(b); + if (a->is_sum()) { + nex_sum * r = mk_sum(); + const nex_sum * m = to_sum(a); + for (auto e : m->children()) { + r->add_child(mk_div(e, bm)); + } + TRACE("nla_cn_details", tout << *r << "\n";); + return r; + } + if (a->is_var() || (a->is_mul() && to_mul(a)->children().size() == 1)) { + return mk_scalar(rational(1)); + } + SASSERT(a->is_mul()); + const nex_mul* am = to_mul(a); + bm->get_powers_from_mul(m_powers); + nex_mul* ret = new nex_mul(); + for (auto e : am->children()) { + TRACE("nla_cn_details", tout << "e=" << *e << "\n";); + + if (!e->is_var()) { + SASSERT(e->is_scalar()); + ret->add_child(e); + TRACE("nla_cn_details", tout << "continue\n";); + continue; + } + SASSERT(e->is_var()); + lpvar j = to_var(e)->var(); + auto it = m_powers.find(j); + if (it == m_powers.end()) { + ret->add_child(e); + } else { + it->second --; + if (it->second == 0) + m_powers.erase(it); + } + TRACE("nla_cn_details", tout << *ret << "\n";); + } + SASSERT(m_powers.size() == 0); + if (ret->children().size() == 0) { + delete ret; + TRACE("nla_cn_details", tout << "return 1\n";); + return mk_scalar(rational(1)); + } + add_to_allocated(ret); + TRACE("nla_cn_details", tout << *ret << "\n";); + return ret; + } + +}; +} diff --git a/src/math/lp/nla_common.h b/src/math/lp/nla_common.h index 7753c167b..e82ea16ca 100644 --- a/src/math/lp/nla_common.h +++ b/src/math/lp/nla_common.h @@ -24,6 +24,8 @@ #include "math/lp/monic.h" #include "math/lp/emonics.h" #include "math/lp/factorization.h" +#include "util/dependency.h" +#include "util/region.h" namespace nla { @@ -92,5 +94,26 @@ struct common { std::ostream& print_rooted_monic_with_vars(const monic&, std::ostream& out) const; bool check_monic(const monic&) const; unsigned random(); + + class ci_value_manager { + public: + void inc_ref(lp::constraint_index const & v) { + } + + void dec_ref(lp::constraint_index const & v) { + } + }; + + struct ci_dependency_config { + typedef ci_value_manager value_manager; + typedef region allocator; + static const bool ref_count = false; + typedef lp::constraint_index value; + }; + + typedef dependency_manager ci_dependency_manager; + + typedef ci_dependency_manager::dependency ci_dependency; + }; } diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 5356a5a1b..560c0a66b 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -628,23 +628,17 @@ bool core::sign_contradiction(const monic& m) const { bool core:: var_is_fixed_to_zero(lpvar j) const { return - m_lar_solver.column_has_upper_bound(j) && - m_lar_solver.column_has_lower_bound(j) && - m_lar_solver.get_upper_bound(j) == lp::zero_of_type() && + m_lar_solver.column_is_fixed(j) && m_lar_solver.get_lower_bound(j) == lp::zero_of_type(); } bool core:: var_is_fixed_to_val(lpvar j, const rational& v) const { return - m_lar_solver.column_has_upper_bound(j) && - m_lar_solver.column_has_lower_bound(j) && - m_lar_solver.get_upper_bound(j) == lp::impq(v) && m_lar_solver.get_lower_bound(j) == lp::impq(v); + m_lar_solver.column_is_fixed(j) && + m_lar_solver.get_lower_bound(j) == lp::impq(v); } bool core:: var_is_fixed(lpvar j) const { - return - m_lar_solver.column_has_upper_bound(j) && - m_lar_solver.column_has_lower_bound(j) && - m_lar_solver.get_upper_bound(j) == m_lar_solver.get_lower_bound(j); + return m_lar_solver.column_is_fixed(j); } std::ostream & core::print_ineq(const ineq & in, std::ostream & out) const { diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index da3684414..df1f9273d 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -21,7 +21,7 @@ #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) {} +nla_grobner::nla_grobner(core *c) : common(c), m_nl_gb_exhausted(false), m_dep_manager(m_val_manager, m_alloc) {} // 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 @@ -142,8 +142,81 @@ void nla_grobner::display(std::ostream & out) { c().print_term(r, out) << std::endl; } } -void nla_grobner::add_row_to_gb(unsigned) { + +void nla_grobner::process_var(nex_mul* m, lpvar j, ci_dependency* & dep, rational & coeff) { + if (c().var_is_fixed(j)) { + if (!m_tmp_var_set.contains(j)) { + m_tmp_var_set.insert(j); + lp::constraint_index lc,uc; + c().m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc); + dep = m_dep_manager.mk_join(dep, m_dep_manager.mk_join(m_dep_manager.mk_leaf(lc), m_dep_manager.mk_leaf(uc))); + } + coeff *= c().m_lar_solver.column_upper_bound(j).x; + } + else { + m->add_child(m_nex_creator.mk_var(j)); + } +} + +/** + \brief Create a new monomial using the given coeff and m. Fixed + variables in m are substituted by their values. The arg dep is + updated to store these dependencies. The set already_found is + updated with the fixed variables in m. A variable is only + added to dep if it is not already in already_found. + + Return null if the monomial was simplified to 0. +*/ +nex * nla_grobner::mk_monomial_in_row(rational coeff, lpvar j, ci_dependency * & dep) { NOT_IMPLEMENTED_YET(); + return nullptr; + /* + ptr_buffer vars; + rational r; + + if (c().is_monic_var(j)) { + coeff *= get_monomial_coeff(m); + m = get_monomial_body(m); + if (m_util.is_mul(m)) { + SASSERT(is_pure_monomial(m)); + for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) { + expr * arg = to_app(m)->get_arg(i); + process_var(arg); + } + } + else { + process_var(m); + } + } + else { + process_var(m); + } + if (!coeff.is_zero()) + return gb.mk_monomial(coeff, vars.size(), vars.c_ptr()); + else + return nullptr; + */ +} + + +void nla_grobner::add_row(unsigned i) { + NOT_IMPLEMENTED_YET(); + /* + const auto& row = c().m_lar_solver.A_r().m_rows[i]; + TRACE("non_linear", tout << "adding row to gb\n"; c().m_lar_solver.print_row(row, tout);); + nex * row_nex; + v_dependency * dep = nullptr; + m_tmp_var_set.reset(); + for (const auto & p : row) { + rational coeff = p.coeff(); + lpvar j = p.var(); + // TRACE("non_linear", tout << "monomial: " << mk_pp(m, get_manager()) << "\n";); + nex * new_m = mk_monomial(coeff, j, dep, m_tmp_var_set); + TRACE("non_linear", tout << "new monomial:\n"; if (new_m) gb.display_monomial(tout, *new_m); else tout << "null"; tout << "\n";); + if (new_m) + monomials.push_back(new_m); + } + assert_eq_0(monomials, dep);*/ } void nla_grobner::add_monomial_def(lpvar) { NOT_IMPLEMENTED_YET(); @@ -151,7 +224,7 @@ void nla_grobner::add_monomial_def(lpvar) { void nla_grobner::init() { find_nl_cluster(); for (unsigned i : m_rows) { - add_row_to_gb(i); + add_row(i); } for (lpvar j : m_active_vars) { add_monomial_def(j); @@ -178,7 +251,7 @@ bool nla_grobner:: is_better_choice(equation * eq1, equation * eq2) { } void nla_grobner::del_equation(equation * eq) { - SASSERT(false); + NOT_IMPLEMENTED_YET(); /* m_processed.erase(eq); m_to_process.erase(eq); @@ -377,4 +450,9 @@ void nla_grobner::display(std::ostream & out) const { NOT_IMPLEMENTED_YET(); } +void nla_grobner::assert_eq_0(ptr_buffer &, v_dependency * dep) { + NOT_IMPLEMENTED_YET(); +} + + } // end of nla namespace diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index 93f7aa591..8f5050ba3 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -21,6 +21,7 @@ #include "math/lp/nla_common.h" #include "math/lp/nex.h" +#include "math/lp/nex_creator.h" #include "util/dependency.h" namespace nla { @@ -35,21 +36,6 @@ struct grobner_stats { grobner_stats() { reset(); } }; -struct monomial { - rational m_coeff; - svector m_vars; //!< sorted variables - - friend class grobner; - friend struct monomial_lt; - - monomial() {} -public: - rational const & get_coeff() const { return m_coeff; } - unsigned get_degree() const { return m_vars.size(); } - unsigned get_size() const { return get_degree(); } - lpvar get_var(unsigned idx) const { return m_vars[idx]; } -}; - enum class var_weight { FIXED = 0, QUOTED_FIXED = 1, @@ -64,6 +50,21 @@ enum class var_weight { class nla_grobner : common { + struct monomial { + rational m_coeff; + svector m_vars; //!< sorted variables + + friend class grobner; + friend struct monomial_lt; + + monomial() {} + public: + rational const & get_coeff() const { return m_coeff; } + unsigned get_degree() const { return m_vars.size(); } + unsigned get_size() const { return get_degree(); } + lpvar get_var(unsigned idx) const { return m_vars[idx]; } + }; + class equation { unsigned m_scope_lvl; //!< scope level when this equation was created. unsigned m_bidx:31; //!< position at m_equations_to_delete @@ -95,6 +96,12 @@ class nla_grobner : common { 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; public: nla_grobner(core *core); void grobner_lemmas(); @@ -137,7 +144,17 @@ private: void get_equations(ptr_vector& eqs); bool try_to_modify_eqs(ptr_vector& eqs, unsigned& next_weight); bool internalize_gb_eq(equation*); - void add_row_to_gb(unsigned); + void add_row(unsigned); void add_monomial_def(lpvar); + void assert_eq_0(ptr_buffer &, v_dependency * dep); + void process_var(nex_mul*, lpvar j, ci_dependency *& dep, rational&); + + nex* mk_monomial_in_row(rational, lpvar, ci_dependency*&); + rational get_monomial_coeff(const nex_mul* m) { + const nex* a = m->children()[0]; + if (a->is_scalar()) + return static_cast(a)->value(); + return rational(1); + } }; // end of grobner } diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index 74c351ac6..d0c7f8a82 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -130,11 +130,11 @@ bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i) { return true; } -intervals::ci_dependency *intervals::mk_dep(lp::constraint_index ci) const { +common::ci_dependency *intervals::mk_dep(lp::constraint_index ci) const { return m_dep_manager.mk_leaf(ci); } -intervals::ci_dependency *intervals::mk_dep(const lp::explanation& expl) const { +common::ci_dependency *intervals::mk_dep(const lp::explanation& expl) const { intervals::ci_dependency * r = nullptr; for (auto p : expl) { if (r == nullptr) { diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index 2b9e5bf40..fe2702c4b 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -29,25 +29,6 @@ namespace nla { class core; class intervals : common { - class ci_value_manager { - public: - void inc_ref(lp::constraint_index const & v) { - } - - void dec_ref(lp::constraint_index const & v) { - } - }; - - struct ci_dependency_config { - typedef ci_value_manager value_manager; - typedef region allocator; - static const bool ref_count = false; - typedef lp::constraint_index value; - }; - - typedef dependency_manager ci_dependency_manager; - - typedef ci_dependency_manager::dependency ci_dependency; class im_config { unsynch_mpq_manager& m_manager; @@ -139,7 +120,7 @@ class intervals : common { ci_value_manager m_val_manager; mutable unsynch_mpq_manager m_num_manager; mutable ci_dependency_manager m_dep_manager; - im_config m_config; + im_config m_config; mutable interval_manager m_imanager; public: