mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 12:28:44 +00:00
move sorting of nex expressions to nex_creator
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
8cd9989dcf
commit
090851559b
|
|
@ -26,7 +26,7 @@ z3_add_component(lp
|
|||
lp_utils.cpp
|
||||
matrix.cpp
|
||||
mon_eq.cpp
|
||||
nex.cpp
|
||||
nex_creator.cpp
|
||||
nla_basics_lemmas.cpp
|
||||
nla_common.cpp
|
||||
nla_core.cpp
|
||||
|
|
|
|||
|
|
@ -35,7 +35,7 @@ class cross_nested {
|
|||
int m_reported;
|
||||
bool m_random_bit;
|
||||
nex_creator m_nex_creator;
|
||||
nex_lt m_lt;
|
||||
const lt_on_vars& m_lt;
|
||||
std::function<nex_scalar*()> m_mk_scalar;
|
||||
#ifdef Z3DEBUG
|
||||
nex* m_e_clone;
|
||||
|
|
@ -47,14 +47,12 @@ public:
|
|||
cross_nested(std::function<bool (const nex*)> call_on_result,
|
||||
std::function<bool (unsigned)> var_is_fixed,
|
||||
std::function<unsigned ()> random,
|
||||
nex_lt lt):
|
||||
lt_on_vars 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_lt(lt),
|
||||
m_mk_scalar([this]{return m_nex_creator.mk_scalar(rational(1));})
|
||||
{}
|
||||
|
||||
|
|
|
|||
|
|
@ -93,9 +93,7 @@ bool horner::lemmas_on_row(const T& row) {
|
|||
[this](const nex* n) { return check_cross_nested_expr(n); },
|
||||
[this](unsigned j) { return c().var_is_fixed(j); },
|
||||
[this]() { return c().random(); },
|
||||
[](const nex* a, const nex* b) { return
|
||||
less_than_nex(a, b, [](lpvar j, lpvar k) { return j < k;}); }
|
||||
);
|
||||
[](lpvar j, lpvar k) { return j < k;}); // todo : consider using weights here - the same way they are used in Grobner basis
|
||||
|
||||
SASSERT (row_is_interesting(row));
|
||||
create_sum_from_row(row, cn.get_nex_creator(), m_row_sum);
|
||||
|
|
|
|||
|
|
@ -1,198 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2017 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
<name>
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
Lev Nachmanson (levnach)
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
#include "math/lp/nex.h"
|
||||
#include <map>
|
||||
namespace nla {
|
||||
|
||||
|
||||
bool is_zero_scalar(nex* e) {
|
||||
return e->is_scalar() && to_scalar(e)->value().is_zero();
|
||||
}
|
||||
|
||||
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));
|
||||
}
|
||||
|
||||
std::sort(children.begin(), children.end(), [lt](const nex_pow& a, const nex_pow& b) {
|
||||
return less_than(a, b, lt);
|
||||
});
|
||||
}
|
||||
|
||||
rational extract_coeff(const nex_mul* m) {
|
||||
const nex* e = m->children().begin()->e();
|
||||
if (e->is_scalar())
|
||||
return to_scalar(e)->value();
|
||||
return rational(1);
|
||||
}
|
||||
|
||||
|
||||
bool sum_simplify_lt(const nex_mul* a, const nex_mul* b, const nex_lt& lt) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
}
|
||||
|
||||
// a + 3bc + 2bc => a + 5bc
|
||||
void sort_join_sum(ptr_vector<nex> & children, nex_lt& lt, std::function<nex_scalar*()> mk_scalar) {
|
||||
ptr_vector<nex> non_muls;
|
||||
std::map<nex_mul*, rational, std::function<bool(const nex_mul *a , const nex_mul *b)>>
|
||||
m([lt](const nex_mul *a , const nex_mul *b) { return sum_simplify_lt(a, b, lt); });
|
||||
for (nex* e : children) {
|
||||
SASSERT(e->is_simplified(lt));
|
||||
if (!e->is_mul()) {
|
||||
non_muls.push_back(e);
|
||||
} else {
|
||||
nex_mul * em = to_mul(e);
|
||||
rational r = extract_coeff(em);
|
||||
auto it = m.find(em);
|
||||
if (it == m.end()) {
|
||||
m[em] = r;
|
||||
} else {
|
||||
it->second += r;
|
||||
}
|
||||
}
|
||||
}
|
||||
NOT_IMPLEMENTED_YET();
|
||||
}
|
||||
|
||||
void simplify_children_of_sum(ptr_vector<nex> & children, nex_lt lt, std::function<nex_scalar*()> mk_scalar ) {
|
||||
ptr_vector<nex> to_promote;
|
||||
int skipped = 0;
|
||||
for(unsigned j = 0; j < children.size(); j++) {
|
||||
nex** e = &(children[j]);
|
||||
(*e)->simplify(e, lt, mk_scalar);
|
||||
if ((*e)->is_sum()) {
|
||||
to_promote.push_back(*e);
|
||||
} else if (is_zero_scalar(*e)) {
|
||||
skipped ++;
|
||||
continue;
|
||||
} else {
|
||||
unsigned offset = to_promote.size() + skipped;
|
||||
if (offset) {
|
||||
children[j - offset] = *e;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
children.shrink(children.size() - to_promote.size() - skipped);
|
||||
|
||||
for (nex *e : to_promote) {
|
||||
for (nex *ee : *(to_sum(e)->children_ptr())) {
|
||||
if (!is_zero_scalar(ee))
|
||||
children.push_back(ee);
|
||||
}
|
||||
}
|
||||
|
||||
sort_join_sum(children, lt, mk_scalar);
|
||||
}
|
||||
|
||||
bool eat_scalar_pow(nex_scalar *& r, nex_pow& p) {
|
||||
if (!p.e()->is_scalar())
|
||||
return false;
|
||||
nex_scalar *pe = to_scalar(p.e());
|
||||
if (r == nullptr) {
|
||||
r = pe;
|
||||
r->value() = r->value().expt(p.pow());
|
||||
} else {
|
||||
r->value() *= pe->value().expt(p.pow());
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
void simplify_children_of_mul(vector<nex_pow> & children, nex_lt lt, std::function<nex_scalar*()> mk_scalar) {
|
||||
nex_scalar* r = nullptr;
|
||||
TRACE("nla_cn_details", print_vector(children, tout););
|
||||
vector<nex_pow> to_promote;
|
||||
int skipped = 0;
|
||||
for(unsigned j = 0; j < children.size(); j++) {
|
||||
nex_pow& p = children[j];
|
||||
if (eat_scalar_pow(r, p)) {
|
||||
skipped++;
|
||||
continue;
|
||||
}
|
||||
(p.e())->simplify(p.ee(), lt, mk_scalar );
|
||||
if ((p.e())->is_mul()) {
|
||||
to_promote.push_back(p);
|
||||
} else {
|
||||
unsigned offset = to_promote.size() + skipped;
|
||||
if (offset) {
|
||||
children[j - offset] = p;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
children.shrink(children.size() - to_promote.size() - skipped);
|
||||
|
||||
for (nex_pow & p : to_promote) {
|
||||
for (nex_pow& pp : to_mul(p.e())->children()) {
|
||||
if (!eat_scalar_pow(r, pp))
|
||||
children.push_back(nex_pow(pp.e(), pp.pow() * p.pow()));
|
||||
}
|
||||
}
|
||||
|
||||
if (r != nullptr) {
|
||||
children.push_back(nex_pow(r));
|
||||
}
|
||||
|
||||
mul_to_powers(children, lt);
|
||||
|
||||
TRACE("nla_cn_details", print_vector(children, tout););
|
||||
}
|
||||
|
||||
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;
|
||||
}
|
||||
SASSERT(a->type() == b->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;
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -79,13 +79,7 @@ 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, nex_lt, std::function<nex_scalar*()>) = 0;
|
||||
void simplify(nex** e, std::function<nex_scalar*()> mk_scalar) { return simplify(e, less_than_nex_standard, mk_scalar); }
|
||||
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() {};
|
||||
|
|
@ -116,7 +110,6 @@ public:
|
|||
bool contains(lpvar j) const { return j == m_j; }
|
||||
int get_degree() const { return 1; }
|
||||
bool virtual is_linear() const { return true; }
|
||||
void simplify(nex** e, nex_lt, std::function<nex_scalar*()>) {*e = this;}
|
||||
};
|
||||
|
||||
class nex_scalar : public nex {
|
||||
|
|
@ -134,18 +127,12 @@ public:
|
|||
|
||||
int get_degree() const { return 0; }
|
||||
bool is_linear() const { return true; }
|
||||
void simplify(nex** e, nex_lt, std::function<nex_scalar*()>) {*e = this;}
|
||||
|
||||
};
|
||||
|
||||
const nex_scalar * to_scalar(const nex* a);
|
||||
class nex_sum;
|
||||
const nex_sum* to_sum(const nex*a);
|
||||
|
||||
void simplify_children_of_sum(ptr_vector<nex> & children, nex_lt, std::function<nex_scalar*()>);
|
||||
class nex_pow;
|
||||
void simplify_children_of_mul(vector<nex_pow> & children, nex_lt, std::function<nex_scalar*()>);
|
||||
|
||||
class nex_pow {
|
||||
nex* m_e;
|
||||
int m_power;
|
||||
|
|
@ -153,7 +140,8 @@ public:
|
|||
explicit nex_pow(nex* e): m_e(e), m_power(1) {}
|
||||
explicit nex_pow(nex* e, int p): m_e(e), m_power(p) {}
|
||||
const nex * e() const { return m_e; }
|
||||
nex * e() { return m_e; }
|
||||
nex *& e() { return m_e; }
|
||||
|
||||
nex ** ee() { return & m_e; }
|
||||
int pow() const { return m_power; }
|
||||
int& pow() { return m_power; }
|
||||
|
|
@ -169,10 +157,8 @@ public:
|
|||
friend std::ostream& operator<<(std::ostream& out, const nex_pow & p) { out << p.to_string(); return out; }
|
||||
};
|
||||
|
||||
bool less_than_nex(const nex* a, const nex* b, const lt_on_vars& lt);
|
||||
|
||||
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 {
|
||||
|
|
@ -240,50 +226,6 @@ public:
|
|||
}
|
||||
return degree;
|
||||
}
|
||||
// the second argument is the comparison less than operator
|
||||
void simplify(nex **e, nex_lt lt, std::function<nex_scalar*()> mk_scalar) {
|
||||
TRACE("nla_cn_details", tout << *this << "\n";);
|
||||
TRACE("nla_cn_details", tout << "**e = " << **e << "\n";);
|
||||
*e = this;
|
||||
TRACE("nla_cn_details", tout << *this << "\n";);
|
||||
simplify_children_of_mul(m_children, lt, mk_scalar);
|
||||
if (size() == 1 && m_children[0].pow() == 1)
|
||||
*e = m_children[0].e();
|
||||
TRACE("nla_cn_details", tout << *this << "\n";);
|
||||
SASSERT((*e)->is_simplified(lt));
|
||||
}
|
||||
|
||||
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());
|
||||
|
|
@ -364,24 +306,6 @@ public:
|
|||
return out;
|
||||
}
|
||||
|
||||
void simplify(nex **e, nex_lt lt, std::function<nex_scalar*()> mk_scalar) {
|
||||
*e = this;
|
||||
simplify_children_of_sum(m_children, lt, mk_scalar);
|
||||
if (size() == 1)
|
||||
*e = m_children[0];
|
||||
}
|
||||
|
||||
virtual bool is_simplified() const {
|
||||
if (size() < 2) return false;
|
||||
for (nex * e : children()) {
|
||||
if (e->is_sum())
|
||||
return false;
|
||||
if (e->is_scalar() && to_scalar(e)->value().is_zero())
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
int get_degree() const {
|
||||
int degree = 0;
|
||||
for (auto e : children()) {
|
||||
|
|
@ -446,9 +370,6 @@ inline std::ostream& operator<<(std::ostream& out, const nex& e ) {
|
|||
return e.print(out);
|
||||
}
|
||||
|
||||
|
||||
bool less_than_nex(const nex* a, const nex* b, lt_on_vars lt);
|
||||
|
||||
inline bool less_than_nex_standard(const nex* a, const nex* b) {
|
||||
lt_on_vars lt = [](lpvar j, lpvar k) { return j < k; };
|
||||
return less_than_nex(a, b, lt);
|
||||
|
|
|
|||
|
|
@ -18,6 +18,7 @@
|
|||
|
||||
--*/
|
||||
#pragma once
|
||||
#include <map>
|
||||
#include "math/lp/nex.h"
|
||||
namespace nla {
|
||||
|
||||
|
|
@ -33,17 +34,57 @@ struct occ {
|
|||
}
|
||||
};
|
||||
|
||||
enum class var_weight {
|
||||
FIXED = 0,
|
||||
QUOTED_FIXED = 1,
|
||||
BOUNDED = 2,
|
||||
QUOTED_BOUNDED = 3,
|
||||
NOT_FREE = 4,
|
||||
QUOTED_NOT_FREE = 5,
|
||||
FREE = 6,
|
||||
QUOTED_FREE = 7,
|
||||
MAX_DEFAULT_WEIGHT = 7
|
||||
};
|
||||
|
||||
// the purpose of this class is to create nex objects, keep them, and delete them
|
||||
|
||||
// the purpose of this class is to create nex objects, keep them,
|
||||
// sort them, and delete them
|
||||
|
||||
class nex_creator {
|
||||
|
||||
ptr_vector<nex> m_allocated;
|
||||
std::unordered_map<lpvar, occ> m_occurences_map;
|
||||
std::unordered_map<lpvar, unsigned> m_powers;
|
||||
// the "less than" operator on expressions
|
||||
nex_lt m_lt;
|
||||
svector<var_weight> m_active_vars_weights;
|
||||
|
||||
public:
|
||||
|
||||
nex* simplify(nex* e) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
}
|
||||
|
||||
rational extract_coeff_from_mul(const nex_mul* m);
|
||||
|
||||
rational extract_coeff(const nex* );
|
||||
|
||||
bool is_simplified(const nex *e) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
}
|
||||
|
||||
bool less_than(lpvar j, lpvar k) const{
|
||||
unsigned wj = (unsigned)m_active_vars_weights[j];
|
||||
unsigned wk = (unsigned)m_active_vars_weights[k];
|
||||
return wj != wk ? wj < wk : j < k;
|
||||
}
|
||||
|
||||
bool less_than_nex(const nex* a, const nex* b) const;
|
||||
|
||||
bool less_than_on_nex_pow(const nex_pow & a, const nex_pow& b) const {
|
||||
return (a.pow() < b.pow()) || (a.pow() == b.pow() && less_than_nex(a.e(), b.e()));
|
||||
}
|
||||
|
||||
void simplify_children_of_mul(vector<nex_pow> & children);
|
||||
|
||||
|
||||
nex * clone(const nex* a) {
|
||||
switch (a->type()) {
|
||||
case expr_type::VAR: {
|
||||
|
|
@ -77,7 +118,7 @@ public:
|
|||
}
|
||||
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; }
|
||||
|
|
@ -162,104 +203,60 @@ 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";);
|
||||
SASSERT((a->is_mul() && a->contains(j)) || (a->is_var() && to_var(a)->var() == j));
|
||||
if (a->is_var())
|
||||
return mk_scalar(rational(1));
|
||||
vector<nex_pow> bv;
|
||||
bool seenj = false;
|
||||
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(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;
|
||||
}
|
||||
} else {
|
||||
bv.push_back(nex_pow(clone(c)));
|
||||
}
|
||||
}
|
||||
if (bv.size() > 1) {
|
||||
return mk_mul(bv);
|
||||
}
|
||||
if (bv.size() == 1 && bv.begin()->pow() == 1) {
|
||||
return bv.begin()->e();
|
||||
}
|
||||
if (bv.size() == 0)
|
||||
return mk_scalar(rational(1));
|
||||
return mk_mul(bv);
|
||||
}
|
||||
|
||||
nex * mk_div(const nex* a, const nex* b) {
|
||||
TRACE("nla_cn_details", tout <<"(" << *a << ") / (" << *b << ")\n";);
|
||||
if (b->is_var()) {
|
||||
return mk_div(a, to_var(b)->var());
|
||||
}
|
||||
SASSERT(b->is_mul());
|
||||
const nex_mul *bm = to_mul(b);
|
||||
if (a->is_sum()) {
|
||||
nex_sum * r = mk_sum();
|
||||
const nex_sum * m = to_sum(a);
|
||||
for (auto e : m->children()) {
|
||||
r->add_child(mk_div(e, bm));
|
||||
}
|
||||
TRACE("nla_cn_details", tout << *r << "\n";);
|
||||
return r;
|
||||
}
|
||||
if (a->is_var() || (a->is_mul() && to_mul(a)->children().size() == 1)) {
|
||||
return mk_scalar(rational(1));
|
||||
}
|
||||
SASSERT(a->is_mul());
|
||||
|
||||
const nex_mul* am = to_mul(a);
|
||||
bm->get_powers_from_mul(m_powers);
|
||||
TRACE("nla_cn_details", print_vector(m_powers, tout););
|
||||
nex_mul* ret = new nex_mul();
|
||||
for (const nex_pow& p : am->children()) {
|
||||
const nex *e = p.e();
|
||||
TRACE("nla_cn_details", tout << "e=" << *e << "\n";);
|
||||
|
||||
if (!e->is_var()) {
|
||||
SASSERT(e->is_scalar());
|
||||
ret->add_child(mk_scalar(to_scalar(e)->value()));
|
||||
TRACE("nla_cn_details", tout << "continue\n";);
|
||||
continue;
|
||||
}
|
||||
SASSERT(e->is_var());
|
||||
lpvar j = to_var(e)->var();
|
||||
auto it = m_powers.find(j);
|
||||
if (it == m_powers.end()) {
|
||||
ret->add_child(mk_var(j));
|
||||
} else {
|
||||
it->second --;
|
||||
if (it->second == 0)
|
||||
m_powers.erase(it);
|
||||
}
|
||||
TRACE("nla_cn_details", tout << *ret << "\n";);
|
||||
}
|
||||
SASSERT(m_powers.size() == 0);
|
||||
if (ret->children().size() == 0) {
|
||||
delete ret;
|
||||
TRACE("nla_cn_details", tout << "return 1\n";);
|
||||
return mk_scalar(rational(1));
|
||||
}
|
||||
add_to_allocated(ret);
|
||||
TRACE("nla_cn_details", tout << *ret << "\n";);
|
||||
return ret;
|
||||
nex * mk_div(const nex* a, lpvar j);
|
||||
nex * mk_div(const nex* a, const nex* b);
|
||||
|
||||
nex * simplify_mul(nex_mul *e);
|
||||
bool is_sorted(const nex_mul * e) const;
|
||||
bool mul_is_simplified(const nex_mul*e ) const;
|
||||
|
||||
nex* simplify_sum(nex_sum *e);
|
||||
|
||||
bool sum_is_simplified(nex_sum* e) const;
|
||||
|
||||
void mul_to_powers(vector<nex_pow>& children);
|
||||
|
||||
nex* create_child_from_nex_and_coeff(nex *e,
|
||||
const rational& coeff) ;
|
||||
|
||||
void sort_join_sum(ptr_vector<nex> & children);
|
||||
|
||||
void simplify_children_of_sum(ptr_vector<nex> & children);
|
||||
|
||||
bool eat_scalar_pow(nex_scalar *& r, nex_pow& p);
|
||||
void simplify_children_of_mul(vector<nex_pow> & children, lt_on_vars lt, std::function<nex_scalar*()> mk_scalar);
|
||||
|
||||
bool sum_simplify_lt(const nex* a, const nex* b);
|
||||
|
||||
bool less_than_nex(const nex* a, const nex* b, const lt_on_vars& lt) {
|
||||
int r = (int)(a->type()) - (int)(b->type());
|
||||
if (r) {
|
||||
return r < 0;
|
||||
}
|
||||
SASSERT(a->type() == b->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;
|
||||
}
|
||||
bool mul_simplify_lt(const nex_mul* a, const nex_mul* b);
|
||||
void fill_map_with_children(std::map<nex*, rational, nex_lt> & m, ptr_vector<nex> & children);
|
||||
};
|
||||
}
|
||||
|
|
|
|||
|
|
@ -26,8 +26,11 @@ nla_grobner::nla_grobner(core *c
|
|||
common(c),
|
||||
m_nl_gb_exhausted(false),
|
||||
m_dep_manager(m_val_manager, m_alloc),
|
||||
m_nex_creator([this](const nex* a, const nex* b) { return
|
||||
this->less_than_on_expr(a, b); }) {}
|
||||
m_nex_creator([this](lpvar a, lpvar b) {
|
||||
if (m_active_vars_weights[a] != m_active_vars_weights[b])
|
||||
return m_active_vars_weights[a] < m_active_vars_weights[b];
|
||||
return a < b;
|
||||
}) {}
|
||||
|
||||
// Scan the grobner basis eqs for equations of the form x - k = 0 or x = 0 is found, and x is not fixed,
|
||||
// then assert bounds for x, and continue
|
||||
|
|
|
|||
|
|
@ -36,17 +36,6 @@ struct grobner_stats {
|
|||
grobner_stats() { reset(); }
|
||||
};
|
||||
|
||||
enum class var_weight {
|
||||
FIXED = 0,
|
||||
QUOTED_FIXED = 1,
|
||||
BOUNDED = 2,
|
||||
QUOTED_BOUNDED = 3,
|
||||
NOT_FREE = 4,
|
||||
QUOTED_NOT_FREE = 5,
|
||||
FREE = 6,
|
||||
QUOTED_FREE = 7,
|
||||
MAX_DEFAULT_WEIGHT = 7
|
||||
};
|
||||
|
||||
class nla_grobner : common {
|
||||
|
||||
|
|
@ -90,7 +79,6 @@ class nla_grobner : common {
|
|||
equation_vector m_equations_to_delete;
|
||||
lp::int_set m_rows;
|
||||
lp::int_set m_active_vars;
|
||||
svector<var_weight> m_active_vars_weights;
|
||||
unsigned m_num_of_equations;
|
||||
grobner_stats m_stats;
|
||||
equation_set m_processed;
|
||||
|
|
@ -158,21 +146,21 @@ private:
|
|||
return rational(1);
|
||||
}
|
||||
|
||||
bool less_than_on_vars(lpvar a, lpvar b) const {
|
||||
const auto &aw = m_active_vars_weights[a];
|
||||
const auto &ab = m_active_vars_weights[b];
|
||||
if (aw < ab)
|
||||
return true;
|
||||
if (aw > ab)
|
||||
return false;
|
||||
// aw == ab
|
||||
return a < b;
|
||||
}
|
||||
// bool less_than_on_vars(lpvar a, lpvar b) const {
|
||||
// const auto &aw = m_nex_creatorm_active_vars_weights[a];
|
||||
// const auto &ab = m_active_vars_weights[b];
|
||||
// if (aw < ab)
|
||||
// return true;
|
||||
// if (aw > ab)
|
||||
// return false;
|
||||
// // aw == ab
|
||||
// return a < b;
|
||||
// }
|
||||
|
||||
bool less_than_on_expr(const nex* a, const nex* b) const {
|
||||
lt_on_vars lt = [this](lpvar j, lpvar k) {return less_than_on_vars(j, k);};
|
||||
return less_than_nex(a, b, lt);
|
||||
}
|
||||
// bool less_than_on_expr(const nex* a, const nex* b) const {
|
||||
// lt_on_vars lt = [this](lpvar j, lpvar k) {return less_than_on_vars(j, k);};
|
||||
// return less_than_nex(a, b, lt);
|
||||
// }
|
||||
|
||||
|
||||
}; // end of grobner
|
||||
|
|
|
|||
|
|
@ -73,6 +73,8 @@ void test_cn_on_expr(nex_sum *t, cross_nested& cn) {
|
|||
cn.run(t);
|
||||
}
|
||||
|
||||
lt_on_vars lpvar_lt() { return [](lpvar a, lpvar b) { return a < b; };}
|
||||
|
||||
void test_simplify() {
|
||||
cross_nested cn(
|
||||
[](const nex* n) {
|
||||
|
|
@ -80,9 +82,7 @@ void test_simplify() {
|
|||
return false;
|
||||
} ,
|
||||
[](unsigned) { return false; },
|
||||
[]{ return 1; },
|
||||
less_than_nex_standard
|
||||
);
|
||||
[]{ return 1; }, lpvar_lt());
|
||||
enable_trace("nla_cn");
|
||||
enable_trace("nla_cn_details");
|
||||
nex_creator & r = cn.get_nex_creator();
|
||||
|
|
@ -104,11 +104,11 @@ void test_simplify() {
|
|||
nex * e = r.mk_sum(a, r.mk_sum(b, m));
|
||||
TRACE("nla_cn", tout << "e = " << *e << "\n";);
|
||||
std::function<nex_scalar*()> mks = [&r] {return r.mk_scalar(rational(1)); };
|
||||
e->simplify(&e, mks);
|
||||
e->simplify(&e, lpvar_lt(), mks);
|
||||
TRACE("nla_cn", tout << "simplified e = " << *e << "\n";);
|
||||
nex * l = r.mk_sum(e, r.mk_mul(r.mk_scalar(rational(3)), r.clone(e)));
|
||||
TRACE("nla_cn", tout << "sum l = " << *l << "\n";);
|
||||
l->simplify(&l, mks);
|
||||
l->simplify(&l, lpvar_lt(), mks);
|
||||
TRACE("nla_cn", tout << "simplified sum l = " << *l << "\n";);
|
||||
}
|
||||
|
||||
|
|
@ -119,9 +119,7 @@ void test_cn() {
|
|||
return false;
|
||||
} ,
|
||||
[](unsigned) { return false; },
|
||||
[]{ return 1; },
|
||||
less_than_nex_standard
|
||||
);
|
||||
[]{ return 1; }, lpvar_lt());
|
||||
enable_trace("nla_cn");
|
||||
enable_trace("nla_cn_details");
|
||||
nex_var* a = cn.get_nex_creator().mk_var(0);
|
||||
|
|
@ -147,8 +145,8 @@ void test_cn() {
|
|||
nex* _6aad = cn.get_nex_creator().mk_mul(cn.get_nex_creator().mk_scalar(rational(6)), a, a, d);
|
||||
#ifdef Z3DEBUG
|
||||
nex * clone = cn.get_nex_creator().clone(cn.get_nex_creator().mk_sum(_6aad, abcd, aaccd, add, eae, eac, ed));
|
||||
clone->simplify(&clone,[&cn] {return cn.get_nex_creator().mk_scalar(rational(1));});
|
||||
SASSERT(clone->is_simplified());
|
||||
clone->simplify(&clone, lpvar_lt(), [&cn] {return cn.get_nex_creator().mk_scalar(rational(1));});
|
||||
SASSERT(clone->is_simplified(lpvar_lt()));
|
||||
TRACE("nla_cn", tout << "clone = " << *clone << "\n";);
|
||||
#endif
|
||||
// test_cn_on_expr(cn.get_nex_creator().mk_sum(aad, abcd, aaccd, add, eae, eac, ed), cn);
|
||||
|
|
|
|||
Loading…
Reference in a new issue