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 nits (#97)

Browse source 
* code nits

nits from review pass

* Update cross_nested.h
This commit is contained in:
Nikolaj Bjorner 2019-12-10 03:11:02 +01:00 committed by Lev Nachmanson
parent 21d9875239
commit 04f0a310a2
5 changed files with 189 additions and 249 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -83,7 +83,7 @@ public:
TRACE("nla_cn", tout << "c=" << *c << "\n"; tout << "occs:"; dump_occurences(tout, m_nex_creator.occurences_map()) << "\n";); TRACE("nla_cn", tout << "c=" << *c << "\n"; tout << "occs:"; dump_occurences(tout, m_nex_creator.occurences_map()) << "\n";);
unsigned size = c->size(); unsigned size = c->size();
bool have_factor = false; bool have_factor = false;
for(const auto & p : m_nex_creator.occurences_map()) { for (const auto & p : m_nex_creator.occurences_map()) {
if (p.second.m_occs == size) { if (p.second.m_occs == size) {
have_factor = true; have_factor = true;
break; break;
@ -91,7 +91,7 @@ public:
} }
if (have_factor == false) return nullptr; if (have_factor == false) return nullptr;
nex_mul* f = m_nex_creator.mk_mul(); nex_mul* f = m_nex_creator.mk_mul();
for(const auto & p : m_nex_creator.occurences_map()) { // randomize here: todo for (const auto & p : m_nex_creator.occurences_map()) { // randomize here: todo
if (p.second.m_occs == size) { if (p.second.m_occs == size) {
f->add_child_in_power(m_nex_creator.mk_var(p.first), p.second.m_power); f->add_child_in_power(m_nex_creator.mk_var(p.first), p.second.m_power);
} }
@ -105,7 +105,7 @@ public:
auto common_vars = get_vars_of_expr(ch[0]); auto common_vars = get_vars_of_expr(ch[0]);
for (lpvar j : common_vars) { for (lpvar j : common_vars) {
bool divides_the_rest = true; bool divides_the_rest = true;
for(unsigned i = 1; i < ch.size() && divides_the_rest; i++) { for (unsigned i = 1; i < ch.size() && divides_the_rest; i++) {
if (!ch[i]->contains(j)) if (!ch[i]->contains(j))
divides_the_rest = false; divides_the_rest = false;
} }
@ -163,7 +163,7 @@ public:
nex* copy_of_c = *c; nex* copy_of_c = *c;
auto copy_of_front = copy_front(front); auto copy_of_front = copy_front(front);
int alloc_size = m_nex_creator.size(); int alloc_size = m_nex_creator.size();
for(lpvar j : vars) { for (lpvar j : vars) {
if (m_var_is_fixed(j)) { if (m_var_is_fixed(j)) {
// it does not make sense to explore fixed multupliers // it does not make sense to explore fixed multupliers
// because the interval products do not become smaller // because the interval products do not become smaller
@ -184,9 +184,8 @@ public:
template <typename T> template <typename T>
static std::ostream& dump_occurences(std::ostream& out, const T& occurences) { static std::ostream& dump_occurences(std::ostream& out, const T& occurences) {
out << "{"; out << "{";
for(const auto& p: occurences) { for (const auto& p: occurences) {
const occ& o = p.second; out << "(v" << p.first << "->" << p.second << ")";
out << "(v" << p.first << "->" << o << ")";
} }
out << "}" << std::endl; out << "}" << std::endl;
return out; return out;
@ -252,7 +251,7 @@ public:
print_vector(vars, tout) << "; front:"; print_front(front, tout) << "\n";); print_vector(vars, tout) << "; front:"; print_front(front, tout) << "\n";);
if (vars.empty()) { if (vars.empty()) {
if(front.empty()) { if (front.empty()) {
TRACE("nla_cn", tout << "got the cn form: =" << *m_e << "\n";); TRACE("nla_cn", tout << "got the cn form: =" << *m_e << "\n";);
m_done = m_call_on_result(m_e) || ++m_reported > 100; m_done = m_call_on_result(m_e) || ++m_reported > 100;
#ifdef Z3DEBUG #ifdef Z3DEBUG

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

@ -108,8 +108,7 @@ public:
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 {
// out << (char)('a' + m_j); // out << (char)('a' + m_j);
out << "v" << m_j; return out << "v" << m_j;
return out;
} }
bool contains(lpvar j) const { return j == m_j; } bool contains(lpvar j) const { return j == m_j; }
@ -125,10 +124,7 @@ 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 { std::ostream& print(std::ostream& out) const { return out << m_v; }
out << m_v;
return out;
}
int get_degree() const { return 0; } int get_degree() const { return 0; }
bool is_linear() const { return true; } bool is_linear() const { return true; }
@ -136,7 +132,6 @@ public:
const nex_scalar * to_scalar(const nex* a); const nex_scalar * to_scalar(const nex* a);
class nex_sum; class nex_sum;
const nex_sum* to_sum(const nex*a);
class nex_pow { class nex_pow {
nex* m_e; nex* m_e;
@ -149,25 +144,30 @@ public:
nex ** ee() { return & m_e; } nex ** ee() { return & m_e; }
int pow() const { return m_power; } int pow() const { return m_power; }
int& pow() { return m_power; }
std::string to_string() const { std::ostream& print(std::ostream& s) const {
std::stringstream s;
if (pow() == 1) { if (pow() == 1) {
if (e()->is_elementary()) { if (e()->is_elementary()) {
s << *e(); s << *e();
} else { } else {
s <<"(" << *e() << ")"; s <<"(" << *e() << ")";
} }
} else { }
else {
if (e()->is_elementary()){ if (e()->is_elementary()){
s << "(" << *e() << "^" << pow() << ")"; s << "(" << *e() << "^" << pow() << ")";
} else { } else {
s << "((" << *e() << ")^" << pow() << ")"; s << "((" << *e() << ")^" << pow() << ")";
} }
} }
return s;
}
std::string to_string() const {
std::stringstream s;
print(s);
return s.str(); return s.str();
} }
friend std::ostream& operator<<(std::ostream& out, const nex_pow & p) { out << p.to_string(); return out; } friend std::ostream& operator<<(std::ostream& out, const nex_pow & p) { return p.print(out); }
}; };
inline unsigned get_degree_children(const vector<nex_pow>& children) { inline unsigned get_degree_children(const vector<nex_pow>& children) {
@ -206,20 +206,19 @@ public:
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 {
bool first = true; bool first = true;
if (!m_coeff.is_one()) { if (!m_coeff.is_one()) {
out << m_coeff; out << m_coeff;
first = false; first = false;
} }
for (const nex_pow& v : m_children) { for (const nex_pow& v : m_children) {
std::string s = v.to_string();
if (first) { if (first) {
first = false; first = false;
out << s; out << v;
} else { } else {
out << "*" << s; out << "*" << v;
} }
} }
return out; return out;
@ -252,9 +251,10 @@ public:
void add_child_in_power(nex* e, int power) { void add_child_in_power(nex* e, int power) {
if (e->is_scalar()) { if (e->is_scalar()) {
m_coeff *= (to_scalar(e)->value()).expt(power); m_coeff *= (to_scalar(e)->value()).expt(power);
return;
} }
m_children.push_back(nex_pow(e, power)); else {
m_children.push_back(nex_pow(e, power));
}
} }
bool contains(lpvar j) const { bool contains(lpvar j) const {
@ -335,8 +335,7 @@ public:
for (auto e : *this) { for (auto e : *this) {
int d = e->get_degree(); int d = e->get_degree();
if (d == 0) continue; if (d == 0) continue;
if (d > 1) return false; if (d > 1) return false;
number_of_non_scalars++; number_of_non_scalars++;
} }
TRACE("nex_details", tout << (number_of_non_scalars > 1?"linear":"non-linear") << "\n";); TRACE("nex_details", tout << (number_of_non_scalars > 1?"linear":"non-linear") << "\n";);
@ -398,7 +397,7 @@ public:
#endif #endif
}; };
inline const nex_sum* to_sum(const nex*a) { inline const nex_sum* to_sum(const nex* a) {
SASSERT(a->is_sum()); SASSERT(a->is_sum());
return static_cast<const nex_sum*>(a); return static_cast<const nex_sum*>(a);
} }
@ -407,7 +406,6 @@ inline nex_sum* to_sum(nex * a) {
SASSERT(a->is_sum()); SASSERT(a->is_sum());
return static_cast<nex_sum*>(a); return static_cast<nex_sum*>(a);
} }
inline const nex_var* to_var(const nex*a) { inline const nex_var* to_var(const nex*a) {
SASSERT(a->is_var()); SASSERT(a->is_var());
@ -447,22 +445,20 @@ inline rational get_nex_val(const nex* e, std::function<rational (unsigned)> var
switch (e->type()) { switch (e->type()) {
case expr_type::SCALAR: case expr_type::SCALAR:
return to_scalar(e)->value(); return to_scalar(e)->value();
case expr_type::SUM: case expr_type::SUM: {
{ rational r(0);
rational r(0); for (auto c: *to_sum(e)) {
for (auto c: *to_sum(e)) { r += get_nex_val(c, var_val);
r += get_nex_val(c, var_val);
}
return r;
}
case expr_type::MUL:
{
const nex_mul * m = to_mul(e);
rational t = m->coeff();
for (auto& c: *m)
t *= get_nex_val(c.e(), var_val).expt(c.pow());
return t;
} }
return r;
}
case expr_type::MUL: {
auto & m = *to_mul(e);
rational t = m.coeff();
for (auto& c: m)
t *= get_nex_val(c.e(), var_val).expt(c.pow());
return t;
}
case expr_type::VAR: case expr_type::VAR:
return var_val(to_var(e)->var()); return var_val(to_var(e)->var());
default: default:
@ -477,20 +473,18 @@ inline std::unordered_set<lpvar> get_vars_of_expr(const nex *e ) {
switch (e->type()) { switch (e->type()) {
case expr_type::SCALAR: case expr_type::SCALAR:
return r; return r;
case expr_type::SUM: case expr_type::SUM: {
{ for (auto c: *to_sum(e))
for (auto c: *to_sum(e)) for ( lpvar j : get_vars_of_expr(c))
for ( lpvar j : get_vars_of_expr(c)) r.insert(j);
r.insert(j);
}
return r; return r;
case expr_type::MUL: }
{ case expr_type::MUL: {
for (auto &c: *to_mul(e)) for (auto &c: *to_mul(e))
for ( lpvar j : get_vars_of_expr(c.e())) for ( lpvar j : get_vars_of_expr(c.e()))
r.insert(j); r.insert(j);
}
return r; return r;
}
case expr_type::VAR: case expr_type::VAR:
r.insert(to_var(e)->var()); r.insert(to_var(e)->var());
return r; return r;

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

@ -17,9 +17,9 @@
--*/ --*/
#include "util/lbool.h"
#include "math/lp/nex_creator.h" #include "math/lp/nex_creator.h"
#include <map> #include <map>
#include <vector>
namespace nla { namespace nla {
@ -30,8 +30,8 @@ nex * nex_creator::mk_div(const nex* a, lpvar j) {
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 = *to_mul(a);
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)) {
@ -51,24 +51,24 @@ nex * nex_creator::mk_div(const nex* a, lpvar j) {
bv.push_back(nex_pow(clone(c), pow)); bv.push_back(nex_pow(clone(c), pow));
} }
} }
if (bv.size() == 1 && bv.begin()->pow() == 1 && ma->coeff().is_one()) { if (bv.size() == 1 && bv.begin()->pow() == 1 && ma.coeff().is_one()) {
return bv.begin()->e(); return bv.begin()->e();
} }
if (bv.size() == 0) { if (bv.empty()) {
return mk_scalar(rational(ma->coeff())); return mk_scalar(rational(ma.coeff()));
} }
auto m = mk_mul(bv); auto m = mk_mul(bv);
m->coeff() = ma->coeff(); m->coeff() = ma.coeff();
return m; return m;
} }
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 = *to_mul(p.e());
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())
return true; return true;
r *= coeff.expt(p.pow() * pow); r *= coeff.expt(p.pow() * pow);
@ -90,7 +90,7 @@ void nex_creator::simplify_children_of_mul(vector<nex_pow> & children, rational&
TRACE("grobner_d", print_vector(children, tout);); TRACE("grobner_d", print_vector(children, tout););
vector<nex_pow> to_promote; vector<nex_pow> to_promote;
int skipped = 0; int skipped = 0;
for(unsigned j = 0; j < children.size(); j++) { for (unsigned j = 0; j < children.size(); j++) {
nex_pow& p = children[j]; nex_pow& p = children[j];
if (eat_scalar_pow(coeff, p, 1)) { if (eat_scalar_pow(coeff, p, 1)) {
skipped++; skipped++;
@ -112,49 +112,48 @@ 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 = *to_mul(p.e());
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);
TRACE("grobner_d", print_vector(children, tout);); TRACE("grobner_d", print_vector(children, tout););
} }
bool nex_creator:: less_than_on_powers_mul_same_degree(const vector<nex_pow>& a, const nex_mul* b) const { bool nex_creator:: less_than_on_powers_mul_same_degree(const vector<nex_pow>& a, const nex_mul& b) const {
bool inside_a_p = false; // inside_a_p is true means we still compare the old position of it_a bool inside_a_p = false; // inside_a_p is true means we still compare the old position of it_a
bool inside_b_p = false; // inside_b_p is true means we still compare the old position of it_b bool inside_b_p = false; // inside_b_p is true means we still compare the old position of it_b
auto it_a = a.begin(); auto it_a = a.begin();
auto it_b = b->begin(); auto it_b = b.begin();
auto a_end = a.end(); auto a_end = a.end();
auto b_end = b->end(); auto b_end = b.end();
unsigned a_pow, b_pow; unsigned a_pow, b_pow;
int ret = - 1; lbool ret = l_undef;
do { while (true) {
if (!inside_a_p) { a_pow = it_a->pow(); } if (!inside_a_p) { a_pow = it_a->pow(); }
if (!inside_b_p) { b_pow = it_b->pow(); } if (!inside_b_p) { b_pow = it_b->pow(); }
if (lt(it_a->e(), it_b->e())){ if (lt(it_a->e(), it_b->e())){
ret = true; ret = l_true;
break; break;
} }
if (lt(it_b->e(), it_a->e())) { if (lt(it_b->e(), it_a->e())) {
ret = false; ret = l_false;
break; break;
} }
if (a_pow == b_pow) { if (a_pow == b_pow) {
inside_a_p = inside_b_p = false; inside_a_p = inside_b_p = false;
it_a++; it_b++; it_a++; it_b++;
if (it_a == a_end) { if (it_a == a_end) {
ret = false; ret = l_false;
break; break;
} }
if (it_b == b_end) { // it_a is not at the end if (it_b == b_end) { // it_a is not at the end
ret = false; ret = l_false;
break; break;
} }
// no iterator reached the end // no iterator reached the end
@ -163,7 +162,7 @@ bool nex_creator:: less_than_on_powers_mul_same_degree(const vector<nex_pow>& a,
if (a_pow > b_pow) { if (a_pow > b_pow) {
it_a++; it_a++;
if (it_a == a_end) { if (it_a == a_end) {
ret = true; ret = l_true;
break; break;
} }
inside_a_p = false; inside_a_p = false;
@ -174,54 +173,51 @@ bool nex_creator:: less_than_on_powers_mul_same_degree(const vector<nex_pow>& a,
a_pow -= b_pow; a_pow -= b_pow;
it_b++; it_b++;
if (it_b == b_end) { if (it_b == b_end) {
ret = false; ret = l_false;
break; break;
} }
inside_a_p = true; inside_a_p = true;
inside_b_p = false; inside_b_p = false;
} }
} while (true); }
if (ret == -1) TRACE("nex_less", tout << "a = "; print_vector(a, tout) << (ret != l_false?" < ":" >= ") << b << "\n";);
ret = true; return ret != l_false;
TRACE("nex_less", tout << "a = "; print_vector(a, tout) << (ret == 1?" < ":" >= ") << *b << "\n";);
return ret;
} }
bool nex_creator::less_than_on_mul_mul_same_degree(const nex_mul* a, const nex_mul* b) const { bool nex_creator::less_than_on_mul_mul_same_degree(const nex_mul& a, const nex_mul& b) const {
bool inside_a_p = false; // inside_a_p is true means we still compare the old position of it_a bool inside_a_p = false; // inside_a_p is true means we still compare the old position of it_a
bool inside_b_p = false; // inside_b_p is true means we still compare the old position of it_b bool inside_b_p = false; // inside_b_p is true means we still compare the old position of it_b
auto it_a = a->begin(); auto it_a = a.begin();
auto it_b = b->begin(); auto it_b = b.begin();
auto a_end = a->end(); auto a_end = a.end();
auto b_end = b->end(); auto b_end = b.end();
unsigned a_pow, b_pow; unsigned a_pow, b_pow;
int ret = - 1; lbool ret = l_undef;
do { while (true) {
if (!inside_a_p) { a_pow = it_a->pow(); } if (!inside_a_p) { a_pow = it_a->pow(); }
if (!inside_b_p) { b_pow = it_b->pow(); } if (!inside_b_p) { b_pow = it_b->pow(); }
if (lt(it_a->e(), it_b->e())){ if (lt(it_a->e(), it_b->e())){
ret = true; ret = l_true;
break; break;
} }
if (lt(it_b->e(), it_a->e())) { if (lt(it_b->e(), it_a->e())) {
ret = false; ret = l_false;
break; break;
} }
if (a_pow == b_pow) { if (a_pow == b_pow) {
inside_a_p = inside_b_p = false; inside_a_p = inside_b_p = false;
it_a++; it_b++; it_a++; it_b++;
if (it_a == a_end) { if (it_a == a_end) {
if (it_b != b_end) { if (it_b != b_end) {
ret = false; ret = l_false;
break; break;
} }
SASSERT(it_a == a_end && it_b == b_end); SASSERT(it_a == a_end && it_b == b_end);
ret = a->coeff() > b->coeff(); ret = to_lbool(a.coeff() > b.coeff());
break; break;
} }
if (it_b == b_end) { // it_a is not at the end if (it_b == b_end) { // it_a is not at the end
ret = false; ret = l_false;
break; break;
} }
// no iterator reached the end // no iterator reached the end
@ -230,7 +226,7 @@ bool nex_creator::less_than_on_mul_mul_same_degree(const nex_mul* a, const nex_m
if (a_pow > b_pow) { if (a_pow > b_pow) {
it_a++; it_a++;
if (it_a == a_end) { if (it_a == a_end) {
ret = true; ret = l_true;
break; break;
} }
inside_a_p = false; inside_a_p = false;
@ -241,17 +237,15 @@ bool nex_creator::less_than_on_mul_mul_same_degree(const nex_mul* a, const nex_m
a_pow -= b_pow; a_pow -= b_pow;
it_b++; it_b++;
if (it_b == b_end) { if (it_b == b_end) {
ret = false; ret = l_false;
break; break;
} }
inside_a_p = true; inside_a_p = true;
inside_b_p = false; inside_b_p = false;
} }
} while (true); }
if (ret == -1) TRACE("grobner_d", tout << "a = " << a << (ret != l_false?" < ":" >= ") << b << "\n";);
ret = true; return ret != l_false;
TRACE("grobner_d", tout << "a = " << *a << (ret == 1?" < ":" >= ") << *b << "\n";);
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 {
@ -260,60 +254,34 @@ bool nex_creator::children_are_simplified(const vector<nex_pow>& children) const
return false; return false;
return true; return true;
} }
bool nex_creator::less_than_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";); bool nex_creator::less_than_on_powers_mul(const vector<nex_pow>& children, const nex_mul& b) const {
SASSERT(children_are_simplified(children) && is_simplified(b)); TRACE("nex_less", tout << "children = "; print_vector(children, tout) << " , b = " << b << "\n";);
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();
bool ret;
if (a_deg > b_deg) {
ret = true;
} else if (a_deg < b_deg) {
ret = false;
} else {
ret = less_than_on_powers_mul_same_degree(children, b);
}
return ret;
return a_deg == b_deg ? less_than_on_powers_mul_same_degree(children, b) : a_deg > b_deg;
} }
bool nex_creator::less_than_on_mul_mul(const nex_mul& a, const nex_mul& b) const {
bool nex_creator::less_than_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 ? less_than_on_mul_mul_same_degree(a, b) : a_deg > b_deg;
bool ret;
if (a_deg > b_deg) {
ret = true;
} else if (a_deg < b_deg) {
ret = false;
} else {
ret = less_than_on_mul_mul_same_degree(a, b);
}
return ret;
} }
bool nex_creator::less_than_on_var_nex(const nex_var* a, const nex* b) const { bool nex_creator::less_than_on_var_nex(const nex_var* a, const nex* b) const {
switch(b->type()) { switch (b->type()) {
case expr_type::SCALAR: return true; case expr_type::SCALAR:
return true;
case expr_type::VAR: case expr_type::VAR:
return less_than(a->var() , to_var(b)->var()); return less_than(a->var() , to_var(b)->var());
case expr_type::MUL: case expr_type::MUL:
{ return b->get_degree() <= 1 && less_than_on_var_nex(a, (*to_mul(b))[0].e());
if (b->get_degree() > 1)
return false;
auto it = to_mul(b)->begin();
const nex_pow & c = *it;
const nex * f = c.e();
return less_than_on_var_nex(a, f);
}
case expr_type::SUM: case expr_type::SUM:
{ return !lt((*to_sum(b))[0], a);
return !lt((*to_sum(b))[0], a);
}
default: default:
UNREACHABLE(); UNREACHABLE();
return false; return false;
@ -321,21 +289,20 @@ bool nex_creator::less_than_on_var_nex(const nex_var* a, const nex* b) const {
} }
bool nex_creator::lt_nex_powers(const vector<nex_pow>& children, const nex* b) const { bool nex_creator::lt_nex_powers(const vector<nex_pow>& children, const nex* b) const {
switch(b->type()) { switch (b->type()) {
case expr_type::SCALAR: return false; case expr_type::SCALAR:
case expr_type::VAR: return false;
{ case expr_type::VAR: {
if (get_degree_children(children) > 1) if (get_degree_children(children) > 1)
return true; return true;
auto it = children.begin(); const nex_pow & c = children[0];
const nex_pow & c = *it; SASSERT(c.pow() == 1);
SASSERT(c.pow() == 1); const nex * f = c.e();
const nex * f = c.e(); SASSERT(!f->is_scalar());
SASSERT(!f->is_scalar()); return lt(f, b);
return lt(f, b); }
}
case expr_type::MUL: case expr_type::MUL:
return less_than_on_powers_mul(children, to_mul(b)); return less_than_on_powers_mul(children, *to_mul(b));
case expr_type::SUM: case expr_type::SUM:
return lt_nex_powers(children, (*to_sum(b))[0]); return lt_nex_powers(children, (*to_sum(b))[0]);
default: default:
@ -344,23 +311,21 @@ bool nex_creator::lt_nex_powers(const vector<nex_pow>& children, const nex* b) c
} }
} }
bool nex_creator::less_than_on_mul_nex(const nex_mul* a, const nex* b) const { bool nex_creator::less_than_on_mul_nex(const nex_mul* a, const nex* b) const {
switch(b->type()) { switch (b->type()) {
case expr_type::SCALAR: return false; case expr_type::SCALAR:
case expr_type::VAR: return false;
{ case expr_type::VAR: {
if (a->get_degree() > 1) if (a->get_degree() > 1)
return true; return true;
auto it = a->begin(); const nex_pow & c = *a->begin();
const nex_pow & c = *it; SASSERT(c.pow() == 1);
SASSERT(c.pow() == 1); const nex * f = c.e();
const nex * f = c.e(); SASSERT(!f->is_scalar());
SASSERT(!f->is_scalar()); return lt(f, b);
return lt(f, b); }
}
case expr_type::MUL: case expr_type::MUL:
return less_than_on_mul_mul(a, to_mul(b)); return less_than_on_mul_mul(*a, *to_mul(b));
case expr_type::SUM: case expr_type::SUM:
return lt(a, (*to_sum(b))[0]); return lt(a, (*to_sum(b))[0]);
default: default:
@ -391,22 +356,19 @@ bool nex_creator::lt_for_sort_join_sum(const nex* a, const nex* b) const {
case expr_type::VAR: case expr_type::VAR:
ret = less_than_on_var_nex(to_var(a), b); ret = less_than_on_var_nex(to_var(a), b);
break; break;
case expr_type::SCALAR: { case expr_type::SCALAR:
if (b->is_scalar()) if (b->is_scalar())
ret = to_scalar(a)->value() > to_scalar(b)->value(); ret = to_scalar(a)->value() > to_scalar(b)->value();
else else
ret = false; // the scalars are the largest ret = false; // the scalars are the largest
break; break;
} case expr_type::MUL:
case expr_type::MUL: {
ret = lt_nex_powers(to_mul(a)->children(), b); ret = lt_nex_powers(to_mul(a)->children(), b);
break; break;
} case expr_type::SUM:
case expr_type::SUM: {
if (b->is_sum()) if (b->is_sum())
return less_than_on_sum_sum(to_sum(a), to_sum(b)); return less_than_on_sum_sum(to_sum(a), to_sum(b));
return lt((*to_sum(a))[0], b); return lt((*to_sum(a))[0], b);
}
default: default:
UNREACHABLE(); UNREACHABLE();
return false; return false;
@ -424,22 +386,17 @@ bool nex_creator::lt(const nex* a, const nex* b) const {
case expr_type::VAR: case expr_type::VAR:
ret = less_than_on_var_nex(to_var(a), b); ret = less_than_on_var_nex(to_var(a), b);
break; break;
case expr_type::SCALAR: { case expr_type::SCALAR:
if (b->is_scalar()) ret = b->is_scalar() && to_scalar(a)->value() > to_scalar(b)->value();
ret = to_scalar(a)->value() > to_scalar(b)->value(); // the scalars are the largest
else
ret = false; // the scalars are the largest
break; break;
} case expr_type::MUL:
case expr_type::MUL: {
ret = less_than_on_mul_nex(to_mul(a), b); ret = less_than_on_mul_nex(to_mul(a), b);
break; break;
} case expr_type::SUM:
case expr_type::SUM: {
if (b->is_sum()) if (b->is_sum())
return less_than_on_sum_sum(to_sum(a), to_sum(b)); return less_than_on_sum_sum(to_sum(a), to_sum(b));
return lt((*to_sum(a))[0], b); return lt((*to_sum(a))[0], b);
}
default: default:
UNREACHABLE(); UNREACHABLE();
return false; return false;
@ -460,9 +417,6 @@ 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) {
@ -562,14 +516,14 @@ bool nex_creator::sum_is_simplified(const nex_sum* e) const {
} }
void nex_creator::mul_to_powers(vector<nex_pow>& children) { void nex_creator::mul_to_powers(vector<nex_pow>& children) {
std::map<nex*, int, nex_lt> m([this](const nex* a, const nex* b) {return lt(a, b); }); std::map<nex*, int, nex_lt> m([this](const nex* a, const nex* b) { return lt(a, b); });
for (auto & p : children) { for (auto & p : children) {
auto it = m.find(p.e()); auto it = m.find(p.e());
if (it == m.end()) { if (it == m.end()) {
m[p.e()] = p.pow(); m[p.e()] = p.pow();
} else { } else {
it->second+= p.pow(); it->second += p.pow();
} }
} }
children.clear(); children.clear();
@ -607,12 +561,11 @@ nex* nex_creator::create_child_from_nex_and_coeff(nex *e,
} }
em->add_child(mk_scalar(coeff)); em->add_child(mk_scalar(coeff));
std::sort(em->begin(), em->end(), [this](const nex_pow& a, std::sort(em->begin(), em->end(), [this](const nex_pow& a,
const nex_pow& b) {return less_than_on_nex_pow(a, b);}); const nex_pow& b) {return less_than_on_nex_pow(a, b); });
return em; return em;
} }
case expr_type::SUM: { case expr_type::SUM:
return mk_mul(mk_scalar(coeff), e); return mk_mul(mk_scalar(coeff), e);
}
default: default:
UNREACHABLE(); UNREACHABLE();
return nullptr; return nullptr;
@ -634,10 +587,11 @@ bool nex_creator::register_in_join_map(std::map<nex*, rational, nex_lt>& map, ne
} }
} }
bool nex_creator::fill_join_map_for_sum(ptr_vector<nex> & children, bool nex_creator::fill_join_map_for_sum(
std::map<nex*, rational, nex_lt>& map, ptr_vector<nex> & children,
std::unordered_set<nex*>& existing_nex, std::map<nex*, rational, nex_lt>& map,
nex_scalar*& common_scalar) { std::unordered_set<nex*>& existing_nex,
nex_scalar*& common_scalar) {
common_scalar = nullptr; common_scalar = nullptr;
bool simplified = false; bool simplified = false;
for (auto e : children) { for (auto e : children) {
@ -690,7 +644,7 @@ 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;
int skipped = 0; int skipped = 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()) {
to_promote.push_back(e); to_promote.push_back(e);
@ -828,6 +782,7 @@ nex* nex_creator::simplify(nex* e) {
SASSERT(is_simplified(es)); SASSERT(is_simplified(es));
return es; return es;
} }
// adds to children the corrected expression and also adds to allocated the new expressions // adds to children the corrected expression and also adds to allocated the new expressions
void nex_creator::process_map_pair(nex *e, const rational& coeff, ptr_vector<nex> & children, std::unordered_set<nex*>& allocated_nexs) { void nex_creator::process_map_pair(nex *e, const rational& coeff, ptr_vector<nex> & children, std::unordered_set<nex*>& allocated_nexs) {
TRACE("grobner_d", tout << "e=" << *e << " , coeff= " << coeff << "\n";); TRACE("grobner_d", tout << "e=" << *e << " , coeff= " << coeff << "\n";);
@ -870,6 +825,7 @@ unsigned nex_creator::find_sum_in_mul(const nex_mul* a) const {
return -1; return -1;
} }
nex* nex_creator::canonize_mul(nex_mul *a) { nex* nex_creator::canonize_mul(nex_mul *a) {
TRACE("grobner_d", tout << "a = " << *a << "\n";); TRACE("grobner_d", tout << "a = " << *a << "\n";);
unsigned j = find_sum_in_mul(a); unsigned j = find_sum_in_mul(a);
@ -897,7 +853,6 @@ nex* nex_creator::canonize_mul(nex_mul *a) {
return canonize(r); return canonize(r);
} }
nex* nex_creator::canonize(const nex *a) { nex* nex_creator::canonize(const nex *a) {
if (a->is_elementary()) if (a->is_elementary())
return clone(a); return clone(a);

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

@ -29,22 +29,21 @@ struct occ {
occ(unsigned k, unsigned p) : m_occs(k), m_power(p) {} occ(unsigned k, unsigned p) : m_occs(k), m_power(p) {}
// use the "name injection rule here" // use the "name injection rule here"
friend std::ostream& operator<<(std::ostream& out, const occ& c) { friend std::ostream& operator<<(std::ostream& out, const occ& c) {
out << "(occs:" << c.m_occs <<", pow:" << c.m_power << ")"; return out << "(occs:" << c.m_occs <<", pow:" << c.m_power << ")";
return out;
} }
}; };
enum class var_weight { enum var_weight {
FIXED = 0, FIXED = 0,
QUOTED_FIXED = 1, QUOTED_FIXED = 1,
BOUNDED = 2, BOUNDED = 2,
QUOTED_BOUNDED = 3, QUOTED_BOUNDED = 3,
NOT_FREE = 4, NOT_FREE = 4,
QUOTED_NOT_FREE = 5, QUOTED_NOT_FREE = 5,
FREE = 6, FREE = 6,
QUOTED_FREE = 7, QUOTED_FREE = 7,
MAX_DEFAULT_WEIGHT = 7 MAX_DEFAULT_WEIGHT = 7
}; };
// the purpose of this class is to create nex objects, keep them, // the purpose of this class is to create nex objects, keep them,
@ -54,14 +53,13 @@ class nex_creator {
ptr_vector<nex> m_allocated; ptr_vector<nex> m_allocated;
std::unordered_map<lpvar, occ> m_occurences_map; std::unordered_map<lpvar, occ> m_occurences_map;
std::unordered_map<lpvar, unsigned> m_powers; std::unordered_map<lpvar, unsigned> m_powers;
svector<unsigned> m_active_vars_weights; unsigned_vector m_active_vars_weights;
public: public:
static std::string ch(unsigned j) { static std::string ch(unsigned j) {
std::stringstream s; std::stringstream s;
s << "v" << j; s << "v" << j;
return s.str(); return s.str();
// return (char)('a'+j);
} }
// assuming that every lpvar is less than this number // assuming that every lpvar is less than this number
@ -72,11 +70,11 @@ public:
unsigned get_number_of_vars() const { unsigned get_number_of_vars() const {
return m_active_vars_weights.size(); return m_active_vars_weights.size();
} }
void set_var_weight(unsigned j, unsigned weight) { void set_var_weight(unsigned j, unsigned weight) {
m_active_vars_weights[j] = weight; m_active_vars_weights[j] = weight;
} }
private: private:
svector<unsigned>& active_vars_weights() { return m_active_vars_weights;} svector<unsigned>& active_vars_weights() { return m_active_vars_weights;}
const svector<unsigned>& active_vars_weights() const { return m_active_vars_weights;} const svector<unsigned>& active_vars_weights() const { return m_active_vars_weights;}
@ -84,8 +82,8 @@ public:
nex* simplify(nex* e); nex* simplify(nex* e);
bool less_than(lpvar j, lpvar k) const{ bool less_than(lpvar j, lpvar k) const{
unsigned wj = (unsigned)m_active_vars_weights[j]; unsigned wj = m_active_vars_weights[j];
unsigned wk = (unsigned)m_active_vars_weights[k]; unsigned wk = m_active_vars_weights[k];
return wj != wk ? wj > wk : j > k; return wj != wk ? wj > wk : j > k;
} }
@ -97,15 +95,10 @@ public:
nex * clone(const nex* a) { nex * clone(const nex* a) {
switch (a->type()) { switch (a->type()) {
case expr_type::VAR: { case expr_type::VAR:
auto v = to_var(a); return mk_var(to_var(a)->var());
return mk_var(v->var()); case expr_type::SCALAR:
} return mk_scalar(to_scalar(a)->value());
case expr_type::SCALAR: {
auto v = to_scalar(a);
return mk_scalar(v->value());
}
case expr_type::MUL: { case expr_type::MUL: {
auto m = to_mul(a); auto m = to_mul(a);
auto r = mk_mul(); auto r = mk_mul();
@ -116,9 +109,8 @@ public:
return r; return r;
} }
case expr_type::SUM: { case expr_type::SUM: {
auto m = to_sum(a);
auto r = mk_sum(); auto r = mk_sum();
for (nex * e : m->children()) { for (nex * e : *to_sum(a)) {
r->add_child(clone(e)); r->add_child(clone(e));
} }
return r; return r;
@ -181,7 +173,6 @@ public:
r->children() = v; r->children() = v;
return r; return r;
} }
template <typename K, typename...Args> template <typename K, typename...Args>
nex_sum* mk_sum(K e, Args... es) { nex_sum* mk_sum(K e, Args... es) {
@ -191,6 +182,7 @@ public:
add_children(r, es...); add_children(r, es...);
return r; return r;
} }
nex_var* mk_var(lpvar j) { nex_var* mk_var(lpvar j) {
auto r = new nex_var(j); auto r = new nex_var(j);
add_to_allocated(r); add_to_allocated(r);
@ -239,8 +231,8 @@ public:
void sort_join_sum(ptr_vector<nex> & children); void sort_join_sum(ptr_vector<nex> & children);
bool fill_join_map_for_sum(ptr_vector<nex> & children, bool fill_join_map_for_sum(ptr_vector<nex> & children,
std::map<nex*, rational, nex_lt>& map, std::map<nex*, rational, nex_lt>& map,
std::unordered_set<nex*>& existing_nex, std::unordered_set<nex*>& existing_nex,
nex_scalar*& common_scalar); nex_scalar*& common_scalar);
bool register_in_join_map(std::map<nex*, rational, nex_lt>&, nex*, const rational&) const; bool register_in_join_map(std::map<nex*, rational, nex_lt>&, nex*, const rational&) const;
@ -252,11 +244,11 @@ public:
bool children_are_simplified(const vector<nex_pow>& children) const; bool children_are_simplified(const vector<nex_pow>& children) const;
bool lt(const nex* a, const nex* b) const; bool lt(const nex* a, const nex* b) const;
bool lt_nex_powers(const vector<nex_pow>&, const nex* b) const; bool lt_nex_powers(const vector<nex_pow>&, const nex* b) const;
bool less_than_on_powers_mul(const vector<nex_pow>&, const nex_mul* b) const; bool less_than_on_powers_mul(const vector<nex_pow>&, const nex_mul& b) const;
bool less_than_on_powers_mul_same_degree(const vector<nex_pow>&, const nex_mul* b) const; bool less_than_on_powers_mul_same_degree(const vector<nex_pow>&, const nex_mul& b) const;
bool lt_for_sort_join_sum(const nex* a, const nex* b) const; bool lt_for_sort_join_sum(const nex* a, const nex* b) const;
bool less_than_on_mul_mul(const nex_mul* a, const nex_mul* b) const; bool less_than_on_mul_mul(const nex_mul& a, const nex_mul& b) const;
bool less_than_on_mul_mul_same_degree(const nex_mul* a, const nex_mul* b) const; bool less_than_on_mul_mul_same_degree(const nex_mul& a, const nex_mul& b) const;
bool less_than_on_var_nex(const nex_var* a, const nex* b) const; bool less_than_on_var_nex(const nex_var* a, const nex* b) const;
bool less_than_on_mul_nex(const nex_mul* a, const nex* b) const; bool less_than_on_mul_nex(const nex_mul* a, const nex* b) const;
bool less_than_on_sum_sum(const nex_sum* a, const nex_sum* b) const; bool less_than_on_sum_sum(const nex_sum* a, const nex_sum* b) const;

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

@ -178,7 +178,7 @@ void nla_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);
m_equations_to_delete[eq->m_bidx] = 0; m_equations_to_delete[eq->m_bidx] = nullptr;
dealloc(eq); dealloc(eq);
} }