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

build of template

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-13 18:21:56 -07:00 committed by Lev Nachmanson
parent 1aaf6d879f
commit c68d15f441
4 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/math/dd/pdd_interval.h
View file

@ -63,7 +63,9 @@ public:
// f meant to be called when the separation happens
template <typename T>
bool separated_from_zero(pdd const& p, u_dependency*& dep, std::function<void (const T)>& f) {
return m_dep_intervals.check_interval_for_conflict_on_zero(get_interval<w_dep::with_deps>(p), dep, f);
scoped_dep_interval i(m());
get_interval<w_dep::with_deps>(p, i);
return m_dep_intervals.check_interval_for_conflict_on_zero(i, dep, f);
}
};

4
src/math/lp/emonics.cpp
View file

@ -55,7 +55,7 @@ void emonics::pop(unsigned n) {
lpvar last_var = UINT_MAX;
for (lpvar v : m.vars()) {
if (v != last_var) {
remove_cell(m_use_lists[v], i);
remove_cell(m_use_lists[v]);
last_var = v;
}
}
@ -69,7 +69,7 @@ void emonics::pop(unsigned n) {
m_u_f_stack.pop_scope(n);
}
void emonics::remove_cell(head_tail& v, unsigned mIndex) {
void emonics::remove_cell(head_tail& v) {
cell*& cur_head = v.m_head;
cell*& cur_tail = v.m_tail;
cell* old_head = cur_head->m_next;

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

@ -97,7 +97,7 @@ class emonics {
void inc_visited() const;
void remove_cell(head_tail& v, unsigned mIndex);
void remove_cell(head_tail& v);
void insert_cell(head_tail& v, unsigned mIndex);
void merge_cells(head_tail& root, head_tail& other);
void unmerge_cells(head_tail& root, head_tail& other);

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

@ -1487,8 +1487,7 @@ std::ostream& core::diagnose_pdd_miss(std::ostream& out) {
bool core::check_pdd_eq(const dd::solver::equation* e) {
auto& di = m_intervals.get_dep_intervals();
dd::pdd_interval eval(di);
eval.var2interval() =
[this](lpvar j, bool deps, scoped_dep_interval& a) {
eval.var2interval() = [this](lpvar j, bool deps, scoped_dep_interval& a) {
if (deps) m_intervals.set_var_interval<dd::w_dep::with_deps>(j, a);
else m_intervals.set_var_interval<dd::w_dep::without_deps>(j, a);
};
@ -1497,8 +1496,7 @@ bool core::check_pdd_eq(const dd::solver::equation* e) {
if (!di.separated_from_zero(i))
return false;
eval.get_interval<dd::w_dep::with_deps>(e->poly(), i_wd);
std::function<void (const lp::explanation&)> f =
[this](const lp::explanation& e) {
std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
add_empty_lemma();
current_expl().add(e);
};