michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/blast/congruence_closure): add add/assume API

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-23 15:21:28 -08:00
parent f0ccffe968
commit c50d7ac4b8
2 changed files with 48 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

70
src/library/blast/congruence_closure.cpp
View file

@ -884,41 +884,55 @@ void congruence_closure::add_eqv(name const & R, expr const & lhs, expr const &
}
void congruence_closure::add(hypothesis_idx hidx) {
state & s = curr_state();
hypothesis const & h = s.get_hypothesis_decl(hidx);
add(h.get_type(), h.get_self());
}
void congruence_closure::assume(expr const & type) {
lean_assert(m_froze_partitions);
expr dummy = mk_true_intro();
add(type, dummy);
}
expr congruence_closure::mk_iff_false_intro(expr const & proof) {
return m_froze_partitions ? proof : get_app_builder().mk_iff_false_intro(proof);
}
expr congruence_closure::mk_iff_true_intro(expr const & proof) {
return m_froze_partitions ? proof : get_app_builder().mk_iff_true_intro(proof);
}
void congruence_closure::add(expr const & type, expr const & proof) {
if (is_inconsistent())
return;
flet<congruence_closure *> set_cc(g_cc, this);
clear_todo();
state & s = curr_state();
app_builder & b = get_app_builder();
hypothesis const & h = s.get_hypothesis_decl(hidx);
try {
expr const & type = h.get_type();
expr p = type;
bool is_neg = is_not(type, p);
if (is_neg && !is_standard(env()))
return;
name R; expr lhs, rhs;
if (is_relation_app(p, R, lhs, rhs)) {
if (is_neg) {
bool toplevel = true; bool to_propagate = false;
internalize_core(get_iff_name(), p, toplevel, to_propagate);
add_eqv_core(get_iff_name(), p, mk_false(), b.mk_iff_false_intro(h.get_self()));
} else {
bool toplevel = false; bool to_propagate = false;
internalize_core(R, lhs, toplevel, to_propagate);
internalize_core(R, rhs, toplevel, to_propagate);
add_eqv_core(R, lhs, rhs, h.get_self());
}
} else if (is_prop(p)) {
expr p = type;
bool is_neg = is_not(type, p);
if (is_neg && !is_standard(env()))
return;
name R; expr lhs, rhs;
if (is_relation_app(p, R, lhs, rhs)) {
if (is_neg) {
bool toplevel = true; bool to_propagate = false;
internalize_core(get_iff_name(), p, toplevel, to_propagate);
if (is_neg) {
add_eqv_core(get_iff_name(), p, mk_false(), b.mk_iff_false_intro(h.get_self()));
} else {
add_eqv_core(get_iff_name(), p, mk_true(), b.mk_iff_true_intro(h.get_self()));
}
add_eqv_core(get_iff_name(), p, mk_false(), mk_iff_false_intro(proof));
} else {
bool toplevel = false; bool to_propagate = false;
internalize_core(R, lhs, toplevel, to_propagate);
internalize_core(R, rhs, toplevel, to_propagate);
add_eqv_core(R, lhs, rhs, proof);
}
} catch (app_builder_exception &) {}
} else if (is_prop(p)) {
bool toplevel = true; bool to_propagate = false;
internalize_core(get_iff_name(), p, toplevel, to_propagate);
if (is_neg) {
add_eqv_core(get_iff_name(), p, mk_false(), mk_iff_false_intro(proof));
} else {
add_eqv_core(get_iff_name(), p, mk_true(), mk_iff_true_intro(proof));
}
}
}
bool congruence_closure::is_eqv(name const & R, expr const & e1, expr const & e2) const {

6
src/library/blast/congruence_closure.h
View file

@ -133,6 +133,8 @@ class congruence_closure {
void remove_parents(name const & R, expr const & e);
void reinsert_parents(name const & R, expr const & e);
void update_mt(name const & R, expr const & e);
expr mk_iff_false_intro(expr const & proof);
expr mk_iff_true_intro(expr const & proof);
void add_eqv_step(name const & R, expr e1, expr e2, expr const & H);
void add_eqv_core(name const & R, expr const & lhs, expr const & rhs, expr const & H);
@ -171,6 +173,10 @@ public:
If H is none of the forms above, this method does nothing. */
void add(hypothesis_idx hidx);
void add(expr const & type, expr const & proof);
/** \brief Similar to \c add but asserts the given type without proof
\pre It can only be used after \c freeze_partitions has been invoked (i.e., proof extraction has been disabled). */
void assume(expr const & type);
/** \brief Assert the equivalence (R a b) with proof H. */
void add_eqv(name const & R, expr const & a, expr const & b, expr const & H);