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

feat(library/blast/congruence_closure): add support for 'no_confusion' in the congruence closure module

Browse source
This commit is contained in:
Leonardo de Moura 2016-01-06 17:30:25 -08:00
parent cb02d1deae
commit 76cebb45f9
4 changed files with 99 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -100,11 +100,21 @@ scope_congruence_closure::~scope_congruence_closure() {
}
void congruence_closure::initialize() {
mk_entry_core(get_iff_name(), mk_true(), false, true);
mk_entry_core(get_iff_name(), mk_false(), false, true);
bool propagate_back = false;
bool interpreted = true;
bool constructor = false;
mk_entry_core(get_iff_name(), mk_true(), propagate_back, interpreted, constructor);
mk_entry_core(get_iff_name(), mk_false(), propagate_back, interpreted, constructor);
/* Put (nat.zero) and (@zero nat nat_has_zero) in the same equivalence class.
TODO(Leo): this is hackish, we should have a more general solution for this kind of equality. */
app_builder & b = get_app_builder();
expr nat_zero = mk_constant(get_nat_zero_name());
expr zero_nat = normalize(b.mk_zero(mk_constant(get_nat_name())));
add_eqv(get_eq_name(), nat_zero, zero_nat, b.mk_eq_refl(nat_zero));
}
void congruence_closure::mk_entry_core(name const & R, expr const & e, bool to_propagate, bool interpreted) {
void congruence_closure::mk_entry_core(name const & R, expr const & e, bool to_propagate, bool interpreted, bool constructor) {
lean_assert(!m_entries.find(eqc_key(R, e)));
entry n;
n.m_next = e;
@ -113,6 +123,7 @@ void congruence_closure::mk_entry_core(name const & R, expr const & e, bool to_p
n.m_size = 1;
n.m_flipped = false;
n.m_interpreted = interpreted;
n.m_constructor = constructor;
n.m_to_propagate = to_propagate;
n.m_mt = m_gmt;
m_entries.insert(eqc_key(R, e), n);
@ -135,6 +146,12 @@ void congruence_closure::mk_entry_core(name const & R, expr const & e, bool to_p
}
}
void congruence_closure::mk_entry_core(name const & R, expr const & e, bool to_propagate) {
bool interpreted = false;
bool constructor = R == get_eq_name() && is_constructor_app(env(), e);
return mk_entry_core(R, e, to_propagate, interpreted, constructor);
}
void congruence_closure::mk_entry(name const & R, expr const & e, bool to_propagate) {
if (to_propagate && !is_prop(e))
to_propagate = false;
@ -146,8 +163,7 @@ void congruence_closure::mk_entry(name const & R, expr const & e, bool to_propag
}
return;
}
bool interpreted = false;
mk_entry_core(R, e, to_propagate, interpreted);
mk_entry_core(R, e, to_propagate);
}
static bool all_distinct(buffer<expr> const & es) {
@ -618,15 +634,15 @@ void congruence_closure::internalize_core(name const & R, expr const & e, bool t
return;
case expr_kind::Constant: case expr_kind::Local:
case expr_kind::Meta:
mk_entry_core(R, e, to_propagate, false);
mk_entry_core(R, e, to_propagate);
return;
case expr_kind::Lambda:
mk_entry_core(R, e, false, false);
mk_entry_core(R, e, false);
return;
case expr_kind::Macro:
for (unsigned i = 0; i < macro_num_args(e); i++)
internalize_core(R, macro_arg(e, i), false, false);
mk_entry_core(R, e, to_propagate, false);
mk_entry_core(R, e, to_propagate);
break;
case expr_kind::Pi:
// TODO(Leo): should we support congruence for arrows?
@ -636,12 +652,12 @@ void congruence_closure::internalize_core(name const & R, expr const & e, bool t
internalize_core(R, binding_body(e), toplevel, to_propagate);
}
if (is_prop(e)) {
mk_entry_core(R, e, false, false);
mk_entry_core(R, e, false);
}
return;
case expr_kind::App: {
bool is_lapp = is_logical_app(e);
mk_entry_core(R, e, to_propagate && !is_lapp, false);
mk_entry_core(R, e, to_propagate && !is_lapp);
buffer<expr> args;
expr const & fn = get_app_args(e, args);
if (toplevel) {
@ -757,6 +773,19 @@ static bool is_true_or_false(expr const & e) {
return is_constant(e, get_true_name()) || is_constant(e, get_false_name());
}
void congruence_closure::propagate_no_confusion_eq(expr const & e1, expr const & e2) {
lean_assert(is_constructor_app(env(), e1));
lean_assert(is_constructor_app(env(), e2));
/* Add equality e1 =?= e2 to set of hypotheses. no_confusion_action will process it */
app_builder & b = get_app_builder();
state & s = curr_state();
expr type = b.mk_eq(e1, e2);
expr pr = *get_eqv_proof(get_eq_name(), e1, e2);
expr H = s.mk_hypothesis(type, pr);
lean_trace(name({"cc", "propagation"}),
tout() << "no confusion eq: " << ppb(H) << " : " << ppb(infer_type(H)) << "\n";);
}
/* Remark: If added_prop is not none, then it contains the proposition provided to ::add.
We use it here to avoid an unnecessary propagation back to the current_state. */
void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr const & H, optional<expr> const & added_prop) {
@ -774,14 +803,18 @@ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr con
// We want r2 to be the root of the combined class.
// We swap (e1,n1,r1) with (e2,n2,r2) when
// 1- is_interpreted(n1->m_root) && !is_interpreted(n2->m_root).
// 1- r1->m_interpreted && !r2->m_interpreted.
// Reason: to decide when to propagate we check whether the root of the equivalence class
// is true/false. So, this condition is to make sure if true/false is an equivalence class,
// then one of them is the root. If both are, it doesn't matter, since the state is inconsistent
// anyway.
// 2- r1->m_size > r2->m_size
// Reason: performance. Condition was has precedence
if ((r1->m_size > r2->m_size && !r2->m_interpreted) || r1->m_interpreted) {
// 2- r1->m_constructor && !r2->m_interpreted && !r2->m_constructor
// Reason: we want constructors to be the representative of their equivalence classes.
// 2- r1->m_size > r2->m_size && !r2->m_interpreted && !r2->m_constructor
// Reason: performance.
if ((r1->m_interpreted && !r2->m_interpreted) ||
(r1->m_constructor && !r2->m_interpreted && !r2->m_constructor) ||
(r1->m_size > r2->m_size && !r2->m_interpreted && !r2->m_constructor)) {
std::swap(e1, e2);
std::swap(n1, n2);
std::swap(r1, r2);
@ -792,6 +825,8 @@ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr con
if (r1->m_interpreted && r2->m_interpreted)
m_inconsistent = true;
bool use_no_confusion = R == get_eq_name() && r1->m_constructor && r2->m_constructor;
expr e1_root = n1->m_root;
expr e2_root = n2->m_root;
entry new_n1 = *n1;
@ -862,8 +897,9 @@ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr con
for (name const & R2 : m_non_eq_relations) {
if (m_entries.find(eqc_key(R2, e1)) ||
m_entries.find(eqc_key(R2, e2))) {
mk_entry(R2, e1, false);
mk_entry(R2, e2, false);
bool propagate_back = false;
mk_entry(R2, e1, propagate_back);
mk_entry(R2, e2, propagate_back);
push_todo(R2, e1, e2, *g_lift_mark);
}
}
@ -892,9 +928,13 @@ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr con
}
}
if (use_no_confusion) {
propagate_no_confusion_eq(e1_root, e2_root);
}
update_mt(R, e2_root);
lean_trace(name({"cc", "merge"}), tout() << ppb(e1) << " [" << R << "] " << ppb(e2) << "\n";);
lean_trace(name({"cc", "merge"}), tout() << ppb(e1_root) << " [" << R << "] " << ppb(e2_root) << "\n";);
lean_trace(name({"cc", "state"}), trace(););
}

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

@ -47,6 +47,7 @@ class congruence_closure {
unsigned m_flipped:1; // proof has been flipped
unsigned m_to_propagate:1; // must be propagated back to state when in equivalence class containing true/false
unsigned m_interpreted:1; // true if the node should be viewed as an abstract value
unsigned m_constructor:1; // true if head symbol is a constructor
unsigned m_size; // number of elements in the equivalence class, it is meaningless if 'e' != m_root
unsigned m_mt;
// The field m_mt is used to implement the mod-time optimization introduce by the Simplify theorem prover.
@ -125,7 +126,8 @@ class congruence_closure {
congr_key mk_congr_key(ext_congr_lemma const & lemma, expr const & e) const;
void check_iff_true(congr_key const & k);
void mk_entry_core(name const & R, expr const & e, bool to_propagate, bool interpreted);
void mk_entry_core(name const & R, expr const & e, bool to_propagate, bool interpreted, bool constructor);
void mk_entry_core(name const & R, expr const & e, bool to_propagate);
void mk_entry(name const & R, expr const & e, bool to_propagate);
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);
@ -138,6 +140,7 @@ class congruence_closure {
expr mk_iff_true_intro(expr const & proof);
void add_eqv_step(name const & R, expr e1, expr e2, expr const & H, optional<expr> const & added_prop);
void add_eqv_core(name const & R, expr const & lhs, expr const & rhs, expr const & H, optional<expr> const & added_prop);
void propagate_no_confusion_eq(expr const & e1, expr const & e2);
expr mk_congr_proof_core(name const & R, expr const & lhs, expr const & rhs) const;
expr mk_congr_proof(name const & R, expr const & lhs, expr const & rhs) const;

7
src/library/blast/strategies/portfolio.cpp
View file

@ -43,7 +43,12 @@ static optional<expr> apply_simple() {
static optional<expr> apply_cc() {
flet<bool> set(get_config().m_cc, true);
return mk_pre_action_strategy("cc", assert_cc_action)();
return mk_pre_action_strategy("cc",
[](hypothesis_idx hidx) {
Try(no_confusion_action(hidx));
Try(assert_cc_action(hidx));
return action_result::new_branch();
})();
}
static optional<expr> apply_ematch() {

32
tests/lean/run/blast_cc_noconfusion.lean Normal file
View file

@ -0,0 +1,32 @@
import data.list
open nat
constant f : nat → nat
example (a b c d : nat) : f d = f b → succ a = f b → f d = succ c → a = c :=
by blast
example (a b c d e : nat) : f d = f b → f e = f b → succ a = f b → f e = succ c → a = c :=
by blast
example (a b c d e : nat) : f d = f b → f e = f b → succ a = f b → f e = zero → false :=
by blast
example (a b c d e : nat) : f d = f b → f e = f b → succ a = f b → f e = 0 → false :=
by blast
open list
example (a b c d e f : nat) (l1 l2 l3 l4 : list nat) : l1 = l2 → l2 = l3 → l4 = [a, b, succ c] → l1 = [c, d, succ e] → l3 = l4 → c = e :=
by blast
example (a b c d e f : nat) (l1 l2 l3 l4 : list nat) : l4 = [a, b, succ (succ c)] → l1 = [c, d, succ (succ e)] → l3 = l4 → l1 = l2 → l2 = l3 → c = e :=
by blast
example (a b c d e f : nat) (l1 l2 l3 l4 : list nat) : l4 = [a, b, succ c] → l1 = [c, d, 0] → l3 = l4 → l1 = l2 → l2 = l3 → false :=
by blast
example (a b c d e f : nat) (l1 l2 l3 l4 : list nat) : l4 = [a, b, succ c] → l1 = nil → l3 = l4 → l1 = l2 → l2 = l3 → false :=
by blast
example (a b c d e f : nat) (l1 l2 l3 l4 : list nat) : l1 = l2 → l2 = l3 → l4 = [a, b, succ c] → l1 = nil → l3 = l4 → false :=
by blast