diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h
index 835f563bc..4b281efdc 100644
--- a/src/math/lp/cross_nested.h
+++ b/src/math/lp/cross_nested.h
@@ -24,9 +24,18 @@ namespace nla {
class cross_nested {
typedef nla_expr<rational> nex;
nex& m_e;
- std::function<void (const nex&)> m_call_on_result;
+ std::function<bool (const nex&)> m_call_on_result;
+ std::function<bool (unsigned)> m_var_is_fixed;
+ bool m_done;
public:
- cross_nested(nex &e, std::function<void (const nex&)> call_on_result): m_e(e), m_call_on_result(call_on_result) {}
+ cross_nested(nex &e,
+ std::function<bool (const nex&)> call_on_result,
+ std::function<bool (unsigned)> var_is_fixed):
+ m_e(e),
+ m_call_on_result(call_on_result),
+ m_var_is_fixed(var_is_fixed),
+ m_done(false)
+ {}
void run() {
vector<nex*> front;
@@ -123,7 +132,15 @@ public:
for(auto& p : occurences) {
SASSERT(p.second.m_occs > 1);
lpvar j = p.first;
+ if (m_var_is_fixed(j)) {
+ // it does not make sense to explore fixed multupliers
+ // because the interval products do not become smaller
+ // after factoring those out
+ continue;
+ }
explore_of_expr_on_sum_and_var(c, j, front);
+ if (m_done)
+ return;
*c = copy_of_c;
TRACE("nla_cn", tout << "restore c=" << *c << ", m_e=" << m_e << "\n";);
restore_front(copy_of_front, front);
@@ -151,7 +168,7 @@ public:
if (occurences.empty()) {
if(front.empty()) {
TRACE("nla_cn", tout << "got the cn form: =" << m_e << "\n";);
- m_call_on_result(m_e);
+ m_done = m_call_on_result(m_e);
} else {
nex* c = pop_back(front);
explore_expr_on_front_elem(c, front);
diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index d51b9e159..e8ce097b8 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -52,23 +52,29 @@ bool horner::row_is_interesting(const T& row) const {
return false;
}
-void horner::lemmas_on_expr(nex& e) {
- TRACE("nla_horner", tout << "e = " << e << "\n";);
- cross_nested cn(e, [this](const nex& n) {
+bool horner::lemmas_on_expr(nex& e) {
+ TRACE("nla_horner", tout << "e = " << e << "\n";);
+ bool conflict = false;
+ cross_nested cn(e, [this, & conflict](const nex& n) {
auto i = interval_of_expr(n);
TRACE("nla_horner", tout << "callback n = " << n << "\ni="; m_intervals.display(tout, i) << "\n";);
- m_intervals.check_interval_for_conflict_on_zero(i);} );
+ conflict = m_intervals.check_interval_for_conflict_on_zero(i);
+ return conflict;
+ },
+ [this](unsigned j) { return c().var_is_fixed(j); }
+ );
cn.run();
+ return conflict;
}
template <typename T>
-void horner::lemmas_on_row(const T& row) {
+bool horner::lemmas_on_row(const T& row) {
if (!row_is_interesting(row))
- return;
+ return false;
nex e = create_sum_from_row(row);
- lemmas_on_expr(e);
+ return lemmas_on_expr(e);
}
void horner::horner_lemmas() {
@@ -84,8 +90,16 @@ void horner::horner_lemmas() {
for (auto & s : matrix.m_columns[j])
rows_to_check.insert(s.var());
}
- for (unsigned i : rows_to_check) {
- lemmas_on_row(matrix.m_rows[i]);
+ svector<unsigned> rows;
+ for (unsigned i : rows_to_check) {
+ rows.push_back(i);
+ }
+
+ unsigned r = c().random();
+ unsigned sz = rows.size();
+ for (unsigned i = 0; i < sz; i++) {
+ if (lemmas_on_row(matrix.m_rows[(i + r) % sz]))
+ break;
}
}
@@ -145,7 +159,6 @@ interv horner::interval_of_expr(const nex& e) {
interv horner::interval_of_mul(const nex& e) {
SASSERT(e.is_mul());
auto & es = e.children();
- interval_deps_combine_rule comb_rule;
interv a = interval_of_expr(es[0]);
if (m_intervals.is_zero(a)) {
m_intervals.set_zero_interval_deps_for_mult(a);
@@ -161,9 +174,11 @@ interv horner::interval_of_mul(const nex& e) {
TRACE("nla_horner_details", tout << "got zero\n"; );
return b;
}
- TRACE("nla_horner_details", tout << "es[k]= "<< es[k] << ", "; m_intervals.display(tout, b); );
+ TRACE("nla_horner_details", tout << "es[" << k << "] "<< es[k] << ", "; m_intervals.display(tout, b); );
interv c;
+ interval_deps_combine_rule comb_rule;
m_intervals.mul(a, b, c, comb_rule);
+ TRACE("nla_horner_details", tout << "c before combine_deps() "; m_intervals.display(tout, c););
m_intervals.combine_deps(a, b, comb_rule, c);
TRACE("nla_horner_details", tout << "a "; m_intervals.display(tout, a););
TRACE("nla_horner_details", tout << "c "; m_intervals.display(tout, c););
diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h
index e45a92512..a08852956 100644
--- a/src/math/lp/horner.h
+++ b/src/math/lp/horner.h
@@ -35,7 +35,7 @@ public:
horner(core *core);
void horner_lemmas();
template <typename T> // T has an iterator of (coeff(), var())
- void lemmas_on_row(const T&);
+ bool lemmas_on_row(const T&);
template <typename T> bool row_is_interesting(const T&) const;
template <typename T> nex create_sum_from_row(const T&);
intervals::interval interval_of_expr(const nex& e);
@@ -46,6 +46,6 @@ public:
void set_interval_for_scalar(intervals::interval&, const rational&);
void set_var_interval(lpvar j, intervals::interval&);
std::set<lpvar> get_vars_of_expr(const nex &) const;
- void lemmas_on_expr(nex &);
+ bool lemmas_on_expr(nex &);
}; // end of horner
}
diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h
index e60884fcb..5581bdce1 100644
--- a/src/math/lp/nla_intervals.h
+++ b/src/math/lp/nla_intervals.h
@@ -74,7 +74,8 @@ class intervals : common {
};
- void add_deps(interval const& a, interval const& b, interval_deps_combine_rule const& deps, interval& i) const {
+ void add_deps(interval const& a, interval const& b,
+ interval_deps_combine_rule const& deps, interval& i) const {
i.m_lower_dep = mk_dependency(a, b, deps.m_lower_combine);
i.m_upper_dep = mk_dependency(a, b, deps.m_upper_combine);
}
@@ -176,8 +177,8 @@ public:
void add(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.add(a, b, c, deps); }
void set(interval& a, const interval& b) {
m_imanager.set(a, b);
- a.m_lower_dep = b.m_lower_dep;
- a.m_upper_dep = b.m_upper_dep;
+ a.m_lower_dep = lower_is_inf(a)? nullptr : b.m_lower_dep;
+ a.m_upper_dep = upper_is_inf(a)?nullptr : b.m_upper_dep;
}
void mul(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.mul(a, b, c, deps); }
void combine_deps(interval const& a, interval const& b, interval_deps_combine_rule const& deps, interval& i) const {
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index 25cdd75c3..f25d10f40 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -72,7 +72,9 @@ void test_cn_on_expr(horner::nex t) {
TRACE("nla_cn", tout << "t=" << t << '\n';);
cross_nested cn(t, [](const horner::nex& n) {
TRACE("nla_cn_test", tout << n << "\n";);
- } );
+ return false;
+ } ,
+ [](unsigned) { return false; });
cn.run();
}