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

move to scoped intervals for memory management

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-13 15:12:46 -07:00 • committed by Lev Nachmanson
parent 79fefe5fb3
commit a7158772ad
3 changed files with 21 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/math/lp/nla_core.cpp
View file

@ -1494,16 +1494,16 @@ bool core::check_pdd_eq(const dd::solver::equation* e) {
else m_intervals.set_var_interval<dd::w_dep::without_deps>(j, a);
return a;
};
auto i = eval.get_interval<dd::w_dep::without_deps>(e->poly());
dep_intervals di(m_reslim);
if (!di.separated_from_zero(i))
scoped_dep_interval i(eval.m()), i_wd(eval.m());
eval.get_interval<dd::w_dep::without_deps>(e->poly(), i);
if (!eval.m().separated_from_zero(i))
return false;
auto i_wd = eval.get_interval<dd::w_dep::with_deps>(e->poly());
eval.get_interval<dd::w_dep::with_deps>(e->poly(), i_wd);
std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
add_empty_lemma();
current_expl().add(e);
};
if (di.check_interval_for_conflict_on_zero(i_wd, e->dep(), f)) {
if (eval.m().check_interval_for_conflict_on_zero(i_wd, e->dep(), f)) {
lp_settings().stats().m_grobner_conflicts++;
return true;
}