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

move set_var_interval2 to header

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-07-25 11:15:29 -07:00
parent e9e1fb2f37
commit 1441c0daea
3 changed files with 9 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -289,13 +289,10 @@ namespace nla {
auto coeff = m.coeff * denom; auto coeff = m.coeff * denom;
if (m.vars.empty()) if (m.vars.empty())
k -= coeff; k -= coeff;
else if (m.vars.size() == 1) { else if (m.vars.size() == 1)
lo_t.add_monomial(coeff, m.vars[0]); lo_t.add_monomial(coeff, m.vars[0]);
} else if (c().find_canonical_monic_of_vars(m.vars, j))
else if (c().find_canonical_monic_of_vars(m.vars, j)) {
//verbose_stream() << "canonical monic\n";
lo_t.add_monomial(coeff, j); lo_t.add_monomial(coeff, j);
}
else else
return false; return false;
} }

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

@ -276,14 +276,6 @@ void intervals::set_var_interval1(lpvar v, interval& b) {
} }
} }
template <e_with_deps wd>
bool intervals::set_var_interval2(lpvar v, scoped_dep_interval& b) {
if (ls().column_corresponds_to_term(v)) {
auto const& lt = ls().column_index_to_term(v);
return interval_from_lar_term<wd>(lt, b);
}
return false;
}
template <e_with_deps wd> template <e_with_deps wd>
void intervals::set_var_interval(lpvar v, interval& b) { void intervals::set_var_interval(lpvar v, interval& b) {
@ -505,7 +497,6 @@ lp::lar_solver& intervals::ls() { return m_core->m_lar_solver; }
const lp::lar_solver& intervals::ls() const { return m_core->m_lar_solver; } const lp::lar_solver& intervals::ls() const { return m_core->m_lar_solver; }
} // end of nla namespace } // end of nla namespace

8
src/math/lp/nla_intervals.h
View file

@ -56,7 +56,13 @@ public:
void set_var_interval1(lpvar v, interval& b); void set_var_interval1(lpvar v, interval& b);
template <dep_intervals::with_deps_t wd> template <dep_intervals::with_deps_t wd>
bool set_var_interval2(lpvar v, scoped_dep_interval& b); bool set_var_interval2(lpvar v, scoped_dep_interval& b) {
if (ls().column_corresponds_to_term(v)) {
auto const& lt = ls().column_index_to_term(v);
return interval_from_lar_term<wd>(lt, b);
}
return false;
}
template <dep_intervals::with_deps_t wd> template <dep_intervals::with_deps_t wd>
bool interval_from_term(const nex& e, scoped_dep_interval& i); bool interval_from_term(const nex& e, scoped_dep_interval& i);