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

fixes in horner's heuristic

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-08-07 16:14:46 -07:00
parent 1b8b09cddb
commit e46de3bc3d
2 changed files with 19 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -206,7 +206,11 @@ interv horner::interval_of_mul(const nex& e) {
void horner::add_mul_to_vector(const nex& e, vector<std::pair<rational, lpvar>> &v) { void horner::add_mul_to_vector(const nex& e, vector<std::pair<rational, lpvar>> &v) {
TRACE("nla_horner_details", tout << e << "\n";); TRACE("nla_horner_details", tout << e << "\n";);
SASSERT(e.is_mul() && e.children().size() == 2); SASSERT(e.is_mul() && e.size() > 0);
if (e.size() == 1) {
add_linear_to_vector(*(e.children().begin()), v);
return;
}
rational r; rational r;
lpvar j = -1; lpvar j = -1;
for (const nex & c : e.children()) { for (const nex & c : e.children()) {
@ -236,9 +240,8 @@ void horner::add_linear_to_vector(const nex& e, vector<std::pair<rational, lpvar
v.push_back(std::make_pair(rational(1), e.var())); v.push_back(std::make_pair(rational(1), e.var()));
break; break;
default: default:
TRACE("nla_horner_details", tout << e.type() << "\n";); SASSERT(!e.is_sum());
UNREACHABLE(); // noop
SASSERT(false);
} }
} }
// e = a * can_t + b // e = a * can_t + b
@ -253,7 +256,9 @@ lp::lar_term horner::expression_to_normalized_term(nex& e, rational& a, rational
b += c.value(); b += c.value();
} else { } else {
add_linear_to_vector(c, v); add_linear_to_vector(c, v);
if (v.size() == 1 || smallest_j > v.back().second) { if (v.empty())
continue;
if (v.size() == 1 || smallest_j > v.back().second) {
smallest_j = v.back().second; smallest_j = v.back().second;
a_index = v.size() - 1; a_index = v.size() - 1;
} }

18
src/math/lp/nla_expr.h
View file

@ -177,7 +177,7 @@ public:
} }
} }
unsigned size() { unsigned size() const {
switch(m_type) { switch(m_type) {
case expr_type::SUM: case expr_type::SUM:
case expr_type::MUL: case expr_type::MUL:
@ -376,20 +376,20 @@ public:
return *this; return *this;
} }
// we need a linear combination of at least two variables
bool sum_is_a_linear_term() const { bool sum_is_a_linear_term() const {
SASSERT(is_sum()); SASSERT(is_sum());
int degree = 0; TRACE("nla_expr_details", tout << *this << "\n";);
unsigned number_of_non_scalars = 0; unsigned number_of_non_scalars = 0;
for (auto & e : children()) { for (auto & e : children()) {
int d = e.get_degree(); int d = e.get_degree();
if (d > 1) if (d == 0) continue;
return false; if (d > 1) return false;
if (d > degree)
degree = d; number_of_non_scalars++;
if (!e.is_scalar())
number_of_non_scalars++;
} }
return degree == 1 && number_of_non_scalars > 1; TRACE("nla_expr_details", tout << (number_of_non_scalars > 1?"linear":"non-linear") << "\n";);
return number_of_non_scalars > 1;
} }
int get_degree() const { int get_degree() const {