mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

review of NB

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-11 16:02:05 -10:00
parent 0db79b1c79
commit d0f682b239
7 changed files with 223 additions and 259 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/math/lp/cross_nested.h
View file

@ -59,7 +59,7 @@ public:
void run(nex *e) { void run(nex *e) {
TRACE("nla_cn", tout << *e << "\n";); TRACE("nla_cn", tout << *e << "\n";);
SASSERT(m_nex_creator.is_simplified(e)); SASSERT(m_nex_creator.is_simplified(*e));
m_e = e; m_e = e;
#ifdef Z3DEBUG #ifdef Z3DEBUG
m_e_clone = m_nex_creator.clone(m_e); m_e_clone = m_nex_creator.clone(m_e);
@ -126,7 +126,7 @@ public:
} }
TRACE("nla_cn", tout << "common factor f=" << *f << "\n";); TRACE("nla_cn", tout << "common factor f=" << *f << "\n";);
nex* c_over_f = m_nex_creator.mk_div(*c, f); nex* c_over_f = m_nex_creator.mk_div(**c, *f);
c_over_f = m_nex_creator.simplify(c_over_f); c_over_f = m_nex_creator.simplify(c_over_f);
TRACE("nla_cn", tout << "c_over_f = " << *c_over_f << std::endl;); TRACE("nla_cn", tout << "c_over_f = " << *c_over_f << std::endl;);
nex_mul* cm; nex_mul* cm;
@ -376,13 +376,13 @@ public:
// all factors of j go to a, the rest to b // all factors of j go to a, the rest to b
void pre_split(nex_sum * e, lpvar j, nex_sum*& a, nex*& b) { void pre_split(nex_sum * e, lpvar j, nex_sum*& a, nex*& b) {
TRACE("nla_cn_details", tout << "e = " << * e << ", j = " << m_nex_creator.ch(j) << std::endl;); TRACE("nla_cn_details", tout << "e = " << * e << ", j = " << m_nex_creator.ch(j) << std::endl;);
SASSERT(m_nex_creator.is_simplified(e)); SASSERT(m_nex_creator.is_simplified(*e));
a = m_nex_creator.mk_sum(); a = m_nex_creator.mk_sum();
m_b_split_vec.clear(); m_b_split_vec.clear();
for (nex * ce: *e) { for (nex * ce: *e) {
TRACE("nla_cn_details", tout << "ce = " << *ce << "\n";); TRACE("nla_cn_details", tout << "ce = " << *ce << "\n";);
if (is_divisible_by_var(ce, j)) { if (is_divisible_by_var(ce, j)) {
a->add_child(m_nex_creator.mk_div(ce , j)); a->add_child(m_nex_creator.mk_div(*ce , j));
} else { } else {
m_b_split_vec.push_back(ce); m_b_split_vec.push_back(ce);
} }

35
src/math/lp/nex.h
View file

@ -122,13 +122,10 @@ public:
expr_type type() const { return expr_type::VAR; } expr_type type() const { return expr_type::VAR; }
lpvar var() const { return m_j; } lpvar var() const { return m_j; }
lpvar& var() { return m_j; } // the setter lpvar& var() { return m_j; } // the setter
std::ostream & print(std::ostream& out) const { std::ostream & print(std::ostream& out) const override { return out << "v" << m_j; }
// out << (char)('a' + m_j);
return out << "v" << m_j;
}
bool contains(lpvar j) const { return j == m_j; } bool contains(lpvar j) const { return j == m_j; }
int get_degree() const { return 1; } int get_degree() const override { return 1; }
bool is_linear() const override { return true; } bool is_linear() const override { return true; }
}; };
@ -140,10 +137,10 @@ public:
expr_type type() const { return expr_type::SCALAR; } expr_type type() const { return expr_type::SCALAR; }
const rational& value() const { return m_v; } const rational& value() const { return m_v; }
rational& value() { return m_v; } // the setter rational& value() { return m_v; } // the setter
std::ostream& print(std::ostream& out) const { return out << m_v; } std::ostream& print(std::ostream& out) const override { return out << m_v; }
int get_degree() const { return 0; } int get_degree() const override { return 0; }
bool is_linear() const { return true; } bool is_linear() const override { return true; }
}; };
class nex_pow { class nex_pow {
@ -200,7 +197,7 @@ public:
unsigned number_of_child_powers() const { return m_children.size(); } unsigned number_of_child_powers() const { return m_children.size(); }
nex_mul() : m_coeff(rational(1)) {} nex_mul() : m_coeff(1) {}
const rational& coeff() const { const rational& coeff() const {
return m_coeff; return m_coeff;
@ -210,14 +207,14 @@ public:
return m_coeff; return m_coeff;
} }
unsigned size() const { return m_children.size(); } unsigned size() const override { return m_children.size(); }
expr_type type() const { return expr_type::MUL; } expr_type type() const override { return expr_type::MUL; }
vector<nex_pow>& children() { return m_children;} vector<nex_pow>& children() { return m_children;}
const vector<nex_pow>& children() const { return m_children;} const vector<nex_pow>& children() const { return m_children;}
// A monomial is 'pure' if does not have a numeric coefficient. // A monomial is 'pure' if does not have a numeric coefficient.
bool is_pure_monomial() const { return size() == 0 || (!m_children[0].e()->is_scalar()); } bool is_pure_monomial() const { return size() == 0 || (!m_children[0].e()->is_scalar()); }
std::ostream & print(std::ostream& out) const { std::ostream & print(std::ostream& out) const override {
bool first = true; bool first = true;
if (!m_coeff.is_one()) { if (!m_coeff.is_one()) {
out << m_coeff; out << m_coeff;
@ -289,11 +286,11 @@ public:
TRACE("nla_cn_details", tout << "powers of " << *this << "\n"; print_vector(r, tout)<< "\n";); TRACE("nla_cn_details", tout << "powers of " << *this << "\n"; print_vector(r, tout)<< "\n";);
} }
int get_degree() const { int get_degree() const override {
return get_degree_children(children()); return get_degree_children(children());
} }
bool is_linear() const { bool is_linear() const override {
return get_degree() < 2; // todo: make it more efficient return get_degree() < 2; // todo: make it more efficient
} }
@ -315,15 +312,15 @@ class nex_sum : public nex {
ptr_vector<nex> m_children; ptr_vector<nex> m_children;
public: public:
nex_sum() {} nex_sum() {}
expr_type type() const { return expr_type::SUM; } expr_type type() const override { return expr_type::SUM; }
ptr_vector<nex>& children() { return m_children;} ptr_vector<nex>& children() { return m_children;}
const ptr_vector<nex>& children() const { return m_children;} const ptr_vector<nex>& children() const { return m_children;}
const ptr_vector<nex>* children_ptr() const { return &m_children;} const ptr_vector<nex>* children_ptr() const { return &m_children;}
ptr_vector<nex>* children_ptr() { return &m_children;} ptr_vector<nex>* children_ptr() { return &m_children;}
unsigned size() const { return m_children.size(); } unsigned size() const override { return m_children.size(); }
bool is_linear() const { bool is_linear() const override {
TRACE("nex_details", tout << *this << "\n";); TRACE("nex_details", tout << *this << "\n";);
for (auto e : *this) { for (auto e : *this) {
if (!e->is_linear()) if (!e->is_linear())
@ -347,7 +344,7 @@ public:
return number_of_non_scalars > 1; return number_of_non_scalars > 1;
} }
std::ostream & print(std::ostream& out) const { std::ostream & print(std::ostream& out) const override {
bool first = true; bool first = true;
for (const nex* v : m_children) { for (const nex* v : m_children) {
std::string s = v->str(); std::string s = v->str();
@ -372,7 +369,7 @@ public:
return out; return out;
} }
int get_degree() const { int get_degree() const override {
int degree = 0; int degree = 0;
for (auto e : *this) { for (auto e : *this) {
degree = std::max(degree, e->get_degree()); degree = std::max(degree, e->get_degree());

230
src/math/lp/nex_creator.cpp
View file

@ -21,30 +21,28 @@
#include "math/lp/nex_creator.h" #include "math/lp/nex_creator.h"
#include <map> #include <map>
namespace nla { using namespace nla;
nex * nex_creator::mk_div(const nex* a, lpvar j) { // divides by variable j. A precondition is that a is a multiple of j.
nex * nex_creator::mk_div(const nex& a, lpvar j) {
SASSERT(is_simplified(a)); SASSERT(is_simplified(a));
SASSERT((a->is_mul() && a->contains(j)) || (a->is_var() && to_var(a)->var() == j)); SASSERT(a.contains(j));
if (a->is_var()) SASSERT(a.is_mul() || (a.is_var() && a.to_var().var() == j));
if (a.is_var())
return mk_scalar(rational(1)); return mk_scalar(rational(1));
vector<nex_pow> bv; vector<nex_pow> bv;
bool seenj = false; bool seenj = false;
auto ma = *to_mul(a); auto ma = a.to_mul();
for (auto& p : ma) { for (auto& p : ma) {
const nex * c = p.e(); const nex * c = p.e();
int pow = p.pow(); int pow = p.pow();
if (!seenj && c->contains(j)) { if (!seenj && c->contains(j)) {
if (!c->is_var()) { SASSERT(!c->is_var() || c->to_var().var() == j);
bv.push_back(nex_pow(mk_div(c, j))); if (!c->is_var()) {
if (pow != 1) { bv.push_back(nex_pow(mk_div(*c, j)));
bv.push_back(nex_pow(clone(c), pow - 1)); }
} if (pow != 1) {
} else { bv.push_back(nex_pow(clone(c), pow - 1));
SASSERT(to_var(c)->var() == j);
if (p.pow() != 1) {
bv.push_back(nex_pow(mk_var(j), pow - 1));
}
} }
seenj = true; seenj = true;
} else { } else {
@ -64,9 +62,10 @@ nex * nex_creator::mk_div(const nex* a, lpvar j) {
} }
// TBD: describe what this does
bool nex_creator::eat_scalar_pow(rational& r, const nex_pow& p, unsigned pow) { bool nex_creator::eat_scalar_pow(rational& r, const nex_pow& p, unsigned pow) {
if (p.e()->is_mul()) { if (p.e()->is_mul()) {
const nex_mul & m = *to_mul(p.e()); const nex_mul & m = p.e()->to_mul();
if (m.size() == 0) { if (m.size() == 0) {
const rational& coeff = m.coeff(); const rational& coeff = m.coeff();
if (coeff.is_one()) if (coeff.is_one())
@ -78,10 +77,10 @@ bool nex_creator::eat_scalar_pow(rational& r, const nex_pow& p, unsigned pow) {
} }
if (!p.e()->is_scalar()) if (!p.e()->is_scalar())
return false; return false;
const nex_scalar *pe = to_scalar(p.e()); const nex_scalar &pe = p.e()->to_scalar();
if (pe->value().is_one()) if (pe.value().is_one())
return true; // r does not change here return true; // r does not change here
r *= pe->value().expt(p.pow() * pow); r *= pe.value().expt(p.pow() * pow);
return true; return true;
} }
@ -89,22 +88,16 @@ bool nex_creator::eat_scalar_pow(rational& r, const nex_pow& p, unsigned pow) {
void nex_creator::simplify_children_of_mul(vector<nex_pow> & children, rational& coeff) { void nex_creator::simplify_children_of_mul(vector<nex_pow> & children, rational& coeff) {
TRACE("grobner_d", print_vector(children, tout);); TRACE("grobner_d", print_vector(children, tout););
vector<nex_pow> to_promote; vector<nex_pow> to_promote;
bool skipped = false;
unsigned j = 0; unsigned j = 0;
for (nex_pow& p : children) { for (nex_pow& p : children) {
if (eat_scalar_pow(coeff, p, 1)) { if (eat_scalar_pow(coeff, p, 1)) {
skipped = true;
continue; continue;
} }
p.e() = simplify(p.e()); p.e() = simplify(p.e());
if ((p.e())->is_mul()) { if (p.e()->is_mul()) {
skipped = true;
to_promote.push_back(p); to_promote.push_back(p);
} else { } else {
if (skipped) children[j++] = p;
children[j] = p;
j++;
} }
} }
@ -112,13 +105,13 @@ void nex_creator::simplify_children_of_mul(vector<nex_pow> & children, rational&
for (nex_pow & p : to_promote) { for (nex_pow & p : to_promote) {
TRACE("grobner_d", tout << p << "\n";); TRACE("grobner_d", tout << p << "\n";);
nex_mul *pm = to_mul(p.e()); nex_mul &pm = p.e()->to_mul();
for (nex_pow& pp : *pm) { for (nex_pow& pp : pm) {
TRACE("grobner_d", tout << pp << "\n";); TRACE("grobner_d", tout << pp << "\n";);
if (!eat_scalar_pow(coeff, pp, p.pow())) if (!eat_scalar_pow(coeff, pp, p.pow()))
children.push_back(nex_pow(pp.e(), pp.pow() * p.pow())); children.push_back(nex_pow(pp.e(), pp.pow() * p.pow()));
} }
coeff *= pm->coeff().expt(p.pow()); coeff *= pm.coeff().expt(p.pow());
} }
mul_to_powers(children); mul_to_powers(children);
@ -159,29 +152,28 @@ bool nex_creator::gt_on_powers_mul_same_degree(const T& a, const nex_mul& b) con
if (it_b != b.end()) b_pow = it_b->pow(); if (it_b != b.end()) b_pow = it_b->pow();
} }
} }
TRACE("nex_less", tout << "a = "; print_vector(a, tout) << (ret?" > ":" <= ") << b << "\n";); TRACE("nex_gt", tout << "a = "; print_vector(a, tout) << (ret?" > ":" <= ") << b << "\n";);
return ret; return ret;
} }
bool nex_creator::children_are_simplified(const vector<nex_pow>& children) const { bool nex_creator::children_are_simplified(const vector<nex_pow>& children) const {
for (auto c : children) for (auto c : children)
if (!is_simplified(c.e()) || c.pow() == 0) if (!is_simplified(*c.e()) || c.pow() == 0)
return false; return false;
return true; return true;
} }
bool nex_creator::gt_on_powers_mul(const vector<nex_pow>& children, const nex_mul& b) const { bool nex_creator::gt_on_powers_mul(const vector<nex_pow>& children, const nex_mul& b) const {
TRACE("nex_less", tout << "children = "; print_vector(children, tout) << " , b = " << b << "\n";); TRACE("nex_gt", tout << "children = "; print_vector(children, tout) << " , b = " << b << "\n";);
SASSERT(children_are_simplified(children) && is_simplified(&b)); SASSERT(children_are_simplified(children) && is_simplified(b));
unsigned a_deg = get_degree_children(children); unsigned a_deg = get_degree_children(children);
unsigned b_deg = b.get_degree(); unsigned b_deg = b.get_degree();
return a_deg == b_deg ? gt_on_powers_mul_same_degree(children, b) : a_deg > b_deg; return a_deg == b_deg ? gt_on_powers_mul_same_degree(children, b) : a_deg > b_deg;
} }
bool nex_creator::gt_on_mul_mul(const nex_mul& a, const nex_mul& b) const { bool nex_creator::gt_on_mul_mul(const nex_mul& a, const nex_mul& b) const {
TRACE("grobner_d", tout << "a = " << a << " , b = " << b << "\n";); TRACE("grobner_d", tout << "a = " << a << " , b = " << b << "\n";);
SASSERT(is_simplified(&a) && is_simplified(&b)); SASSERT(is_simplified(a) && is_simplified(b));
unsigned a_deg = a.get_degree(); unsigned a_deg = a.get_degree();
unsigned b_deg = b.get_degree(); unsigned b_deg = b.get_degree();
return a_deg == b_deg ? gt_on_powers_mul_same_degree(a, b) : a_deg > b_deg; return a_deg == b_deg ? gt_on_powers_mul_same_degree(a, b) : a_deg > b_deg;
@ -208,15 +200,12 @@ bool nex_creator::gt_nex_powers(const vector<nex_pow>& children, const nex* b) c
switch (b->type()) { switch (b->type()) {
case expr_type::SCALAR: case expr_type::SCALAR:
return false; return false;
case expr_type::VAR: { case expr_type::VAR:
if (get_degree_children(children) > 1) if (get_degree_children(children) > 1)
return true; return true;
const nex_pow & c = children[0]; SASSERT(children[0].pow() == 1);
SASSERT(c.pow() == 1); SASSERT(!children[0].e()->is_scalar());
const nex * f = c.e(); return gt(children[0].e(), b);
SASSERT(!f->is_scalar());
return gt(f, b);
}
case expr_type::MUL: case expr_type::MUL:
return gt_on_powers_mul(children, *to_mul(b)); return gt_on_powers_mul(children, *to_mul(b));
case expr_type::SUM: case expr_type::SUM:
@ -231,15 +220,12 @@ bool nex_creator::gt_on_mul_nex(const nex_mul* a, const nex* b) const {
switch (b->type()) { switch (b->type()) {
case expr_type::SCALAR: case expr_type::SCALAR:
return false; return false;
case expr_type::VAR: { case expr_type::VAR:
if (a->get_degree() > 1) if (a->get_degree() > 1)
return true; return true;
const nex_pow & c = *a->begin(); SASSERT(a->begin()->pow() == 1);
SASSERT(c.pow() == 1); SASSERT(!a->begin()->e()->is_scalar());
const nex * f = c.e(); return gt(a->begin()->e(), b);
SASSERT(!f->is_scalar());
return gt(f, b);
}
case expr_type::MUL: case expr_type::MUL:
return gt_on_mul_mul(*a, *to_mul(b)); return gt_on_mul_mul(*a, *to_mul(b));
case expr_type::SUM: case expr_type::SUM:
@ -258,8 +244,7 @@ bool nex_creator::gt_on_sum_sum(const nex_sum* a, const nex_sum* b) const {
if (gt((*b)[j], (*a)[j])) if (gt((*b)[j], (*a)[j]))
return false; return false;
} }
return size > b->size(); return a->size() > size;
} }
// the only difference with gt() that it disregards the coefficient in nex_mul // the only difference with gt() that it disregards the coefficient in nex_mul
@ -321,11 +306,11 @@ bool nex_creator::gt(const nex* a, const nex* b) const {
return ret; return ret;
} }
bool nex_creator::is_sorted(const nex_mul* e) const { bool nex_creator::is_sorted(const nex_mul& e) const {
for (unsigned j = 0; j < e->size() - 1; j++) { for (unsigned j = 0; j < e.size() - 1; j++) {
if (!(gt_on_nex_pow((*e)[j], (*e)[j+1]))) { if (!(gt_on_nex_pow(e[j], e[j+1]))) {
TRACE("grobner_d", tout << "not sorted e " << * e << "\norder is incorrect " << TRACE("grobner_d", tout << "not sorted e " << e << "\norder is incorrect " <<
(*e)[j] << " >= " << (*e)[j + 1]<< "\n";); e[j] << " >= " << e[j + 1]<< "\n";);
return false; return false;
} }
@ -333,18 +318,18 @@ bool nex_creator::is_sorted(const nex_mul* e) const {
return true; return true;
} }
bool nex_creator::mul_is_simplified(const nex_mul* e) const { bool nex_creator::mul_is_simplified(const nex_mul& e) const {
TRACE("nla_cn_", tout << "e = " << *e << "\n";); TRACE("nla_cn_", tout << "e = " << e << "\n";);
if (e->size() == 0) { if (e.size() == 0) {
TRACE("nla_cn", ); TRACE("nla_cn", );
return false; // it has to be a scalar return false; // it has to be a scalar
} }
if (e->size() == 1 && e->begin()->pow() == 1 && e->coeff().is_one()) { if (e.size() == 1 && e.begin()->pow() == 1 && e.coeff().is_one()) {
TRACE("nla_cn", ); TRACE("nla_cn", );
return false; return false;
} }
std::set<const nex*, nex_lt> s([this](const nex* a, const nex* b) {return gt(a, b); }); std::set<const nex*, nex_lt> s([this](const nex* a, const nex* b) {return gt(a, b); });
for (const auto &p : *e) { for (const auto &p : e) {
const nex* ee = p.e(); const nex* ee = p.e();
if (p.pow() == 0) { if (p.pow() == 0) {
TRACE("nla_cn", tout << "not simplified " << *ee << "\n";); TRACE("nla_cn", tout << "not simplified " << *ee << "\n";);
@ -380,7 +365,7 @@ nex * nex_creator::simplify_mul(nex_mul *e) {
if (e->size() == 0 || e->coeff().is_zero()) if (e->size() == 0 || e->coeff().is_zero())
return mk_scalar(e->coeff()); return mk_scalar(e->coeff());
TRACE("grobner_d", tout << *e << "\n";); TRACE("grobner_d", tout << *e << "\n";);
SASSERT(is_simplified(e)); SASSERT(is_simplified(*e));
return e; return e;
} }
@ -399,19 +384,19 @@ nex* nex_creator::simplify_sum(nex_sum *e) {
return r; return r;
} }
bool nex_creator::sum_is_simplified(const nex_sum* e) const { bool nex_creator::sum_is_simplified(const nex_sum& e) const {
if (e->size() < 2) return false; if (e.size() < 2) return false;
bool scalar = false; bool scalar = false;
for (nex * ee : *e) { for (nex * ee : e) {
TRACE("nla_cn_details", tout << "ee = " << *ee << "\n";); TRACE("nla_cn_details", tout << "ee = " << *ee << "\n";);
if (ee->is_sum()) { if (ee->is_sum()) {
TRACE("nla_cn", tout << "not simplified e = " << *e << "\n" TRACE("nla_cn", tout << "not simplified e = " << e << "\n"
<< " has a child which is a sum " << *ee << "\n";); << " has a child which is a sum " << *ee << "\n";);
return false; return false;
} }
if (ee->is_scalar()) { if (ee->is_scalar()) {
if (scalar) { if (scalar) {
TRACE("nla_cn", tout << "not simplified e = " << *e << "\n" TRACE("nla_cn", tout << "not simplified e = " << e << "\n"
<< " have more than one scalar " << *ee << "\n";); << " have more than one scalar " << *ee << "\n";);
return false; return false;
@ -425,7 +410,7 @@ bool nex_creator::sum_is_simplified(const nex_sum* e) const {
scalar = true; scalar = true;
} }
} }
if (!is_simplified(ee)) if (!is_simplified(*ee))
return false; return false;
} }
return true; return true;
@ -457,7 +442,7 @@ nex* nex_creator::create_child_from_nex_and_coeff(nex *e,
TRACE("grobner_d", tout << *e << ", coeff = " << coeff << "\n";); TRACE("grobner_d", tout << *e << ", coeff = " << coeff << "\n";);
if (coeff.is_one()) if (coeff.is_one())
return e; return e;
SASSERT(is_simplified(e)); SASSERT(is_simplified(*e));
switch (e->type()) { switch (e->type()) {
case expr_type::VAR: { case expr_type::VAR: {
if (coeff.is_one()) if (coeff.is_one())
@ -538,7 +523,7 @@ void nex_creator::sort_join_sum(ptr_vector<nex> & children) {
std::map<nex*, rational, nex_lt> map([this](const nex *a , const nex *b) std::map<nex*, rational, nex_lt> map([this](const nex *a , const nex *b)
{ return gt_for_sort_join_sum(a, b); }); { return gt_for_sort_join_sum(a, b); });
std::unordered_set<nex*> allocated_nexs; // handling (nex*) as numbers std::unordered_set<nex*> allocated_nexs; // handling (nex*) as numbers
nex_scalar * common_scalar; nex_scalar * common_scalar = nullptr;
fill_join_map_for_sum(children, map, allocated_nexs, common_scalar); fill_join_map_for_sum(children, map, allocated_nexs, common_scalar);
TRACE("grobner_d", for (auto & p : map ) { tout << "(" << *p.first << ", " << p.second << ") ";}); TRACE("grobner_d", for (auto & p : map ) { tout << "(" << *p.first << ", " << p.second << ") ";});
@ -551,32 +536,24 @@ void nex_creator::sort_join_sum(ptr_vector<nex> & children) {
} }
TRACE("grobner_d", TRACE("grobner_d",
tout << "map="; tout << "map=";
for (auto & p : map ) for (auto & p : map ) tout << "(" << *p.first << ", " << p.second << ") ";
{ tout << "(" << *p.first << ", " << p.second << ") "; }
tout << "\nchildren="; print_vector_of_ptrs(children, tout) << "\n";); tout << "\nchildren="; print_vector_of_ptrs(children, tout) << "\n";);
} }
void nex_creator::simplify_children_of_sum(ptr_vector<nex> & children) { void nex_creator::simplify_children_of_sum(ptr_vector<nex> & children) {
TRACE("grobner_d", print_vector_of_ptrs(children, tout);); TRACE("grobner_d", print_vector_of_ptrs(children, tout););
ptr_vector<nex> to_promote; ptr_vector<nex> to_promote;
bool skipped = false;
unsigned k = 0; unsigned k = 0;
for (unsigned j = 0; j < children.size(); j++) { for (unsigned j = 0; j < children.size(); j++) {
nex* e = children[j] = simplify(children[j]); nex* e = children[j] = simplify(children[j]);
if (e->is_sum()) { if (e->is_sum()) {
skipped = true;
to_promote.push_back(e); to_promote.push_back(e);
} else if (is_zero_scalar(e)) { } else if (is_zero_scalar(e)) {
skipped = true;
continue; continue;
} else if (e->is_mul() && to_mul(e)->coeff().is_zero() ) { } else if (e->is_mul() && to_mul(e)->coeff().is_zero() ) {
skipped = true;
continue; continue;
}else { } else {
if (skipped) { children[k++] = e;
children[k] = e;
}
k++;
} }
} }
@ -584,7 +561,7 @@ void nex_creator::simplify_children_of_sum(ptr_vector<nex> & children) {
children.shrink(k); children.shrink(k);
for (nex *e : to_promote) { for (nex *e : to_promote) {
for (nex *ee : *(to_sum(e)->children_ptr())) { for (nex *ee : *(e->to_sum().children_ptr())) {
if (!is_zero_scalar(ee)) if (!is_zero_scalar(ee))
children.push_back(ee); children.push_back(ee);
} }
@ -594,11 +571,10 @@ void nex_creator::simplify_children_of_sum(ptr_vector<nex> & children) {
} }
bool have_no_scalars(const nex_mul* a) { static bool have_no_scalars(const nex_mul& a) {
for (auto & p : *a) for (auto & p : a)
if (p.e()->is_scalar() && !to_scalar(p.e())->value().is_one()) if (p.e()->is_scalar() && !to_scalar(p.e())->value().is_one())
return false; return false;
return true; return true;
} }
@ -606,24 +582,23 @@ bool nex_mul::all_factors_are_elementary() const {
for (auto & p : *this) for (auto & p : *this)
if (!p.e()->is_elementary()) if (!p.e()->is_elementary())
return false; return false;
return true; return true;
} }
nex * nex_creator::mk_div_sum_by_mul(const nex_sum* m, const nex_mul* b) { nex * nex_creator::mk_div_sum_by_mul(const nex_sum& m, const nex_mul& b) {
nex_sum * r = mk_sum(); nex_sum * r = mk_sum();
for (auto e : *m) { for (auto e : m) {
r->add_child(mk_div_by_mul(e, b)); r->add_child(mk_div_by_mul(*e, b));
} }
TRACE("grobner_d", tout << *r << "\n";); TRACE("grobner_d", tout << *r << "\n";);
return r; return r;
} }
nex * nex_creator::mk_div_mul_by_mul(const nex_mul *a, const nex_mul* b) { nex * nex_creator::mk_div_mul_by_mul(const nex_mul& a, const nex_mul& b) {
SASSERT(a->all_factors_are_elementary() && b->all_factors_are_elementary()); SASSERT(a.all_factors_are_elementary() && b.all_factors_are_elementary());
b->get_powers_from_mul(m_powers); b.get_powers_from_mul(m_powers);
nex_mul* ret = new nex_mul(); nex_mul* ret = new nex_mul();
for (auto& p_from_a : *a) { for (auto& p_from_a : a) {
TRACE("grobner_d", tout << "p_from_a = " << p_from_a << "\n";); TRACE("grobner_d", tout << "p_from_a = " << p_from_a << "\n";);
const nex* e = p_from_a.e(); const nex* e = p_from_a.e();
if (e->is_scalar()) { if (e->is_scalar()) {
@ -658,46 +633,45 @@ nex * nex_creator::mk_div_mul_by_mul(const nex_mul *a, const nex_mul* b) {
if (ret->size() == 0) { if (ret->size() == 0) {
delete ret; delete ret;
TRACE("grobner_d", tout << "return scalar\n";); TRACE("grobner_d", tout << "return scalar\n";);
return mk_scalar(a->coeff() / b->coeff()); return mk_scalar(a.coeff() / b.coeff());
} }
ret->coeff() = a->coeff() / b->coeff(); ret->coeff() = a.coeff() / b.coeff();
add_to_allocated(ret); add_to_allocated(ret);
TRACE("grobner_d", tout << *ret << "\n";); TRACE("grobner_d", tout << *ret << "\n";);
return ret; return ret;
} }
nex * nex_creator::mk_div_by_mul(const nex* a, const nex_mul* b) { nex * nex_creator::mk_div_by_mul(const nex& a, const nex_mul& b) {
SASSERT(have_no_scalars(b)); SASSERT(have_no_scalars(b));
if (a->is_sum()) { SASSERT(!a.is_var() || (b.get_degree() == 1 && get_vars_of_expr(&a) == get_vars_of_expr(&b) && b.coeff().is_one()));
return mk_div_sum_by_mul(to_sum(a), b); if (a.is_sum()) {
} return mk_div_sum_by_mul(a.to_sum(), b);
}
if (a->is_var()) { if (a.is_var()) {
SASSERT(b->get_degree() == 1 && get_vars_of_expr(a) == get_vars_of_expr(b) && b->coeff().is_one());
return mk_scalar(rational(1)); return mk_scalar(rational(1));
} }
return mk_div_mul_by_mul(to_mul(a), b); return mk_div_mul_by_mul(a.to_mul(), b);
} }
nex * nex_creator::mk_div(const nex* a, const nex* b) { nex * nex_creator::mk_div(const nex& a, const nex& b) {
TRACE("grobner_d", tout << *a <<" / " << *b << "\n";); TRACE("grobner_d", tout << a <<" / " << b << "\n";);
if (b->is_var()) { if (b.is_var()) {
return mk_div(a, to_var(b)->var()); return mk_div(a, b.to_var().var());
} }
return mk_div_by_mul(a, to_mul(b)); return mk_div_by_mul(a, b.to_mul());
} }
nex* nex_creator::simplify(nex* e) { nex* nex_creator::simplify(nex* e) {
nex* es; nex* es;
TRACE("grobner_d", tout << *e << std::endl;); TRACE("grobner_d", tout << *e << std::endl;);
if (e->is_mul()) if (e->is_mul())
es = simplify_mul(to_mul(e)); es = simplify_mul(to_mul(e));
else if (e->is_sum()) else if (e->is_sum())
es = simplify_sum(to_sum(e)); es = simplify_sum(to_sum(e));
else else
es = e; es = e;
TRACE("grobner_d", tout << "simplified = " << *es << std::endl;); TRACE("grobner_d", tout << "simplified = " << *es << std::endl;);
SASSERT(is_simplified(es)); SASSERT(is_simplified(*es));
return es; return es;
} }
@ -713,7 +687,7 @@ void nex_creator::process_map_pair(nex *e, const rational& coeff, ptr_vector<nex
m_allocated.push_back(e); m_allocated.push_back(e);
} }
if (e->is_mul()) { if (e->is_mul()) {
to_mul(e)->coeff() = coeff; e->to_mul().coeff() = coeff;
children.push_back(simplify(e)); children.push_back(simplify(e));
} else { } else {
SASSERT(e->is_var()); SASSERT(e->is_var());
@ -725,13 +699,12 @@ void nex_creator::process_map_pair(nex *e, const rational& coeff, ptr_vector<nex
} }
} }
bool nex_creator::is_simplified(const nex *e) const bool nex_creator::is_simplified(const nex& e) const {
{ TRACE("nla_cn_details", tout << "e = " << e << "\n";);
TRACE("nla_cn_details", tout << "e = " << *e << "\n";); if (e.is_mul())
if (e->is_mul()) return mul_is_simplified(e.to_mul());
return mul_is_simplified(to_mul(e)); if (e.is_sum())
if (e->is_sum()) return sum_is_simplified(e.to_sum());
return sum_is_simplified(to_sum(e));
return true; return true;
} }
@ -752,10 +725,10 @@ nex* nex_creator::canonize_mul(nex_mul *a) {
nex_pow& np = (*a)[j]; nex_pow& np = (*a)[j];
SASSERT(np.pow()); SASSERT(np.pow());
unsigned power = np.pow(); unsigned power = np.pow();
nex_sum * s = to_sum(np.e()); // s is going to explode nex_sum const& s = np.e()->to_sum(); // s is going to explode
nex_sum * r = mk_sum(); nex_sum * r = mk_sum();
nex *sclone = power > 1? clone(s) : nullptr; nex *sclone = power > 1 ? clone(&s) : nullptr;
for (nex *e : *s) { for (nex *e : s) {
nex_mul *m = mk_mul(); nex_mul *m = mk_mul();
if (power > 1) if (power > 1)
m->add_child_in_power(sclone, power - 1); m->add_child_in_power(sclone, power - 1);
@ -777,11 +750,11 @@ nex* nex_creator::canonize(const nex *a) {
nex *t = simplify(clone(a)); nex *t = simplify(clone(a));
if (t->is_sum()) { if (t->is_sum()) {
nex_sum * s = to_sum(t); nex_sum & s = t->to_sum();
for (unsigned j = 0; j < s->size(); j++) { for (unsigned j = 0; j < s.size(); j++) {
(*s)[j] = canonize((*s)[j]); s[j] = canonize(s[j]);
} }
t = simplify(s); t = simplify(&s);
TRACE("grobner_d", tout << *t << "\n";); TRACE("grobner_d", tout << *t << "\n";);
return t; return t;
} }
@ -810,4 +783,3 @@ bool nex_creator::equal(const nex* a, const nex* b) {
} }
#endif #endif
}

19
src/math/lp/nex_creator.h
View file

@ -19,6 +19,7 @@
--*/ --*/
#pragma once #pragma once
#include <map> #include <map>
#include "util/map.h"
#include "math/lp/nex.h" #include "math/lp/nex.h"
namespace nla { namespace nla {
@ -209,20 +210,20 @@ public:
return r; return r;
} }
nex * mk_div(const nex* a, lpvar j); nex * mk_div(const nex& a, lpvar j);
nex * mk_div(const nex* a, const nex* b); nex * mk_div(const nex& a, const nex& b);
nex * mk_div_by_mul(const nex* a, const nex_mul* b); nex * mk_div_by_mul(const nex& a, const nex_mul& b);
nex * mk_div_sum_by_mul(const nex_sum* a, const nex_mul* b); nex * mk_div_sum_by_mul(const nex_sum& a, const nex_mul& b);
nex * mk_div_mul_by_mul(const nex_mul* a, const nex_mul* b); nex * mk_div_mul_by_mul(const nex_mul& a, const nex_mul& b);
nex * simplify_mul(nex_mul *e); nex * simplify_mul(nex_mul *e);
bool is_sorted(const nex_mul * e) const; bool is_sorted(const nex_mul & e) const;
nex* simplify_sum(nex_sum *e); nex* simplify_sum(nex_sum *e);
bool is_simplified(const nex *e) const; bool is_simplified(const nex &e) const;
bool sum_is_simplified(const nex_sum* e) const; bool sum_is_simplified(const nex_sum& e) const;
bool mul_is_simplified(const nex_mul*e ) const; bool mul_is_simplified(const nex_mul& e) const;
void mul_to_powers(vector<nex_pow>& children); void mul_to_powers(vector<nex_pow>& children);

2
src/math/lp/nla_core.h
View file

@ -90,7 +90,7 @@ public:
intervals m_intervals; intervals m_intervals;
horner m_horner; horner m_horner;
nla_settings m_nla_settings; nla_settings m_nla_settings;
nla_grobner m_grobner; grobner m_grobner;
private: private:
emonics m_emons; emonics m_emons;
svector<lpvar> m_add_buffer; svector<lpvar> m_add_buffer;

167
src/math/lp/nla_grobner.cpp
View file

@ -20,8 +20,9 @@
#include "math/lp/nla_grobner.h" #include "math/lp/nla_grobner.h"
#include "math/lp/nla_core.h" #include "math/lp/nla_core.h"
#include "math/lp/factorization_factory_imp.h" #include "math/lp/factorization_factory_imp.h"
namespace nla { using namespace nla;
nla_grobner::nla_grobner(core *c, intervals *s)
grobner::grobner(core *c, intervals *s)
: common(c, s), : common(c, s),
m_nl_gb_exhausted(false), m_nl_gb_exhausted(false),
m_dep_manager(m_val_manager, m_alloc), m_dep_manager(m_val_manager, m_alloc),
@ -29,12 +30,30 @@ nla_grobner::nla_grobner(core *c, intervals *s)
m_look_for_fixed_vars_in_rows(false) m_look_for_fixed_vars_in_rows(false)
{} {}
bool nla_grobner::internalize_gb_eq(equation* ) { void grobner::grobner_lemmas() {
c().lp_settings().stats().m_grobner_calls++;
init();
ptr_vector<equation> eqs;
unsigned next_weight =
(unsigned)(var_weight::MAX_DEFAULT_WEIGHT) + 1; // next weight using during perturbation phase.
do {
TRACE("grobner", tout << "before:\n"; display(tout););
compute_basis();
update_statistics();
TRACE("grobner", tout << "after:\n"; display(tout););
// if (find_conflict(eqs))
// return;
} while (push_calculation_forward(eqs, next_weight));
}
bool grobner::internalize_gb_eq(equation* ) {
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
return false; return false;
} }
void nla_grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::queue<lpvar> & q) { void grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::queue<lpvar> & q) {
SASSERT(!c().active_var_set_contains(j) && !c().var_is_fixed(j)); SASSERT(!c().active_var_set_contains(j) && !c().var_is_fixed(j));
TRACE("grobner", tout << "j = " << j << ", "; c().print_var(j, tout) << "\n";); TRACE("grobner", tout << "j = " << j << ", "; c().print_var(j, tout) << "\n";);
const auto& matrix = c().m_lar_solver.A_r(); const auto& matrix = c().m_lar_solver.A_r();
@ -69,7 +88,7 @@ void nla_grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std
} }
} }
void nla_grobner::find_nl_cluster() { void grobner::find_nl_cluster() {
prepare_rows_and_active_vars(); prepare_rows_and_active_vars();
std::queue<lpvar> q; std::queue<lpvar> q;
for (lpvar j : c().m_to_refine) { for (lpvar j : c().m_to_refine) {
@ -92,13 +111,13 @@ void nla_grobner::find_nl_cluster() {
TRACE("grobner", display(tout);); TRACE("grobner", display(tout););
} }
void nla_grobner::prepare_rows_and_active_vars() { void grobner::prepare_rows_and_active_vars() {
m_rows.clear(); m_rows.clear();
m_rows.resize(c().m_lar_solver.row_count()); m_rows.resize(c().m_lar_solver.row_count());
c().clear_and_resize_active_var_set(); c().clear_and_resize_active_var_set();
} }
void nla_grobner::display_matrix(std::ostream & out) const { void grobner::display_matrix(std::ostream & out) const {
const auto& matrix = c().m_lar_solver.A_r(); const auto& matrix = c().m_lar_solver.A_r();
out << m_rows.size() << " rows" <<"\n"; out << m_rows.size() << " rows" <<"\n";
out << "the matrix\n"; out << "the matrix\n";
@ -107,21 +126,21 @@ void nla_grobner::display_matrix(std::ostream & out) const {
c().print_term(r, out) << std::endl; c().print_term(r, out) << std::endl;
} }
} }
std::ostream & nla_grobner::display(std::ostream & out) const { std::ostream & grobner::display(std::ostream & out) const {
display_equations(out, m_to_superpose, "m_to_superpose:"); display_equations(out, m_to_superpose, "m_to_superpose:");
display_equations(out, m_to_simplify, "m_to_simplify:"); display_equations(out, m_to_simplify, "m_to_simplify:");
return out; return out;
} }
common::ci_dependency* nla_grobner::dep_from_vector(svector<lp::constraint_index> & cs) { common::ci_dependency* grobner::dep_from_vector(svector<lp::constraint_index> & cs) {
ci_dependency * d = nullptr; ci_dependency * d = nullptr;
for (auto c : cs) for (auto c : cs)
d = m_dep_manager.mk_join(d, m_dep_manager.mk_leaf(c)); d = m_dep_manager.mk_join(d, m_dep_manager.mk_leaf(c));
return d; return d;
} }
void nla_grobner::add_row(unsigned i) { void grobner::add_row(unsigned i) {
const auto& row = c().m_lar_solver.A_r().m_rows[i]; const auto& row = c().m_lar_solver.A_r().m_rows[i];
TRACE("grobner", tout << "adding row to gb\n"; c().m_lar_solver.print_row(row, tout) << '\n'; TRACE("grobner", tout << "adding row to gb\n"; c().m_lar_solver.print_row(row, tout) << '\n';
for (auto p : row) { for (auto p : row) {
@ -135,13 +154,13 @@ void nla_grobner::add_row(unsigned i) {
assert_eq_0(e, dep); assert_eq_0(e, dep);
} }
void nla_grobner::simplify_equations_in_m_to_simplify() { void grobner::simplify_equations_in_m_to_simplify() {
for (equation *eq : m_to_simplify) { for (equation *eq : m_to_simplify) {
eq->expr() = m_nex_creator.simplify(eq->expr()); eq->expr() = m_nex_creator.simplify(eq->expr());
} }
} }
void nla_grobner::init() { void grobner::init() {
m_reported = 0; m_reported = 0;
del_equations(0); del_equations(0);
SASSERT(m_equations_to_delete.size() == 0); SASSERT(m_equations_to_delete.size() == 0);
@ -157,13 +176,13 @@ void nla_grobner::init() {
simplify_equations_in_m_to_simplify(); simplify_equations_in_m_to_simplify();
} }
bool nla_grobner::is_trivial(equation* eq) const { bool grobner::is_trivial(equation* eq) const {
SASSERT(m_nex_creator.is_simplified(eq->expr())); SASSERT(m_nex_creator.is_simplified(*eq->expr()));
return eq->expr()->size() == 0; return eq->expr()->size() == 0;
} }
// returns true if eq1 is simpler than eq2 // returns true if eq1 is simpler than eq2
bool nla_grobner::is_simpler(equation * eq1, equation * eq2) { bool grobner::is_simpler(equation * eq1, equation * eq2) {
if (!eq2) if (!eq2)
return true; return true;
if (is_trivial(eq1)) if (is_trivial(eq1))
@ -173,7 +192,7 @@ bool nla_grobner::is_simpler(equation * eq1, equation * eq2) {
return m_nex_creator.gt(eq2->expr(), eq1->expr()); return m_nex_creator.gt(eq2->expr(), eq1->expr());
} }
void nla_grobner::del_equation(equation * eq) { void grobner::del_equation(equation * eq) {
m_to_superpose.erase(eq); m_to_superpose.erase(eq);
m_to_simplify.erase(eq); m_to_simplify.erase(eq);
SASSERT(m_equations_to_delete[eq->m_bidx] == eq); SASSERT(m_equations_to_delete[eq->m_bidx] == eq);
@ -181,7 +200,7 @@ void nla_grobner::del_equation(equation * eq) {
dealloc(eq); dealloc(eq);
} }
nla_grobner::equation* nla_grobner::pick_next() { grobner::equation* grobner::pick_next() {
equation * r = nullptr; equation * r = nullptr;
ptr_buffer<equation> to_delete; ptr_buffer<equation> to_delete;
for (equation * curr : m_to_simplify) { for (equation * curr : m_to_simplify) {
@ -200,7 +219,7 @@ nla_grobner::equation* nla_grobner::pick_next() {
return r; return r;
} }
nla_grobner::equation* nla_grobner::simplify_using_to_superpose(equation* eq) { grobner::equation* grobner::simplify_using_to_superpose(equation* eq) {
bool result = false; bool result = false;
bool simplified; bool simplified;
TRACE("grobner", tout << "simplifying: "; display_equation(tout, *eq); tout << "using equalities of m_to_superpose of size " << m_to_superpose.size() << "\n";); TRACE("grobner", tout << "simplifying: "; display_equation(tout, *eq); tout << "using equalities of m_to_superpose of size " << m_to_superpose.size() << "\n";);
@ -229,7 +248,7 @@ nla_grobner::equation* nla_grobner::simplify_using_to_superpose(equation* eq) {
return result ? eq : nullptr; return result ? eq : nullptr;
} }
const nex* nla_grobner::get_highest_monomial(const nex* e) const { const nex* grobner::get_highest_monomial(const nex* e) const {
switch (e->type()) { switch (e->type()) {
case expr_type::MUL: case expr_type::MUL:
return to_mul(e); return to_mul(e);
@ -245,7 +264,7 @@ const nex* nla_grobner::get_highest_monomial(const nex* e) const {
// source 3f + k + l = 0, so f = (-k - l)/3 // source 3f + k + l = 0, so f = (-k - l)/3
// target 2fg + 3fp + e = 0 // target 2fg + 3fp + e = 0
// target is replaced by 2(-k/3 - l/3)g + 3(-k/3 - l/3)p + e = -2/3kg -2/3lg - kp -lp + e // target is replaced by 2(-k/3 - l/3)g + 3(-k/3 - l/3)p + e = -2/3kg -2/3lg - kp -lp + e
bool nla_grobner::simplify_target_monomials(equation * source, equation * target) { bool grobner::simplify_target_monomials(equation * source, equation * target) {
auto * high_mon = get_highest_monomial(source->expr()); auto * high_mon = get_highest_monomial(source->expr());
if (high_mon == nullptr) if (high_mon == nullptr)
return false; return false;
@ -266,7 +285,7 @@ bool nla_grobner::simplify_target_monomials(equation * source, equation * target
return simplify_target_monomials_sum(source, target, targ_sum, high_mon); return simplify_target_monomials_sum(source, target, targ_sum, high_mon);
} }
unsigned nla_grobner::find_divisible(nex_sum* targ_sum, unsigned grobner::find_divisible(nex_sum* targ_sum,
const nex* high_mon) const { const nex* high_mon) const {
for (unsigned j = 0; j < targ_sum->size(); j++) { for (unsigned j = 0; j < targ_sum->size(); j++) {
auto t = (*targ_sum)[j]; auto t = (*targ_sum)[j];
@ -280,7 +299,7 @@ unsigned nla_grobner::find_divisible(nex_sum* targ_sum,
} }
bool nla_grobner::simplify_target_monomials_sum(equation * source, bool grobner::simplify_target_monomials_sum(equation * source,
equation * target, nex_sum* targ_sum, equation * target, nex_sum* targ_sum,
const nex* high_mon) { const nex* high_mon) {
unsigned j = find_divisible(targ_sum, high_mon); unsigned j = find_divisible(targ_sum, high_mon);
@ -298,16 +317,16 @@ bool nla_grobner::simplify_target_monomials_sum(equation * source,
return true; return true;
} }
nex_mul* nla_grobner::divide_ignore_coeffs(nex* ej, const nex* h) { nex_mul* grobner::divide_ignore_coeffs(nex* ej, const nex* h) {
TRACE("grobner", tout << "ej = " << *ej << " , h = " << *h << "\n";); TRACE("grobner", tout << "ej = " << *ej << " , h = " << *h << "\n";);
if (!divide_ignore_coeffs_check_only(ej, h)) if (!divide_ignore_coeffs_check_only(ej, h))
return nullptr; return nullptr;
return divide_ignore_coeffs_perform(ej, h); return divide_ignore_coeffs_perform(ej, h);
} }
bool nla_grobner::divide_ignore_coeffs_check_only_nex_mul(nex_mul* t , const nex* h) const { bool grobner::divide_ignore_coeffs_check_only_nex_mul(nex_mul* t , const nex* h) const {
TRACE("grobner", tout << "t = " << *t << ", h=" << *h << "\n";); TRACE("grobner", tout << "t = " << *t << ", h=" << *h << "\n";);
SASSERT(m_nex_creator.is_simplified(t) && m_nex_creator.is_simplified(h)); SASSERT(m_nex_creator.is_simplified(*t) && m_nex_creator.is_simplified(*h));
unsigned j = 0; // points to t unsigned j = 0; // points to t
for(unsigned k = 0; k < h->number_of_child_powers(); k++) { for(unsigned k = 0; k < h->number_of_child_powers(); k++) {
lpvar h_var = to_var(h->get_child_exp(k))->var(); lpvar h_var = to_var(h->get_child_exp(k))->var();
@ -331,7 +350,7 @@ bool nla_grobner::divide_ignore_coeffs_check_only_nex_mul(nex_mul* t , const nex
} }
// return true if h divides t // return true if h divides t
bool nla_grobner::divide_ignore_coeffs_check_only(nex* n , const nex* h) const { bool grobner::divide_ignore_coeffs_check_only(nex* n , const nex* h) const {
if (n->is_mul()) if (n->is_mul())
return divide_ignore_coeffs_check_only_nex_mul(to_mul(n), h); return divide_ignore_coeffs_check_only_nex_mul(to_mul(n), h);
if (!n->is_var()) if (!n->is_var())
@ -354,7 +373,7 @@ bool nla_grobner::divide_ignore_coeffs_check_only(nex* n , const nex* h) const {
return false; return false;
} }
nex_mul * nla_grobner::divide_ignore_coeffs_perform_nex_mul(nex_mul* t, const nex* h) { nex_mul * grobner::divide_ignore_coeffs_perform_nex_mul(nex_mul* t, const nex* h) {
nex_mul * r = m_nex_creator.mk_mul(); nex_mul * r = m_nex_creator.mk_mul();
unsigned j = 0; // points to t unsigned j = 0; // points to t
for(unsigned k = 0; k < h->number_of_child_powers(); k++) { for(unsigned k = 0; k < h->number_of_child_powers(); k++) {
@ -379,7 +398,7 @@ nex_mul * nla_grobner::divide_ignore_coeffs_perform_nex_mul(nex_mul* t, const ne
// perform the division t / h, but ignores the coefficients // perform the division t / h, but ignores the coefficients
// h does not change // h does not change
nex_mul * nla_grobner::divide_ignore_coeffs_perform(nex* e, const nex* h) { nex_mul * grobner::divide_ignore_coeffs_perform(nex* e, const nex* h) {
if (e->is_mul()) if (e->is_mul())
return divide_ignore_coeffs_perform_nex_mul(to_mul(e), h); return divide_ignore_coeffs_perform_nex_mul(to_mul(e), h);
SASSERT(e->is_var()); SASSERT(e->is_var());
@ -390,7 +409,7 @@ nex_mul * nla_grobner::divide_ignore_coeffs_perform(nex* e, const nex* h) {
// and b*high_mon + e = 0, so high_mon = -e/b // and b*high_mon + e = 0, so high_mon = -e/b
// then targ_sum->children()[j] = - (c/b) * e*p // then targ_sum->children()[j] = - (c/b) * e*p
void nla_grobner::simplify_target_monomials_sum_j(equation * source, equation *target, nex_sum* targ_sum, const nex* high_mon, unsigned j) { void grobner::simplify_target_monomials_sum_j(equation * source, equation *target, nex_sum* targ_sum, const nex* high_mon, unsigned j) {
nex * ej = (*targ_sum)[j]; nex * ej = (*targ_sum)[j];
TRACE("grobner_d", tout << "high_mon = " << *high_mon << ", ej = " << *ej << "\n";); TRACE("grobner_d", tout << "high_mon = " << *high_mon << ", ej = " << *ej << "\n";);
nex_mul * ej_over_high_mon = divide_ignore_coeffs(ej, high_mon); nex_mul * ej_over_high_mon = divide_ignore_coeffs(ej, high_mon);
@ -409,11 +428,11 @@ void nla_grobner::simplify_target_monomials_sum_j(equation * source, equation *t
} }
// return true iff simplified // return true iff simplified
bool nla_grobner::simplify_source_target(equation * source, equation * target) { bool grobner::simplify_source_target(equation * source, equation * target) {
TRACE("grobner", tout << "simplifying: "; display_equation(tout, *target); tout << "using: "; display_equation(tout, *source);); TRACE("grobner", tout << "simplifying: "; display_equation(tout, *target); tout << "using: "; display_equation(tout, *source););
TRACE("grobner_d", tout << "simplifying: " << *(target->expr()) << " using " << *(source->expr()) << "\n";); TRACE("grobner_d", tout << "simplifying: " << *(target->expr()) << " using " << *(source->expr()) << "\n";);
SASSERT(m_nex_creator.is_simplified(source->expr())); SASSERT(m_nex_creator.is_simplified(*source->expr()));
SASSERT(m_nex_creator.is_simplified(target->expr())); SASSERT(m_nex_creator.is_simplified(*target->expr()));
if (target->expr()->is_scalar()) { if (target->expr()->is_scalar()) {
TRACE("grobner_d", tout << "no simplification\n";); TRACE("grobner_d", tout << "no simplification\n";);
return false; return false;
@ -442,7 +461,7 @@ bool nla_grobner::simplify_source_target(equation * source, equation * target) {
return false; return false;
} }
void nla_grobner::process_simplified_target(equation* target, ptr_buffer<equation>& to_remove) { void grobner::process_simplified_target(equation* target, ptr_buffer<equation>& to_remove) {
if (is_trivial(target)) { if (is_trivial(target)) {
to_remove.push_back(target); to_remove.push_back(target);
} else if (m_changed_leading_term) { } else if (m_changed_leading_term) {
@ -451,7 +470,7 @@ void nla_grobner::process_simplified_target(equation* target, ptr_buffer<equatio
} }
} }
void nla_grobner::check_eq(equation* target) { void grobner::check_eq(equation* target) {
if(m_intervals->check_nex(target->expr(), target->dep())) { if(m_intervals->check_nex(target->expr(), target->dep())) {
TRACE("grobner", tout << "created a lemma for "; display_equation(tout, *target) << "\n"; TRACE("grobner", tout << "created a lemma for "; display_equation(tout, *target) << "\n";
tout << "vars = \n"; tout << "vars = \n";
@ -463,7 +482,7 @@ void nla_grobner::check_eq(equation* target) {
} }
} }
bool nla_grobner::simplify_to_superpose_with_eq(equation* eq) { bool grobner::simplify_to_superpose_with_eq(equation* eq) {
TRACE("grobner_d", tout << "eq->exp " << *(eq->expr()) << "\n";); TRACE("grobner_d", tout << "eq->exp " << *(eq->expr()) << "\n";);
ptr_buffer<equation> to_insert; ptr_buffer<equation> to_insert;
@ -481,7 +500,7 @@ bool nla_grobner::simplify_to_superpose_with_eq(equation* eq) {
if (is_trivial(target)) if (is_trivial(target))
to_delete.push_back(target); to_delete.push_back(target);
else else
SASSERT(m_nex_creator.is_simplified(target->expr())); SASSERT(m_nex_creator.is_simplified(*target->expr()));
} }
for (equation* eq : to_insert) for (equation* eq : to_insert)
insert_to_superpose(eq); insert_to_superpose(eq);
@ -495,7 +514,7 @@ bool nla_grobner::simplify_to_superpose_with_eq(equation* eq) {
/* /*
Use the given equation to simplify m_to_simplify equations Use the given equation to simplify m_to_simplify equations
*/ */
void nla_grobner::simplify_m_to_simplify(equation* eq) { void grobner::simplify_m_to_simplify(equation* eq) {
TRACE("grobner_d", tout << "eq->exp " << *(eq->expr()) << "\n";); TRACE("grobner_d", tout << "eq->exp " << *(eq->expr()) << "\n";);
ptr_buffer<equation> to_delete; ptr_buffer<equation> to_delete;
for (equation* target : m_to_simplify) { for (equation* target : m_to_simplify) {
@ -509,7 +528,7 @@ void nla_grobner::simplify_m_to_simplify(equation* eq) {
// if e is the sum then add to r all children of e multiplied by beta, except the first one // if e is the sum then add to r all children of e multiplied by beta, except the first one
// which corresponds to the highest monomial, // which corresponds to the highest monomial,
// otherwise do nothing // otherwise do nothing
void nla_grobner::add_mul_skip_first(nex_sum* r, const rational& beta, nex *e, nex_mul* c) { void grobner::add_mul_skip_first(nex_sum* r, const rational& beta, nex *e, nex_mul* c) {
if (e->is_sum()) { if (e->is_sum()) {
nex_sum *es = to_sum(e); nex_sum *es = to_sum(e);
for (unsigned j = 1; j < es->size(); j++) { for (unsigned j = 1; j < es->size(); j++) {
@ -523,7 +542,7 @@ void nla_grobner::add_mul_skip_first(nex_sum* r, const rational& beta, nex *e, n
// let e1: alpha*ab+q=0, and e2: beta*ac+e=0, then beta*qc - alpha*eb = 0 // let e1: alpha*ab+q=0, and e2: beta*ac+e=0, then beta*qc - alpha*eb = 0
nex * nla_grobner::expr_superpose(nex* e1, nex* e2, const nex* ab, const nex* ac, nex_mul* b, nex_mul* c) { nex * grobner::expr_superpose(nex* e1, nex* e2, const nex* ab, const nex* ac, nex_mul* b, nex_mul* c) {
TRACE("grobner", tout << "e1 = " << *e1 << "\ne2 = " << *e2 <<"\n";); TRACE("grobner", tout << "e1 = " << *e1 << "\ne2 = " << *e2 <<"\n";);
nex_sum * r = m_nex_creator.mk_sum(); nex_sum * r = m_nex_creator.mk_sum();
rational alpha = - ab->coeff(); rational alpha = - ab->coeff();
@ -540,7 +559,7 @@ nex * nla_grobner::expr_superpose(nex* e1, nex* e2, const nex* ab, const nex* ac
return ret; return ret;
} }
// let eq1: ab+q=0, and eq2: ac+e=0, then qc - eb = 0 // let eq1: ab+q=0, and eq2: ac+e=0, then qc - eb = 0
void nla_grobner::superpose(equation * eq1, equation * eq2) { void grobner::superpose(equation * eq1, equation * eq2) {
TRACE("grobner", tout << "eq1="; display_equation(tout, *eq1) << "eq2="; display_equation(tout, *eq2);); TRACE("grobner", tout << "eq1="; display_equation(tout, *eq1) << "eq2="; display_equation(tout, *eq2););
const nex * ab = get_highest_monomial(eq1->expr()); const nex * ab = get_highest_monomial(eq1->expr());
const nex * ac = get_highest_monomial(eq2->expr()); const nex * ac = get_highest_monomial(eq2->expr());
@ -562,13 +581,13 @@ void nla_grobner::superpose(equation * eq1, equation * eq2) {
} }
void nla_grobner::register_report() { void grobner::register_report() {
m_reported++; m_reported++;
m_conflict = true; m_conflict = true;
} }
// Let a be the greatest common divider of ab and bc, // Let a be the greatest common divider of ab and bc,
// then ab/a is stored in b, and ac/a is stored in c // then ab/a is stored in b, and ac/a is stored in c
bool nla_grobner::find_b_c(const nex* ab, const nex* ac, nex_mul*& b, nex_mul*& c) { bool grobner::find_b_c(const nex* ab, const nex* ac, nex_mul*& b, nex_mul*& c) {
if (!find_b_c_check_only(ab, ac)) if (!find_b_c_check_only(ab, ac))
return false; return false;
b = m_nex_creator.mk_mul(); c = m_nex_creator.mk_mul(); b = m_nex_creator.mk_mul(); c = m_nex_creator.mk_mul();
@ -614,10 +633,10 @@ bool nla_grobner::find_b_c(const nex* ab, const nex* ac, nex_mul*& b, nex_mul*&
return true; return true;
} }
// Finds out if ab and bc have a non-trivial common divider // Finds out if ab and bc have a non-trivial common divider
bool nla_grobner::find_b_c_check_only(const nex* ab, const nex* ac) const { bool grobner::find_b_c_check_only(const nex* ab, const nex* ac) const {
if (ab == nullptr || ac == nullptr) if (ab == nullptr || ac == nullptr)
return false; return false;
SASSERT(m_nex_creator.is_simplified(ab) && m_nex_creator.is_simplified(ab)); SASSERT(m_nex_creator.is_simplified(*ab) && m_nex_creator.is_simplified(*ac));
unsigned i = 0, j = 0; // i points to ab, j points to ac unsigned i = 0, j = 0; // i points to ab, j points to ac
for (;;) { for (;;) {
const nex* m = ab->get_child_exp(i); const nex* m = ab->get_child_exp(i);
@ -641,14 +660,14 @@ bool nla_grobner::find_b_c_check_only(const nex* ab, const nex* ac) const {
} }
void nla_grobner::superpose(equation * eq) { void grobner::superpose(equation * eq) {
for (equation * target : m_to_superpose) { for (equation * target : m_to_superpose) {
superpose(eq, target); superpose(eq, target);
} }
} }
// return true iff cannot pick_next() // return true iff cannot pick_next()
bool nla_grobner::compute_basis_step() { bool grobner::compute_basis_step() {
equation * eq = pick_next(); equation * eq = pick_next();
if (!eq) { if (!eq) {
TRACE("grobner", tout << "cannot pick an equation\n";); TRACE("grobner", tout << "cannot pick an equation\n";);
@ -671,7 +690,7 @@ bool nla_grobner::compute_basis_step() {
return false; return false;
} }
void nla_grobner::compute_basis(){ void grobner::compute_basis(){
compute_basis_init(); compute_basis_init();
if (m_rows.size() < 2) { if (m_rows.size() < 2) {
TRACE("nla_grobner", tout << "there are only " << m_rows.size() << " rows, exiting compute_basis()\n";); TRACE("nla_grobner", tout << "there are only " << m_rows.size() << " rows, exiting compute_basis()\n";);
@ -690,16 +709,16 @@ void nla_grobner::compute_basis(){
} }
} }
} }
void nla_grobner::compute_basis_init(){ void grobner::compute_basis_init(){
c().lp_settings().stats().m_grobner_basis_computatins++; c().lp_settings().stats().m_grobner_basis_computatins++;
} }
bool nla_grobner::canceled() const { bool grobner::canceled() const {
return c().lp_settings().get_cancel_flag(); return c().lp_settings().get_cancel_flag();
} }
bool nla_grobner::done() const { bool grobner::done() const {
if ( if (
num_of_equations() >= c().m_nla_settings.grobner_eqs_threshold() num_of_equations() >= c().m_nla_settings.grobner_eqs_threshold()
|| ||
@ -725,7 +744,7 @@ bool nla_grobner::done() const {
return false; return false;
} }
bool nla_grobner::compute_basis_loop(){ bool grobner::compute_basis_loop(){
int i = 0; int i = 0;
while (!done()) { while (!done()) {
if (compute_basis_step()) { if (compute_basis_step()) {
@ -738,11 +757,11 @@ bool nla_grobner::compute_basis_loop(){
return false; return false;
} }
void nla_grobner::set_gb_exhausted(){ void grobner::set_gb_exhausted(){
m_nl_gb_exhausted = true; m_nl_gb_exhausted = true;
} }
void nla_grobner::update_statistics(){ void grobner::update_statistics(){
/* todo : implement /* todo : implement
m_stats.m_gb_simplify += gb.m_stats.m_simplify; m_stats.m_gb_simplify += gb.m_stats.m_simplify;
m_stats.m_gb_superpose += gb.m_stats.m_superpose; m_stats.m_gb_superpose += gb.m_stats.m_superpose;
@ -751,36 +770,17 @@ void nla_grobner::update_statistics(){
} }
bool nla_grobner::push_calculation_forward(ptr_vector<equation>& eqs, unsigned & next_weight) { bool grobner::push_calculation_forward(ptr_vector<equation>& eqs, unsigned & next_weight) {
return (!m_nl_gb_exhausted) && return (!m_nl_gb_exhausted) &&
try_to_modify_eqs(eqs, next_weight); try_to_modify_eqs(eqs, next_weight);
} }
bool nla_grobner::try_to_modify_eqs(ptr_vector<equation>& eqs, unsigned& next_weight) { bool grobner::try_to_modify_eqs(ptr_vector<equation>& eqs, unsigned& next_weight) {
// NOT_IMPLEMENTED_YET(); // NOT_IMPLEMENTED_YET();
return false; return false;
} }
void grobner:: del_equations(unsigned old_size) {
void nla_grobner::grobner_lemmas() {
c().lp_settings().stats().m_grobner_calls++;
init();
ptr_vector<equation> eqs;
unsigned next_weight =
(unsigned)(var_weight::MAX_DEFAULT_WEIGHT) + 1; // next weight using during perturbation phase.
do {
TRACE("grobner", tout << "before:\n"; display(tout););
compute_basis();
update_statistics();
TRACE("grobner", tout << "after:\n"; display(tout););
// if (find_conflict(eqs))
// return;
}
while(push_calculation_forward(eqs, next_weight));
}
void nla_grobner:: del_equations(unsigned old_size) {
TRACE("grobner", ); TRACE("grobner", );
SASSERT(m_equations_to_delete.size() >= old_size); SASSERT(m_equations_to_delete.size() >= old_size);
equation_vector::iterator it = m_equations_to_delete.begin(); equation_vector::iterator it = m_equations_to_delete.begin();
@ -794,18 +794,18 @@ void nla_grobner:: del_equations(unsigned old_size) {
m_equations_to_delete.shrink(old_size); m_equations_to_delete.shrink(old_size);
} }
void nla_grobner::display_equations(std::ostream & out, equation_set const & v, char const * header) const { void grobner::display_equations(std::ostream & out, equation_set const & v, char const * header) const {
out << header << "\n"; out << header << "\n";
for (const equation* e : v) for (const equation* e : v)
display_equation(out, *e); display_equation(out, *e);
} }
std::ostream& nla_grobner::display_equation(std::ostream & out, const equation & eq) const { std::ostream& grobner::display_equation(std::ostream & out, const equation & eq) const {
out << "expr = " << *eq.expr() << "\n"; out << "expr = " << *eq.expr() << "\n";
display_dependency(out, eq.dep()); display_dependency(out, eq.dep());
return out; return out;
} }
std::unordered_set<lpvar> nla_grobner::get_vars_of_expr_with_opening_terms(const nex *e ) { std::unordered_set<lpvar> grobner::get_vars_of_expr_with_opening_terms(const nex *e ) {
auto ret = get_vars_of_expr(e); auto ret = get_vars_of_expr(e);
auto & ls = c().m_lar_solver; auto & ls = c().m_lar_solver;
do { do {
@ -827,7 +827,7 @@ std::unordered_set<lpvar> nla_grobner::get_vars_of_expr_with_opening_terms(const
} while (true); } while (true);
} }
void nla_grobner::assert_eq_0(nex* e, ci_dependency * dep) { void grobner::assert_eq_0(nex* e, ci_dependency * dep) {
if (e == nullptr || is_zero_scalar(e)) if (e == nullptr || is_zero_scalar(e))
return; return;
m_tmp_var_set.clear(); m_tmp_var_set.clear();
@ -843,7 +843,7 @@ void nla_grobner::assert_eq_0(nex* e, ci_dependency * dep) {
insert_to_simplify(eq); insert_to_simplify(eq);
} }
void nla_grobner::init_equation(equation* eq, nex*e, ci_dependency * dep) { void grobner::init_equation(equation* eq, nex*e, ci_dependency * dep) {
unsigned bidx = m_equations_to_delete.size(); unsigned bidx = m_equations_to_delete.size();
eq->m_bidx = bidx; eq->m_bidx = bidx;
eq->dep() = dep; eq->dep() = dep;
@ -852,11 +852,11 @@ void nla_grobner::init_equation(equation* eq, nex*e, ci_dependency * dep) {
SASSERT(m_equations_to_delete[eq->m_bidx] == eq); SASSERT(m_equations_to_delete[eq->m_bidx] == eq);
} }
nla_grobner::~nla_grobner() { grobner::~grobner() {
del_equations(0); del_equations(0);
} }
std::ostream& nla_grobner::display_dependency(std::ostream& out, ci_dependency* dep) const { std::ostream& grobner::display_dependency(std::ostream& out, ci_dependency* dep) const {
svector<lp::constraint_index> expl; svector<lp::constraint_index> expl;
m_dep_manager.linearize(dep, expl); m_dep_manager.linearize(dep, expl);
{ {
@ -872,5 +872,4 @@ std::ostream& nla_grobner::display_dependency(std::ostream& out, ci_dependency*
return out; return out;
} }
} // end of nla namespace

21
src/math/lp/nla_grobner.h
View file

@ -36,13 +36,11 @@ struct grobner_stats {
grobner_stats() { reset(); } grobner_stats() { reset(); }
}; };
class grobner : common {
class nla_grobner : common {
class equation { class equation {
unsigned m_bidx; //!< position at m_equations_to_delete unsigned m_bidx; //!< position at m_equations_to_delete
nex * m_expr; // simplified expressionted monomials
nex * m_expr; // simplified expressionted monomials ci_dependency * m_dep; //!< justification for the equality
ci_dependency * m_dep; //!< justification for the equality
public: public:
unsigned get_num_monomials() const { unsigned get_num_monomials() const {
switch(m_expr->type()) { switch(m_expr->type()) {
@ -71,7 +69,7 @@ class nla_grobner : common {
ci_dependency * dep() const { return m_dep; } ci_dependency * dep() const { return m_dep; }
ci_dependency *& dep() { return m_dep; } ci_dependency *& dep() { return m_dep; }
unsigned hash() const { return m_bidx; } unsigned hash() const { return m_bidx; }
friend class nla_grobner; friend class grobner;
}; };
typedef obj_hashtable<equation> equation_set; typedef obj_hashtable<equation> equation_set;
@ -95,9 +93,9 @@ class nla_grobner : common {
bool m_conflict; bool m_conflict;
bool m_look_for_fixed_vars_in_rows; bool m_look_for_fixed_vars_in_rows;
public: public:
nla_grobner(core *core, intervals *); grobner(core *, intervals *);
void grobner_lemmas(); void grobner_lemmas();
~nla_grobner(); ~grobner();
private: private:
void find_nl_cluster(); void find_nl_cluster();
void prepare_rows_and_active_vars(); void prepare_rows_and_active_vars();
@ -105,8 +103,6 @@ private:
void init(); void init();
void compute_basis(); void compute_basis();
void update_statistics(); void update_statistics();
bool find_conflict(ptr_vector<equation>& eqs);
bool is_inconsistent(equation*);
bool push_calculation_forward(ptr_vector<equation>& eqs, unsigned&); bool push_calculation_forward(ptr_vector<equation>& eqs, unsigned&);
void compute_basis_init(); void compute_basis_init();
bool compute_basis_loop(); bool compute_basis_loop();
@ -133,7 +129,6 @@ private:
void display_matrix(std::ostream & out) const; void display_matrix(std::ostream & out) const;
std::ostream& display(std::ostream & out) const; std::ostream& display(std::ostream & out) const;
void get_equations(ptr_vector<equation>& eqs);
bool try_to_modify_eqs(ptr_vector<equation>& eqs, unsigned& next_weight); bool try_to_modify_eqs(ptr_vector<equation>& eqs, unsigned& next_weight);
bool internalize_gb_eq(equation*); bool internalize_gb_eq(equation*);
void add_row(unsigned); void add_row(unsigned);
@ -146,13 +141,13 @@ private:
m_to_simplify.insert(eq); m_to_simplify.insert(eq);
} }
void insert_to_superpose(equation *eq) { void insert_to_superpose(equation *eq) {
SASSERT(m_nex_creator.is_simplified(eq->expr())); SASSERT(m_nex_creator.is_simplified(*eq->expr()));
TRACE("nla_grobner", display_equation(tout, *eq);); TRACE("nla_grobner", display_equation(tout, *eq););
m_to_superpose.insert(eq); m_to_superpose.insert(eq);
} }
void simplify_equations_in_m_to_simplify(); void simplify_equations_in_m_to_simplify();
const nex * get_highest_monomial(const nex * e) const; const nex * get_highest_monomial(const nex * e) const;
ci_dependency* dep_from_vector( svector<lp::constraint_index> & fixed_vars_constraints); ci_dependency* dep_from_vector(svector<lp::constraint_index> & fixed_vars_constraints);
bool simplify_target_monomials_sum(equation *, equation *, nex_sum*, const nex*); bool simplify_target_monomials_sum(equation *, equation *, nex_sum*, const nex*);
unsigned find_divisible(nex_sum*, const nex*) const; unsigned find_divisible(nex_sum*, const nex*) const;
void simplify_target_monomials_sum_j(equation *, equation *, nex_sum*, const nex*, unsigned); void simplify_target_monomials_sum_j(equation *, equation *, nex_sum*, const nex*, unsigned);