mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-18 09:12:16 +00:00
Code Activity

debug horner

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-07-05 15:32:12 -07:00
parent 87cc5c8d96
commit 8d808983f5
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -56,8 +56,8 @@ void horner::horner_lemmas() {
const auto& m = c().m_lar_solver.A_r(); const auto& m = c().m_lar_solver.A_r();
unsigned r = random(); unsigned r = random();
unsigned s = m.row_count(); unsigned s = m.row_count();
for (unsigned i = 0; i < s && !done(); i++) { for (unsigned i = 0; i < s && c().m_lemma_vec->size() < 3 ; i++) {
lemma_on_row(m.m_rows[((i + r) %s)]); lemma_on_row(m.m_rows[((i + r) % s)]);
} }
} }
@ -86,7 +86,7 @@ void process_mul_occurences(const nex& e, std::unordered_set<lpvar>& seen, std::
SASSERT(e.type() == expr_type::MUL); SASSERT(e.type() == expr_type::MUL);
for (const auto & ce : e.children()) { for (const auto & ce : e.children()) {
if (ce.type() == expr_type::SCALAR) { if (ce.type() == expr_type::SCALAR) {
} else if (ce.type() == expr_type::VAR) { } else if (ce.type() == expr_type::VAR) {
process_var_occurences(ce.var(), seen, occurences); process_var_occurences(ce.var(), seen, occurences);
} else if (ce.type() == expr_type::MUL){ } else if (ce.type() == expr_type::MUL){
process_mul_occurences(ce, seen, occurences); process_mul_occurences(ce, seen, occurences);
@ -182,7 +182,7 @@ nex horner::split_with_var(const nex& e, lpvar j) {
return r; return r;
} }
TRACE("nla_cn", tout << "b = " << b << "\n";); TRACE("nla_cn", tout << "b = " << b << "\n";);
return nex::sum(nex::mul(cross_nested_of_sum(a), nex::var(j)), b); return nex::sum(nex::mul(cross_nested_of_sum(a), nex::var(j)), cross_nested_of_sum(b));
} }
nex horner::cross_nested_of_sum(const nex& e) { nex horner::cross_nested_of_sum(const nex& e) {