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

feat(library/blast/congruence_closure): add proved/disproved aux methods

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-17 19:06:23 -08:00
parent 3f6b79227f
commit d833410f0d
2 changed files with 42 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -320,6 +320,40 @@ optional<expr> congruence_closure::get_inconsistency_proof() const {
}
}
bool congruence_closure::prove(expr const & e) const {
return is_eqv(get_iff_name(), e, mk_true());
}
optional<expr> congruence_closure::get_proof(expr const & e) const {
try {
app_builder & b = get_app_builder();
if (auto p = get_eqv_proof(get_iff_name(), e, mk_true())) {
return some_expr(b.mk_of_iff_true(*p));
} else {
return none_expr();
}
} catch (app_builder_exception &) {
return none_expr();
}
}
bool congruence_closure::disproved(expr const & e) const {
return is_eqv(get_iff_name(), e, mk_false());
}
optional<expr> congruence_closure::get_disproof(expr const & e) const {
try {
app_builder & b = get_app_builder();
if (auto p = get_eqv_proof(get_iff_name(), e, mk_false())) {
return some_expr(b.mk_not_of_iff_false(*p));
} else {
return none_expr();
}
} catch (app_builder_exception &) {
return none_expr();
}
}
bool congruence_closure::is_congr_root(name const & R, expr const & e) const {
if (auto n = m_entries.find(eqc_key(R, e))) {
return n->m_cg_root;

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

@ -139,6 +139,14 @@ public:
bool is_uneqv(name const & R, expr const & e1, expr const & e2) const;
optional<expr> get_uneqv_proof(name const & R, expr const & e1, expr const & e2) const;
/** \brief Return true iff \c e has been proved by this module. That is, the proposition \c e is inhabited */
bool prove(expr const & e) const;
optional<expr> get_proof(expr const & e) const;
/** \brief Return true iff \c (not e) has been proved by this module. That is, the proposition \c (not e) is inhabited */
bool disproved(expr const & e) const;
optional<expr> get_disproof(expr const & e) const;
bool is_congr_root(name const & R, expr const & e) const;
bool is_root(name const & R, expr const & e) const { return get_root(R, e) == e; }
expr get_root(name const & R, expr const & e) const;