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

full exploration in horner

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-07-09 16:56:45 -07:00
parent 97ef190f4f
commit ef3ad55e0c
3 changed files with 45 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -42,43 +42,49 @@ void horner::lemmas_on_expr(nex& e) {
vector<nex*> front;
front.push_back(&e);
cross_nested_of_expr(e, front);
}
void horner::cross_nested_of_expr(nex& e, vector<nex*> & front) {
void horner::cross_nested_of_expr(nex& e, vector<nex*> front) {
TRACE("nla_cn", tout << "e = " << e << ", front has " << front.size() << "\n";);
if (front.empty()) {
while (!front.empty()) {
nex& c = *front.back();
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) {
TRACE("nla_cn", tout << "e=" << e << "\nc=" << c << "\n";);
SASSERT(c.is_sum());
auto occurences = get_mult_occurences(c);
if (occurences.empty() && 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);
}
nex & c = *(front.back());
front.pop_back();
TRACE("nla_cn", tout << "pop from front\n";);
cross_nested_of_expr_on_front_elem(e, c, front);
}
void horner::cross_nested_of_expr_on_front_elem(nex& e, nex& c, vector<nex*> & front) {
SASSERT(c.is_sum());
std::unordered_map<unsigned, lpvar> occurences;
TRACE("nla_cn", tout << "c = " << c << "\n";);
get_occurences_map(c, occurences);
nex copy_of_c(c);
for(const auto & p : occurences) {
TRACE("nla_cn", tout << "v" << p.first << ", " << p.second << "\n";);
if (p.second < 2)
continue;
cross_nested_of_expr_on_sum_and_var(e, c, p.first, front);
c = copy_of_c;
} else {
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 << "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 << "\n";);
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";);
split_with_var(c, j, front);
cross_nested_of_expr(e, front);
TRACE("nla_cn", tout << "after split c=" << c << "\n";);
do {
nex& c = *front.back();
front.pop_back();
cross_nested_of_expr_on_front_elem(e, c, front);
} while (!front.empty());
}
template <typename T>
void horner::lemmas_on_row(const T& row) {
if (!row_is_interesting(row))
@ -137,7 +143,8 @@ void process_mul_occurences(const nex& e, std::unordered_set<lpvar>& seen, std::
// j -> the number of expressions j appears in as a multiplier
void horner::get_occurences_map(const nla_expr<rational>& e, std::unordered_map<lpvar, unsigned>& occurences) const {
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;
@ -159,12 +166,18 @@ void horner::get_occurences_map(const nla_expr<rational>& e, std::unordered_map<
SASSERT(false);
}
}
TRACE("nla_cn_details",
TRACE("nla_cn",
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;
}
void horner::split_with_var(nex& e, lpvar j, vector<nex*> & front) {

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

@ -42,8 +42,7 @@ public:
nex nexvar(lpvar j) const;
nex cross_nested_of_sum(const nex&, lpvar);
void get_occurences_map(const nex& e,
std::unordered_map<unsigned, lpvar>& ) const;
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>&);
@ -51,8 +50,8 @@ public:
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(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(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);
}; // end of horner
}

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

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