mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

fix errors with dependency manager reset

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-01-12 10:11:13 -08:00
parent 6bc5400c5d
commit 1b07ad0952
4 changed files with 4 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -87,7 +87,10 @@ bool horner::lemmas_on_row(const T& row) {
[this, dep](const nex* n) { return m_intervals->check_nex(n, dep); },
[this](unsigned j) { return c().var_is_fixed(j); },
[this]() { return c().random(); }, m_nex_creator);
return lemmas_on_expr(cn, to_sum(e));
bool ret = lemmas_on_expr(cn, to_sum(e));
c().m_intervals.get_dep_intervals().reset(); // clean the memory allocated by the interval bound dependencies
return ret;
}
bool horner::horner_lemmas() {

15
src/math/lp/nex_creator.cpp
View file

@ -138,13 +138,6 @@ bool nex_creator::gt_on_powers_mul_same_degree(const T& a, const nex_mul& b) con
return ret;
}
bool nex_creator::children_are_simplified(const vector<nex_pow>& children) const {
for (auto c : children)
if (!is_simplified(*c.e()) || c.pow() == 0)
return false;
return true;
}
bool nex_creator::gt_on_mul_mul(const nex_mul& a, const nex_mul& b) const {
TRACE("grobner_d", tout << "a = " << a << " , b = " << b << "\n";);
SASSERT(is_simplified(a) && is_simplified(b));
@ -479,14 +472,6 @@ void nex_creator::simplify_children_of_sum(nex_sum& s) {
sort_join_sum(s);
}
static bool have_no_scalars(const nex_mul& a) {
for (auto & p : a)
if (p.e()->is_scalar() && !to_scalar(p.e())->value().is_one())
return false;
return true;
}
bool nex_mul::all_factors_are_elementary() const {
for (auto & p : *this)
if (!p.e()->is_elementary())

2
src/math/lp/nex_creator.h
View file

@ -279,8 +279,6 @@ public:
void simplify_children_of_sum(nex_sum & sum);
bool eat_scalar_pow(rational& r, const nex_pow& p, unsigned);
bool children_are_simplified(const vector<nex_pow>& children) const;
bool gt(const nex& a, const nex& b) const;
bool gt(const nex* a, const nex* b) const { return gt(*a, *b); }
template <typename T>

2
src/math/lp/nla_intervals.cpp
View file

@ -74,7 +74,6 @@ bool intervals::check_nex(const nex* n, u_dependency* initial_deps) {
m_core->lp_settings().stats().m_cross_nested_forms++;
auto i = interval_of_expr<e_with_deps::without_deps>(n, 1);
if (!m_dep_intervals.separated_from_zero(i)) {
m_dep_intervals.reset();
return false;
}
auto interv_wd = interval_of_expr<e_with_deps::with_deps>(n, 1);
@ -84,7 +83,6 @@ bool intervals::check_nex(const nex* n, u_dependency* initial_deps) {
m_core->current_expl().add(e);
};
m_dep_intervals.check_interval_for_conflict_on_zero(interv_wd, initial_deps, f);
m_dep_intervals.reset(); // clean the memory allocated by the interval bound dependencies
return true;
}