mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
work on horner
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
ad9ecad73c
commit
23a825aff8
|
|
@ -21,8 +21,9 @@
|
|||
#include "math/lp/horner.h"
|
||||
#include "math/lp/nla_core.h"
|
||||
#include "math/lp/lp_utils.h"
|
||||
#include "math/lp/cross_nested.h"
|
||||
|
||||
namespace nla {
|
||||
typedef nla_expr<rational> nex;
|
||||
typedef intervals::interval interv;
|
||||
horner::horner(core * c) : common(c), m_intervals(c, c->reslim()) {}
|
||||
|
||||
|
|
@ -50,44 +51,6 @@ nex* pop_back(vector<nex*>& front) {
|
|||
return c;
|
||||
}
|
||||
|
||||
void horner::cross_nested_of_expr_on_front_elem(nex& e, nex* c, vector<nex*>& front) {
|
||||
SASSERT(c->is_sum());
|
||||
vector<lpvar> occurences = get_mult_occurences(*c);
|
||||
TRACE("nla_cn", tout << "e=" << e << "\nc=" << *c << "\noccurences="; print_vector(occurences, tout) << "\nfront:"; print_vector_of_ptrs(front, tout) << "\n";);
|
||||
|
||||
if (occurences.empty()) {
|
||||
if(front.empty()) {
|
||||
TRACE("nla_cn_cn", tout << "got the cn form: e=" << e << "\n";);
|
||||
SASSERT(!can_be_cross_nested_more(e));
|
||||
auto i = interval_of_expr(e);
|
||||
m_intervals.check_interval_for_conflict_on_zero(i);
|
||||
} else {
|
||||
nex* c = pop_back(front);
|
||||
cross_nested_of_expr_on_front_elem(e, c, front);
|
||||
}
|
||||
} else {
|
||||
TRACE("nla_cn", tout << "save c=" << *c << "front:"; print_vector_of_ptrs(front, tout) << "\n";);
|
||||
nex copy_of_c = *c;
|
||||
for(lpvar j : occurences) {
|
||||
cross_nested_of_expr_on_sum_and_var(e, c, j, front);
|
||||
*c = copy_of_c;
|
||||
TRACE("nla_cn", tout << "restore c=" << *c << ", e=" << e << "\n";);
|
||||
}
|
||||
}
|
||||
TRACE("nla_cn", tout << "exit\n";);
|
||||
}
|
||||
// e is the global expression, c is the sub expressiond which is going to changed from sum to the cross nested form
|
||||
void horner::cross_nested_of_expr_on_sum_and_var(nex& e, nex* c, lpvar j, vector<nex*>& front) {
|
||||
TRACE("nla_cn", tout << "e=" << e << "\nc=" << *c << "\nj = v" << j << "\nfront="; print_vector_of_ptrs(front, tout) << "\n";);
|
||||
split_with_var(*c, j, front);
|
||||
TRACE("nla_cn", tout << "after split c=" << *c << "\nfront="; print_vector_of_ptrs(front, tout) << "\n";);
|
||||
do {
|
||||
nex* n = pop_back(front);
|
||||
cross_nested_of_expr_on_front_elem(e, n, front);
|
||||
} while (!front.empty());
|
||||
}
|
||||
|
||||
|
||||
template <typename T>
|
||||
void horner::lemmas_on_row(const T& row) {
|
||||
if (!row_is_interesting(row))
|
||||
|
|
@ -120,151 +83,6 @@ nex horner::nexvar(lpvar j) const {
|
|||
return e;
|
||||
}
|
||||
|
||||
void process_var_occurences(lpvar j, std::unordered_set<lpvar>& seen, std::unordered_map<lpvar, unsigned>& occurences) {
|
||||
if (seen.find(j) != seen.end()) return;
|
||||
seen.insert(j);
|
||||
auto it = occurences.find(j);
|
||||
if (it == occurences.end())
|
||||
occurences[j] = 1;
|
||||
else
|
||||
it->second ++;
|
||||
}
|
||||
|
||||
void process_mul_occurences(const nex& e, std::unordered_set<lpvar>& seen, std::unordered_map<lpvar, unsigned>& occurences) {
|
||||
SASSERT(e.type() == expr_type::MUL);
|
||||
for (const auto & ce : e.children()) {
|
||||
if (ce.type() == expr_type::VAR) {
|
||||
process_var_occurences(ce.var(), seen, occurences);
|
||||
} else if (ce.type() == expr_type::MUL){
|
||||
process_mul_occurences(ce, seen, occurences);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
// j -> the number of expressions j appears in as a multiplier
|
||||
vector<lpvar> horner::get_mult_occurences(const nex& e) const {
|
||||
std::unordered_map<lpvar, unsigned> occurences;
|
||||
SASSERT(e.type() == expr_type::SUM);
|
||||
for (const auto & ce : e.children()) {
|
||||
std::unordered_set<lpvar> seen;
|
||||
if (ce.type() == expr_type::MUL) {
|
||||
for (const auto & cce : ce.children()) {
|
||||
if (cce.type() == expr_type::VAR) {
|
||||
process_var_occurences(cce.var(), seen, occurences);
|
||||
} else if (cce.type() == expr_type::MUL) {
|
||||
process_mul_occurences(cce, seen, occurences);
|
||||
} else {
|
||||
continue;
|
||||
}
|
||||
}
|
||||
} else if (ce.type() == expr_type::VAR) {
|
||||
process_var_occurences(ce.var(), seen, occurences);
|
||||
}
|
||||
}
|
||||
TRACE("nla_cn_details",
|
||||
tout << "{";
|
||||
for(auto p: occurences) {
|
||||
tout << "(v" << p.first << "->" << p.second << ")";
|
||||
}
|
||||
tout << "}" << std::endl;);
|
||||
vector<lpvar> r;
|
||||
for(auto p: occurences) {
|
||||
if (p.second > 1)
|
||||
r.push_back(p.first);
|
||||
}
|
||||
return r;
|
||||
}
|
||||
bool horner::can_be_cross_nested_more(const nex& e) const {
|
||||
switch (e.type()) {
|
||||
case expr_type::SCALAR:
|
||||
return false;
|
||||
case expr_type::SUM: {
|
||||
return !get_mult_occurences(e).empty();
|
||||
}
|
||||
case expr_type::MUL:
|
||||
{
|
||||
for (const auto & c: e.children()) {
|
||||
if (can_be_cross_nested_more(c))
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
case expr_type::VAR:
|
||||
return false;
|
||||
default:
|
||||
TRACE("nla_cn_details", tout << e.type() << "\n";);
|
||||
SASSERT(false);
|
||||
return false;
|
||||
}
|
||||
}
|
||||
void horner::split_with_var(nex& e, lpvar j, vector<nex*> & front) {
|
||||
TRACE("nla_cn_details", tout << "e = " << e << ", j = v" << j << "\n";);
|
||||
if (!e.is_sum())
|
||||
return;
|
||||
nex a, 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);
|
||||
} else {
|
||||
b.add_child(ce);
|
||||
}
|
||||
}
|
||||
a.type() = expr_type::SUM;
|
||||
TRACE("nla_cn_details", tout << "a = " << a << "\n";);
|
||||
SASSERT(a.children().size() >= 2);
|
||||
|
||||
if (b.children().size() == 1) {
|
||||
nex t = b.children()[0];
|
||||
b = t;
|
||||
} else if (b.children().size() > 1) {
|
||||
b.type() = expr_type::SUM;
|
||||
}
|
||||
|
||||
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) {
|
||||
front.push_back(&e.children().back());
|
||||
TRACE("nla_cn_details", tout << "push to front " << e.children().back() << "\n";);
|
||||
}
|
||||
|
||||
} else {
|
||||
TRACE("nla_cn_details", tout << "b = " << b << "\n";);
|
||||
e = nex::sum(nex::mul(nex::var(j), a), b);
|
||||
if (a.is_sum()) {
|
||||
front.push_back(&(e.children()[0].children()[1]));
|
||||
TRACE("nla_cn_details", tout << "push to front " << e.children()[0].children()[1] << "\n";);
|
||||
}
|
||||
if (b.is_sum()) {
|
||||
front.push_back(&(e.children()[1]));
|
||||
TRACE("nla_cn_details", tout << "push to front " << e.children()[1] << "\n";);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
nex horner::cross_nested_of_sum(const nex& e, lpvar j) {
|
||||
if (!e.is_sum())
|
||||
return e;
|
||||
/*
|
||||
std::unordered_map<lpvar, unsigned> occurences;
|
||||
get_occurences_map(e, occurences);
|
||||
lpvar j = random_most_occured_var(occurences);
|
||||
if (j + 1 == 0) return e;
|
||||
TRACE("nla_cn_details",
|
||||
tout << "e = " << e << "\noccurences ";
|
||||
for (auto p : occurences){
|
||||
tout << "(v"<<p.first << ", "<< p.second<<")";
|
||||
}
|
||||
tout << std::endl << "most occured = v" << j << std::endl;);
|
||||
nex ret = split_with_var(e, j);
|
||||
TRACE("nla_cn_details", tout << "ret =" << ret << "\n";);
|
||||
return ret;*/
|
||||
SASSERT(false);
|
||||
return nex();
|
||||
}
|
||||
|
||||
template <typename T> nex horner::create_sum_from_row(const T& row) {
|
||||
TRACE("nla_cn", tout << "row="; m_core->print_term(row, tout) << "\n";);
|
||||
|
|
@ -276,29 +94,6 @@ template <typename T> nex horner::create_sum_from_row(const T& row) {
|
|||
return e;
|
||||
}
|
||||
|
||||
std::set<lpvar> horner::get_vars_of_expr(const nex &e ) const {
|
||||
std::set<lpvar> r;
|
||||
switch (e.type()) {
|
||||
case expr_type::SCALAR:
|
||||
return r;
|
||||
case expr_type::SUM:
|
||||
case expr_type::MUL:
|
||||
{
|
||||
for (const auto & c: e.children())
|
||||
for ( lpvar j : get_vars_of_expr(c))
|
||||
r.insert(j);
|
||||
}
|
||||
return r;
|
||||
case expr_type::VAR:
|
||||
r.insert(e.var());
|
||||
return r;
|
||||
default:
|
||||
TRACE("nla_cn_details", tout << e.type() << "\n";);
|
||||
SASSERT(false);
|
||||
return r;
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
void horner::set_interval_for_scalar(interv& a, const rational& v) {
|
||||
m_intervals.set_lower(a, v);
|
||||
|
|
|
|||
|
|
@ -41,17 +41,10 @@ public:
|
|||
intervals::interval interval_of_expr(const nex& e);
|
||||
|
||||
nex nexvar(lpvar j) const;
|
||||
nex cross_nested_of_sum(const nex&, lpvar);
|
||||
vector<lpvar> get_mult_occurences(const nex& e) const;
|
||||
void split_with_var(nex &, lpvar, vector<nex*> & front);
|
||||
void set_var_interval(lpvar j, intervals::interval&);
|
||||
intervals::interval interval_of_sum(const vector<nex>&);
|
||||
intervals::interval interval_of_mul(const vector<nex>&);
|
||||
void set_interval_for_scalar(intervals::interval&, const rational&);
|
||||
std::set<lpvar> get_vars_of_expr(const nex &) const;
|
||||
void lemmas_on_expr(nex &);
|
||||
void cross_nested_of_expr_on_front_elem(nex& , nex*, vector<nex*>& front);
|
||||
void cross_nested_of_expr_on_sum_and_var(nex& , nex*, lpvar, vector<nex*>& front);
|
||||
bool can_be_cross_nested_more(const nex&) const;
|
||||
}; // end of horner
|
||||
}
|
||||
|
|
|
|||
|
|
@ -119,7 +119,7 @@ public:
|
|||
case expr_type::MUL:
|
||||
return print_mul(out);
|
||||
case expr_type::VAR:
|
||||
out << "v" << m_j;
|
||||
out << static_cast<char>('a'+m_j);
|
||||
return out;
|
||||
case expr_type::SCALAR:
|
||||
out << m_v;
|
||||
|
|
@ -223,6 +223,51 @@ public:
|
|||
return false;
|
||||
}
|
||||
};
|
||||
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);
|
||||
}
|
||||
|
||||
template <typename T>
|
||||
nla_expr<T> operator*(const nla_expr<T>& a, const nla_expr<T>& b) {
|
||||
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);
|
||||
}
|
||||
|
||||
|
||||
template <typename T>
|
||||
nla_expr<T> operator/(const nla_expr<T>& a, lpvar j) {
|
||||
SASSERT((a.is_mul() && a.contains(j)) || (a.is_var() && a.var() == j));
|
||||
|
|
|
|||
|
|
@ -69,11 +69,10 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial();
|
|||
void test_cn() {
|
||||
typedef horner::nex nex;
|
||||
enable_trace("nla_cn");
|
||||
|
||||
// (a(a+(b+c)c+d)d + e(a(e+c)+d)
|
||||
nex a = nex::var(0), b = nex::var(1), c = nex::var(2), d = nex::var(3), e = nex::var(4);
|
||||
nex aad = nex::mul(a, a, d);
|
||||
|
||||
|
||||
nex t = a*a*d + a*b*c*d + a*c*c*d + e*a*e + e*a*c + e*d;
|
||||
TRACE("nla_cn", tout << "t=" << t << '\n';);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in a new issue