max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/tactic/smt/congruence_closure): add check_congr_keys assertions

Browse source
This commit is contained in:
Leonardo de Moura 2017-03-17 13:46:25 -07:00
parent 37c69427b3
commit 8ff176717c
2 changed files with 19 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/library/tactic/smt/congruence_closure.cpp
View file

@ -895,6 +895,22 @@ void congruence_closure::invert_trans(expr const & e) {
invert_trans(e, false, none_expr(), none_expr());
}
bool congruence_closure::check_congr_keys() const {
flet<congruence_closure *> set_cc(g_cc, const_cast<congruence_closure*>(this));
buffer<congr_key> keys;
m_state.m_congruences.to_buffer(keys);
for (unsigned i = 0; i < keys.size(); i++) {
for (unsigned j = i + 1; j < keys.size(); j++) {
if (congr_key_cmp()(keys[i], keys[j]) >= 0) {
tout() << keys[i].m_expr << "\n";
tout() << keys[j].m_expr << "\n";
lean_unreachable();
}
}
}
return true;
}
void congruence_closure::remove_parents(expr const & e, buffer<expr> & parents_to_propagate) {
auto ps = m_state.m_parents.find(e);
if (!ps) return;
@ -909,7 +925,9 @@ void congruence_closure::remove_parents(expr const & e, buffer<expr> & parents_t
m_state.m_symm_congruences.erase(k);
} else {
congr_key k = mk_congr_key(p);
lean_cond_assert("cc", check_congr_keys());
m_state.m_congruences.erase(k);
lean_cond_assert("cc", check_congr_keys());
}
}
});

1
src/library/tactic/smt/congruence_closure.h
View file

@ -272,6 +272,7 @@ private:
void process_todo();
void add_eqv_core(expr const & lhs, expr const & rhs, expr const & H, bool heq_proof);
bool check_eqc(expr const & e) const;
bool check_congr_keys() const;
friend ext_congr_lemma_cache_ptr const & get_cache_ptr(congruence_closure const & cc);
public: