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

progress in horner's heuristic

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-07-03 19:21:03 -07:00
parent 2181c982e8
commit 5d2ba2fce1
1 changed files with 18 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -20,6 +20,7 @@
#include "math/lp/horner.h"
#include "math/lp/nla_core.h"
#include "math/lp/lp_utils.h"
namespace nla {
typedef nla_expr<rational> nex;
@ -41,7 +42,7 @@ void horner::lemma_on_row(const T& row) {
return;
nex e = create_expr_from_row(row);
TRACE("nla_cn", tout << "cross nested e = " << e << std::endl;);
intervals::interval a = interval_of_expr(e);
interv a = interval_of_expr(e);
TRACE("nla_cn", tout << "interval a = "; m_intervals.display(tout, a) << "\n";);
check_interval_for_conflict(a, row);
}
@ -202,6 +203,7 @@ nex horner::cross_nested_of_sum(const nex& e) {
}
template <typename T> nex horner::create_expr_from_row(const T& row) {
TRACE("nla_cn", tout << "row="; m_core->m_lar_solver.print_term_as_indices(row, tout););
nex e;
if (row.size() > 1) {
e.type() = expr_type::SUM;
@ -228,7 +230,7 @@ void horner::set_interval_for_scalar(interv& a, const T& v) {
m_intervals.set_upper_is_inf(a, false);
}
intervals::interval horner::interval_of_expr(const nex& e) {
interv horner::interval_of_expr(const nex& e) {
TRACE("nla_cn_details", tout << e.type() << " e=" << e << std::endl;);
interv a;
switch (e.type()) {
@ -251,25 +253,24 @@ intervals::interval horner::interval_of_expr(const nex& e) {
template <typename T>
interv horner::interval_of_mul(const vector<nla_expr<T>>& es) {
interv a = interval_of_expr(es[0]);
if (m_intervals.is_zero(a)) {
TRACE("nla_cn", m_intervals.display(tout, a) << "\ngot zero for " << es[0] << "\n";);
return a;
}
TRACE("nla_cn", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); tout << "\n";);
for (unsigned k = 1; k < es.size(); k++) {
interv b = interval_of_expr(es[k]);
if (m_intervals.is_zero(b)) {
TRACE("nla_cn", m_intervals.display(tout, b) << "\ngot zero for " << es[k] << "\n";);
return b;
}
interv c;
interval_deps deps;
m_intervals.mul(a, b, c, deps);
m_intervals.set(a, c);
m_intervals.add_deps(a, b, deps, a);
TRACE("nla_cn", tout << "es["<< k << "] = " << es[k] << std::endl << "a = "; m_intervals.display(tout, a); tout << "\n";);
if (m_intervals.is_zero(a)) {
TRACE("nla_cn", tout << "got zero\n"; );
break;
}
}
TRACE("nla_cn",
for (const auto &e : es) tout << e;
for (const auto &e : es) {
tout << "("<< e << ")";
}
tout << " interv a = ";
m_intervals.display(tout, a) << "\n";);
return a;
@ -292,10 +293,14 @@ interv horner::interval_of_sum(const vector<nla_expr<T>>& es) {
}
interv c;
interval_deps deps;
TRACE("nla_cn_details", tout << "a = "; m_intervals.display(tout, a) << "\nb = "; m_intervals.display(tout, b) << "\n";);
m_intervals.add(a, b, c, deps);
TRACE("nla_cn_details", tout << "c = "; m_intervals.display(tout, c); tout << "\n";);
m_intervals.set(a, c);
TRACE("nla_cn_details", tout << "a = "; m_intervals.display(tout, a); tout << "\n";);
m_intervals.add_deps(a, b, deps, a);
TRACE("nla_cn_details", tout << "interv = "; m_intervals.display(tout, a); tout << "\n";);
TRACE("nla_cn_details", tout << "final a with deps = "; m_intervals.display(tout, a); tout << "\n";);
if (m_intervals.is_inf(a)) {
TRACE("nla_cn_details", tout << "got infinity\n";);
return a;
@ -311,7 +316,7 @@ void horner::set_var_interval(lpvar v, interv& b) {
}
template <typename T>
void horner::check_interval_for_conflict(const intervals::interval& i, const T& row) {
void horner::check_interval_for_conflict(const interv& i, const T& row) {
if (m_intervals.check_interval_for_conflict_on_zero(i)) {
TRACE("nla_cn", print_lemma(tout););
} else {