mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 20:38:43 +00:00
rewrite horner scheme on top of nex_expr as a pointer
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
0f2c8c21ff
commit
9fbd0da931
|
|
@ -22,7 +22,6 @@
|
|||
#include "math/lp/nla_expr.h"
|
||||
namespace nla {
|
||||
class cross_nested {
|
||||
typedef nla_expr<rational> nex;
|
||||
struct occ {
|
||||
unsigned m_occs;
|
||||
unsigned m_power;
|
||||
|
|
@ -36,61 +35,179 @@ class cross_nested {
|
|||
};
|
||||
|
||||
// fields
|
||||
nex& m_e;
|
||||
std::function<bool (const nex&)> m_call_on_result;
|
||||
nex_sum * m_e;
|
||||
std::function<bool (const nex*)> m_call_on_result;
|
||||
std::function<bool (unsigned)> m_var_is_fixed;
|
||||
bool m_done;
|
||||
std::unordered_map<lpvar, occ> m_occurences_map;
|
||||
std::unordered_map<lpvar, unsigned> m_powers;
|
||||
|
||||
vector<nex*> m_allocated;
|
||||
vector<nex*> m_b_vec;
|
||||
public:
|
||||
cross_nested(nex &e,
|
||||
std::function<bool (const nex&)> call_on_result,
|
||||
cross_nested(std::function<bool (const nex*)> call_on_result,
|
||||
std::function<bool (unsigned)> var_is_fixed):
|
||||
m_e(e),
|
||||
m_call_on_result(call_on_result),
|
||||
m_var_is_fixed(var_is_fixed),
|
||||
m_done(false)
|
||||
{}
|
||||
|
||||
void run() {
|
||||
vector<nex*> front;
|
||||
explore_expr_on_front_elem(&m_e, front); // true for trivial form - no change
|
||||
void run(nex_sum *e) {
|
||||
m_e = e;
|
||||
|
||||
vector<nex_sum*> front;
|
||||
explore_expr_on_front_elem(m_e, front);
|
||||
}
|
||||
|
||||
static nex* pop_back(vector<nex*>& front) {
|
||||
nex* c = front.back();
|
||||
static nex_sum* pop_back(vector<nex_sum*>& front) {
|
||||
nex_sum* c = front.back();
|
||||
TRACE("nla_cn", tout << *c << "\n";);
|
||||
front.pop_back();
|
||||
return c;
|
||||
}
|
||||
|
||||
static bool extract_common_factor(nex* c, nex& f, const vector<std::pair<lpvar, occ>> & occurences) {
|
||||
nex_sum* mk_sum() {
|
||||
auto r = new nex_sum();
|
||||
m_allocated.push_back(r);
|
||||
return r;
|
||||
}
|
||||
|
||||
nex_sum* mk_sum(const vector<nex*>& v) {
|
||||
auto r = new nex_sum();
|
||||
m_allocated.push_back(r);
|
||||
r->children() = v;
|
||||
return r;
|
||||
}
|
||||
|
||||
nex_sum* mk_sum(nex *a, nex* b) {
|
||||
auto r = new nex_sum();
|
||||
m_allocated.push_back(r);
|
||||
r->children().push_back(a);
|
||||
r->children().push_back(b);
|
||||
return r;
|
||||
}
|
||||
|
||||
nex_var* mk_var(lpvar j) {
|
||||
auto r = new nex_var(j);
|
||||
m_allocated.push_back(r);
|
||||
return r;
|
||||
}
|
||||
|
||||
nex_mul* mk_mul() {
|
||||
auto r = new nex_mul();
|
||||
m_allocated.push_back(r);
|
||||
return r;
|
||||
}
|
||||
|
||||
nex_mul* mk_mul(nex * a, nex * b) {
|
||||
auto r = new nex_mul();
|
||||
m_allocated.push_back(r);
|
||||
r->add_child(a); r->add_child(b);
|
||||
return r;
|
||||
}
|
||||
|
||||
nex_mul* mk_mul(nex * a, nex * b, nex *c) {
|
||||
auto r = new nex_mul();
|
||||
m_allocated.push_back(r);
|
||||
r->add_child(a); r->add_child(b); r->add_child(c);
|
||||
return r;
|
||||
}
|
||||
|
||||
nex_scalar* mk_scalar(const rational& v) {
|
||||
auto r = new nex_scalar(v);
|
||||
m_allocated.push_back(r);
|
||||
return r;
|
||||
}
|
||||
|
||||
|
||||
nex * mk_div(const nex* a, lpvar j) {
|
||||
SASSERT(false);
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
nex * mk_div(const nex* a, const nex* b) {
|
||||
TRACE("nla_cn_details", tout << *a <<" / " << *b << "\n";);
|
||||
if (b->is_var()) {
|
||||
return mk_div(a, to_var(b)->var());
|
||||
}
|
||||
SASSERT(b->is_mul());
|
||||
const nex_mul *bm = to_mul(b);
|
||||
if (a->is_sum()) {
|
||||
nex_sum * r = mk_sum();
|
||||
const nex_sum * m = to_sum(a);
|
||||
for (auto e : m->children()) {
|
||||
r->add_child(mk_div(e, bm));
|
||||
}
|
||||
TRACE("nla_cn_details", tout << *r << "\n";);
|
||||
return r;
|
||||
}
|
||||
if (a->is_var() || (a->is_mul() && to_mul(a)->children().size() == 1)) {
|
||||
return mk_scalar(rational(1));
|
||||
}
|
||||
SASSERT(a->is_mul());
|
||||
const nex_mul* am = to_mul(a);
|
||||
bm->get_powers_from_mul(m_powers);
|
||||
nex_mul* ret = new nex_mul();
|
||||
for (auto e : am->children()) {
|
||||
TRACE("nla_cn_details", tout << "e=" << *e << "\n";);
|
||||
|
||||
if (!e->is_var()) {
|
||||
SASSERT(e->is_scalar());
|
||||
ret->add_child(e);
|
||||
TRACE("nla_cn_details", tout << "continue\n";);
|
||||
continue;
|
||||
}
|
||||
SASSERT(e->is_var());
|
||||
lpvar j = to_var(e)->var();
|
||||
auto it = m_powers.find(j);
|
||||
if (it == m_powers.end()) {
|
||||
ret->add_child(e);
|
||||
} else {
|
||||
it->second --;
|
||||
if (it->second == 0)
|
||||
m_powers.erase(it);
|
||||
}
|
||||
TRACE("nla_cn_details", tout << *ret << "\n";);
|
||||
}
|
||||
SASSERT(m_powers.size() == 0);
|
||||
if (ret->children().size() == 0) {
|
||||
delete ret;
|
||||
TRACE("nla_cn_details", tout << "return 1\n";);
|
||||
return mk_scalar(rational(1));
|
||||
}
|
||||
m_allocated.push_back(ret);
|
||||
TRACE("nla_cn_details", tout << *ret << "\n";);
|
||||
return ret;
|
||||
}
|
||||
|
||||
nex* extract_common_factor(nex* e, const vector<std::pair<lpvar, occ>> & occurences) {
|
||||
nex_sum* c = to_sum(e);
|
||||
TRACE("nla_cn", tout << "c=" << *c << "\n";);
|
||||
SASSERT(c->is_sum());
|
||||
f.type() = expr_type::MUL;
|
||||
SASSERT(f.children().empty());
|
||||
unsigned size = c->children().size();
|
||||
for(const auto & p : occurences) {
|
||||
if (p.second.m_occs < size) {
|
||||
return nullptr;
|
||||
}
|
||||
}
|
||||
nex_mul* f = mk_mul();
|
||||
for(const auto & p : occurences) { // randomize here: todo
|
||||
if (p.second.m_occs == size) {
|
||||
unsigned pow = p.second.m_power;
|
||||
while (pow --) {
|
||||
f *= nex::var(p.first);
|
||||
f->add_child(mk_var(p.first));
|
||||
}
|
||||
}
|
||||
}
|
||||
return !f.children().empty();
|
||||
return f;
|
||||
}
|
||||
|
||||
static bool has_common_factor(const nex& c) {
|
||||
TRACE("nla_cn", tout << "c=" << c << "\n";);
|
||||
SASSERT(c.is_sum());
|
||||
auto & ch = c.children();
|
||||
static bool has_common_factor(const nex_sum* c) {
|
||||
TRACE("nla_cn", tout << "c=" << *c << "\n";);
|
||||
auto & ch = c->children();
|
||||
auto common_vars = get_vars_of_expr(ch[0]);
|
||||
for (lpvar j : common_vars) {
|
||||
bool divides_the_rest = true;
|
||||
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;
|
||||
}
|
||||
if (divides_the_rest) {
|
||||
|
|
@ -101,45 +218,45 @@ public:
|
|||
return false;
|
||||
}
|
||||
|
||||
bool proceed_with_common_factor(nex* c, vector<nex*>& front, const vector<std::pair<lpvar, occ>> & occurences) {
|
||||
bool proceed_with_common_factor(nex*& c, vector<nex_sum*>& front, const vector<std::pair<lpvar, occ>> & occurences) {
|
||||
TRACE("nla_cn", tout << "c=" << *c << "\n";);
|
||||
SASSERT(c->is_sum());
|
||||
nex f;
|
||||
if (!extract_common_factor(c, f, occurences))
|
||||
nex* f = extract_common_factor(c, occurences);
|
||||
if (f == nullptr)
|
||||
return false;
|
||||
|
||||
*c /= f;
|
||||
f.simplify();
|
||||
* c = nex::mul(f, *c);
|
||||
TRACE("nla_cn", tout << "common factor=" << f << ", c=" << *c << "\n";);
|
||||
explore_expr_on_front_elem(&(c->children()[1]), front);
|
||||
nex_sum* c_over_f = to_sum(mk_div(c, f));
|
||||
c_over_f->simplify();
|
||||
c = mk_mul(f, c_over_f);
|
||||
TRACE("nla_cn", tout << "common factor=" << *f << ", c=" << *c << "\ne = " << *m_e << "\n";);
|
||||
|
||||
explore_expr_on_front_elem(c_over_f, front);
|
||||
return true;
|
||||
}
|
||||
|
||||
static void push(vector<nex*>& front, nex* e) {
|
||||
static void push(vector<nex_sum*>& front, nex_sum* e) {
|
||||
TRACE("nla_cn", tout << *e << "\n";);
|
||||
front.push_back(e);
|
||||
}
|
||||
|
||||
static vector<nex> copy_front(const vector<nex*>& front) {
|
||||
vector<nex> v;
|
||||
for (nex* n: front)
|
||||
v.push_back(*n);
|
||||
static vector<nex_sum*> copy_front(const vector<nex_sum*>& front) {
|
||||
vector<nex_sum*> v;
|
||||
for (nex_sum* n: front)
|
||||
v.push_back(n);
|
||||
return v;
|
||||
}
|
||||
|
||||
static void restore_front(const vector<nex> ©, vector<nex*>& front) {
|
||||
static void restore_front(const vector<nex_sum*> ©, vector<nex_sum*>& front) {
|
||||
SASSERT(copy.size() == front.size());
|
||||
for (unsigned i = 0; i < front.size(); i++)
|
||||
*(front[i]) = copy[i];
|
||||
front[i] = copy[i];
|
||||
}
|
||||
|
||||
void explore_expr_on_front_elem_occs(nex* c, vector<nex*>& front, const vector<std::pair<lpvar, occ>> & occurences) {
|
||||
void explore_expr_on_front_elem_occs(nex* c, vector<nex_sum*>& front, const vector<std::pair<lpvar, occ>> & occurences) {
|
||||
if (proceed_with_common_factor(c, front, occurences))
|
||||
return;
|
||||
TRACE("nla_cn", tout << "save c=" << *c << "; front:"; print_vector_of_ptrs(front, tout) << "\n";);
|
||||
nex copy_of_c = *c;
|
||||
vector<nex> copy_of_front = copy_front(front);
|
||||
nex* copy_of_c = c;
|
||||
auto copy_of_front = copy_front(front);
|
||||
for(auto& p : occurences) {
|
||||
SASSERT(p.second.m_occs > 1);
|
||||
lpvar j = p.first;
|
||||
|
|
@ -152,7 +269,7 @@ public:
|
|||
explore_of_expr_on_sum_and_var(c, j, front);
|
||||
if (m_done)
|
||||
return;
|
||||
*c = copy_of_c;
|
||||
c = copy_of_c;
|
||||
TRACE("nla_cn", tout << "restore c=" << *c << ", m_e=" << m_e << "\n";);
|
||||
restore_front(copy_of_front, front);
|
||||
TRACE("nla_cn", tout << "restore c=" << *c << "\n";);
|
||||
|
|
@ -171,9 +288,8 @@ public:
|
|||
return out;
|
||||
}
|
||||
|
||||
void explore_expr_on_front_elem(nex* c, vector<nex*>& front) {
|
||||
SASSERT(c->is_sum());
|
||||
auto occurences = get_mult_occurences(*c);
|
||||
void explore_expr_on_front_elem(nex_sum* c, vector<nex_sum*>& front) {
|
||||
auto occurences = get_mult_occurences(c);
|
||||
TRACE("nla_cn", tout << "m_e=" << m_e << "\nc=" << *c << ", c occurences=";
|
||||
dump_occurences(tout, occurences) << "; front:"; print_vector_of_ptrs(front, tout) << "\n";);
|
||||
|
||||
|
|
@ -182,7 +298,7 @@ public:
|
|||
TRACE("nla_cn", tout << "got the cn form: =" << m_e << "\n";);
|
||||
m_done = m_call_on_result(m_e);
|
||||
} else {
|
||||
nex* c = pop_back(front);
|
||||
auto c = pop_back(front);
|
||||
explore_expr_on_front_elem(c, front);
|
||||
}
|
||||
} else {
|
||||
|
|
@ -196,17 +312,17 @@ public:
|
|||
// return (char)('a'+j);
|
||||
}
|
||||
// e is the global expression, c is the sub expressiond which is going to changed from sum to the cross nested form
|
||||
void explore_of_expr_on_sum_and_var(nex* c, lpvar j, vector<nex*> front) {
|
||||
void explore_of_expr_on_sum_and_var(nex* & c, lpvar j, vector<nex_sum*> front) {
|
||||
TRACE("nla_cn", tout << "m_e=" << m_e << "\nc=" << *c << "\nj = " << ch(j) << "\nfront="; print_vector_of_ptrs(front, tout) << "\n";);
|
||||
if (!split_with_var(*c, j, front))
|
||||
if (!split_with_var(c, j, front))
|
||||
return;
|
||||
TRACE("nla_cn", tout << "after split c=" << *c << "\nfront="; print_vector_of_ptrs(front, tout) << "\n";);
|
||||
SASSERT(front.size());
|
||||
nex* n = pop_back(front); TRACE("nla_cn", tout << "n=" << *n <<"\n";);
|
||||
auto n = pop_back(front); TRACE("nla_cn", tout << "n=" << *n <<"\n";);
|
||||
explore_expr_on_front_elem(n, front);
|
||||
}
|
||||
|
||||
void process_var_occurences(lpvar j) {
|
||||
void add_var_occs(lpvar j) {
|
||||
auto it = m_occurences_map.find(j);
|
||||
if (it != m_occurences_map.end()) {
|
||||
it->second.m_occs++;
|
||||
|
|
@ -251,15 +367,14 @@ public:
|
|||
|
||||
// j -> the number of expressions j appears in as a multiplier
|
||||
// The result is sorted by large number of occurences first
|
||||
vector<std::pair<lpvar, occ>> get_mult_occurences(const nex& e) {
|
||||
vector<std::pair<lpvar, occ>> get_mult_occurences(const nex_sum* e) {
|
||||
clear_maps();
|
||||
SASSERT(e.type() == expr_type::SUM);
|
||||
for (const auto & ce : e.children()) {
|
||||
if (ce.is_mul()) {
|
||||
auto powers = ce.get_powers_from_mul();
|
||||
for (const auto * ce : e->children()) {
|
||||
if (ce->is_mul()) {
|
||||
to_mul(ce)->get_powers_from_mul(m_powers);
|
||||
update_occurences_with_powers();
|
||||
} else if (ce.type() == expr_type::VAR) {
|
||||
process_var_occurences(ce.var());
|
||||
} else if (ce->is_var()) {
|
||||
add_var_occs(to_var(ce)->var());
|
||||
}
|
||||
}
|
||||
remove_singular_occurences();
|
||||
|
|
@ -281,63 +396,65 @@ public:
|
|||
});
|
||||
return ret;
|
||||
}
|
||||
|
||||
static bool is_divisible_by_var(nex* ce, lpvar j) {
|
||||
return (ce->is_mul() && to_mul(ce)->contains(j))
|
||||
|| (ce->is_var() && to_var(ce)->var() == j);
|
||||
}
|
||||
// all factors of j go to a, the rest to b
|
||||
static void pre_split(nex &e, lpvar j, nex &a, nex&b) {
|
||||
for (const nex & ce: e.children()) {
|
||||
if ((ce.is_mul() && ce.contains(j)) || (ce.is_var() && ce.var() == j)) {
|
||||
a.add_child(ce / j);
|
||||
void pre_split(nex_sum * e, lpvar j, nex_sum* & a, nex* & b) {
|
||||
|
||||
a = mk_sum();
|
||||
m_b_vec.clear();
|
||||
for (nex * ce: e->children()) {
|
||||
if (is_divisible_by_var(ce, j)) {
|
||||
a->add_child(mk_div(ce , j));
|
||||
} else {
|
||||
b.add_child(ce);
|
||||
m_b_vec.push_back(ce);
|
||||
}
|
||||
}
|
||||
a.type() = expr_type::SUM;
|
||||
TRACE("nla_cn_details", tout << "a = " << a << "\n";);
|
||||
SASSERT(a.children().size() >= 2);
|
||||
a.simplify();
|
||||
TRACE("nla_cn_details", tout << "a = " << *a << "\n";);
|
||||
SASSERT(a->children().size() >= 2 && m_b_vec.size());
|
||||
a->simplify();
|
||||
|
||||
if (b.children().size() == 1) {
|
||||
nex t = b.children()[0];
|
||||
b = t;
|
||||
} else if (b.children().size() > 1) {
|
||||
b.type() = expr_type::SUM;
|
||||
}
|
||||
if (m_b_vec.size() == 1) {
|
||||
b = m_b_vec[0];
|
||||
} else {
|
||||
SASSERT(m_b_vec.size() > 1);
|
||||
b = mk_sum(m_b_vec);
|
||||
}
|
||||
}
|
||||
|
||||
// returns true if the recursion is done inside
|
||||
void update_front_with_split_with_non_empty_b(nex& e, lpvar j, vector<nex*> & front, nex& a, nex& b) {
|
||||
nex f;
|
||||
SASSERT(a.is_sum());
|
||||
void update_front_with_split_with_non_empty_b(nex* &e, lpvar j, vector<nex_sum*> & front, nex_sum* a, nex* b) {
|
||||
|
||||
SASSERT(a->is_sum());
|
||||
|
||||
TRACE("nla_cn_details", tout << "b = " << b << "\n";);
|
||||
e = nex::sum(nex::mul(nex::var(j), a), b);
|
||||
push(front, &(e.children()[0].children()[1])); // pushing 'a'
|
||||
TRACE("nla_cn", tout << "push to front " << e.children()[0].children()[1] << "\n";);
|
||||
e = mk_sum(mk_mul(mk_var(j), a), b); // e = j*a + b
|
||||
push(front, a); // pushing 'a'
|
||||
TRACE("nla_cn", tout << "push to front " << *a << "\n";);
|
||||
|
||||
if (b.is_sum()) {
|
||||
push(front, &(e.children()[1]));
|
||||
TRACE("nla_cn", tout << "push to front " << e.children()[1] << "\n";);
|
||||
if (b->is_sum()) {
|
||||
push(front, to_sum(b));
|
||||
TRACE("nla_cn", tout << "push to front " << *b << "\n";);
|
||||
}
|
||||
}
|
||||
|
||||
void update_front_with_split(nex& e, lpvar j, vector<nex*> & front, nex& a, nex& b) {
|
||||
if (b.is_undef()) {
|
||||
SASSERT(b.children().size() == 0);
|
||||
e = nex(expr_type::MUL);
|
||||
e.add_child(nex::var(j));
|
||||
e.add_child(a);
|
||||
if (a.size() > 1) {
|
||||
push(front, &e.children().back());
|
||||
TRACE("nla_cn_details", tout << "push to front " << e.children().back() << "\n";);
|
||||
}
|
||||
void update_front_with_split(nex* & e, lpvar j, vector<nex_sum*> & front, nex_sum* a, nex* b) {
|
||||
if (b == nullptr) {
|
||||
e = mk_mul(mk_var(j), a);
|
||||
push(front, a);
|
||||
TRACE("nla_cn_details", tout << "push to front " << *a << "\n";);
|
||||
} else {
|
||||
update_front_with_split_with_non_empty_b(e, j, front, a, b);
|
||||
}
|
||||
update_front_with_split_with_non_empty_b(e, j, front, a, b);
|
||||
}
|
||||
// it returns true if the recursion brings a cross-nested form
|
||||
bool split_with_var(nex& e, lpvar j, vector<nex*> & front) {
|
||||
bool split_with_var(nex*& e, lpvar j, vector<nex_sum*> & front) {
|
||||
SASSERT(e->is_sum());
|
||||
TRACE("nla_cn", tout << "e = " << e << ", j=" << ch(j) << "\n";);
|
||||
if (!e.is_sum()) return false;
|
||||
nex a, b;
|
||||
pre_split(e, j, a, b);
|
||||
nex_sum* a; nex * b;
|
||||
pre_split(to_sum(e), j, a, b);
|
||||
/*
|
||||
When we have e without a non-trivial common factor then
|
||||
there is a variable j such that e = jP + Q, where Q has all members
|
||||
|
|
@ -352,28 +469,42 @@ public:
|
|||
update_front_with_split(e, j, front, a, b);
|
||||
return true;
|
||||
}
|
||||
static std::unordered_set<lpvar> get_vars_of_expr(const nex &e ) {
|
||||
|
||||
static std::unordered_set<lpvar> get_vars_of_expr(const nex *e ) {
|
||||
std::unordered_set<lpvar> r;
|
||||
switch (e.type()) {
|
||||
switch (e->type()) {
|
||||
case expr_type::SCALAR:
|
||||
return r;
|
||||
case expr_type::SUM:
|
||||
{
|
||||
for (auto c: to_sum(e)->children())
|
||||
for ( lpvar j : get_vars_of_expr(c))
|
||||
r.insert(j);
|
||||
}
|
||||
case expr_type::MUL:
|
||||
{
|
||||
for (const auto & c: e.children())
|
||||
for (auto c: to_mul(e)->children())
|
||||
for ( lpvar j : get_vars_of_expr(c))
|
||||
r.insert(j);
|
||||
}
|
||||
return r;
|
||||
case expr_type::VAR:
|
||||
r.insert(e.var());
|
||||
r.insert(to_var(e)->var());
|
||||
return r;
|
||||
default:
|
||||
TRACE("nla_cn_details", tout << e.type() << "\n";);
|
||||
TRACE("nla_cn_details", tout << e->type() << "\n";);
|
||||
SASSERT(false);
|
||||
return r;
|
||||
}
|
||||
}
|
||||
|
||||
~cross_nested() {
|
||||
for (auto e: m_allocated)
|
||||
delete e;
|
||||
m_allocated.clear();
|
||||
}
|
||||
|
||||
bool done() const { return m_done; }
|
||||
|
||||
};
|
||||
}
|
||||
|
|
|
|||
|
|
@ -63,31 +63,31 @@ bool horner::row_is_interesting(const T& row) const {
|
|||
return false;
|
||||
}
|
||||
|
||||
bool horner::lemmas_on_expr(nex& e) {
|
||||
bool horner::lemmas_on_expr(nex_sum* e, cross_nested& cn) {
|
||||
TRACE("nla_horner", tout << "e = " << e << "\n";);
|
||||
bool conflict = false;
|
||||
cross_nested cn(e, [this, & conflict](const nex& n) {
|
||||
cn.run(e);
|
||||
return cn.done();
|
||||
}
|
||||
|
||||
|
||||
template <typename T>
|
||||
bool horner::lemmas_on_row(const T& row) {
|
||||
cross_nested cn([this](const nex* n) {
|
||||
TRACE("nla_horner", tout << "cross-nested n = " << n << "\n";);
|
||||
auto i = interval_of_expr(n);
|
||||
TRACE("nla_horner", tout << "callback n = " << n << "\ni="; m_intervals.display(tout, i) << "\n";);
|
||||
|
||||
conflict = m_intervals.check_interval_for_conflict_on_zero(i);
|
||||
bool conflict = m_intervals.check_interval_for_conflict_on_zero(i);
|
||||
c().lp_settings().st().m_cross_nested_forms++;
|
||||
m_intervals.reset(); // clean the memory allocated by the interval bound dependencies
|
||||
return conflict;
|
||||
},
|
||||
[this](unsigned j) { return c().var_is_fixed(j); }
|
||||
);
|
||||
cn.run();
|
||||
return conflict;
|
||||
}
|
||||
|
||||
|
||||
template <typename T>
|
||||
bool horner::lemmas_on_row(const T& row) {
|
||||
SASSERT (row_is_interesting(row));
|
||||
nex e = create_sum_from_row(row);
|
||||
return lemmas_on_expr(e);
|
||||
nex_sum* e = create_sum_from_row(row, cn);
|
||||
return lemmas_on_expr(e, cn);
|
||||
}
|
||||
|
||||
void horner::horner_lemmas() {
|
||||
|
|
@ -120,27 +120,28 @@ void horner::horner_lemmas() {
|
|||
}
|
||||
}
|
||||
|
||||
typedef nla_expr<rational> nex;
|
||||
|
||||
nex horner::nexvar(lpvar j) const {
|
||||
nex * horner::nexvar(lpvar j, cross_nested& cn) const {
|
||||
// todo: consider deepen the recursion
|
||||
if (!c().is_monomial_var(j))
|
||||
return nex::var(j);
|
||||
return cn.mk_var(j);
|
||||
const monomial& m = c().emons()[j];
|
||||
nex e(expr_type::MUL);
|
||||
nex_mul * e = cn.mk_mul();
|
||||
for (lpvar k : m.vars()) {
|
||||
e.add_child(nex::var(k));
|
||||
e->add_child(cn.mk_var(k));
|
||||
CTRACE("nla_horner", c().is_monomial_var(k), c().print_var(k, tout) << "\n";);
|
||||
}
|
||||
return e;
|
||||
}
|
||||
|
||||
template <typename T> nex horner::create_sum_from_row(const T& row) {
|
||||
template <typename T> nex_sum* horner::create_sum_from_row(const T& row, cross_nested& cn) {
|
||||
TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";);
|
||||
SASSERT(row.size() > 1);
|
||||
nex e(expr_type::SUM);
|
||||
for (const auto &p : row) {
|
||||
e.add_child(nex::scalar(p.coeff())* nexvar(p.var()));
|
||||
nex_sum *e = cn.mk_sum();
|
||||
for (const auto &p : row) {
|
||||
if (p.coeff().is_one())
|
||||
e->add_child(nexvar(p.var(), cn));
|
||||
else
|
||||
e->add_child(cn.mk_mul(cn.mk_scalar(p.coeff()), nexvar(p.var(), cn)));
|
||||
}
|
||||
return e;
|
||||
}
|
||||
|
|
@ -155,28 +156,28 @@ void horner::set_interval_for_scalar(interv& a, const rational& v) {
|
|||
m_intervals.set_upper_is_inf(a, false);
|
||||
}
|
||||
|
||||
interv horner::interval_of_expr(const nex& e) {
|
||||
interv horner::interval_of_expr(const nex* e) {
|
||||
interv a;
|
||||
switch (e.type()) {
|
||||
switch (e->type()) {
|
||||
case expr_type::SCALAR:
|
||||
set_interval_for_scalar(a, e.value());
|
||||
set_interval_for_scalar(a, to_scalar(e)->value());
|
||||
return a;
|
||||
case expr_type::SUM:
|
||||
return interval_of_sum(e);
|
||||
return interval_of_sum(to_sum(e));
|
||||
case expr_type::MUL:
|
||||
return interval_of_mul(e);
|
||||
return interval_of_mul(to_mul(e));
|
||||
case expr_type::VAR:
|
||||
set_var_interval(e.var(), a);
|
||||
set_var_interval(to_var(e)->var(), a);
|
||||
return a;
|
||||
default:
|
||||
TRACE("nla_horner_details", tout << e.type() << "\n";);
|
||||
TRACE("nla_horner_details", tout << e->type() << "\n";);
|
||||
SASSERT(false);
|
||||
return interv();
|
||||
}
|
||||
}
|
||||
interv horner::interval_of_mul(const nex& e) {
|
||||
SASSERT(e.is_mul());
|
||||
auto & es = e.children();
|
||||
interv horner::interval_of_mul(const nex_mul* e) {
|
||||
SASSERT(e->is_mul());
|
||||
auto & es = to_mul(e)->children();
|
||||
interv a = interval_of_expr(es[0]);
|
||||
if (m_intervals.is_zero(a)) {
|
||||
m_intervals.set_zero_interval_deps_for_mult(a);
|
||||
|
|
@ -208,25 +209,25 @@ interv horner::interval_of_mul(const nex& e) {
|
|||
return a;
|
||||
}
|
||||
|
||||
void horner::add_mul_to_vector(const nex& e, vector<std::pair<rational, lpvar>> &v) {
|
||||
void horner::add_mul_to_vector(const nex_mul* e, vector<std::pair<rational, lpvar>> &v) {
|
||||
TRACE("nla_horner_details", tout << e << "\n";);
|
||||
SASSERT(e.is_mul() && e.size() > 0);
|
||||
if (e.size() == 1) {
|
||||
add_linear_to_vector(*(e.children().begin()), v);
|
||||
SASSERT(e->size() > 0);
|
||||
if (e->size() == 1) {
|
||||
add_linear_to_vector(*(e->children().begin()), v);
|
||||
return;
|
||||
}
|
||||
rational r;
|
||||
lpvar j = -1;
|
||||
for (const nex & c : e.children()) {
|
||||
switch (c.type()) {
|
||||
for (const nex * c : e->children()) {
|
||||
switch (c->type()) {
|
||||
case expr_type::SCALAR:
|
||||
r = c.value();
|
||||
r = to_scalar(c)->value();
|
||||
break;
|
||||
case expr_type::VAR:
|
||||
j = c.var();
|
||||
j = to_var(c)->var();
|
||||
break;
|
||||
default:
|
||||
TRACE("nla_horner_details", tout << e.type() << "\n";);
|
||||
TRACE("nla_horner_details", tout << e->type() << "\n";);
|
||||
SASSERT(false);
|
||||
}
|
||||
}
|
||||
|
|
@ -234,30 +235,30 @@ void horner::add_mul_to_vector(const nex& e, vector<std::pair<rational, lpvar>>
|
|||
v.push_back(std::make_pair(r, j));
|
||||
}
|
||||
|
||||
void horner::add_linear_to_vector(const nex& e, vector<std::pair<rational, lpvar>> &v) {
|
||||
void horner::add_linear_to_vector(const nex* e, vector<std::pair<rational, lpvar>> &v) {
|
||||
TRACE("nla_horner_details", tout << e << "\n";);
|
||||
switch (e.type()) {
|
||||
switch (e->type()) {
|
||||
case expr_type::MUL:
|
||||
add_mul_to_vector(e, v);
|
||||
add_mul_to_vector(to_mul(e), v);
|
||||
break;
|
||||
case expr_type::VAR:
|
||||
v.push_back(std::make_pair(rational(1), e.var()));
|
||||
v.push_back(std::make_pair(rational(1), to_var(e)->var()));
|
||||
break;
|
||||
default:
|
||||
SASSERT(!e.is_sum());
|
||||
SASSERT(!e->is_sum());
|
||||
// noop
|
||||
}
|
||||
}
|
||||
// e = a * can_t + b
|
||||
lp::lar_term horner::expression_to_normalized_term(nex& e, rational& a, rational& b) {
|
||||
lp::lar_term horner::expression_to_normalized_term(const nex_sum* e, rational& a, rational& b) {
|
||||
TRACE("nla_horner_details", tout << e << "\n";);
|
||||
lpvar smallest_j;
|
||||
vector<std::pair<rational, lpvar>> v;
|
||||
b = rational(0);
|
||||
unsigned a_index;
|
||||
for (const nex& c : e.children()) {
|
||||
if (c.is_scalar()) {
|
||||
b += c.value();
|
||||
for (const nex* c : e->children()) {
|
||||
if (c->is_scalar()) {
|
||||
b += to_scalar(c)->value();
|
||||
} else {
|
||||
add_linear_to_vector(c, v);
|
||||
if (v.empty())
|
||||
|
|
@ -295,9 +296,10 @@ lp::lar_term horner::expression_to_normalized_term(nex& e, rational& a, rational
|
|||
|
||||
// we should have in the case of found a*m_terms[k] + b = e,
|
||||
// where m_terms[k] corresponds to the returned lpvar
|
||||
lpvar horner::find_term_column(const nex& e, rational& a, rational& b) const {
|
||||
nex n = e;
|
||||
lp::lar_term norm_t = expression_to_normalized_term(n, a, b);
|
||||
lpvar horner::find_term_column(const nex* e, rational& a, rational& b) const {
|
||||
if (!e->is_sum())
|
||||
return -1;
|
||||
lp::lar_term norm_t = expression_to_normalized_term(to_sum(e), a, b);
|
||||
std::pair<rational, lpvar> a_j;
|
||||
if (c().m_lar_solver.fetch_normalized_term_column(norm_t, a_j)) {
|
||||
a /= a_j.first;
|
||||
|
|
@ -306,8 +308,8 @@ lpvar horner::find_term_column(const nex& e, rational& a, rational& b) const {
|
|||
return -1;
|
||||
}
|
||||
|
||||
interv horner::interval_of_sum_no_terms(const nex& e) {
|
||||
auto & es = e.children();
|
||||
interv horner::interval_of_sum_no_terms(const nex_sum* e) {
|
||||
auto & es = e->children();
|
||||
interv a = interval_of_expr(es[0]);
|
||||
if (m_intervals.is_inf(a)) {
|
||||
TRACE("nla_horner_details", tout << "e=" << e << "\n";
|
||||
|
|
@ -340,10 +342,9 @@ interv horner::interval_of_sum_no_terms(const nex& e) {
|
|||
return a;
|
||||
}
|
||||
|
||||
bool horner::interval_from_term(const nex& e, interv & i) const {
|
||||
bool horner::interval_from_term(const nex* e, interv & i) const {
|
||||
rational a, b;
|
||||
nex n = e;
|
||||
lpvar j = find_term_column(n, a, b);
|
||||
lpvar j = find_term_column(e, a, b);
|
||||
if (j + 1 == 0)
|
||||
return false;
|
||||
|
||||
|
|
@ -361,11 +362,10 @@ bool horner::interval_from_term(const nex& e, interv & i) const {
|
|||
}
|
||||
|
||||
|
||||
interv horner::interval_of_sum(const nex& e) {
|
||||
interv horner::interval_of_sum(const nex_sum* e) {
|
||||
TRACE("nla_horner_details", tout << "e=" << e << "\n";);
|
||||
SASSERT(e.is_sum());
|
||||
interv i_e = interval_of_sum_no_terms(e);
|
||||
if (e.sum_is_a_linear_term()) {
|
||||
if (e->is_a_linear_term()) {
|
||||
interv i_from_term ;
|
||||
if (interval_from_term(e, i_from_term)) {
|
||||
interv r = m_intervals.intersect(i_e, i_from_term);
|
||||
|
|
|
|||
|
|
@ -22,6 +22,7 @@
|
|||
#include "math/lp/nla_common.h"
|
||||
#include "math/lp/nla_intervals.h"
|
||||
#include "math/lp/nla_expr.h"
|
||||
#include "math/lp/cross_nested.h"
|
||||
|
||||
namespace nla {
|
||||
class core;
|
||||
|
|
@ -30,31 +31,30 @@ class core;
|
|||
class horner : common {
|
||||
intervals m_intervals;
|
||||
public:
|
||||
typedef nla_expr<rational> nex;
|
||||
typedef intervals::interval interv;
|
||||
horner(core *core);
|
||||
void horner_lemmas();
|
||||
template <typename T> // T has an iterator of (coeff(), var())
|
||||
bool lemmas_on_row(const T&);
|
||||
template <typename T> bool row_is_interesting(const T&) const;
|
||||
template <typename T> nex create_sum_from_row(const T&);
|
||||
intervals::interval interval_of_expr(const nex& e);
|
||||
template <typename T>
|
||||
nex_sum* create_sum_from_row(const T&, cross_nested&);
|
||||
intervals::interval interval_of_expr(const nex* e);
|
||||
|
||||
nex nexvar(lpvar j) const;
|
||||
intervals::interval interval_of_sum(const nex&);
|
||||
intervals::interval interval_of_sum_no_terms(const nex&);
|
||||
intervals::interval interval_of_mul(const nex&);
|
||||
nex* nexvar(lpvar j, cross_nested& cn) const;
|
||||
intervals::interval interval_of_sum(const nex_sum*);
|
||||
intervals::interval interval_of_sum_no_terms(const nex_sum*);
|
||||
intervals::interval interval_of_mul(const nex_mul*);
|
||||
void set_interval_for_scalar(intervals::interval&, const rational&);
|
||||
void set_var_interval(lpvar j, intervals::interval&) const;
|
||||
bool lemmas_on_expr(nex &);
|
||||
bool lemmas_on_expr(nex_sum* , cross_nested&);
|
||||
|
||||
template <typename T> // T has an iterator of (coeff(), var())
|
||||
bool row_has_monomial_to_refine(const T&) const;
|
||||
lpvar find_term_column(const nex& e, rational& a, rational& b) const;
|
||||
static lp::lar_term expression_to_normalized_term(nex&, rational& a, rational & b);
|
||||
static void add_linear_to_vector(const nex&, vector<std::pair<rational, lpvar>> &);
|
||||
static void add_mul_to_vector(const nex&, vector<std::pair<rational, lpvar>> &);
|
||||
bool is_tighter(const interv&, const interv&) const;
|
||||
bool interval_from_term(const nex& e, interv&) const;
|
||||
lpvar find_term_column(const nex* e, rational& a, rational& b) const;
|
||||
static lp::lar_term expression_to_normalized_term(const nex_sum*, rational& a, rational & b);
|
||||
static void add_linear_to_vector(const nex*, vector<std::pair<rational, lpvar>> &);
|
||||
static void add_mul_to_vector(const nex_mul*, vector<std::pair<rational, lpvar>> &);
|
||||
bool interval_from_term(const nex* e, interv&) const;
|
||||
}; // end of horner
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1346,41 +1346,41 @@ lbool core::test_check(
|
|||
return check(l);
|
||||
}
|
||||
|
||||
nla_expr<rational> core::mk_expr(lpvar j) const {
|
||||
return nla_expr<rational>::var(j);
|
||||
}
|
||||
// nla_expr<rational> core::mk_expr(lpvar j) const {
|
||||
// return nla_expr<rational>::var(j);
|
||||
// }
|
||||
|
||||
nla_expr<rational> core::mk_expr(const rational &a, lpvar j) const {
|
||||
if (a == 1)
|
||||
return mk_expr(j);
|
||||
nla_expr<rational> r(expr_type::MUL);
|
||||
r.add_child(nla_expr<rational>::scalar(a));
|
||||
r.add_child(nla_expr<rational>::var(j));
|
||||
return r;
|
||||
}
|
||||
// nla_expr<rational> core::mk_expr(const rational &a, lpvar j) const {
|
||||
// if (a == 1)
|
||||
// return mk_expr(j);
|
||||
// nla_expr<rational> r(expr_type::MUL);
|
||||
// r.add_child(nla_expr<rational>::scalar(a));
|
||||
// r.add_child(nla_expr<rational>::var(j));
|
||||
// return r;
|
||||
// }
|
||||
|
||||
nla_expr<rational> core::mk_expr(const rational &a, const svector<lpvar>& vs) const {
|
||||
nla_expr<rational> r(expr_type::MUL);
|
||||
r.add_child(nla_expr<rational>::scalar(a));
|
||||
for (lpvar j : vs)
|
||||
r.add_child(nla_expr<rational>::var(j));
|
||||
return r;
|
||||
}
|
||||
nla_expr<rational> core::mk_expr(const lp::lar_term& t) const {
|
||||
auto coeffs = t.coeffs_as_vector();
|
||||
if (coeffs.size() == 1) {
|
||||
return mk_expr(coeffs[0].first, coeffs[0].second);
|
||||
}
|
||||
nla_expr<rational> r(expr_type::SUM);
|
||||
for (const auto & p : coeffs) {
|
||||
lpvar j = p.second;
|
||||
if (is_monomial_var(j))
|
||||
r.add_child(mk_expr(p.first, m_emons[j].vars()));
|
||||
else
|
||||
r.add_child(mk_expr(p.first, j));
|
||||
}
|
||||
return r;
|
||||
}
|
||||
// nla_expr<rational> core::mk_expr(const rational &a, const svector<lpvar>& vs) const {
|
||||
// nla_expr<rational> r(expr_type::MUL);
|
||||
// r.add_child(nla_expr<rational>::scalar(a));
|
||||
// for (lpvar j : vs)
|
||||
// r.add_child(nla_expr<rational>::var(j));
|
||||
// return r;
|
||||
// }
|
||||
// nla_expr<rational> core::mk_expr(const lp::lar_term& t) const {
|
||||
// auto coeffs = t.coeffs_as_vector();
|
||||
// if (coeffs.size() == 1) {
|
||||
// return mk_expr(coeffs[0].first, coeffs[0].second);
|
||||
// }
|
||||
// nla_expr<rational> r(expr_type::SUM);
|
||||
// for (const auto & p : coeffs) {
|
||||
// lpvar j = p.second;
|
||||
// if (is_monomial_var(j))
|
||||
// r.add_child(mk_expr(p.first, m_emons[j].vars()));
|
||||
// else
|
||||
// r.add_child(mk_expr(p.first, j));
|
||||
// }
|
||||
// return r;
|
||||
// }
|
||||
|
||||
std::ostream& core::print_terms(std::ostream& out) const {
|
||||
for (unsigned i=0; i< m_lar_solver.m_terms.size(); i++) {
|
||||
|
|
|
|||
|
|
@ -350,11 +350,6 @@ public:
|
|||
lpvar map_to_root(lpvar) const;
|
||||
std::ostream& print_terms(std::ostream&) const;
|
||||
std::ostream& print_term( const lp::lar_term&, std::ostream&) const;
|
||||
nla_expr<rational> mk_expr(lpvar j) const;
|
||||
nla_expr<rational> mk_expr(const rational &a, lpvar j) const;
|
||||
|
||||
nla_expr<rational> mk_expr(const rational &a, const svector<lpvar>& vs) const;
|
||||
nla_expr<rational> mk_expr(const lp::lar_term& t) const;
|
||||
}; // end of core
|
||||
|
||||
struct pp_mon {
|
||||
|
|
|
|||
|
|
@ -47,38 +47,178 @@ inline std::ostream & operator<<(std::ostream& out, expr_type t) {
|
|||
|
||||
|
||||
// This class is needed in horner calculation with intervals
|
||||
template <typename T>
|
||||
class nla_expr {
|
||||
// todo: use union
|
||||
expr_type m_type;
|
||||
lpvar m_j;
|
||||
T m_v; // for the scalar
|
||||
vector<nla_expr> m_children;
|
||||
class nex {
|
||||
public:
|
||||
bool is_sum() const { return m_type == expr_type::SUM; }
|
||||
bool is_var() const { return m_type == expr_type::VAR; }
|
||||
bool is_mul() const { return m_type == expr_type::MUL; }
|
||||
bool is_undef() const { return m_type == expr_type::UNDEF; }
|
||||
bool is_scalar() const { return m_type == expr_type::SCALAR; }
|
||||
lpvar var() const { SASSERT(m_type == expr_type::VAR); return m_j; }
|
||||
expr_type type() const { return m_type; }
|
||||
expr_type& type() { return m_type; }
|
||||
const vector<nla_expr>& children() const { return m_children; }
|
||||
vector<nla_expr>& children() { return m_children; }
|
||||
const T& value() const { SASSERT(m_type == expr_type::SCALAR); return m_v; }
|
||||
std::string str() const { std::stringstream ss; ss << *this; return ss.str(); }
|
||||
std::ostream & print_sum(std::ostream& out) const {
|
||||
virtual expr_type type() const = 0;
|
||||
virtual std::ostream& print(std::ostream&) const = 0;
|
||||
nex() {}
|
||||
bool is_simple() const {
|
||||
switch(type()) {
|
||||
case expr_type::SUM:
|
||||
case expr_type::MUL:
|
||||
return false;
|
||||
default:
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
bool is_sum() const { return type() == expr_type::SUM; }
|
||||
bool is_mul() const { return type() == expr_type::MUL; }
|
||||
bool is_var() const { return type() == expr_type::VAR; }
|
||||
bool is_scalar() const { return type() == expr_type::SCALAR; }
|
||||
std::string str() const { std::stringstream ss; print(ss); return ss.str(); }
|
||||
virtual ~nex() {}
|
||||
virtual bool contains(lpvar j) const { return false; }
|
||||
virtual int get_degree() const = 0;
|
||||
};
|
||||
std::ostream& operator<<(std::ostream& out, const nex&);
|
||||
|
||||
class nex_var : public nex {
|
||||
lpvar m_j;
|
||||
public:
|
||||
nex_var(lpvar j) : m_j(j) {}
|
||||
nex_var() {}
|
||||
expr_type type() const { return expr_type::VAR; }
|
||||
lpvar var() const { return m_j; }
|
||||
lpvar& var() { return m_j; } // the setter
|
||||
std::ostream & print(std::ostream& out) const {
|
||||
out << 'v' << m_j;
|
||||
return out;
|
||||
}
|
||||
|
||||
bool contains(lpvar j) const { return j == m_j; }
|
||||
int get_degree() const { return 1; }
|
||||
};
|
||||
|
||||
class nex_scalar : public nex {
|
||||
rational m_v;
|
||||
public:
|
||||
nex_scalar(const rational& v) : m_v(v) {}
|
||||
nex_scalar() {}
|
||||
expr_type type() const { return expr_type::SCALAR; }
|
||||
const rational& value() const { return m_v; }
|
||||
rational& value() { return m_v; } // the setter
|
||||
std::ostream& print(std::ostream& out) const {
|
||||
out << m_v;
|
||||
return out;
|
||||
}
|
||||
|
||||
int get_degree() const { return 0; }
|
||||
|
||||
};
|
||||
|
||||
class nex_mul : public nex {
|
||||
vector<nex*> m_children;
|
||||
public:
|
||||
nex_mul() {}
|
||||
unsigned size() const { return m_children.size(); }
|
||||
expr_type type() const { return expr_type::MUL; }
|
||||
vector<nex*>& children() { return m_children;}
|
||||
const vector<nex*>& children() const { return m_children;}
|
||||
std::ostream & print(std::ostream& out) const {
|
||||
bool first = true;
|
||||
for (const nla_expr& v : m_children) {
|
||||
std::string s = v.str();
|
||||
for (const nex* v : m_children) {
|
||||
std::string s = v->str();
|
||||
if (first) {
|
||||
first = false;
|
||||
if (v.is_simple())
|
||||
out << v;
|
||||
if (v->is_simple())
|
||||
out << s;
|
||||
else
|
||||
out << "(" << s << ")";
|
||||
} else {
|
||||
if (v.is_simple()) {
|
||||
if (v->is_simple()) {
|
||||
if (s[0] == '-') {
|
||||
out << "*(" << s << ")";
|
||||
} else {
|
||||
out << "*" << s;
|
||||
}
|
||||
} else {
|
||||
out << "*(" << s << ")";
|
||||
}
|
||||
}
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
void add_child(nex* e) { m_children.push_back(e); }
|
||||
|
||||
bool contains(lpvar j) const {
|
||||
for (const nex* c : children()) {
|
||||
if (c->contains(j))
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
static const nex_var* to_var(const nex*a) {
|
||||
SASSERT(a->is_var());
|
||||
return static_cast<const nex_var*>(a);
|
||||
}
|
||||
|
||||
void get_powers_from_mul(std::unordered_map<lpvar, unsigned> & r) const {
|
||||
r.clear();
|
||||
for (const auto & c : children()) {
|
||||
if (!c->is_var()) {
|
||||
continue;
|
||||
}
|
||||
lpvar j = to_var(c)->var();
|
||||
auto it = r.find(j);
|
||||
if (it == r.end()) {
|
||||
r[j] = 1;
|
||||
} else {
|
||||
it->second++;
|
||||
}
|
||||
}
|
||||
TRACE("nla_cn_details", tout << "powers of " << *this << "\n"; print_vector(r, tout)<< "\n";);
|
||||
}
|
||||
|
||||
int get_degree() const {
|
||||
int degree = 0;
|
||||
for (auto e : children()) {
|
||||
degree += e->get_degree();
|
||||
}
|
||||
return degree;
|
||||
}
|
||||
|
||||
|
||||
};
|
||||
|
||||
class nex_sum : public nex {
|
||||
vector<nex*> m_children;
|
||||
public:
|
||||
nex_sum() {}
|
||||
expr_type type() const { return expr_type::SUM; }
|
||||
vector<nex*>& children() { return m_children;}
|
||||
const vector<nex*>& children() const { return m_children;}
|
||||
unsigned size() const { return m_children.size(); }
|
||||
|
||||
// we need a linear combination of at least two variables
|
||||
bool is_a_linear_term() const {
|
||||
TRACE("nex_details", tout << *this << "\n";);
|
||||
unsigned number_of_non_scalars = 0;
|
||||
for (auto e : children()) {
|
||||
int d = e->get_degree();
|
||||
if (d == 0) continue;
|
||||
if (d > 1) return false;
|
||||
|
||||
number_of_non_scalars++;
|
||||
}
|
||||
TRACE("nex_details", tout << (number_of_non_scalars > 1?"linear":"non-linear") << "\n";);
|
||||
return number_of_non_scalars > 1;
|
||||
}
|
||||
|
||||
std::ostream & print(std::ostream& out) const {
|
||||
bool first = true;
|
||||
for (const nex* v : m_children) {
|
||||
std::string s = v->str();
|
||||
if (first) {
|
||||
first = false;
|
||||
if (v->is_simple())
|
||||
out << s;
|
||||
else
|
||||
out << "(" << s << ")";
|
||||
} else {
|
||||
if (v->is_simple()) {
|
||||
if (s[0] == '-') {
|
||||
out << s;
|
||||
} else {
|
||||
|
|
@ -93,457 +233,52 @@ public:
|
|||
}
|
||||
|
||||
void simplify() {
|
||||
if (is_simple()) return;
|
||||
bool has_sum = false;
|
||||
if (is_sum()) {
|
||||
for (auto & e : m_children) {
|
||||
e.simplify();
|
||||
has_sum |= e.is_sum();
|
||||
}
|
||||
if (has_sum) {
|
||||
nla_expr n(expr_type::SUM);
|
||||
for (auto &e : m_children) {
|
||||
n += e;
|
||||
}
|
||||
m_children = n.m_children;
|
||||
}
|
||||
} else if (is_mul()) {
|
||||
bool has_mul = false;
|
||||
for (auto & e : m_children) {
|
||||
e.simplify();
|
||||
has_mul |= e.is_mul();
|
||||
}
|
||||
if (has_mul) {
|
||||
nla_expr n(expr_type::MUL);
|
||||
for (auto &e : m_children) {
|
||||
n *= e;
|
||||
}
|
||||
m_children = n.m_children;
|
||||
}
|
||||
TRACE("nla_cn_details", tout << "simplified " << *this << "\n";);
|
||||
}
|
||||
}
|
||||
|
||||
std::ostream & print_mul(std::ostream& out) const {
|
||||
bool first = true;
|
||||
for (const nla_expr& v : m_children) {
|
||||
std::string s = v.str();
|
||||
if (first) {
|
||||
first = false;
|
||||
if (v.is_simple())
|
||||
out << s;
|
||||
else
|
||||
out << "(" << s << ")";
|
||||
} else {
|
||||
if (v.is_simple()) {
|
||||
if (s[0] == '-') {
|
||||
out << "*(" << s << ")";
|
||||
} else {
|
||||
out << "*" << s;
|
||||
}
|
||||
} else {
|
||||
out << "*(" << s << ")";
|
||||
}
|
||||
}
|
||||
}
|
||||
return out;
|
||||
}
|
||||
std::ostream & print(std::ostream& out) const {
|
||||
switch(m_type) {
|
||||
case expr_type::SUM:
|
||||
return print_sum(out);
|
||||
case expr_type::MUL:
|
||||
return print_mul(out);
|
||||
case expr_type::VAR:
|
||||
out << 'v' << m_j;
|
||||
return out;
|
||||
case expr_type::SCALAR:
|
||||
out << m_v;
|
||||
return out;
|
||||
default:
|
||||
out << "undef";
|
||||
return out;
|
||||
}
|
||||
}
|
||||
|
||||
bool is_simple() const {
|
||||
switch(m_type) {
|
||||
case expr_type::SUM:
|
||||
case expr_type::MUL:
|
||||
return false;
|
||||
|
||||
default:
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
unsigned size() const {
|
||||
switch(m_type) {
|
||||
case expr_type::SUM:
|
||||
case expr_type::MUL:
|
||||
return m_children.size();
|
||||
|
||||
default:
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
nla_expr(expr_type t): m_type(t) {}
|
||||
nla_expr(): m_type(expr_type::UNDEF) {}
|
||||
|
||||
void add_child(const nla_expr& e) {
|
||||
m_children.push_back(e);
|
||||
}
|
||||
|
||||
void add_child(const T& k) {
|
||||
m_children.push_back(scalar(k));
|
||||
}
|
||||
|
||||
void add_children() { }
|
||||
|
||||
template <typename K, typename ...Args>
|
||||
void add_children(K e, Args ... es) {
|
||||
add_child(e);
|
||||
add_children(es ...);
|
||||
}
|
||||
|
||||
template <typename K, typename ... Args>
|
||||
static nla_expr sum(K e, Args ... es) {
|
||||
nla_expr r(expr_type::SUM);
|
||||
r.add_children(e, es...);
|
||||
return r;
|
||||
}
|
||||
|
||||
template <typename K, typename ... Args>
|
||||
static nla_expr mul(K e, Args ... es) {
|
||||
nla_expr r(expr_type::MUL);
|
||||
r.add_children(e, es...);
|
||||
return r;
|
||||
}
|
||||
|
||||
static nla_expr mul(const T& v, nla_expr & w) {
|
||||
if (v == 1)
|
||||
return w;
|
||||
nla_expr r(expr_type::MUL);
|
||||
r.add_child(scalar(v));
|
||||
r.add_child(w);
|
||||
return r;
|
||||
}
|
||||
|
||||
static nla_expr mul() {
|
||||
return nla_expr(expr_type::MUL);
|
||||
}
|
||||
|
||||
static nla_expr mul(const T& v, lpvar j) {
|
||||
if (v == 1)
|
||||
return var(j);
|
||||
return mul(scalar(v), var(j));
|
||||
}
|
||||
|
||||
static nla_expr scalar(const T& v) {
|
||||
nla_expr r(expr_type::SCALAR);
|
||||
r.m_v = v;
|
||||
return r;
|
||||
}
|
||||
|
||||
static nla_expr var(lpvar j) {
|
||||
nla_expr r(expr_type::VAR);
|
||||
r.m_j = j;
|
||||
return r;
|
||||
}
|
||||
|
||||
bool contains(lpvar j) const {
|
||||
if (is_var())
|
||||
return m_j == j;
|
||||
if (is_mul()) {
|
||||
for (const nla_expr<T>& c : children()) {
|
||||
if (c.contains(j))
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
nla_expr& operator*=(const nla_expr& b) {
|
||||
if (is_mul()) {
|
||||
if (b.is_mul()) {
|
||||
for (auto& e: b.children())
|
||||
add_child(e);
|
||||
} else {
|
||||
add_child(b);
|
||||
}
|
||||
return *this;
|
||||
}
|
||||
SASSERT(false); // not impl
|
||||
return *this;
|
||||
}
|
||||
|
||||
std::unordered_map<lpvar, int> get_powers_from_mul() const {
|
||||
SASSERT(is_mul());
|
||||
std::unordered_map<lpvar, int> r;
|
||||
for (const auto & c : children()) {
|
||||
if (!c.is_var()) {
|
||||
continue;
|
||||
}
|
||||
lpvar j = c.var();
|
||||
auto it = r.find(j);
|
||||
if (it == r.end()) {
|
||||
r[j] = 1;
|
||||
} else {
|
||||
it->second++;
|
||||
}
|
||||
}
|
||||
TRACE("nla_cn_details", tout << "powers of " << *this << "\n"; print_vector(r, tout)<< "\n";);
|
||||
return r;
|
||||
}
|
||||
|
||||
friend nla_expr operator-(const nla_expr& a, const nla_expr&b) {
|
||||
return a + scalar(T(-1))*b;
|
||||
SASSERT(false);
|
||||
}
|
||||
|
||||
nla_expr& operator/=(const nla_expr& b) {
|
||||
TRACE("nla_cn_details", tout << *this <<" / " << b << "\n";);
|
||||
if (b.is_var()) {
|
||||
*this = (*this) / b.var();
|
||||
TRACE("nla_cn_details", tout << *this << "\n";);
|
||||
return *this;
|
||||
}
|
||||
SASSERT(b.is_mul());
|
||||
if (is_sum()) {
|
||||
for (auto & e : children()) {
|
||||
e /= b;
|
||||
}
|
||||
TRACE("nla_cn_details", tout << *this << "\n";);
|
||||
return *this;
|
||||
}
|
||||
if (is_var() || children().size() == 1) {
|
||||
*this = scalar(T(1));
|
||||
TRACE("nla_cn_details", tout << *this << "\n";);
|
||||
return *this;
|
||||
}
|
||||
SASSERT(is_mul());
|
||||
auto powers = b.get_powers_from_mul();
|
||||
unsigned i = 0, k = 0;
|
||||
for (; i < children().size(); i++, k++) {
|
||||
auto & e = children()[i];
|
||||
TRACE("nla_cn_details", tout << "e=" << e << ",i=" <<i<< ",k=" << k<< "\n";);
|
||||
|
||||
if (!e.is_var()) {
|
||||
SASSERT(e.is_scalar());
|
||||
if (i != k)
|
||||
children()[k] = children()[i];
|
||||
|
||||
TRACE("nla_cn_details", tout << "continue\n";);
|
||||
continue;
|
||||
|
||||
}
|
||||
lpvar j = e.var();
|
||||
auto it = powers.find(j);
|
||||
if (it == powers.end()) {
|
||||
if (i != k)
|
||||
children()[k] = children()[i];
|
||||
} else {
|
||||
it->second --;
|
||||
if (it->second == 0)
|
||||
powers.erase(it);
|
||||
k--;
|
||||
}
|
||||
TRACE("nla_cn_details", tout << *this << "\n";);
|
||||
|
||||
}
|
||||
SASSERT(powers.size() == 0);
|
||||
while(k ++ < i)
|
||||
children().pop_back();
|
||||
|
||||
if (children().size() == 0)
|
||||
*this = scalar(T(1));
|
||||
TRACE("nla_cn_details", tout << *this << "\n";);
|
||||
|
||||
return *this;
|
||||
}
|
||||
|
||||
|
||||
nla_expr& operator+=(const nla_expr& b) {
|
||||
if (is_sum()) {
|
||||
if (b.is_sum()) {
|
||||
for (auto& e: b.children())
|
||||
add_child(e);
|
||||
} else {
|
||||
add_child(b);
|
||||
}
|
||||
return *this;
|
||||
}
|
||||
SASSERT(false); // not impl
|
||||
return *this;
|
||||
}
|
||||
|
||||
// we need a linear combination of at least two variables
|
||||
bool sum_is_a_linear_term() const {
|
||||
SASSERT(is_sum());
|
||||
TRACE("nla_expr_details", tout << *this << "\n";);
|
||||
unsigned number_of_non_scalars = 0;
|
||||
for (auto & e : children()) {
|
||||
int d = e.get_degree();
|
||||
if (d == 0) continue;
|
||||
if (d > 1) return false;
|
||||
|
||||
number_of_non_scalars++;
|
||||
}
|
||||
TRACE("nla_expr_details", tout << (number_of_non_scalars > 1?"linear":"non-linear") << "\n";);
|
||||
return number_of_non_scalars > 1;
|
||||
}
|
||||
|
||||
int get_degree() const {
|
||||
switch (type()) {
|
||||
case expr_type::SUM: {
|
||||
int degree = 0;
|
||||
for (auto & e : children()) {
|
||||
degree = std::max(degree, e.get_degree());
|
||||
}
|
||||
return degree;
|
||||
int degree = 0;
|
||||
for (auto e : children()) {
|
||||
degree = std::max(degree, e->get_degree());
|
||||
}
|
||||
|
||||
case expr_type::MUL: {
|
||||
int degree = 0;
|
||||
for (auto & e : children()) {
|
||||
degree += e.get_degree();
|
||||
}
|
||||
return degree;
|
||||
}
|
||||
case expr_type::VAR:
|
||||
return 1;
|
||||
case expr_type::SCALAR:
|
||||
return 0;
|
||||
case expr_type::UNDEF:
|
||||
default:
|
||||
UNREACHABLE();
|
||||
break;
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
return degree;
|
||||
}
|
||||
|
||||
void add_child(nex* e) { m_children.push_back(e); }
|
||||
};
|
||||
|
||||
/*
|
||||
nla_expr operator/=(const nla_expr &a, const nla_expr& b) {
|
||||
TRACE("nla_cn_details", tout << a <<" / " << b << "\n";);
|
||||
if (b.is_var()) {
|
||||
return a / b.var();
|
||||
}
|
||||
SASSERT(b.is_mul());
|
||||
if (a.is_sum()) {
|
||||
auto r = nex::sum();
|
||||
for (auto & e : a.children()) {
|
||||
r.add_child(e/b);
|
||||
}
|
||||
return r;
|
||||
}
|
||||
if (is_var()) {
|
||||
return scalar(T(1));
|
||||
return *this;
|
||||
}
|
||||
SASSERT(a.is_mul());
|
||||
auto powers = b.get_powers_from_mul();
|
||||
auto r=nex::mul();
|
||||
for (unsigned i = 0; i < a.children().size(); i++, k++) {
|
||||
auto & e = children()[i];
|
||||
if (!e.is_var()) {
|
||||
SASSERT(e.is_scalar());
|
||||
r.add_child(e);
|
||||
continue;
|
||||
}
|
||||
lpvar j = e.var();
|
||||
auto it = powers.find(j);
|
||||
if (it == powers.end()) {
|
||||
r.add_child(e);
|
||||
} else {
|
||||
it->second --; // finish h
|
||||
if (it->second == 0)
|
||||
powers.erase(it);
|
||||
}
|
||||
}
|
||||
|
||||
return r;
|
||||
}
|
||||
*/
|
||||
template <typename T>
|
||||
nla_expr<T> operator+(const nla_expr<T>& a, const nla_expr<T>& b) {
|
||||
if (a.is_sum()) {
|
||||
nla_expr<T> r(expr_type::SUM);
|
||||
r.children() = a.children();
|
||||
if (b.is_sum()) {
|
||||
for (auto& e: b.children())
|
||||
r.add_child(e);
|
||||
} else {
|
||||
r.add_child(b);
|
||||
}
|
||||
return r;
|
||||
}
|
||||
if (b.is_sum()) {
|
||||
nla_expr<T> r(expr_type::SUM);
|
||||
r.children() = b.children();
|
||||
r.add_child(a);
|
||||
return r;
|
||||
}
|
||||
return nla_expr<T>::sum(a, b);
|
||||
inline const nex_sum* to_sum(const nex*a) {
|
||||
SASSERT(a->is_sum());
|
||||
return static_cast<const nex_sum*>(a);
|
||||
}
|
||||
|
||||
template <typename T>
|
||||
nla_expr<T> operator*(const nla_expr<T>& a, const nla_expr<T>& b) {
|
||||
if (a.is_scalar() && a.value() == T(1))
|
||||
return b;
|
||||
if (b.is_scalar() && b.value() == T(1))
|
||||
return a;
|
||||
if (a.is_mul()) {
|
||||
nla_expr<T> r(expr_type::MUL);
|
||||
r.children() = a.children();
|
||||
if (b.is_mul()) {
|
||||
for (auto& e: b.children())
|
||||
r.add_child(e);
|
||||
} else {
|
||||
r.add_child(b);
|
||||
}
|
||||
return r;
|
||||
}
|
||||
if (b.is_mul()) {
|
||||
nla_expr<T> r(expr_type::MUL);
|
||||
r.children() = b.children();
|
||||
r.add_child(a);
|
||||
return r;
|
||||
}
|
||||
return nla_expr<T>::mul(a, b);
|
||||
inline nex_sum* to_sum(nex * a) {
|
||||
SASSERT(a->is_sum());
|
||||
return static_cast<nex_sum*>(a);
|
||||
}
|
||||
|
||||
|
||||
template <typename T>
|
||||
nla_expr<T> operator/(const nla_expr<T>& a, lpvar j) {
|
||||
TRACE("nla_cn_details", tout << "a=" << a << ", v" << j << "\n";);
|
||||
SASSERT((a.is_mul() && a.contains(j)) || (a.is_var() && a.var() == j));
|
||||
if (a.is_var())
|
||||
return nla_expr<T>::scalar(T(1));
|
||||
nla_expr<T> b;
|
||||
bool seenj = false;
|
||||
for (const nla_expr<T>& c : a.children()) {
|
||||
if (!seenj) {
|
||||
if (c.contains(j)) {
|
||||
if (!c.is_var())
|
||||
b.add_child(c / j);
|
||||
seenj = true;
|
||||
continue;
|
||||
}
|
||||
}
|
||||
b.add_child(c);
|
||||
}
|
||||
if (b.children().size() > 1) {
|
||||
b.type() = expr_type::MUL;
|
||||
} else if (b.children().size() == 1) {
|
||||
auto t = b.children()[0];
|
||||
b = t;
|
||||
} else {
|
||||
b = nla_expr<T>::scalar(T(1));
|
||||
}
|
||||
return b;
|
||||
|
||||
inline const nex_var* to_var(const nex*a) {
|
||||
SASSERT(a->is_var());
|
||||
return static_cast<const nex_var*>(a);
|
||||
}
|
||||
template <typename T>
|
||||
std::ostream& operator<<(std::ostream& out, const nla_expr<T>& e ) {
|
||||
|
||||
inline const nex_mul* to_mul(const nex*a) {
|
||||
SASSERT(a->is_mul());
|
||||
return static_cast<const nex_mul*>(a);
|
||||
}
|
||||
|
||||
inline nex_mul* to_mul(nex*a) {
|
||||
SASSERT(a->is_mul());
|
||||
return static_cast<nex_mul*>(a);
|
||||
}
|
||||
|
||||
inline const nex_scalar * to_scalar(const nex* a) {
|
||||
SASSERT(a->is_scalar());
|
||||
return static_cast<const nex_scalar*>(a);
|
||||
}
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, const nex& e ) {
|
||||
return e.print(out);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -68,26 +68,33 @@ void test_basic_lemma_for_mon_zero_from_factors_to_monomial();
|
|||
void test_basic_lemma_for_mon_neutral_from_monomial_to_factors();
|
||||
void test_basic_lemma_for_mon_neutral_from_factors_to_monomial();
|
||||
|
||||
void test_cn_on_expr(horner::nex t) {
|
||||
TRACE("nla_cn", tout << "t=" << t << '\n';);
|
||||
cross_nested cn(t, [](const horner::nex& n) {
|
||||
TRACE("nla_cn_test", tout << n << "\n";);
|
||||
return false;
|
||||
} ,
|
||||
[](unsigned) { return false; });
|
||||
cn.run();
|
||||
void test_cn_on_expr(nex_sum *t, cross_nested& cn) {
|
||||
TRACE("nla_cn", tout << "t=" << *t << '\n';);
|
||||
cn.run(t);
|
||||
}
|
||||
|
||||
void test_cn() {
|
||||
typedef horner::nex nex;
|
||||
cross_nested cn([](const nex* n) {
|
||||
TRACE("nla_cn_test", tout << *n << "\n";);
|
||||
return false;
|
||||
} ,
|
||||
[](unsigned) { return false; });
|
||||
enable_trace("nla_cn");
|
||||
enable_trace("nla_cn_details");
|
||||
nex a = nex::var(0), b = nex::var(1), c = nex::var(2), d = nex::var(3), e = nex::var(4), f = nex::var(5), g = nex::var(6);
|
||||
nex min_1 = nex::scalar(rational(-1));
|
||||
nex_var* a = cn.mk_var(0);
|
||||
nex_var* b = cn.mk_var(1);
|
||||
nex_var* c = cn.mk_var(2);
|
||||
nex_var* d = cn.mk_var(3);
|
||||
nex_var* e = cn.mk_var(4);
|
||||
nex_var* f = cn.mk_var(5);
|
||||
nex_var* g = cn.mk_var(6);
|
||||
nex* min_1 = cn.mk_scalar(rational(-1));
|
||||
// test_cn_on_expr(min_1*c*e + min_1*b*d + min_1*a*b + a*c);
|
||||
TRACE("nla_cn", tout << "done\n";);
|
||||
|
||||
test_cn_on_expr(b*c*d - b*c*g);
|
||||
nex* bcd = cn.mk_mul(b, c, d);
|
||||
nex_mul* bcg = cn.mk_mul(b, c, g);
|
||||
bcg->add_child(min_1);
|
||||
nex_sum* t = cn.mk_sum(bcd, bcg);
|
||||
test_cn_on_expr(t, cn);
|
||||
// test_cn_on_expr(a*a*d + a*b*c*d + a*a*c*c*d + a*d*d + e*a*e + e*a*c + e*d);
|
||||
// TRACE("nla_cn", tout << "done\n";);
|
||||
// test_cn_on_expr(a*b*d + a*b*c + c*b*d + a*c*d);
|
||||
|
|
|
|||
Loading…
Reference in a new issue