mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

sort expressions by power

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-09-25 16:46:50 -07:00
parent 705607fba0
commit 4e2cd2c8de
6 changed files with 202 additions and 83 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -35,7 +35,7 @@ class cross_nested {
int m_reported;
bool m_random_bit;
nex_creator m_nex_creator;
std::function<bool (const nex*, const nex*)> m_lt;
nex_lt m_lt;
#ifdef Z3DEBUG
nex* m_e_clone;
@ -47,18 +47,19 @@ public:
cross_nested(std::function<bool (const nex*)> call_on_result,
std::function<bool (unsigned)> var_is_fixed,
std::function<unsigned ()> random,
std::function<bool (const nex*, const nex*)> lt):
nex_lt lt):
m_call_on_result(call_on_result),
m_var_is_fixed(var_is_fixed),
m_random(random),
m_done(false),
m_reported(0),
m_nex_creator(lt) {}
m_nex_creator(lt),
m_lt(lt) {}
void run(nex *e) {
TRACE("nla_cn", tout << *e << "\n";);
SASSERT(e->is_simplified());
SASSERT(e->is_simplified(m_lt));
m_e = e;
#ifdef Z3DEBUG
// m_e_clone = clone(m_e);
@ -482,40 +483,6 @@ public:
bool done() const { return m_done; }
#if Z3DEBUG
nex *clone (const nex * a) {
switch (a->type()) {
case expr_type::VAR: {
auto v = to_var(a);
return m_nex_creator.mk_var(v->var());
}
case expr_type::SCALAR: {
auto v = to_scalar(a);
return m_nex_creator.mk_scalar(v->value());
}
case expr_type::MUL: {
auto m = to_mul(a);
auto r = m_nex_creator.mk_mul();
for (const auto& p : m->children()) {
r->add_child_in_power(clone(p.e()), p.pow());
}
return r;
}
case expr_type::SUM: {
auto m = to_sum(a);
auto r = m_nex_creator.mk_sum();
for (nex * e : m->children()) {
r->add_child(clone(e));
}
return r;
}
default:
SASSERT(false);
break;
}
return nullptr;
}
nex * normalize_sum(nex_sum* a) {
for (unsigned j = 0; j < a->size(); j ++) {
a->children()[j] = normalize(a->children()[j]);

26
src/math/lp/nex.cpp
View file

@ -18,6 +18,7 @@
--*/
#include "math/lp/nex.h"
#include <map>
namespace nla {
@ -32,9 +33,28 @@ bool ignored_child(nex* e, expr_type t) {
return false;
}
void mul_to_powers(vector<nex_pow>& children, nex_lt lt) {
std::map<nex*, int, nex_lt> m(lt);
for (auto & p : children) {
auto it = m.find(p.e());
if (it == m.end()) {
m[p.e()] = p.pow();
} else {
it->second+= p.pow();
}
}
children.clear();
for (auto & p : m) {
children.push_back(nex_pow(p.first, p.second));
}
void promote_children_of_sum(ptr_vector<nex> & children,std::function<bool (const nex*, const nex*)> lt ) {
std::sort(children.begin(), children.end(), [lt](const nex_pow& a, const nex_pow& b) {
return less_than(a, b, lt);
});
}
void promote_children_of_sum(ptr_vector<nex> & children, nex_lt lt ) {
ptr_vector<nex> to_promote;
int skipped = 0;
for(unsigned j = 0; j < children.size(); j++) {
@ -63,7 +83,7 @@ void promote_children_of_sum(ptr_vector<nex> & children,std::function<bool (cons
}
}
void promote_children_of_mul(vector<nex_pow> & children, std::function<bool (const nex*, const nex*)> lt) {
void promote_children_of_mul(vector<nex_pow> & children, nex_lt lt) {
TRACE("nla_cn_details", print_vector(children, tout););
vector<nex_pow> to_promote;
int skipped = 0;
@ -92,6 +112,8 @@ void promote_children_of_mul(vector<nex_pow> & children, std::function<bool (con
}
}
mul_to_powers(children, lt);
TRACE("nla_cn_details", print_vector(children, tout););
}

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

@ -20,8 +20,14 @@
#include <initializer_list>
#include "math/lp/nla_defs.h"
#include <functional>
#include <set>
namespace nla {
enum class expr_type { VAR, SUM, MUL, SCALAR, UNDEF };
class nex;
typedef std::function<bool (const nex*, const nex*)> nex_lt;
typedef std::function<bool (lpvar, lpvar)> lt_on_vars;
enum class expr_type { SCALAR, VAR, SUM, MUL, UNDEF };
inline std::ostream & operator<<(std::ostream& out, expr_type t) {
switch (t) {
case expr_type::SUM:
@ -72,11 +78,14 @@ public:
virtual bool contains(lpvar j) const { return false; }
virtual int get_degree() const = 0;
// simplifies the expression and also assigns the address of "this" to *e
virtual void simplify(nex** e, std::function<bool (const nex*, const nex*)> lt) { *e = this; }
virtual void simplify(nex** e, nex_lt) { *e = this; }
void simplify(nex** e) { return simplify(e, less_than_nex_standard); }
virtual bool is_simplified() const {
virtual bool is_simplified(nex_lt) const {
return true;
}
virtual bool is_simplified() const { return is_simplified(less_than_nex_standard); }
#ifdef Z3DEBUG
virtual void sort() {};
#endif
@ -130,9 +139,9 @@ const nex_scalar * to_scalar(const nex* a);
class nex_sum;
const nex_sum* to_sum(const nex*a);
void promote_children_of_sum(ptr_vector<nex> & children, std::function<bool (const nex*, const nex*)>);
void promote_children_of_sum(ptr_vector<nex> & children, nex_lt);
class nex_pow;
void promote_children_of_mul(vector<nex_pow> & children, std::function<bool (const nex*, const nex*)> lt);
void promote_children_of_mul(vector<nex_pow> & children, nex_lt);
class nex_pow {
nex* m_e;
@ -145,11 +154,24 @@ public:
nex ** ee() { return & m_e; }
int pow() const { return m_power; }
int& pow() { return m_power; }
std::string to_string() const { std::stringstream s; s << "(" << *e() << ", " << pow() << ")";
return s.str(); }
std::string to_string() const {
std::stringstream s;
if (pow() == 1) {
s <<"(" << *e() << ")";
} else {
s << "(" << *e() << "^" << pow() << ")";
}
return s.str();
}
friend std::ostream& operator<<(std::ostream& out, const nex_pow & p) { out << p.to_string(); return out; }
};
inline bool less_than(const nex_pow & a, const nex_pow& b, nex_lt lt) {
return (a.pow() < b.pow()) || (a.pow() == b.pow() && lt(a.e(), b.e()));
}
class nex_mul : public nex {
vector<nex_pow> m_children;
public:
@ -216,7 +238,7 @@ public:
return degree;
}
// the second argument is the comparison less than operator
void simplify(nex **e, std::function<bool (const nex*, const nex*)> lt) {
void simplify(nex **e, nex_lt lt) {
TRACE("nla_cn_details", tout << *this << "\n";);
TRACE("nla_cn_details", tout << "**e = " << **e << "\n";);
*e = this;
@ -225,24 +247,43 @@ public:
if (size() == 1 && m_children[0].pow() == 1)
*e = m_children[0].e();
TRACE("nla_cn_details", tout << *this << "\n";);
SASSERT((*e)->is_simplified());
SASSERT((*e)->is_simplified(lt));
}
virtual bool is_simplified() const {
if (size() < 2)
return false;
for (const auto &p : children()) {
const nex* e = p.e();
if (e->is_mul())
return false;
if (e->is_scalar() && to_scalar(e)->value().is_one())
bool is_sorted(nex_lt lt) const {
for (unsigned j = 0; j < m_children.size() - 1; j++) {
if (!(less_than(m_children[j], m_children[j+1], lt)))
return false;
}
return true;
}
virtual bool is_simplified(nex_lt lt) const {
if (size() == 1 && m_children.begin()->pow() == 1)
return false;
std::set<const nex*, nex_lt> s(lt);
for (const auto &p : children()) {
const nex* e = p.e();
if (p.pow() == 0)
return false;
if (e->is_mul())
return false;
if (e->is_scalar() && to_scalar(e)->value().is_one())
return false;
auto it = s.find(e);
if (it == s.end()) {
s.insert(e);
} else {
TRACE("nla_cn_details", tout << "not simplified " << *e << "\n";);
return false;
}
}
return is_sorted(lt);
}
bool is_linear() const {
SASSERT(is_simplified());
// SASSERT(is_simplified());
return get_degree() < 2; // todo: make it more efficient
}
@ -320,7 +361,7 @@ public:
return out;
}
void simplify(nex **e, std::function<bool (const nex*, const nex*)> lt ) {
void simplify(nex **e, nex_lt lt ) {
*e = this;
promote_children_of_sum(m_children, lt);
if (size() == 1)
@ -398,8 +439,32 @@ inline std::ostream& operator<<(std::ostream& out, const nex& e ) {
}
inline bool less_than_nex(const nex* a, const nex* b, std::function<bool (lpvar, lpvar)> lt) {
NOT_IMPLEMENTED_YET();
inline bool less_than_nex(const nex* a, const nex* b, lt_on_vars lt) {
int r = (int)(a->type()) - (int)(b->type());
if (r) {
return r < 0;
}
// here a and b have the same type
switch (a->type()) {
case expr_type::VAR: {
return lt(to_var(a)->var() , to_var(b)->var());
}
case expr_type::SCALAR: {
return to_scalar(a)->value() < to_scalar(b)->value();
}
case expr_type::MUL: {
NOT_IMPLEMENTED_YET();
return false; // to_mul(a)->children() < to_mul(b)->children();
}
case expr_type::SUM: {
NOT_IMPLEMENTED_YET();
return false; //to_sum(a)->children() < to_sum(b)->children();
}
default:
SASSERT(false);
return false;
}
return false;
}

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

@ -42,9 +42,42 @@ class nex_creator {
std::unordered_map<lpvar, occ> m_occurences_map;
std::unordered_map<lpvar, unsigned> m_powers;
// the "less than" operator on expressions
std::function<bool (const nex*, const nex*)> m_lt;
nex_lt m_lt;
public:
nex_creator(std::function<bool (const nex*, const nex*)> lt) {}
nex * clone(const nex* a) {
switch (a->type()) {
case expr_type::VAR: {
auto v = to_var(a);
return mk_var(v->var());
}
case expr_type::SCALAR: {
auto v = to_scalar(a);
return mk_scalar(v->value());
}
case expr_type::MUL: {
auto m = to_mul(a);
auto r = mk_mul();
for (const auto& p : m->children()) {
r->add_child_in_power(clone(p.e()), p.pow());
}
return r;
}
case expr_type::SUM: {
auto m = to_sum(a);
auto r = mk_sum();
for (nex * e : m->children()) {
r->add_child(clone(e));
}
return r;
}
default:
UNREACHABLE();
break;
}
return nullptr;
}
nex_creator(nex_lt lt) : m_lt(lt) {}
const std::unordered_map<lpvar, occ>& occurences_map() const { return m_occurences_map; }
std::unordered_map<lpvar, occ>& occurences_map() { return m_occurences_map; }
const std::unordered_map<lpvar, unsigned> & powers() const { return m_powers; }
@ -129,37 +162,45 @@ public:
return r;
}
nex * mk_div(const nex* a, lpvar j) {
SASSERT(a->is_simplified(m_lt));
TRACE("nla_cn_details", tout << "a=" << *a << ", v" << j << "\n";);
NOT_IMPLEMENTED_YET();
return nullptr;
/*
SASSERT((a->is_mul() && a->contains(j)) || (a->is_var() && to_var(a)->var() == j));
if (a->is_var())
return mk_scalar(rational(1));
ptr_vector<nex> bv;
vector<nex_pow> bv;
bool seenj = false;
for (nex* c : to_mul(a)->children()) {
for (auto& p : to_mul(a)->children()) {
const nex * c = p.e();
int pow = p.pow();
if (!seenj) {
if (c->contains(j)) {
if (!c->is_var())
bv.push_back(mk_div(c, j));
if (!c->is_var()) {
bv.push_back(nex_pow(mk_div(c, j)));
if (pow != 1) {
bv.push_back(nex_pow(clone(c), pow));
}
} else {
SASSERT(to_var(c)->var() == j);
if (p.pow() != 1) {
bv.push_back(nex_pow(mk_var(j), pow - 1));
}
}
seenj = true;
continue;
}
} else {
bv.push_back(nex_pow(clone(c)));
}
bv.push_back(c);
}
if (bv.size() > 1) {
return mk_mul(bv);
}
if (bv.size() == 1) {
return bv[0];
if (bv.size() == 1 && bv.begin()->pow() == 1) {
return bv.begin()->e();
}
SASSERT(bv.size() == 0);
return mk_scalar(rational(1));*/
if (bv.size() == 0)
return mk_scalar(rational(1));
return mk_mul(bv);
}
nex * mk_div(const nex* a, const nex* b) {

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

@ -102,7 +102,7 @@ class nla_grobner : common {
ci_value_manager m_val_manager;
ci_dependency_manager m_dep_manager;
nex_creator m_nex_creator;
std::function<bool (const nex*, const nex*)> m_lt;
nex_lt m_lt;
public:
nla_grobner(core *core);
void grobner_lemmas();