mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-19 01:32:17 +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-05 17:57:13 -07:00
parent 13a93e2446
commit 35fad92992
2 changed files with 33 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -41,7 +41,11 @@ void horner::lemma_on_row(const T& row) {
if (!row_is_interesting(row)) if (!row_is_interesting(row))
return; return;
nex e = create_expr_from_row(row); nex e = create_expr_from_row(row);
TRACE("nla_cn_details", tout << "cross nested e = " << e << std::endl;); TRACE("nla_cn", tout << "cross nested e = " << e << std::endl;
for (lpvar j: get_vars_of_expr(e)) {
print_var(j, tout);
}
);
interv a = interval_of_expr(e); interv a = interval_of_expr(e);
TRACE("nla_cn_details", tout << "interval a = "; m_intervals.display(tout, a) << "\n";); TRACE("nla_cn_details", tout << "interval a = "; m_intervals.display(tout, a) << "\n";);
check_interval_for_conflict(a, row); check_interval_for_conflict(a, row);
@ -156,7 +160,7 @@ nex horner::split_with_var(const nex& e, lpvar j) {
return e; return e;
nex a, b; nex a, b;
for (const nex & ce: e.children()) { for (const nex & ce: e.children()) {
if (ce.is_mul() && ce.contains(j)) { if ((ce.is_mul() && ce.contains(j)) || (ce.is_var() && ce.var() == j)) {
a.add_child(ce / j); a.add_child(ce / j);
} else { } else {
b.add_child(ce); b.add_child(ce);
@ -204,12 +208,7 @@ nex horner::cross_nested_of_sum(const nex& e) {
} }
template <typename T> nex horner::create_expr_from_row(const T& row) { template <typename T> nex horner::create_expr_from_row(const T& row) {
TRACE("nla_cn", tout << "row="; m_core->print_term(row, tout) << "\n"; TRACE("nla_cn", tout << "row="; m_core->print_term(row, tout) << "\n";);
for (const auto & p : row) {
print_var(p.var(), tout);
}
tout << "\n";
);
nex e; nex e;
if (row.size() > 1) { if (row.size() > 1) {
e.type() = expr_type::SUM; e.type() = expr_type::SUM;
@ -222,10 +221,33 @@ template <typename T> nex horner::create_expr_from_row(const T& row) {
const auto &p = *row.begin(); const auto &p = *row.begin();
return nex::mul(p.coeff(), nexvar(p.var())); return nex::mul(p.coeff(), nexvar(p.var()));
} }
std::cout << "ops\n";
SASSERT(false); SASSERT(false);
return e; return e;
} }
template <typename T>
std::set<lpvar> horner::get_vars_of_expr(const nla_expr<T> &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;
}
}
template <typename T> template <typename T>
void horner::set_interval_for_scalar(interv& a, const T& v) { void horner::set_interval_for_scalar(interv& a, const T& v) {

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

@ -55,5 +55,7 @@ public:
intervals::interval interval_of_mul(const vector<nla_expr<T>>&); intervals::interval interval_of_mul(const vector<nla_expr<T>>&);
template <typename T> template <typename T>
void set_interval_for_scalar(intervals::interval&, const T&); void set_interval_for_scalar(intervals::interval&, const T&);
template <typename T>
std::set<lpvar> get_vars_of_expr(const nla_expr<T> &) const;
}; // end of horner }; // end of horner
} }