From 82115e69acba3ba68fbdd6e952eced76a3e28eaa Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 31 Jul 2019 12:32:23 -0700 Subject: [PATCH] filter rows for horner's scheme earlier Signed-off-by: Lev Nachmanson --- src/math/lp/horner.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index f6b48cdd2..506a6de78 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -82,8 +82,7 @@ bool horner::lemmas_on_expr(nex& e) { template bool horner::lemmas_on_row(const T& row) { - if (!row_is_interesting(row)) - return false; + SASSERT (row_is_interesting(row)); nex e = create_sum_from_row(row); return lemmas_on_expr(e); } @@ -96,14 +95,15 @@ void horner::horner_lemmas() { const auto& matrix = c().m_lar_solver.A_r(); // choose only rows that depend on m_to_refine variables - std::set rows_to_check; // we need it to be determenistic: cannow work with the unordered_set + std::set rows_to_check; // we need it to be determenistic: cannot work with the unordered_set for (lpvar j : c().m_to_refine) { for (auto & s : matrix.m_columns[j]) rows_to_check.insert(s.var()); } svector rows; for (unsigned i : rows_to_check) { - rows.push_back(i); + if (row_is_interesting(matrix.m_rows[i])) + rows.push_back(i); } unsigned r = c().random();