mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

work on horner

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-07-10 16:22:28 -07:00
parent d0ab508619
commit ee4da1affd
5 changed files with 57 additions and 41 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

80
src/math/lp/horner.cpp
View file

@ -21,7 +21,6 @@
#include "math/lp/horner.h" #include "math/lp/horner.h"
#include "math/lp/nla_core.h" #include "math/lp/nla_core.h"
#include "math/lp/lp_utils.h" #include "math/lp/lp_utils.h"
namespace nla { namespace nla {
typedef nla_expr<rational> nex; typedef nla_expr<rational> nex;
typedef intervals::interval interv; typedef intervals::interval interv;
@ -39,48 +38,59 @@ bool horner::row_is_interesting(const T& row) const {
} }
void horner::lemmas_on_expr(nex& e) { void horner::lemmas_on_expr(nex& e) {
TRACE("nla_cn", tout << "e = " << e << "\n";);
vector<nex*> front; vector<nex*> front;
front.push_back(&e); front.push_back(&e);
cross_nested_of_expr(e, front); cross_nested_of_expr(e, front);
} }
void horner::cross_nested_of_expr(nex& e, vector<nex*> front) { nex* pop_back(vector<nex*>& front) {
TRACE("nla_cn", tout << "e = " << e << ", front has " << front.size() << "\n";); nex* c = front.back();
while (!front.empty()) { front.pop_back();
nex& c = *front.back(); return c;
front.pop_back();
cross_nested_of_expr_on_front_elem(e, c, front);
}
TRACE("nla_cn", tout << "empty front: e=" << "\n";);
} }
void horner::cross_nested_of_expr_on_front_elem(nex& e, nex& c, vector<nex*> front) { void horner::cross_nested_of_expr(nex& e, vector<nex*>& front) {
TRACE("nla_cn", tout << "e=" << e << "\nc=" << c << "\n";); TRACE("nla_cn", tout << "e = " << e << ", front:"; print_vector_of_ptrs(front, tout) << "\n";);
SASSERT(c.is_sum()); while (!front.empty()) {
auto occurences = get_mult_occurences(c); nex* c = pop_back(front);
if (occurences.empty() && front.empty()) { cross_nested_of_expr_on_front_elem(e, c, front);
TRACE("nla_cn", tout << "empty front: e=" << e << "\n";); }
auto i = interval_of_expr(e); }
m_intervals.check_interval_for_conflict_on_zero(i);
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", tout << "empty front: e=" << e << "\n";);
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 { } else {
nex copy_of_c = c; TRACE("nla_cn", tout << "save c=" << *c << "front:"; print_vector_of_ptrs(front, tout) << "\n";);
nex copy_of_c = *c;
for(lpvar j : occurences) { for(lpvar j : occurences) {
cross_nested_of_expr_on_sum_and_var(e, c, j, front); cross_nested_of_expr_on_sum_and_var(e, c, j, front);
c = copy_of_c; *c = copy_of_c;
TRACE("nla_cn", tout << "restore c=" << *c << ", e=" << e << "\n";);
} }
} }
TRACE("nla_cn", tout << "exit\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 // 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) { 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 << "\n";); 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); split_with_var(*c, j, front);
TRACE("nla_cn", tout << "after split c=" << c << "\n";); TRACE("nla_cn", tout << "after split c=" << *c << "\nfront="; print_vector_of_ptrs(front, tout) << "\n";);
do { do {
nex& c = *front.back(); nex* n = pop_back(front);
front.pop_back(); cross_nested_of_expr_on_front_elem(e, n, front);
cross_nested_of_expr_on_front_elem(e, c, front);
} while (!front.empty()); } while (!front.empty());
} }
@ -166,7 +176,7 @@ vector<lpvar> horner::get_mult_occurences(const nex& e) const {
SASSERT(false); SASSERT(false);
} }
} }
TRACE("nla_cn", TRACE("nla_cn_details",
tout << "{"; tout << "{";
for(auto p: occurences) { for(auto p: occurences) {
tout << "(v" << p.first << "->" << p.second << ")"; tout << "(v" << p.first << "->" << p.second << ")";
@ -181,7 +191,7 @@ vector<lpvar> horner::get_mult_occurences(const nex& e) const {
} }
void horner::split_with_var(nex& e, lpvar j, vector<nex*> & front) { void horner::split_with_var(nex& e, lpvar j, vector<nex*> & front) {
TRACE("nla_cn", tout << "e = " << e << ", j = v" << j << "\n";); TRACE("nla_cn_details", tout << "e = " << e << ", j = v" << j << "\n";);
if (!e.is_sum()) if (!e.is_sum())
return; return;
nex a, b; nex a, b;
@ -193,7 +203,7 @@ void horner::split_with_var(nex& e, lpvar j, vector<nex*> & front) {
} }
} }
a.type() = expr_type::SUM; a.type() = expr_type::SUM;
TRACE("nla_cn", tout << "a = " << a << "\n";); TRACE("nla_cn_details", tout << "a = " << a << "\n";);
SASSERT(a.children().size() >= 2); SASSERT(a.children().size() >= 2);
if (b.children().size() == 1) { if (b.children().size() == 1) {
@ -210,20 +220,20 @@ void horner::split_with_var(nex& e, lpvar j, vector<nex*> & front) {
e.add_child(a); e.add_child(a);
if (a.size() > 1) { if (a.size() > 1) {
front.push_back(&e.children().back()); front.push_back(&e.children().back());
TRACE("nla_cn", tout << "push to front " << e.children().back() << "\n";); TRACE("nla_cn_details", tout << "push to front " << e.children().back() << "\n";);
} }
} else { } else {
TRACE("nla_cn", tout << "b = " << b << "\n";); TRACE("nla_cn_details", tout << "b = " << b << "\n";);
e = nex::sum(nex::mul(nex::var(j), a), b); e = nex::sum(nex::mul(nex::var(j), a), b);
if (a.is_sum()) { if (a.is_sum()) {
front.push_back(&(e.children()[0].children()[1])); front.push_back(&(e.children()[0].children()[1]));
TRACE("nla_cn", tout << "push to front " << e.children()[0].children()[1] << "\n";); TRACE("nla_cn_details", tout << "push to front " << e.children()[0].children()[1] << "\n";);
} }
if (b.is_sum()) { if (b.is_sum()) {
front.push_back(&(e.children()[1])); front.push_back(&(e.children()[1]));
TRACE("nla_cn", tout << "push to front " << e.children()[1] << "\n";); TRACE("nla_cn_details", tout << "push to front " << e.children()[1] << "\n";);
} }
} }
} }

6
src/math/lp/horner.h
View file

@ -50,8 +50,8 @@ public:
void set_interval_for_scalar(intervals::interval&, const rational&); void set_interval_for_scalar(intervals::interval&, const rational&);
std::set<lpvar> get_vars_of_expr(const nex &) const; std::set<lpvar> get_vars_of_expr(const nex &) const;
void lemmas_on_expr(nex &); void lemmas_on_expr(nex &);
void cross_nested_of_expr(nex& , vector<nex*> front); void cross_nested_of_expr(nex& , vector<nex*>& front);
void cross_nested_of_expr_on_front_elem(nex& , nex&, vector<nex*> front); 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); void cross_nested_of_expr_on_sum_and_var(nex& , nex*, lpvar, vector<nex*>& front);
}; // end of horner }; // end of horner
} }

