feat(library/blast/congruence_closure): congruence_closure basics
This commit is contained in:
Leonardo de Moura
parent
de67288305
commit
3de9a89d93
10 changed files with 450 additions and 32 deletions
|
|
@ -351,6 +351,9 @@ iff_false_intro (λ H, iff.mp H trivial)
|
|||
theorem false_iff_true : (false ↔ true) ↔ false :=
|
||||
iff_false_intro (λ H, iff.mpr H trivial)
|
||||
|
||||
theorem false_of_true_iff_false : (true ↔ false) → false :=
|
||||
assume H, iff.mp H trivial
|
||||
|
||||
inductive Exists {A : Type} (P : A → Prop) : Prop :=
|
||||
intro : ∀ (a : A), P a → Exists P
|
||||
|
||||
|
|
|
|||
|
|
@ -26,6 +26,7 @@ Author: Leonardo de Moura
|
|||
#include "library/blast/blast_exception.h"
|
||||
#include "library/blast/simple_strategy.h"
|
||||
#include "library/blast/choice_point.h"
|
||||
#include "library/blast/congruence_closure.h"
|
||||
|
||||
namespace lean {
|
||||
namespace blast {
|
||||
|
|
@ -58,6 +59,7 @@ class blastenv {
|
|||
fun_info_manager m_fun_info_manager;
|
||||
congr_lemma_manager m_congr_lemma_manager;
|
||||
abstract_expr_manager m_abstract_expr_manager;
|
||||
relation_info_getter m_rel_getter;
|
||||
refl_info_getter m_refl_getter;
|
||||
|
||||
class tctx : public type_context {
|
||||
|
|
@ -414,6 +416,7 @@ public:
|
|||
m_fun_info_manager(*m_tmp_ctx),
|
||||
m_congr_lemma_manager(m_app_builder, m_fun_info_manager),
|
||||
m_abstract_expr_manager(m_fun_info_manager),
|
||||
m_rel_getter(mk_relation_info_getter(env)),
|
||||
m_refl_getter(mk_refl_info_getter(env)),
|
||||
m_tctx(*this),
|
||||
m_normalizer(m_tctx) {
|
||||
|
|
@ -495,6 +498,14 @@ public:
|
|||
return m_congr_lemma_manager.mk_congr(fn);
|
||||
}
|
||||
|
||||
optional<congr_lemma> mk_rel_iff_congr(expr const & fn) {
|
||||
return m_congr_lemma_manager.mk_rel_iff_congr(fn);
|
||||
}
|
||||
|
||||
optional<congr_lemma> mk_rel_eq_congr(expr const & fn) {
|
||||
return m_congr_lemma_manager.mk_rel_eq_congr(fn);
|
||||
}
|
||||
|
||||
fun_info get_fun_info(expr const & fn) {
|
||||
return m_fun_info_manager.get(fn);
|
||||
}
|
||||
|
|
@ -537,13 +548,17 @@ public:
|
|||
return r;
|
||||
}
|
||||
|
||||
bool is_relation(expr const & e, name & rop, expr & lhs, expr & rhs) {
|
||||
bool is_relation_app(expr const & e, name & rop, expr & lhs, expr & rhs) {
|
||||
return m_is_relation_pred(e, rop, lhs, rhs);
|
||||
}
|
||||
|
||||
bool is_reflexive(name const & rop) const {
|
||||
return static_cast<bool>(m_refl_getter(rop));
|
||||
}
|
||||
|
||||
optional<relation_info> get_relation_info(name const & rop) const {
|
||||
return m_rel_getter(rop);
|
||||
}
|
||||
};
|
||||
|
||||
LEAN_THREAD_PTR(blastenv, g_blastenv);
|
||||
|
|
@ -589,14 +604,14 @@ projection_info const * get_projection_info(name const & n) {
|
|||
return g_blastenv->get_projection_info(n);
|
||||
}
|
||||
|
||||
bool is_relation(expr const & e, name & rop, expr & lhs, expr & rhs) {
|
||||
bool is_relation_app(expr const & e, name & rop, expr & lhs, expr & rhs) {
|
||||
lean_assert(g_blastenv);
|
||||
return g_blastenv->is_relation(e, rop, lhs, rhs);
|
||||
return g_blastenv->is_relation_app(e, rop, lhs, rhs);
|
||||
}
|
||||
|
||||
bool is_relation(expr const & e) {
|
||||
bool is_relation_app(expr const & e) {
|
||||
name rop; expr lhs, rhs;
|
||||
return is_relation(e, rop, lhs, rhs);
|
||||
return is_relation_app(e, rop, lhs, rhs);
|
||||
}
|
||||
|
||||
bool is_reflexive(name const & rop) {
|
||||
|
|
@ -604,6 +619,11 @@ bool is_reflexive(name const & rop) {
|
|||
return g_blastenv->is_reflexive(rop);
|
||||
}
|
||||
|
||||
optional<relation_info> get_relation_info(name const & rop) {
|
||||
lean_assert(g_blastenv);
|
||||
return g_blastenv->get_relation_info(rop);
|
||||
}
|
||||
|
||||
expr whnf(expr const & e) {
|
||||
lean_assert(g_blastenv);
|
||||
return g_blastenv->whnf(e);
|
||||
|
|
@ -669,6 +689,16 @@ optional<congr_lemma> mk_congr_lemma(expr const & fn) {
|
|||
return g_blastenv->mk_congr_lemma(fn);
|
||||
}
|
||||
|
||||
optional<congr_lemma> mk_rel_iff_congr(expr const & fn) {
|
||||
lean_assert(g_blastenv);
|
||||
return g_blastenv->mk_rel_iff_congr(fn);
|
||||
}
|
||||
|
||||
optional<congr_lemma> mk_rel_eq_congr(expr const & fn) {
|
||||
lean_assert(g_blastenv);
|
||||
return g_blastenv->mk_rel_eq_congr(fn);
|
||||
}
|
||||
|
||||
fun_info get_fun_info(expr const & fn) {
|
||||
lean_assert(g_blastenv);
|
||||
return g_blastenv->get_fun_info(fn);
|
||||
|
|
@ -723,9 +753,10 @@ void scope_assignment::commit() {
|
|||
}
|
||||
|
||||
struct scope_debug::imp {
|
||||
scoped_expr_caching m_scope1;
|
||||
blastenv m_benv;
|
||||
scope_blastenv m_scope2;
|
||||
scoped_expr_caching m_scope1;
|
||||
blastenv m_benv;
|
||||
scope_blastenv m_scope2;
|
||||
scope_congruence_closure m_scope3;
|
||||
imp(environment const & env, io_state const & ios):
|
||||
m_scope1(true),
|
||||
m_benv(env, ios, list<name>(), list<name>()),
|
||||
|
|
@ -819,9 +850,10 @@ expr internalize(expr const & e) {
|
|||
}
|
||||
optional<expr> blast_goal(environment const & env, io_state const & ios, list<name> const & ls, list<name> const & ds,
|
||||
goal const & g) {
|
||||
scoped_expr_caching scope1(true);
|
||||
blast::blastenv b(env, ios, ls, ds);
|
||||
blast::scope_blastenv scope2(b);
|
||||
scoped_expr_caching scope1(true);
|
||||
blast::blastenv b(env, ios, ls, ds);
|
||||
blast::scope_blastenv scope2(b);
|
||||
blast::scope_congruence_closure scope3;
|
||||
return b(g);
|
||||
}
|
||||
void initialize_blast() {
|
||||
|
|
|
|||
|
|
@ -9,6 +9,7 @@ Author: Leonardo de Moura
|
|||
#include "kernel/environment.h"
|
||||
#include "library/io_state.h"
|
||||
#include "library/tmp_type_context.h"
|
||||
#include "library/relation_manager.h"
|
||||
#include "library/congr_lemma_manager.h"
|
||||
#include "library/fun_info_manager.h"
|
||||
#include "library/blast/state.h"
|
||||
|
|
@ -37,9 +38,14 @@ bool is_reducible(name const & n);
|
|||
projection_info const * get_projection_info(name const & n);
|
||||
/** \brief Return true iff \c e is a relation application,
|
||||
and store the relation name, lhs and rhs in the output arguments. */
|
||||
bool is_relation(expr const & e, name & rop, expr & lhs, expr & rhs);
|
||||
bool is_relation(expr const & e);
|
||||
bool is_relation_app(expr const & e, name & rop, expr & lhs, expr & rhs);
|
||||
bool is_relation_app(expr const & e);
|
||||
optional<relation_info> get_relation_info(name const & rop);
|
||||
inline optional<relation_info> is_relation(expr const & R) {
|
||||
return is_constant(R) ? get_relation_info(const_name(R)) : optional<relation_info>();
|
||||
}
|
||||
bool is_reflexive(name const & rop);
|
||||
|
||||
/** \brief Put the given expression in weak-head-normal-form with respect to the
|
||||
current state being processed by the blast tactic. */
|
||||
expr whnf(expr const & e);
|
||||
|
|
@ -93,6 +99,8 @@ optional<congr_lemma> mk_congr_lemma_for_simp(expr const & fn);
|
|||
optional<congr_lemma> mk_congr_lemma(expr const & fn, unsigned num_args);
|
||||
/** \brief Similar to previous procedure, but num_args == arith of fn */
|
||||
optional<congr_lemma> mk_congr_lemma(expr const & fn);
|
||||
optional<congr_lemma> mk_rel_iff_congr(expr const & fn);
|
||||
optional<congr_lemma> mk_rel_eq_congr(expr const & fn);
|
||||
|
||||
/** \brief Retrieve information for the given function. */
|
||||
fun_info get_fun_info(expr const & fn);
|
||||
|
|
|
|||
|
|
@ -4,11 +4,352 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include "library/constants.h"
|
||||
#include "library/simplifier/simp_rule_set.h"
|
||||
#include "library/blast/congruence_closure.h"
|
||||
#include "library/blast/util.h"
|
||||
#include "library/blast/blast.h"
|
||||
|
||||
namespace lean {
|
||||
namespace blast {
|
||||
/* Not all user-defined congruence lemmas can be use by this module
|
||||
We cache the ones that can be used. */
|
||||
struct congr_lemma_key {
|
||||
name m_R;
|
||||
expr m_fn;
|
||||
unsigned m_nargs;
|
||||
unsigned m_hash;
|
||||
congr_lemma_key(name const & R, expr const & fn, unsigned nargs):
|
||||
m_R(R), m_fn(fn), m_nargs(nargs),
|
||||
m_hash(hash(hash(R.hash(), fn.hash()), nargs)) {}
|
||||
};
|
||||
|
||||
struct congr_lemma_key_hash_fn {
|
||||
unsigned operator()(congr_lemma_key const & k) const { return k.m_hash; }
|
||||
};
|
||||
|
||||
struct congr_lemma_key_eq_fn {
|
||||
bool operator()(congr_lemma_key const & k1, congr_lemma_key const & k2) const {
|
||||
return k1.m_R == k2.m_R && k1.m_fn == k2.m_fn && k1.m_nargs == k2.m_nargs;
|
||||
}
|
||||
};
|
||||
|
||||
static list<optional<name>> rel_names_from_arg_kinds(list<congr_arg_kind> const & kinds, name const & R) {
|
||||
return map2<optional<name>>(kinds, [&](congr_arg_kind k) {
|
||||
return k == congr_arg_kind::Eq ? optional<name>(R) : optional<name>();
|
||||
});
|
||||
}
|
||||
|
||||
struct ext_congr_lemma {
|
||||
name m_R;
|
||||
congr_lemma m_congr_lemma; // actual lemma
|
||||
list<optional<name>> m_rel_names; // relation congruence to be used with each child, none means child is ignored by congruence closure.
|
||||
unsigned m_lift_needed:1; // if true, m_congr_lemma is for equality, and we need to lift to m_R.
|
||||
unsigned m_fixed_fun:1; // if true, we build equivalences for functions, and use generic congr lemma, and ignore m_congr_lemma
|
||||
ext_congr_lemma(congr_lemma const & H):
|
||||
m_R(get_eq_name()),
|
||||
m_congr_lemma(H),
|
||||
m_rel_names(rel_names_from_arg_kinds(H.get_arg_kinds(), get_eq_name())),
|
||||
m_lift_needed(false),
|
||||
m_fixed_fun(true) {}
|
||||
ext_congr_lemma(name const & R, congr_lemma const & H, bool lift_needed):
|
||||
m_R(R),
|
||||
m_congr_lemma(H),
|
||||
m_rel_names(rel_names_from_arg_kinds(H.get_arg_kinds(), get_eq_name())),
|
||||
m_lift_needed(lift_needed),
|
||||
m_fixed_fun(true) {}
|
||||
ext_congr_lemma(name const & R, congr_lemma const & H, list<optional<name>> const & rel_names, bool lift_needed):
|
||||
m_R(R),
|
||||
m_congr_lemma(H),
|
||||
m_rel_names(rel_names),
|
||||
m_lift_needed(lift_needed),
|
||||
m_fixed_fun(true) {}
|
||||
};
|
||||
|
||||
/* We use the following cache for user-defined lemmas and automatically generated ones. */
|
||||
typedef std::unordered_map<congr_lemma_key, optional<ext_congr_lemma>, congr_lemma_key_hash_fn, congr_lemma_key_eq_fn> congr_cache;
|
||||
|
||||
LEAN_THREAD_VALUE(congr_cache *, g_congr_cache, nullptr);
|
||||
|
||||
scope_congruence_closure::scope_congruence_closure():
|
||||
m_old_cache(g_congr_cache) {
|
||||
g_congr_cache = new congr_cache();
|
||||
}
|
||||
|
||||
scope_congruence_closure::~scope_congruence_closure() {
|
||||
delete g_congr_cache;
|
||||
g_congr_cache = static_cast<congr_cache*>(m_old_cache);
|
||||
}
|
||||
|
||||
void congruence_closure::mk_entry_for(name const & R, expr const & e) {
|
||||
lean_assert(!m_entries.find(eqc_key(R, e)));
|
||||
entry n;
|
||||
n.m_next = e;
|
||||
n.m_root = e;
|
||||
n.m_cg_root = e;
|
||||
n.m_rank = 0;
|
||||
m_entries.insert(eqc_key(R, e), n);
|
||||
}
|
||||
|
||||
static optional<ext_congr_lemma> mk_ext_congr_lemma_core(name const & R, expr const & fn, unsigned nargs) {
|
||||
simp_rule_set const * sr = get_simp_rule_sets(env()).find(R);
|
||||
if (sr) {
|
||||
list<congr_rule> const * crs = sr->find_congr(fn);
|
||||
if (crs) {
|
||||
for (congr_rule const & r : *crs) {
|
||||
// TODO(Leo):
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Automatically generated lemma for equivalence relation over iff/eq
|
||||
if (auto info = is_relation(fn)) {
|
||||
if (info->get_arity() == nargs) {
|
||||
if (R == get_iff_name()) {
|
||||
if (optional<congr_lemma> cgr = mk_rel_iff_congr(fn)) {
|
||||
auto child_rel_names = rel_names_from_arg_kinds(cgr->get_arg_kinds(), const_name(fn));
|
||||
return optional<ext_congr_lemma>(R, *cgr, child_rel_names, false);
|
||||
}
|
||||
}
|
||||
if (optional<congr_lemma> cgr = mk_rel_eq_congr(fn)) {
|
||||
auto child_rel_names = rel_names_from_arg_kinds(cgr->get_arg_kinds(), const_name(fn));
|
||||
bool lift_needed = R != get_eq_name();
|
||||
return optional<ext_congr_lemma>(R, *cgr, child_rel_names, lift_needed);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Automatically generated lemma
|
||||
optional<congr_lemma> eq_congr = mk_congr_lemma(fn, nargs);
|
||||
if (!eq_congr)
|
||||
return optional<ext_congr_lemma>();
|
||||
ext_congr_lemma res1(*eq_congr);
|
||||
// If all arguments are Eq kind, then we can use generic congr axiom and consider equality for the function.
|
||||
if (eq_congr->all_eq_kind())
|
||||
res1.m_fixed_fun = false;
|
||||
if (R == get_eq_name())
|
||||
return optional<ext_congr_lemma>(res1);
|
||||
bool lift_needed = true;
|
||||
return optional<ext_congr_lemma>(R, *eq_congr, lift_needed);
|
||||
}
|
||||
|
||||
static optional<ext_congr_lemma> mk_ext_congr_lemma(name const & R, expr const & fn, unsigned nargs) {
|
||||
congr_lemma_key key(R, fn, nargs);
|
||||
auto it = g_congr_cache->find(key);
|
||||
if (it != g_congr_cache->end())
|
||||
return it->second;
|
||||
auto r = mk_ext_congr_lemma_core(R, fn, nargs);
|
||||
g_congr_cache->insert(mk_pair(key, r));
|
||||
return r;
|
||||
}
|
||||
|
||||
void congruence_closure::add_occurrence(name const & Rp, expr const & parent, name const & Rc, expr const & child) {
|
||||
// TODO(Leo):
|
||||
}
|
||||
|
||||
void congruence_closure::add_congruence_table(ext_congr_lemma const & lemma, expr const & e) {
|
||||
// TODO(Leo):
|
||||
}
|
||||
|
||||
void congruence_closure::internalize(name const & R, expr const & e) {
|
||||
lean_assert(closed(e));
|
||||
if (has_expr_metavar(e))
|
||||
return;
|
||||
switch (e.kind()) {
|
||||
case expr_kind::Var: case expr_kind::Meta:
|
||||
lean_unreachable();
|
||||
case expr_kind::Sort:
|
||||
return;
|
||||
case expr_kind::Constant: case expr_kind::Local:
|
||||
case expr_kind::Lambda:
|
||||
mk_entry_for(R, e);
|
||||
return;
|
||||
case expr_kind::Macro:
|
||||
for (unsigned i = 0; i < macro_num_args(e); i++)
|
||||
internalize(R, macro_arg(e, i));
|
||||
mk_entry_for(R, e);
|
||||
break;
|
||||
case expr_kind::Pi:
|
||||
if (is_arrow(e) && is_prop(binding_domain(e)) && is_prop(binding_body(e))) {
|
||||
internalize(R, binding_domain(e));
|
||||
internalize(R, binding_body(e));
|
||||
}
|
||||
if (is_prop(e)) {
|
||||
mk_entry_for(R, e);
|
||||
}
|
||||
return;
|
||||
case expr_kind::App: {
|
||||
mk_entry_for(R, e);
|
||||
buffer<expr> args;
|
||||
expr const & fn = get_app_args(e, args);
|
||||
if (auto lemma = mk_ext_congr_lemma(R, fn, args.size())) {
|
||||
list<optional<name>> const * it = &(lemma->m_rel_names);
|
||||
for (expr const & arg : args) {
|
||||
lean_assert(*it);
|
||||
if (auto R1 = head(*it)) {
|
||||
internalize(*R1, arg);
|
||||
add_occurrence(R, e, *R1, arg);
|
||||
}
|
||||
it = &tail(*it);
|
||||
}
|
||||
if (!lemma->m_fixed_fun) {
|
||||
internalize(get_eq_name(), fn);
|
||||
add_occurrence(get_eq_name(), e, get_eq_name(), fn);
|
||||
}
|
||||
add_congruence_table(*lemma, e);
|
||||
}
|
||||
break;
|
||||
}}
|
||||
}
|
||||
|
||||
void congruence_closure::internalize(expr const & e) {
|
||||
if (is_prop(e))
|
||||
internalize(get_iff_name(), e);
|
||||
else
|
||||
internalize(get_eq_name(), e);
|
||||
}
|
||||
|
||||
typedef std::tuple<name, expr, expr, expr> cc_todo_entry;
|
||||
|
||||
MK_THREAD_LOCAL_GET_DEF(std::vector<cc_todo_entry>, get_todo);
|
||||
|
||||
static void clear_todo() {
|
||||
get_todo().clear();
|
||||
}
|
||||
|
||||
void congruence_closure::add_eqv(name const & R, expr const & lhs, expr const & rhs, expr const & pr) {
|
||||
auto & todo = get_todo();
|
||||
todo.emplace_back(R, lhs, rhs, pr);
|
||||
while (!todo.empty()) {
|
||||
name R; expr lhs, rhs, pr;
|
||||
std::tie(R, lhs, rhs, pr) = todo.back();
|
||||
todo.pop_back();
|
||||
// TODO(Leo): process
|
||||
}
|
||||
}
|
||||
|
||||
void congruence_closure::add(hypothesis_idx hidx) {
|
||||
if (is_inconsistent())
|
||||
return;
|
||||
clear_todo();
|
||||
state & s = curr_state();
|
||||
app_builder & b = get_app_builder();
|
||||
hypothesis const * h = s.get_hypothesis_decl(hidx);
|
||||
lean_assert(h);
|
||||
try {
|
||||
expr const & type = h->get_type();
|
||||
expr p;
|
||||
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) {
|
||||
internalize(get_iff_name(), p);
|
||||
add_eqv(get_iff_name(), p, mk_false(), b.mk_app(get_iff_false_intro_name(), h->get_self()));
|
||||
} else {
|
||||
internalize(R, lhs);
|
||||
internalize(R, rhs);
|
||||
add_eqv(R, lhs, rhs, h->get_self());
|
||||
}
|
||||
} else if (is_prop(p)) {
|
||||
internalize(get_iff_name(), p);
|
||||
if (is_neg) {
|
||||
add_eqv(get_iff_name(), p, mk_false(), b.mk_app(get_iff_false_intro_name(), h->get_self()));
|
||||
} else {
|
||||
add_eqv(get_iff_name(), p, mk_true(), b.mk_app(get_iff_true_intro_name(), h->get_self()));
|
||||
}
|
||||
}
|
||||
} catch (app_builder_exception &) {}
|
||||
}
|
||||
|
||||
bool congruence_closure::is_eqv(name const & R, expr const & e1, expr const & e2) const {
|
||||
// TODO(Leo):
|
||||
return false;
|
||||
}
|
||||
|
||||
optional<expr> congruence_closure::get_eqv_proof(name const & rel_name, expr const & e1, expr const & e2) const {
|
||||
// TODO(Leo):
|
||||
return none_expr();
|
||||
}
|
||||
|
||||
bool congruence_closure::is_uneqv(name const & R, expr const & e1, expr const & e2) const {
|
||||
if (!is_standard(env()))
|
||||
return false;
|
||||
try {
|
||||
app_builder & b = get_app_builder();
|
||||
// TODO(Leo): check if this is a bootleneck
|
||||
expr tmp = b.mk_rel(R, e1, e2);
|
||||
return is_eqv(get_iff_name(), tmp, mk_false());
|
||||
} catch (app_builder_exception &) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
optional<expr> congruence_closure::get_uneqv_proof(name const & R, expr const & e1, expr const & e2) const {
|
||||
if (!is_standard(env()))
|
||||
return none_expr();
|
||||
try {
|
||||
app_builder & b = get_app_builder();
|
||||
// TODO(Leo): check if this is a bootleneck
|
||||
expr tmp = b.mk_rel(R, e1, e2);
|
||||
if (auto p = get_eqv_proof(get_iff_name(), tmp, mk_false())) {
|
||||
return some_expr(b.mk_app(get_not_of_iff_false_name(), *p));
|
||||
} else {
|
||||
return none_expr();
|
||||
}
|
||||
} catch (app_builder_exception &) {
|
||||
return none_expr();
|
||||
}
|
||||
}
|
||||
|
||||
bool congruence_closure::is_inconsistent() const {
|
||||
return is_eqv(get_iff_name(), mk_true(), mk_false());
|
||||
}
|
||||
|
||||
optional<expr> congruence_closure::get_inconsistency_proof() const {
|
||||
try {
|
||||
app_builder & b = get_app_builder();
|
||||
if (auto p = get_eqv_proof(get_iff_name(), mk_true(), mk_false())) {
|
||||
return some_expr(b.mk_app(get_false_of_true_iff_false_name(), *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;
|
||||
} else {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
expr congruence_closure::get_root(name const & R, expr const & e) const {
|
||||
if (auto n = m_entries.find(eqc_key(R, e))) {
|
||||
return n->m_root;
|
||||
} else {
|
||||
return e;;
|
||||
}
|
||||
}
|
||||
|
||||
expr congruence_closure::get_next(name const & R, expr const & e) const {
|
||||
if (auto n = m_entries.find(eqc_key(R, e))) {
|
||||
return n->m_next;
|
||||
} else {
|
||||
return e;;
|
||||
}
|
||||
}
|
||||
|
||||
void congruence_closure::display() const {
|
||||
// TODO(Leo):
|
||||
}
|
||||
|
||||
bool congruence_closure::check_invariant() const {
|
||||
// TODO(Leo):
|
||||
return true;
|
||||
}
|
||||
}}
|
||||
|
|
|
|||
|
|
@ -11,6 +11,7 @@ Author: Leonardo de Moura
|
|||
|
||||
namespace lean {
|
||||
namespace blast {
|
||||
struct ext_congr_lemma;
|
||||
class congruence_closure {
|
||||
/*
|
||||
We maintain several equivalence relations.
|
||||
|
|
@ -43,9 +44,6 @@ class congruence_closure {
|
|||
optional<expr> m_target;
|
||||
optional<expr> m_proof;
|
||||
unsigned m_rank; // rank of the equivalence class, it is meaningless if 'e' != m_root
|
||||
/* Each equivalence class may contain at most one "interpreted" element. The interpreted element will
|
||||
always be the root. For example, we tag 'true' and 'false' as interpreted. */
|
||||
bool m_interpreted;
|
||||
};
|
||||
|
||||
/* Key (R, e) for the mapping (R, e) -> entry */
|
||||
|
|
@ -57,7 +55,7 @@ class congruence_closure {
|
|||
};
|
||||
|
||||
struct eqc_key_cmp {
|
||||
int operator()(eqc_key const & k1, eqc_key const & k2) {
|
||||
int operator()(eqc_key const & k1, eqc_key const & k2) const {
|
||||
int r = quick_cmp(k1.m_R, k2.m_R);
|
||||
if (r != 0) return r;
|
||||
else return is_lt(k1.m_expr, k2.m_expr, true);
|
||||
|
|
@ -68,15 +66,16 @@ class congruence_closure {
|
|||
struct congr_key {
|
||||
name m_R;
|
||||
expr m_expr;
|
||||
unsigned m_hash;
|
||||
/* We track unequivalences using congruence table.
|
||||
The idea is to store (not a = b) by putting (a = b) in the equivalence class of false.
|
||||
So, we want (a = b) and (b = a) to be the "same" key in the congruence table.
|
||||
eq and iff are ubiquitous. So, we have special treatment for them.
|
||||
|
||||
\remark: the trick can be used with commutative operators, but we currently don't do it. */
|
||||
unsigned m_eq:1; // true if m_expr is an equality
|
||||
unsigned m_iff:1; // true if m_expr is an iff
|
||||
unsigned m_symm_rel; // true if m_expr is another symmetric relation.
|
||||
unsigned m_eq:1; // true if m_expr is an equality
|
||||
unsigned m_iff:1; // true if m_expr is an iff
|
||||
unsigned m_symm_rel:1; // true if m_expr is another symmetric relation.
|
||||
};
|
||||
|
||||
struct congr_key_cmp {
|
||||
|
|
@ -85,6 +84,7 @@ class congruence_closure {
|
|||
|
||||
typedef rb_tree<expr, expr_quick_cmp> expr_set;
|
||||
typedef rb_map<eqc_key, entry, eqc_key_cmp> entries;
|
||||
// TODO(Leo): fix and take relation into account
|
||||
typedef rb_map<expr, expr_set, expr_quick_cmp> parents;
|
||||
typedef rb_tree<congr_key, congr_key_cmp> congruences;
|
||||
|
||||
|
|
@ -92,6 +92,11 @@ class congruence_closure {
|
|||
parents m_parents;
|
||||
congruences m_congruences;
|
||||
|
||||
void mk_entry_for(name const & R, expr const & e);
|
||||
void add_occurrence(name const & Rp, expr const & parent, name const & Rc, expr const & child);
|
||||
void add_congruence_table(ext_congr_lemma const & lemma, expr const & e);
|
||||
void add_eqv(name const & R, expr const & lhs, expr const & rhs, expr const & pr);
|
||||
|
||||
public:
|
||||
/** \brief Register expression \c e in this data-structure.
|
||||
It creates entries for each sub-expression in \c e.
|
||||
|
|
@ -104,7 +109,9 @@ public:
|
|||
3- (A -> B) is not inserted into the data-structures, but their arguments are visited
|
||||
if they are propositions.
|
||||
4- Terms containing meta-variables.
|
||||
5- The subterms of lambda-expressions. */
|
||||
5- The subterms of lambda-expressions.
|
||||
6- Sorts (Type and Prop). */
|
||||
void internalize(name const & R, expr const & e);
|
||||
void internalize(expr const & e);
|
||||
|
||||
/** \brief Given a hypothesis H, this method will do the following based on the type of H
|
||||
|
|
@ -125,19 +132,28 @@ public:
|
|||
optional<expr> get_inconsistency_proof() const;
|
||||
|
||||
/** \brief Return true iff 'e1' and 'e2' are in the same equivalence class for relation \c rel_name. */
|
||||
bool is_eqv(name const & rel_name, expr const & e1, expr const & e2) const;
|
||||
bool is_eqv(name const & R, expr const & e1, expr const & e2) const;
|
||||
optional<expr> get_eqv_proof(name const & rel_name, expr const & e1, expr const & e2) const;
|
||||
|
||||
/** \brief Return true iff `e1 ~ e2` is in the equivalence class of false for iff. */
|
||||
bool is_uneqv(name const & rel_name, expr const & e1, expr const & e2) const;
|
||||
optional<expr> get_uneqv_proof(name const & rel_name, expr const & e1, expr const & e2) const;
|
||||
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;
|
||||
|
||||
bool is_congr_root(expr const & e) const;
|
||||
bool is_root(expr const & e) const;
|
||||
expr get_root(expr const & e) const;
|
||||
expr get_next(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;
|
||||
expr get_next(name const & R, expr const & e) const;
|
||||
|
||||
/** \brief dump for debugging purposes. */
|
||||
void display() const;
|
||||
bool check_invariant() const;
|
||||
};
|
||||
|
||||
/** \brief Auxiliary class for initializing thread-local caches */
|
||||
class scope_congruence_closure {
|
||||
void * m_old_cache;
|
||||
public:
|
||||
scope_congruence_closure();
|
||||
~scope_congruence_closure();
|
||||
};
|
||||
}}
|
||||
|
|
|
|||
|
|
@ -19,7 +19,7 @@ optional<name> is_recursor_action_target(hypothesis_idx hidx) {
|
|||
expr const & type = h->get_type();
|
||||
if (!is_app(type) && !is_constant(type))
|
||||
return optional<name>();
|
||||
if (is_relation(type))
|
||||
if (is_relation_app(type))
|
||||
return optional<name>(); // we don't apply recursors to equivalence relations: =, ~, <->, etc.
|
||||
if (!h->is_assumption())
|
||||
return optional<name>(); // we only consider assumptions
|
||||
|
|
|
|||
|
|
@ -29,7 +29,7 @@ static optional<expr> try_not_refl_relation(hypothesis const & h) {
|
|||
if (!is_not(h.get_type(), p))
|
||||
return none_expr();
|
||||
name rop; expr lhs, rhs;
|
||||
if (is_relation(p, rop, lhs, rhs) && is_def_eq(lhs, rhs)) {
|
||||
if (is_relation_app(p, rop, lhs, rhs) && is_def_eq(lhs, rhs)) {
|
||||
try {
|
||||
app_builder & b = get_app_builder();
|
||||
expr rfl = b.mk_refl(rop, lhs);
|
||||
|
|
@ -90,7 +90,7 @@ optional<expr> trivial_action() {
|
|||
|
||||
/* a ~ a */
|
||||
name rop; expr lhs, rhs;
|
||||
if (is_relation(target, rop, lhs, rhs) && is_def_eq(lhs, rhs)) {
|
||||
if (is_relation_app(target, rop, lhs, rhs) && is_def_eq(lhs, rhs)) {
|
||||
return some_expr(get_app_builder().mk_refl(rop, lhs));
|
||||
}
|
||||
|
||||
|
|
@ -116,7 +116,7 @@ bool discard(hypothesis_idx hidx) {
|
|||
return true;
|
||||
// 2- (H : a ~ a)
|
||||
name rop; expr lhs, rhs;
|
||||
if (is_relation(type, rop, lhs, rhs) && is_def_eq(lhs, rhs) && is_reflexive(rop))
|
||||
if (is_relation_app(type, rop, lhs, rhs) && is_def_eq(lhs, rhs) && is_reflexive(rop))
|
||||
return true;
|
||||
// 3- We already have an equivalent hypothesis
|
||||
for (hypothesis_idx hidx2 : s.get_head_related(hidx)) {
|
||||
|
|
|
|||
|
|
@ -42,6 +42,7 @@ name const * g_eq_subst = nullptr;
|
|||
name const * g_exists_elim = nullptr;
|
||||
name const * g_false = nullptr;
|
||||
name const * g_false_rec = nullptr;
|
||||
name const * g_false_of_true_iff_false = nullptr;
|
||||
name const * g_funext = nullptr;
|
||||
name const * g_has_zero = nullptr;
|
||||
name const * g_has_one = nullptr;
|
||||
|
|
@ -78,9 +79,11 @@ name const * g_nat_succ = nullptr;
|
|||
name const * g_nat_zero = nullptr;
|
||||
name const * g_neg = nullptr;
|
||||
name const * g_not = nullptr;
|
||||
name const * g_not_of_iff_false = nullptr;
|
||||
name const * g_num = nullptr;
|
||||
name const * g_num_zero = nullptr;
|
||||
name const * g_num_pos = nullptr;
|
||||
name const * g_of_iff_true = nullptr;
|
||||
name const * g_one = nullptr;
|
||||
name const * g_option = nullptr;
|
||||
name const * g_option_some = nullptr;
|
||||
|
|
@ -216,6 +219,7 @@ void initialize_constants() {
|
|||
g_exists_elim = new name{"exists", "elim"};
|
||||
g_false = new name{"false"};
|
||||
g_false_rec = new name{"false", "rec"};
|
||||
g_false_of_true_iff_false = new name{"false_of_true_iff_false"};
|
||||
g_funext = new name{"funext"};
|
||||
g_has_zero = new name{"has_zero"};
|
||||
g_has_one = new name{"has_one"};
|
||||
|
|
@ -252,9 +256,11 @@ void initialize_constants() {
|
|||
g_nat_zero = new name{"nat", "zero"};
|
||||
g_neg = new name{"neg"};
|
||||
g_not = new name{"not"};
|
||||
g_not_of_iff_false = new name{"not_of_iff_false"};
|
||||
g_num = new name{"num"};
|
||||
g_num_zero = new name{"num", "zero"};
|
||||
g_num_pos = new name{"num", "pos"};
|
||||
g_of_iff_true = new name{"of_iff_true"};
|
||||
g_one = new name{"one"};
|
||||
g_option = new name{"option"};
|
||||
g_option_some = new name{"option", "some"};
|
||||
|
|
@ -391,6 +397,7 @@ void finalize_constants() {
|
|||
delete g_exists_elim;
|
||||
delete g_false;
|
||||
delete g_false_rec;
|
||||
delete g_false_of_true_iff_false;
|
||||
delete g_funext;
|
||||
delete g_has_zero;
|
||||
delete g_has_one;
|
||||
|
|
@ -427,9 +434,11 @@ void finalize_constants() {
|
|||
delete g_nat_zero;
|
||||
delete g_neg;
|
||||
delete g_not;
|
||||
delete g_not_of_iff_false;
|
||||
delete g_num;
|
||||
delete g_num_zero;
|
||||
delete g_num_pos;
|
||||
delete g_of_iff_true;
|
||||
delete g_one;
|
||||
delete g_option;
|
||||
delete g_option_some;
|
||||
|
|
@ -565,6 +574,7 @@ name const & get_eq_subst_name() { return *g_eq_subst; }
|
|||
name const & get_exists_elim_name() { return *g_exists_elim; }
|
||||
name const & get_false_name() { return *g_false; }
|
||||
name const & get_false_rec_name() { return *g_false_rec; }
|
||||
name const & get_false_of_true_iff_false_name() { return *g_false_of_true_iff_false; }
|
||||
name const & get_funext_name() { return *g_funext; }
|
||||
name const & get_has_zero_name() { return *g_has_zero; }
|
||||
name const & get_has_one_name() { return *g_has_one; }
|
||||
|
|
@ -601,9 +611,11 @@ name const & get_nat_succ_name() { return *g_nat_succ; }
|
|||
name const & get_nat_zero_name() { return *g_nat_zero; }
|
||||
name const & get_neg_name() { return *g_neg; }
|
||||
name const & get_not_name() { return *g_not; }
|
||||
name const & get_not_of_iff_false_name() { return *g_not_of_iff_false; }
|
||||
name const & get_num_name() { return *g_num; }
|
||||
name const & get_num_zero_name() { return *g_num_zero; }
|
||||
name const & get_num_pos_name() { return *g_num_pos; }
|
||||
name const & get_of_iff_true_name() { return *g_of_iff_true; }
|
||||
name const & get_one_name() { return *g_one; }
|
||||
name const & get_option_name() { return *g_option; }
|
||||
name const & get_option_some_name() { return *g_option_some; }
|
||||
|
|
|
|||
|
|
@ -44,6 +44,7 @@ name const & get_eq_subst_name();
|
|||
name const & get_exists_elim_name();
|
||||
name const & get_false_name();
|
||||
name const & get_false_rec_name();
|
||||
name const & get_false_of_true_iff_false_name();
|
||||
name const & get_funext_name();
|
||||
name const & get_has_zero_name();
|
||||
name const & get_has_one_name();
|
||||
|
|
@ -80,9 +81,11 @@ name const & get_nat_succ_name();
|
|||
name const & get_nat_zero_name();
|
||||
name const & get_neg_name();
|
||||
name const & get_not_name();
|
||||
name const & get_not_of_iff_false_name();
|
||||
name const & get_num_name();
|
||||
name const & get_num_zero_name();
|
||||
name const & get_num_pos_name();
|
||||
name const & get_of_iff_true_name();
|
||||
name const & get_one_name();
|
||||
name const & get_option_name();
|
||||
name const & get_option_some_name();
|
||||
|
|
|
|||
|
|
@ -37,6 +37,7 @@ eq.subst
|
|||
exists.elim
|
||||
false
|
||||
false.rec
|
||||
false_of_true_iff_false
|
||||
funext
|
||||
has_zero
|
||||
has_one
|
||||
|
|
@ -73,9 +74,11 @@ nat.succ
|
|||
nat.zero
|
||||
neg
|
||||
not
|
||||
not_of_iff_false
|
||||
num
|
||||
num.zero
|
||||
num.pos
|
||||
of_iff_true
|
||||
one
|
||||
option
|
||||
option.some
|
||||
|
|
|
|||
Loading…
Reference in a new issue