mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-04 18:30:24 +00:00
Code Activity

separate out functions that call set_var_interval1/2 into functions for linker

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-07-25 10:06:11 -07:00
parent f533220482
commit e9e1fb2f37
2 changed files with 15 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/math/lp/nla_grobner.cpp
View file

@ -275,16 +275,7 @@ namespace nla {
return false; return false;
eval.var2intervals() = [&](lpvar j, bool deps, scoped_ptr_vector<scoped_dep_interval>& intervals) { eval.var2intervals() = [&](lpvar j, bool deps, scoped_ptr_vector<scoped_dep_interval>& intervals) {
verbose_stream() << "get-intervals\n"; var2intervals(j, deps, intervals);
scoped_ptr<scoped_dep_interval> a = alloc(scoped_dep_interval, di);
scoped_ptr<scoped_dep_interval> b = alloc(scoped_dep_interval, di);
if (deps) c().m_intervals.set_var_interval1<dd::w_dep::with_deps>(j, *a);
else c().m_intervals.set_var_interval1<dd::w_dep::without_deps>(j, *a);
intervals.push_back(a.detach());
if (deps && c().m_intervals.set_var_interval2<dd::w_dep::with_deps>(j, *b))
intervals.push_back(b.detach());
if (!deps && c().m_intervals.set_var_interval2<dd::w_dep::without_deps>(j, *b))
intervals.push_back(b.detach());
}; };
// TODO - relax bound dependencies to weakest that admit within interval -mx, mx. // TODO - relax bound dependencies to weakest that admit within interval -mx, mx.
eval.explain(lo, i, i_wd); eval.explain(lo, i, i_wd);
@ -325,6 +316,19 @@ namespace nla {
return true; return true;
} }
void grobner::var2intervals(lpvar j, bool deps, scoped_ptr_vector<scoped_dep_interval>& intervals) {
auto& di = c().m_intervals.get_dep_intervals();
scoped_ptr<scoped_dep_interval> a = alloc(scoped_dep_interval, di);
scoped_ptr<scoped_dep_interval> b = alloc(scoped_dep_interval, di);
if (deps) c().m_intervals.set_var_interval1<dd::w_dep::with_deps>(j, *a);
else c().m_intervals.set_var_interval1<dd::w_dep::without_deps>(j, *a);
intervals.push_back(a.detach());
if (deps && c().m_intervals.set_var_interval2<dd::w_dep::with_deps>(j, *b))
intervals.push_back(b.detach());
if (!deps && c().m_intervals.set_var_interval2<dd::w_dep::without_deps>(j, *b))
intervals.push_back(b.detach());
}
void grobner::add_dependencies(new_lemma& lemma, const dd::solver::equation& eq) { void grobner::add_dependencies(new_lemma& lemma, const dd::solver::equation& eq) {
lp::explanation ex; lp::explanation ex;

1
src/math/lp/nla_grobner.h
View file

@ -46,6 +46,7 @@ namespace nla {
bool propagate_gcd(); bool propagate_gcd();
bool propagate_gcd(const dd::solver::equation& eq); bool propagate_gcd(const dd::solver::equation& eq);
void add_dependencies(new_lemma& lemma, const dd::solver::equation& eq); void add_dependencies(new_lemma& lemma, const dd::solver::equation& eq);