6
src/math/lp/lp_utils.h
View file

@ -29,6 +29,12 @@ std::ostream& print_vector(const C & t, std::ostream & out) {
out << p << " "; out << p << " ";
return out; return out;
} }
template <typename C>
std::ostream& print_vector_of_ptrs(const C & t, std::ostream & out) {
for (const auto & p : t)
out << (*p) << ", ";
return out;
}
template <typename C, typename D> template <typename C, typename D>
bool contains(const C & collection, const D & key) { bool contains(const C & collection, const D & key) {

4
src/math/lp/nla_intervals.cpp
View file

@ -90,7 +90,7 @@ bool intervals::check_interval_for_conflict_on_zero_upper(const interval & i) {
svector<lp::constraint_index> expl; svector<lp::constraint_index> expl;
m_dep_manager.linearize(i.m_upper_dep, expl); m_dep_manager.linearize(i.m_upper_dep, expl);
_().current_expl().add_expl(expl); _().current_expl().add_expl(expl);
TRACE("nla_cn", print_lemma(tout);); TRACE("nla_cn_lemmas", print_lemma(tout););
return true; return true;
} }
@ -105,7 +105,7 @@ bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i) {
svector<lp::constraint_index> expl; svector<lp::constraint_index> expl;
m_dep_manager.linearize(i.m_lower_dep, expl); m_dep_manager.linearize(i.m_lower_dep, expl);
_().current_expl().add_expl(expl); _().current_expl().add_expl(expl);
TRACE("nla_cn", print_lemma(tout);); TRACE("nla_cn_lemmas", print_lemma(tout););
return true; return true;
} }

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

@ -31,8 +31,8 @@ namespace nla {
// nonlinear integer incremental linear solver // nonlinear integer incremental linear solver
class solver { class solver {
core* m_core;
reslimit m_res_limit; reslimit m_res_limit;
core* m_core;
public: public:
void add_monomial(lpvar v, unsigned sz, lpvar const* vs); void add_monomial(lpvar v, unsigned sz, lpvar const* vs);