From e46de3bc3d87d97db90232cf8a257327c45642f3 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 7 Aug 2019 16:14:46 -0700
Subject: [PATCH] fixes in horner's heuristic
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
src/math/lp/horner.cpp | 15 ++++++++++-----
src/math/lp/nla_expr.h | 18 +++++++++---------
2 files changed, 19 insertions(+), 14 deletions(-)
diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index f951af5de..2c11cc558 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -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) {
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;
lpvar j = -1;
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()));
break;
default:
- TRACE("nla_horner_details", tout << e.type() << "\n";);
- UNREACHABLE();
- SASSERT(false);
+ SASSERT(!e.is_sum());
+ // noop
}
}
// 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();
} else {
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;
a_index = v.size() - 1;
}
diff --git a/src/math/lp/nla_expr.h b/src/math/lp/nla_expr.h
index f1e00d266..83be7f5eb 100644
--- a/src/math/lp/nla_expr.h
+++ b/src/math/lp/nla_expr.h
@@ -177,7 +177,7 @@ public:
}
}
- unsigned size() {
+ unsigned size() const {
switch(m_type) {
case expr_type::SUM:
case expr_type::MUL:
@@ -376,20 +376,20 @@ public:
return *this;
}
+ // we need a linear combination of at least two variables
bool sum_is_a_linear_term() const {
SASSERT(is_sum());
- int degree = 0;
+ TRACE("nla_expr_details", tout << *this << "\n";);
unsigned number_of_non_scalars = 0;
for (auto & e : children()) {
int d = e.get_degree();
- if (d > 1)
- return false;
- if (d > degree)
- degree = d;
- if (!e.is_scalar())
- number_of_non_scalars++;
+ if (d == 0) continue;
+ if (d > 1) return false;
+
+ 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 {