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

filter rows for horner's scheme earlier

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-07-31 12:32:23 -07:00
parent aef26598e5
commit 82115e69ac
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -82,8 +82,7 @@ bool horner::lemmas_on_expr(nex& e) {
template <typename T> template <typename T>
bool horner::lemmas_on_row(const T& row) { bool horner::lemmas_on_row(const T& row) {
if (!row_is_interesting(row)) SASSERT (row_is_interesting(row));
return false;
nex e = create_sum_from_row(row); nex e = create_sum_from_row(row);
return lemmas_on_expr(e); return lemmas_on_expr(e);
} }
@ -96,14 +95,15 @@ void horner::horner_lemmas() {
const auto& matrix = c().m_lar_solver.A_r(); const auto& matrix = c().m_lar_solver.A_r();
// choose only rows that depend on m_to_refine variables // choose only rows that depend on m_to_refine variables
std::set<unsigned> rows_to_check; // we need it to be determenistic: cannow work with the unordered_set std::set<unsigned> rows_to_check; // we need it to be determenistic: cannot work with the unordered_set
for (lpvar j : c().m_to_refine) { for (lpvar j : c().m_to_refine) {
for (auto & s : matrix.m_columns[j]) for (auto & s : matrix.m_columns[j])
rows_to_check.insert(s.var()); rows_to_check.insert(s.var());
} }
svector<unsigned> rows; svector<unsigned> rows;
for (unsigned i : rows_to_check) { 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(); unsigned r = c().random();