feat(library/tactic/smt): perform "unit propagation" in the congruence closure module
This commit is contained in:
Leonardo de Moura
parent
ca6d3743c7
commit
cefccd0e47
14 changed files with 566 additions and 253 deletions
103
library/init/cc_lemmas.lean
Normal file
103
library/init/cc_lemmas.lean
Normal file
|
|
@ -0,0 +1,103 @@
|
|||
/-
|
||||
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import init.propext init.classical
|
||||
|
||||
/- Lemmas use by the congruence closure module -/
|
||||
|
||||
lemma iff_eq_of_eq_true_left {a b : Prop} (h : a = true) : (a ↔ b) = b :=
|
||||
h^.symm ▸ propext (true_iff _)
|
||||
|
||||
lemma iff_eq_of_eq_true_right {a b : Prop} (h : b = true) : (a ↔ b) = a :=
|
||||
h^.symm ▸ propext (iff_true _)
|
||||
lemma iff_eq_true_of_eq {a b : Prop} (h : a = b) : (a ↔ b) = true :=
|
||||
h ▸ propext (iff_self _)
|
||||
|
||||
lemma and_eq_of_eq_true_left {a b : Prop} (h : a = true) : (a ∧ b) = b :=
|
||||
h^.symm ▸ propext (true_and _)
|
||||
|
||||
lemma and_eq_of_eq_true_right {a b : Prop} (h : b = true) : (a ∧ b) = a :=
|
||||
h^.symm ▸ propext (and_true _)
|
||||
|
||||
lemma and_eq_of_eq_false_left {a b : Prop} (h : a = false) : (a ∧ b) = false :=
|
||||
h^.symm ▸ propext (false_and _)
|
||||
|
||||
lemma and_eq_of_eq_false_right {a b : Prop} (h : b = false) : (a ∧ b) = false :=
|
||||
h^.symm ▸ propext (and_false _)
|
||||
|
||||
lemma and_eq_of_eq {a b : Prop} (h : a = b) : (a ∧ b) = a :=
|
||||
h ▸ propext (and_self _)
|
||||
|
||||
lemma or_eq_of_eq_true_left {a b : Prop} (h : a = true) : (a ∨ b) = true :=
|
||||
h^.symm ▸ propext (true_or _)
|
||||
|
||||
lemma or_eq_of_eq_true_right {a b : Prop} (h : b = true) : (a ∨ b) = true :=
|
||||
h^.symm ▸ propext (or_true _)
|
||||
|
||||
lemma or_eq_of_eq_false_left {a b : Prop} (h : a = false) : (a ∨ b) = b :=
|
||||
h^.symm ▸ propext (false_or _)
|
||||
|
||||
lemma or_eq_of_eq_false_right {a b : Prop} (h : b = false) : (a ∨ b) = a :=
|
||||
h^.symm ▸ propext (or_false _)
|
||||
|
||||
lemma or_eq_of_eq {a b : Prop} (h : a = b) : (a ∨ b) = a :=
|
||||
h ▸ propext (or_self _)
|
||||
|
||||
lemma imp_eq_of_eq_true_left {a b : Prop} (h : a = true) : (a → b) = b :=
|
||||
h^.symm ▸ propext (iff.intro (λ h, h trivial) (λ h₁ h₂, h₁))
|
||||
|
||||
lemma imp_eq_of_eq_true_right {a b : Prop} (h : b = true) : (a → b) = true :=
|
||||
h^.symm ▸ propext (iff.intro (λ h, trivial) (λ h₁ h₂, h₁))
|
||||
|
||||
lemma imp_eq_of_eq_false_left {a b : Prop} (h : a = false) : (a → b) = true :=
|
||||
h^.symm ▸ propext (iff.intro (λ h, trivial) (λ h₁ h₂, false.elim h₂))
|
||||
|
||||
lemma imp_eq_true_of_eq {a b : Prop} (h : a = b) : (a → b) = true :=
|
||||
h ▸ propext (iff.intro (λ h, trivial) (λ h ha, ha))
|
||||
|
||||
lemma not_eq_of_eq_true {a : Prop} (h : a = true) : (not a) = false :=
|
||||
h^.symm ▸ propext not_true_iff
|
||||
|
||||
lemma not_eq_of_eq_false {a : Prop} (h : a = false) : (not a) = true :=
|
||||
h^.symm ▸ propext not_false_iff
|
||||
|
||||
lemma false_of_a_eq_not_a {a : Prop} (h : a = not a) : false :=
|
||||
have not a, from λ ha, absurd ha (eq.mp h ha),
|
||||
absurd (eq.mpr h this) this
|
||||
|
||||
universe variables u
|
||||
|
||||
lemma if_eq_of_eq_true {c : Prop} [d : decidable c] {α : Type u} (t e : α) (h : c = true) : (@ite c d α t e) = t :=
|
||||
if_pos (of_eq_true h)
|
||||
|
||||
lemma if_eq_of_eq_false {c : Prop} [d : decidable c] {α : Type u} (t e : α) (h : c = false) : (@ite c d α t e) = e :=
|
||||
if_neg (not_of_eq_false h)
|
||||
|
||||
lemma if_eq_of_eq (c : Prop) [d : decidable c] {α : Type u} {t e : α} (h : t = e) : (@ite c d α t e) = t :=
|
||||
match d with
|
||||
| (is_true hc) := rfl
|
||||
| (is_false hnc) := eq.symm h
|
||||
end
|
||||
|
||||
lemma eq_true_of_and_eq_true_left {a b : Prop} (h : (a ∧ b) = true) : a = true :=
|
||||
eq_true_intro (and.left (of_eq_true h))
|
||||
|
||||
lemma eq_true_of_and_eq_true_right {a b : Prop} (h : (a ∧ b) = true) : b = true :=
|
||||
eq_true_intro (and.right (of_eq_true h))
|
||||
|
||||
lemma eq_false_of_or_eq_false_left {a b : Prop} (h : (a ∨ b) = false) : a = false :=
|
||||
eq_false_intro (λ ha, false.elim (eq.mp h (or.inl ha)))
|
||||
|
||||
lemma eq_false_of_or_eq_false_right {a b : Prop} (h : (a ∨ b) = false) : b = false :=
|
||||
eq_false_intro (λ hb, false.elim (eq.mp h (or.inr hb)))
|
||||
|
||||
lemma eq_false_of_not_eq_true {a : Prop} (h : (not a) = true) : a = false :=
|
||||
eq_false_intro (λ ha, absurd ha (eq.mpr h trivial))
|
||||
|
||||
/- Remark: the congruence closure module will only use the following lemma is
|
||||
cc_config.em is tt. -/
|
||||
lemma eq_true_of_not_eq_false {a : Prop} (h : (not a) = false) : a = true :=
|
||||
eq_true_intro (classical.by_contradiction (λ hna, eq.mp h hna))
|
||||
|
|
@ -5,7 +5,7 @@ Authors: Leonardo de Moura
|
|||
-/
|
||||
prelude
|
||||
import init.core init.logic init.category init.data.basic
|
||||
import init.propext init.funext init.category.combinators init.function init.classical
|
||||
import init.propext init.cc_lemmas init.funext init.category.combinators init.function init.classical
|
||||
import init.util init.coe init.wf init.meta init.algebra init.data
|
||||
import init.native
|
||||
|
||||
|
|
|
|||
|
|
@ -16,9 +16,12 @@ structure cc_config :=
|
|||
"Congruence Closure in Intensional Type Theory". If ho_fns is none, then full support is provided
|
||||
for *all* constants. -/
|
||||
(ho_fns : option (list name))
|
||||
/- If true, then use excluded middle -/
|
||||
(em : bool)
|
||||
|
||||
|
||||
def default_cc_config : cc_config :=
|
||||
{ignore_instances := tt, ac := tt, ho_fns := some []}
|
||||
{ignore_instances := tt, ac := tt, ho_fns := some [], em := tt}
|
||||
|
||||
/- Congruence closure state -/
|
||||
meta constant cc_state : Type
|
||||
|
|
|
|||
|
|
@ -14,4 +14,4 @@ import init.meta.mk_dec_eq_instance init.meta.mk_inhabited_instance
|
|||
import init.meta.simp_tactic init.meta.set_get_option_tactics
|
||||
import init.meta.interactive init.meta.converter init.meta.vm
|
||||
import init.meta.comp_value_tactics init.meta.congruence_tactics
|
||||
import init.meta.smt_tactic
|
||||
import init.meta.smt_tactic init.cc_lemmas
|
||||
|
|
|
|||
|
|
@ -1,3 +1,3 @@
|
|||
add_library(smt OBJECT congruence_closure.cpp congruence_tactics.cpp
|
||||
hinst_lemmas.cpp ematch.cpp theory_ac.cpp util.cpp
|
||||
unit_propagation.cpp smt_state.cpp init_module.cpp)
|
||||
smt_state.cpp init_module.cpp)
|
||||
|
|
|
|||
|
|
@ -429,6 +429,14 @@ void congruence_closure::push_todo(expr const & lhs, expr const & rhs, expr cons
|
|||
m_todo.emplace_back(lhs, rhs, H, heq_proof);
|
||||
}
|
||||
|
||||
void congruence_closure::push_heq(expr const & lhs, expr const & rhs, expr const & H) {
|
||||
m_todo.emplace_back(lhs, rhs, H, true);
|
||||
}
|
||||
|
||||
void congruence_closure::push_eq(expr const & lhs, expr const & rhs, expr const & H) {
|
||||
m_todo.emplace_back(lhs, rhs, H, false);
|
||||
}
|
||||
|
||||
void congruence_closure::process_subsingleton_elem(expr const & e) {
|
||||
expr type = m_ctx.infer(e);
|
||||
optional<expr> ss = m_ctx.mk_subsingleton_instance(type);
|
||||
|
|
@ -472,8 +480,7 @@ void congruence_closure::apply_simple_eqvs(expr const & e) {
|
|||
expr const & cast = get_app_args(e, args);
|
||||
expr const & a = args[3];
|
||||
expr proof = mk_app(mk_constant(get_cast_heq_name(), const_levels(cast)), args);
|
||||
bool heq_proof = true;
|
||||
push_todo(e, a, proof, heq_proof);
|
||||
push_heq(e, a, proof);
|
||||
}
|
||||
|
||||
if (is_app_of(e, get_eq_rec_name(), 6)) {
|
||||
|
|
@ -488,13 +495,14 @@ void congruence_closure::apply_simple_eqvs(expr const & e) {
|
|||
level l_2 = head(const_levels(eq_rec));
|
||||
level l_1 = head(tail(const_levels(eq_rec)));
|
||||
expr proof = mk_app({mk_constant(get_eq_rec_heq_name(), {l_1, l_2}), A, P, a, a_prime, H, p});
|
||||
bool heq_proof = true;
|
||||
push_todo(e, p, proof, heq_proof);
|
||||
push_heq(e, p, proof);
|
||||
}
|
||||
|
||||
if (auto r = m_ctx.reduce_projection(e)) {
|
||||
push_refl_eq(e, *r);
|
||||
}
|
||||
|
||||
propagate_up(e);
|
||||
}
|
||||
|
||||
void congruence_closure::add_occurrence(expr const & parent, expr const & child, bool symm_table) {
|
||||
|
|
@ -545,8 +553,7 @@ void congruence_closure::check_eq_true(symm_congr_key const & k) {
|
|||
rhs = get_root(rhs);
|
||||
if (lhs != rhs) return;
|
||||
// Add e = true
|
||||
bool heq_proof = false;
|
||||
push_todo(e, mk_true(), *g_eq_true_mark, heq_proof);
|
||||
push_eq(e, mk_true(), *g_eq_true_mark);
|
||||
}
|
||||
|
||||
void congruence_closure::add_symm_congruence_table(expr const & e) {
|
||||
|
|
@ -561,8 +568,7 @@ void congruence_closure::add_symm_congruence_table(expr const & e) {
|
|||
new_entry.m_cg_root = old_k->m_expr;
|
||||
m_state.m_entries.insert(e, new_entry);
|
||||
/* 2. Put new equivalence in the TODO queue */
|
||||
bool heq_proof = false;
|
||||
push_todo(e, old_k->m_expr, *g_congr_mark, heq_proof);
|
||||
push_eq(e, old_k->m_expr, *g_congr_mark);
|
||||
} else {
|
||||
m_state.m_symm_congruences.insert(k);
|
||||
}
|
||||
|
|
@ -594,6 +600,7 @@ void congruence_closure::state::mk_entry_core(expr const & e, bool interpreted,
|
|||
}
|
||||
|
||||
void congruence_closure::mk_entry(expr const & e, bool interpreted) {
|
||||
if (get_entry(e)) return;
|
||||
bool constructor = static_cast<bool>(is_constructor_app(env(), e));
|
||||
m_state.mk_entry_core(e, interpreted, constructor);
|
||||
process_subsingleton_elem(e);
|
||||
|
|
@ -777,6 +784,10 @@ void congruence_closure::internalize_core(expr const & e, optional<expr> const &
|
|||
if (is_arrow(e) && m_ctx.is_prop(binding_domain(e)) && m_ctx.is_prop(binding_body(e))) {
|
||||
internalize_core(binding_domain(e), some_expr(e));
|
||||
internalize_core(binding_body(e), some_expr(e));
|
||||
bool symm_table = false;
|
||||
add_occurrence(e, binding_domain(e), symm_table);
|
||||
add_occurrence(e, binding_body(e), symm_table);
|
||||
propagate_imp_up(e);
|
||||
}
|
||||
if (m_ctx.is_prop(e)) {
|
||||
mk_entry(e, false);
|
||||
|
|
@ -823,17 +834,22 @@ void congruence_closure::invert_trans(expr const & e) {
|
|||
invert_trans(e, false, none_expr(), none_expr());
|
||||
}
|
||||
|
||||
void congruence_closure::remove_parents(expr const & e) {
|
||||
void congruence_closure::remove_parents(expr const & e, buffer<expr> & parents_to_propagate) {
|
||||
auto ps = m_state.m_parents.find(e);
|
||||
if (!ps) return;
|
||||
ps->for_each([&](parent_occ const & p) {
|
||||
lean_trace(name({"debug", "cc"}), scope_trace_env(m_ctx.env(), m_ctx); tout() << "remove parent: " << p.m_expr << "\n";);
|
||||
if (p.m_symm_table) {
|
||||
symm_congr_key k = mk_symm_congr_key(p.m_expr);
|
||||
m_state.m_symm_congruences.erase(k);
|
||||
} else {
|
||||
congr_key k = mk_congr_key(p.m_expr);
|
||||
m_state.m_congruences.erase(k);
|
||||
ps->for_each([&](parent_occ const & pocc) {
|
||||
expr const & p = pocc.m_expr;
|
||||
lean_trace(name({"debug", "cc"}), scope_trace_env(m_ctx.env(), m_ctx); tout() << "remove parent: " << p << "\n";);
|
||||
if (may_propagate(p))
|
||||
parents_to_propagate.push_back(p);
|
||||
if (is_app(p)) {
|
||||
if (pocc.m_symm_table) {
|
||||
symm_congr_key k = mk_symm_congr_key(p);
|
||||
m_state.m_symm_congruences.erase(k);
|
||||
} else {
|
||||
congr_key k = mk_congr_key(p);
|
||||
m_state.m_congruences.erase(k);
|
||||
}
|
||||
}
|
||||
});
|
||||
}
|
||||
|
|
@ -843,10 +859,12 @@ void congruence_closure::reinsert_parents(expr const & e) {
|
|||
if (!ps) return;
|
||||
ps->for_each([&](parent_occ const & p) {
|
||||
lean_trace(name({"debug", "cc"}), scope_trace_env(m_ctx.env(), m_ctx); tout() << "reinsert parent: " << p.m_expr << "\n";);
|
||||
if (p.m_symm_table) {
|
||||
add_symm_congruence_table(p.m_expr);
|
||||
} else {
|
||||
add_congruence_table(p.m_expr);
|
||||
if (is_app(p.m_expr)) {
|
||||
if (p.m_symm_table) {
|
||||
add_symm_congruence_table(p.m_expr);
|
||||
} else {
|
||||
add_congruence_table(p.m_expr);
|
||||
}
|
||||
}
|
||||
});
|
||||
}
|
||||
|
|
@ -1173,14 +1191,12 @@ void congruence_closure::push_subsingleton_eq(expr const & a, expr const & b) {
|
|||
/* TODO(Leo): check if the following test is a performance bottleneck */
|
||||
if (m_ctx.relaxed_is_def_eq(A, B)) {
|
||||
/* TODO(Leo): to improve performance we can create the following proof lazily */
|
||||
bool heq_proof = false;
|
||||
expr proof = mk_app(m_ctx, get_subsingleton_elim_name(), a, b);
|
||||
push_todo(a, b, proof, heq_proof);
|
||||
push_eq(a, b, proof);
|
||||
} else {
|
||||
expr A_eq_B = *get_eq_proof(A, B);
|
||||
expr proof = mk_app(m_ctx, get_subsingleton_helim_name(), A_eq_B, a, b);
|
||||
bool heq_proof = true;
|
||||
push_todo(a, b, proof, heq_proof);
|
||||
push_heq(a, b, proof);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -1213,19 +1229,18 @@ void congruence_closure::propagate_constructor_eq(expr const & e1, expr const &
|
|||
lean_assert(c1 && c2);
|
||||
expr type = mk_eq(m_ctx, e1, e2);
|
||||
expr h = *get_eq_proof(e1, e2);
|
||||
bool heq_proof = false;
|
||||
if (*c1 == *c2) {
|
||||
buffer<std::tuple<expr, expr, expr>> implied_eqs;
|
||||
mk_constructor_eq_constructor_implied_eqs(m_ctx, e1, e2, h, implied_eqs);
|
||||
for (std::tuple<expr, expr, expr> const & t : implied_eqs) {
|
||||
expr lhs, rhs, H;
|
||||
std::tie(lhs, rhs, H) = t;
|
||||
push_todo(lhs, rhs, H, heq_proof);
|
||||
push_eq(lhs, rhs, H);
|
||||
}
|
||||
} else {
|
||||
if (optional<expr> false_pr = mk_constructor_eq_constructor_inconsistency_proof(m_ctx, e1, e2, h)) {
|
||||
expr H = mk_app(mk_constant(get_true_eq_false_of_false_name()), *false_pr);
|
||||
push_todo(mk_true(), mk_false(), H, heq_proof);
|
||||
push_eq(mk_true(), mk_false(), H);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1254,6 +1269,255 @@ void congruence_closure::propagate_projection_constructor(expr const & p, expr c
|
|||
internalize_core(new_p, none_expr());
|
||||
}
|
||||
|
||||
bool congruence_closure::is_eq_true(expr const & e) const {
|
||||
return is_eqv(e, mk_true());
|
||||
}
|
||||
|
||||
bool congruence_closure::is_eq_false(expr const & e) const {
|
||||
return is_eqv(e, mk_false());
|
||||
}
|
||||
|
||||
// Remark: possible optimization: use delayed proof macros for get_eq_true_proof, get_eq_false_proof and get_prop_eq_proof
|
||||
|
||||
expr congruence_closure::get_eq_true_proof(expr const & e) const {
|
||||
lean_assert(is_eq_true(e));
|
||||
return *get_eq_proof(e, mk_true());
|
||||
}
|
||||
|
||||
expr congruence_closure::get_eq_false_proof(expr const & e) const {
|
||||
lean_assert(is_eq_false(e));
|
||||
return *get_eq_proof(e, mk_false());
|
||||
}
|
||||
|
||||
expr congruence_closure::get_prop_eq_proof(expr const & a, expr const & b) const {
|
||||
lean_assert(is_eqv(a, b));
|
||||
return *get_eq_proof(a, b);
|
||||
}
|
||||
|
||||
static expr * g_iff_eq_of_eq_true_left = nullptr;
|
||||
static expr * g_iff_eq_of_eq_true_right = nullptr;
|
||||
static expr * g_iff_eq_true_of_eq = nullptr;
|
||||
|
||||
void congruence_closure::propagate_iff_up(expr const & e) {
|
||||
expr a, b;
|
||||
lean_verify(is_iff(e, a, b));
|
||||
|
||||
if (is_eq_true(a)) {
|
||||
// a = true -> (iff a b) = b
|
||||
push_eq(e, b, mk_app(*g_iff_eq_of_eq_true_left, a, b, get_eq_true_proof(a)));
|
||||
} else if (is_eq_true(b)) {
|
||||
// b = true -> (iff a b) = a
|
||||
push_eq(e, a, mk_app(*g_iff_eq_of_eq_true_right, a, b, get_eq_true_proof(b)));
|
||||
} else if (is_eqv(a, b)) {
|
||||
// a = b -> (iff a b) = true
|
||||
push_eq(e, mk_true(), mk_app(*g_iff_eq_true_of_eq, a, b, get_prop_eq_proof(a, b)));
|
||||
}
|
||||
}
|
||||
|
||||
static expr * g_and_eq_of_eq_true_left = nullptr;
|
||||
static expr * g_and_eq_of_eq_true_right = nullptr;
|
||||
static expr * g_and_eq_of_eq_false_left = nullptr;
|
||||
static expr * g_and_eq_of_eq_false_right = nullptr;
|
||||
static expr * g_and_eq_of_eq = nullptr;
|
||||
|
||||
void congruence_closure::propagate_and_up(expr const & e) {
|
||||
expr a, b;
|
||||
lean_verify(is_and(e, a, b));
|
||||
|
||||
if (is_eq_true(a)) {
|
||||
// a = true -> (and a b) = b
|
||||
push_eq(e, b, mk_app(*g_and_eq_of_eq_true_left, a, b, get_eq_true_proof(a)));
|
||||
} else if (is_eq_true(b)) {
|
||||
// b = true -> (and a b) = a
|
||||
push_eq(e, a, mk_app(*g_and_eq_of_eq_true_right, a, b, get_eq_true_proof(b)));
|
||||
} else if (is_eq_false(a)) {
|
||||
// a = false -> (and a b) = false
|
||||
push_eq(e, mk_false(), mk_app(*g_and_eq_of_eq_false_left, a, b, get_eq_false_proof(a)));
|
||||
} else if (is_eq_false(b)) {
|
||||
// b = false -> (and a b) = false
|
||||
push_eq(e, mk_false(), mk_app(*g_and_eq_of_eq_false_right, a, b, get_eq_false_proof(b)));
|
||||
} else if (is_eqv(a, b)) {
|
||||
// a = b -> (and a b) = a
|
||||
push_eq(e, a, mk_app(*g_and_eq_of_eq, a, b, get_prop_eq_proof(a, b)));
|
||||
}
|
||||
|
||||
// We may also add
|
||||
// a = not b -> (and a b) = false
|
||||
}
|
||||
|
||||
static expr * g_or_eq_of_eq_true_left = nullptr;
|
||||
static expr * g_or_eq_of_eq_true_right = nullptr;
|
||||
static expr * g_or_eq_of_eq_false_left = nullptr;
|
||||
static expr * g_or_eq_of_eq_false_right = nullptr;
|
||||
static expr * g_or_eq_of_eq = nullptr;
|
||||
|
||||
void congruence_closure::propagate_or_up(expr const & e) {
|
||||
expr a, b;
|
||||
lean_verify(is_or(e, a, b));
|
||||
|
||||
if (is_eq_true(a)) {
|
||||
// a = true -> (or a b) = true
|
||||
push_eq(e, mk_true(), mk_app(*g_or_eq_of_eq_true_left, a, b, get_eq_true_proof(a)));
|
||||
} else if (is_eq_true(b)) {
|
||||
// b = true -> (or a b) = true
|
||||
push_eq(e, mk_true(), mk_app(*g_or_eq_of_eq_true_right, a, b, get_eq_true_proof(b)));
|
||||
} else if (is_eq_false(a)) {
|
||||
// a = false -> (or a b) = b
|
||||
push_eq(e, b, mk_app(*g_or_eq_of_eq_false_left, a, b, get_eq_false_proof(a)));
|
||||
} else if (is_eq_false(b)) {
|
||||
// b = false -> (or a b) = a
|
||||
push_eq(e, a, mk_app(*g_or_eq_of_eq_false_right, a, b, get_eq_false_proof(b)));
|
||||
} else if (is_eqv(a, b)) {
|
||||
// a = b -> (or a b) = a
|
||||
push_eq(e, a, mk_app(*g_or_eq_of_eq, a, b, get_prop_eq_proof(a, b)));
|
||||
}
|
||||
|
||||
// We may also add
|
||||
// a = not b -> (or a b) = true
|
||||
}
|
||||
|
||||
static expr * g_not_eq_of_eq_true = nullptr;
|
||||
static expr * g_not_eq_of_eq_false = nullptr;
|
||||
static expr * g_false_of_a_eq_not_a = nullptr;
|
||||
|
||||
void congruence_closure::propagate_not_up(expr const & e) {
|
||||
expr a;
|
||||
lean_verify(is_not(e, a));
|
||||
|
||||
if (is_eq_true(a)) {
|
||||
// a = true -> not a = false
|
||||
push_eq(e, mk_false(), mk_app(*g_not_eq_of_eq_true, a, get_eq_true_proof(a)));
|
||||
} else if (is_eq_false(a)) {
|
||||
// a = false -> not a = true
|
||||
push_eq(e, mk_true(), mk_app(*g_not_eq_of_eq_false, a, get_eq_false_proof(a)));
|
||||
} else if (is_eqv(a, e)) {
|
||||
expr false_pr = mk_app(*g_false_of_a_eq_not_a, a, get_prop_eq_proof(a, e));
|
||||
expr H = mk_app(mk_constant(get_true_eq_false_of_false_name()), false_pr);
|
||||
push_eq(mk_true(), mk_false(), H);
|
||||
}
|
||||
}
|
||||
|
||||
static expr * g_imp_eq_of_eq_true_left = nullptr;
|
||||
static expr * g_imp_eq_of_eq_false_left = nullptr;
|
||||
static expr * g_imp_eq_of_eq_true_right = nullptr;
|
||||
static expr * g_imp_eq_true_of_eq = nullptr;
|
||||
|
||||
void congruence_closure::propagate_imp_up(expr const & e) {
|
||||
lean_assert(is_arrow(e));
|
||||
expr a = binding_domain(e);
|
||||
expr b = binding_body(e);
|
||||
|
||||
if (is_eq_true(a)) {
|
||||
// a = true -> (a -> b) = b
|
||||
push_eq(e, b, mk_app(*g_imp_eq_of_eq_true_left, a, b, get_eq_true_proof(a)));
|
||||
} else if (is_eq_false(a)) {
|
||||
// a = false -> (a -> b) = true
|
||||
push_eq(e, mk_true(), mk_app(*g_imp_eq_of_eq_false_left, a, b, get_eq_false_proof(a)));
|
||||
} else if (is_eq_true(b)) {
|
||||
// b = true -> (a -> b) = true
|
||||
push_eq(e, mk_true(), mk_app(*g_imp_eq_of_eq_true_right, a, b, get_eq_true_proof(b)));
|
||||
} else if (is_eqv(a, b)) {
|
||||
// a = b -> (a -> b) = true
|
||||
push_eq(e, mk_true(), mk_app(*g_imp_eq_true_of_eq, a, b, get_prop_eq_proof(a, b)));
|
||||
}
|
||||
}
|
||||
|
||||
static name * g_if_eq_of_eq_true = nullptr;
|
||||
static name * g_if_eq_of_eq_false = nullptr;
|
||||
static name * g_if_eq_of_eq = nullptr;
|
||||
|
||||
void congruence_closure::propagate_ite_up(expr const & e) {
|
||||
expr c, d, A, a, b;
|
||||
lean_verify(is_ite(e, c, d, A, a, b));
|
||||
|
||||
if (is_eq_true(c)) {
|
||||
// c = true -> (ite c a b) = a
|
||||
level lvl = get_level(m_ctx, A);
|
||||
push_eq(e, a, mk_app({mk_constant(*g_if_eq_of_eq_true, {lvl}), c, d, A, a, b, get_eq_true_proof(c)}));
|
||||
} else if (is_eq_false(c)) {
|
||||
// c = false -> (ite c a b) = b
|
||||
level lvl = get_level(m_ctx, A);
|
||||
push_eq(e, b, mk_app({mk_constant(*g_if_eq_of_eq_false, {lvl}), c, d, A, a, b, get_eq_false_proof(c)}));
|
||||
} else if (is_eqv(a, b)) {
|
||||
// a = b -> (ite c a b) = a
|
||||
level lvl = get_level(m_ctx, A);
|
||||
push_eq(e, a, mk_app({mk_constant(*g_if_eq_of_eq, {lvl}), c, d, A, a, b, get_prop_eq_proof(a, b)}));
|
||||
}
|
||||
}
|
||||
|
||||
bool congruence_closure::may_propagate(expr const & e) {
|
||||
return
|
||||
is_iff(e) || is_and(e) || is_or(e) || is_not(e) || is_arrow(e) || is_ite(e);
|
||||
}
|
||||
|
||||
void congruence_closure::propagate_up(expr const & e) {
|
||||
if (m_state.m_inconsistent) return;
|
||||
if (is_iff(e)) {
|
||||
propagate_iff_up(e);
|
||||
} else if (is_and(e)) {
|
||||
propagate_and_up(e);
|
||||
} else if (is_or(e)) {
|
||||
propagate_or_up(e);
|
||||
} else if (is_not(e)) {
|
||||
propagate_not_up(e);
|
||||
} else if (is_arrow(e)) {
|
||||
propagate_imp_up(e);
|
||||
} else if (is_ite(e)) {
|
||||
propagate_ite_up(e);
|
||||
}
|
||||
}
|
||||
|
||||
static expr * g_eq_true_of_and_eq_true_left = nullptr;
|
||||
static expr * g_eq_true_of_and_eq_true_right = nullptr;
|
||||
|
||||
void congruence_closure::propagate_and_down(expr const & e) {
|
||||
if (is_eq_true(e)) {
|
||||
expr a, b;
|
||||
lean_verify(is_and(e, a, b));
|
||||
expr h = get_eq_true_proof(e);
|
||||
push_eq(a, mk_true(), mk_app(*g_eq_true_of_and_eq_true_left, a, b, h));
|
||||
push_eq(b, mk_true(), mk_app(*g_eq_true_of_and_eq_true_right, a, b, h));
|
||||
}
|
||||
}
|
||||
|
||||
static expr * g_eq_false_of_or_eq_false_left = nullptr;
|
||||
static expr * g_eq_false_of_or_eq_false_right = nullptr;
|
||||
|
||||
void congruence_closure::propagate_or_down(expr const & e) {
|
||||
if (is_eq_false(e)) {
|
||||
expr a, b;
|
||||
lean_verify(is_or(e, a, b));
|
||||
expr h = get_eq_false_proof(e);
|
||||
push_eq(a, mk_false(), mk_app(*g_eq_false_of_or_eq_false_left, a, b, h));
|
||||
push_eq(b, mk_false(), mk_app(*g_eq_false_of_or_eq_false_right, a, b, h));
|
||||
}
|
||||
}
|
||||
|
||||
static expr * g_eq_false_of_not_eq_true = nullptr;
|
||||
static expr * g_eq_true_of_not_eq_false = nullptr;
|
||||
|
||||
void congruence_closure::propagate_not_down(expr const & e) {
|
||||
if (is_eq_true(e)) {
|
||||
expr a;
|
||||
lean_verify(is_not(e, a));
|
||||
push_eq(a, mk_false(), mk_app(*g_eq_false_of_not_eq_true, a, get_eq_true_proof(e)));
|
||||
} else if (m_state.m_config.m_em && is_eq_false(e)) {
|
||||
expr a;
|
||||
lean_verify(is_not(e, a));
|
||||
push_eq(a, mk_true(), mk_app(*g_eq_true_of_not_eq_false, a, get_eq_false_proof(e)));
|
||||
}
|
||||
}
|
||||
|
||||
void congruence_closure::propagate_down(expr const & e) {
|
||||
if (is_and(e)) {
|
||||
propagate_and_down(e);
|
||||
} else if (is_or(e)) {
|
||||
propagate_or_down(e);
|
||||
} else if (is_not(e)) {
|
||||
propagate_not_down(e);
|
||||
}
|
||||
}
|
||||
|
||||
void congruence_closure::propagate_value_inconsistency(expr const & e1, expr const & e2) {
|
||||
lean_assert(is_interpreted_value(e1));
|
||||
lean_assert(is_interpreted_value(e2));
|
||||
|
|
@ -1261,8 +1525,7 @@ void congruence_closure::propagate_value_inconsistency(expr const & e1, expr con
|
|||
expr eq_proof = *get_eq_proof(e1, e2);
|
||||
expr true_eq_false = mk_eq(m_ctx, mk_true(), mk_false());
|
||||
expr H = mk_absurd(m_ctx, eq_proof, ne_proof, true_eq_false);
|
||||
bool heq_proof = false;
|
||||
push_todo(mk_true(), mk_false(), H, heq_proof);
|
||||
push_eq(mk_true(), mk_false(), H);
|
||||
}
|
||||
|
||||
static bool is_true_or_false(expr const & e) {
|
||||
|
|
@ -1337,8 +1600,9 @@ void congruence_closure::add_eqv_step(expr e1, expr e2, expr const & H,
|
|||
new_n1.m_flipped = flipped;
|
||||
m_state.m_entries.insert(e1, new_n1);
|
||||
|
||||
buffer<expr> parents_to_propagate;
|
||||
/* The hash code for the parents is going to change */
|
||||
remove_parents(e1_root);
|
||||
remove_parents(e1_root, parents_to_propagate);
|
||||
|
||||
/* force all m_root fields in e1 equivalence class to point to e2_root */
|
||||
bool propagate = is_true_or_false(e2_root);
|
||||
|
|
@ -1384,7 +1648,7 @@ void congruence_closure::add_eqv_step(expr e1, expr e2, expr const & H,
|
|||
if (auto it = m_state.m_parents.find(e2_root))
|
||||
ps2 = *it;
|
||||
ps1->for_each([&](parent_occ const & p) {
|
||||
if (is_congr_root(p.m_expr)) {
|
||||
if (is_app(p.m_expr) && is_congr_root(p.m_expr)) {
|
||||
if (!constructor_eq && r2->m_constructor) {
|
||||
propagate_projection_constructor(p.m_expr, e2_root);
|
||||
}
|
||||
|
|
@ -1395,25 +1659,32 @@ void congruence_closure::add_eqv_step(expr e1, expr e2, expr const & H,
|
|||
m_state.m_parents.insert(e2_root, ps2);
|
||||
}
|
||||
|
||||
if (!m_state.m_inconsistent && ac_var1 && ac_var2)
|
||||
m_ac.add_eq(*ac_var1, *ac_var2);
|
||||
|
||||
if (!m_state.m_inconsistent && constructor_eq)
|
||||
propagate_constructor_eq(e1_root, e2_root);
|
||||
|
||||
if (!m_state.m_inconsistent && value_inconsistency)
|
||||
propagate_value_inconsistency(e1_root, e2_root);
|
||||
|
||||
if (!m_state.m_inconsistent) {
|
||||
if (ac_var1 && ac_var2)
|
||||
m_ac.add_eq(*ac_var1, *ac_var2);
|
||||
|
||||
if (constructor_eq) {
|
||||
propagate_constructor_eq(e1_root, e2_root);
|
||||
}
|
||||
|
||||
if (value_inconsistency) {
|
||||
propagate_value_inconsistency(e1_root, e2_root);
|
||||
}
|
||||
|
||||
update_mt(e2_root);
|
||||
check_new_subsingleton_eq(e1_root, e2_root);
|
||||
|
||||
if (!to_propagate.empty() && m_phandler) {
|
||||
m_phandler->propagated(to_propagate);
|
||||
}
|
||||
}
|
||||
|
||||
if (!m_state.m_inconsistent) {
|
||||
for (expr const & p : parents_to_propagate)
|
||||
propagate_up(p);
|
||||
}
|
||||
|
||||
if (!m_state.m_inconsistent && !to_propagate.empty()) {
|
||||
for (expr const & e : to_propagate)
|
||||
propagate_down(e);
|
||||
if (m_phandler)
|
||||
m_phandler->propagated(to_propagate);
|
||||
}
|
||||
|
||||
lean_trace(name({"cc", "merge"}), scope_trace_env scope(m_ctx.env(), m_ctx);
|
||||
tout() << e1_root << " = " << e2_root << "\n";);
|
||||
lean_trace(name({"debug", "cc"}), scope_trace_env scope(m_ctx.env(), m_ctx);
|
||||
|
|
@ -1626,11 +1897,87 @@ void initialize_congruence_closure() {
|
|||
g_congr_mark = new expr(mk_constant(name(prefix, "[congruence]")));
|
||||
g_eq_true_mark = new expr(mk_constant(name(prefix, "[iff-true]")));
|
||||
g_refl_mark = new expr(mk_constant(name(prefix, "[refl]")));
|
||||
|
||||
g_iff_eq_of_eq_true_left = new expr(mk_constant("iff_eq_of_eq_true_left"));
|
||||
g_iff_eq_of_eq_true_right = new expr(mk_constant("iff_eq_of_eq_true_right"));
|
||||
g_iff_eq_true_of_eq = new expr(mk_constant("iff_eq_true_of_eq"));
|
||||
|
||||
g_and_eq_of_eq_true_left = new expr(mk_constant("and_eq_of_eq_true_left"));
|
||||
g_and_eq_of_eq_true_right = new expr(mk_constant("and_eq_of_eq_true_right"));
|
||||
g_and_eq_of_eq_false_left = new expr(mk_constant("and_eq_of_eq_false_left"));
|
||||
g_and_eq_of_eq_false_right = new expr(mk_constant("and_eq_of_eq_false_right"));
|
||||
g_and_eq_of_eq = new expr(mk_constant("and_eq_of_eq"));
|
||||
|
||||
g_or_eq_of_eq_true_left = new expr(mk_constant("or_eq_of_eq_true_left"));
|
||||
g_or_eq_of_eq_true_right = new expr(mk_constant("or_eq_of_eq_true_right"));
|
||||
g_or_eq_of_eq_false_left = new expr(mk_constant("or_eq_of_eq_false_left"));
|
||||
g_or_eq_of_eq_false_right = new expr(mk_constant("or_eq_of_eq_false_right"));
|
||||
g_or_eq_of_eq = new expr(mk_constant("or_eq_of_eq"));
|
||||
|
||||
g_not_eq_of_eq_true = new expr(mk_constant("not_eq_of_eq_true "));
|
||||
g_not_eq_of_eq_false = new expr(mk_constant("not_eq_of_eq_false"));
|
||||
g_false_of_a_eq_not_a = new expr(mk_constant("false_of_a_eq_not_a"));
|
||||
|
||||
g_imp_eq_of_eq_true_left = new expr(mk_constant("imp_eq_of_eq_true_left"));
|
||||
g_imp_eq_of_eq_false_left = new expr(mk_constant("imp_eq_of_eq_false_left"));
|
||||
g_imp_eq_of_eq_true_right = new expr(mk_constant("imp_eq_of_eq_true_right"));
|
||||
g_imp_eq_true_of_eq = new expr(mk_constant("imp_eq_true_of_eq"));
|
||||
|
||||
g_if_eq_of_eq_true = new name("if_eq_of_eq_true");
|
||||
g_if_eq_of_eq_false = new name("if_eq_of_eq_false");
|
||||
g_if_eq_of_eq = new name("if_eq_of_eq");
|
||||
|
||||
g_eq_true_of_and_eq_true_left = new expr(mk_constant("eq_true_of_and_eq_true_left"));
|
||||
g_eq_true_of_and_eq_true_right = new expr(mk_constant("eq_true_of_and_eq_true_right"));
|
||||
|
||||
g_eq_false_of_or_eq_false_left = new expr(mk_constant("eq_false_of_or_eq_false_left"));
|
||||
g_eq_false_of_or_eq_false_right = new expr(mk_constant("eq_false_of_or_eq_false_right"));
|
||||
|
||||
g_eq_false_of_not_eq_true = new expr(mk_constant("eq_false_of_not_eq_true"));
|
||||
g_eq_true_of_not_eq_false = new expr(mk_constant("eq_true_of_not_eq_false"));
|
||||
}
|
||||
|
||||
void finalize_congruence_closure() {
|
||||
delete g_congr_mark;
|
||||
delete g_eq_true_mark;
|
||||
delete g_refl_mark;
|
||||
|
||||
delete g_iff_eq_of_eq_true_left;
|
||||
delete g_iff_eq_of_eq_true_right;
|
||||
delete g_iff_eq_true_of_eq;
|
||||
|
||||
delete g_and_eq_of_eq_true_left;
|
||||
delete g_and_eq_of_eq_true_right;
|
||||
delete g_and_eq_of_eq_false_left;
|
||||
delete g_and_eq_of_eq_false_right;
|
||||
delete g_and_eq_of_eq;
|
||||
|
||||
delete g_or_eq_of_eq_true_left;
|
||||
delete g_or_eq_of_eq_true_right;
|
||||
delete g_or_eq_of_eq_false_left;
|
||||
delete g_or_eq_of_eq_false_right;
|
||||
delete g_or_eq_of_eq;
|
||||
|
||||
delete g_not_eq_of_eq_true;
|
||||
delete g_not_eq_of_eq_false;
|
||||
delete g_false_of_a_eq_not_a;
|
||||
|
||||
delete g_imp_eq_of_eq_true_left;
|
||||
delete g_imp_eq_of_eq_false_left;
|
||||
delete g_imp_eq_of_eq_true_right;
|
||||
delete g_imp_eq_true_of_eq;
|
||||
|
||||
delete g_if_eq_of_eq_true;
|
||||
delete g_if_eq_of_eq_false;
|
||||
delete g_if_eq_of_eq;
|
||||
|
||||
delete g_eq_true_of_and_eq_true_left;
|
||||
delete g_eq_true_of_and_eq_true_right;
|
||||
|
||||
delete g_eq_false_of_or_eq_false_left;
|
||||
delete g_eq_false_of_or_eq_false_right;
|
||||
|
||||
delete g_eq_false_of_not_eq_true;
|
||||
delete g_eq_true_of_not_eq_false;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -109,7 +109,8 @@ public:
|
|||
unsigned m_values:1;
|
||||
unsigned m_all_ho:1;
|
||||
unsigned m_ac:1;
|
||||
config() { m_ignore_instances = true; m_values = true; m_all_ho = false; m_ac = true; }
|
||||
unsigned m_em:1;
|
||||
config() { m_ignore_instances = true; m_values = true; m_all_ho = false; m_ac = true; m_em = true; }
|
||||
};
|
||||
|
||||
class state {
|
||||
|
|
@ -197,11 +198,12 @@ private:
|
|||
void internalize_app(expr const & e);
|
||||
void internalize_core(expr const & e, optional<expr> const & parent);
|
||||
void push_todo(expr const & lhs, expr const & rhs, expr const & H, bool heq_proof);
|
||||
void push_new_eq(expr const & lhs, expr const & rhs, expr const & H) { push_todo(lhs, rhs, H, false); }
|
||||
void push_heq(expr const & lhs, expr const & rhs, expr const & H);
|
||||
void push_eq(expr const & lhs, expr const & rhs, expr const & H);
|
||||
void push_refl_eq(expr const & lhs, expr const & rhs);
|
||||
void invert_trans(expr const & e, bool new_flipped, optional<expr> new_target, optional<expr> new_proof);
|
||||
void invert_trans(expr const & e);
|
||||
void remove_parents(expr const & e);
|
||||
void remove_parents(expr const & e, buffer<expr> & parents_to_propagate);
|
||||
void reinsert_parents(expr const & e);
|
||||
void update_mt(expr const & e);
|
||||
bool has_heq_proofs(expr const & root) const;
|
||||
|
|
@ -217,6 +219,23 @@ private:
|
|||
optional<expr> get_eq_proof_core(expr const & e1, expr const & e2, bool as_heq) const;
|
||||
void push_subsingleton_eq(expr const & a, expr const & b);
|
||||
void check_new_subsingleton_eq(expr const & old_root, expr const & new_root);
|
||||
bool is_eq_true(expr const & e) const;
|
||||
bool is_eq_false(expr const & e) const;
|
||||
expr get_eq_true_proof(expr const & e) const;
|
||||
expr get_eq_false_proof(expr const & e) const;
|
||||
expr get_prop_eq_proof(expr const & a, expr const & b) const;
|
||||
static bool may_propagate(expr const & e);
|
||||
void propagate_iff_up(expr const & e);
|
||||
void propagate_and_up(expr const & e);
|
||||
void propagate_or_up(expr const & e);
|
||||
void propagate_not_up(expr const & e);
|
||||
void propagate_imp_up(expr const & e);
|
||||
void propagate_ite_up(expr const & e);
|
||||
void propagate_up(expr const & e);
|
||||
void propagate_and_down(expr const & e);
|
||||
void propagate_or_down(expr const & e);
|
||||
void propagate_not_down(expr const & e);
|
||||
void propagate_down(expr const & e);
|
||||
void propagate_inst_implicit(expr const & e);
|
||||
void propagate_constructor_eq(expr const & e1, expr const & e2);
|
||||
void propagate_projection_constructor(expr const & p, expr const & c);
|
||||
|
|
|
|||
|
|
@ -51,6 +51,7 @@ structure cc_config :=
|
|||
(ignore_instances : bool)
|
||||
(ac : bool)
|
||||
(ho_fns : option (list name))
|
||||
(em : bool)
|
||||
*/
|
||||
pair<name_set, congruence_closure::config> to_ho_fns_cc_config(vm_obj const & cfg) {
|
||||
congruence_closure::config c;
|
||||
|
|
@ -63,6 +64,7 @@ pair<name_set, congruence_closure::config> to_ho_fns_cc_config(vm_obj const & cf
|
|||
c.m_all_ho = false;
|
||||
ho_fns = to_name_set(to_list_name(get_some_value(cfield(cfg, 2))));
|
||||
}
|
||||
c.m_em = to_bool(cfield(cfg, 3));
|
||||
return mk_pair(ho_fns, c);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -33,8 +33,7 @@ smt_goal::smt_goal(smt_config const & cfg):
|
|||
smt::smt(type_context & ctx, smt_goal & g):
|
||||
m_ctx(ctx),
|
||||
m_goal(g),
|
||||
m_cc(ctx, m_goal.m_cc_state, this),
|
||||
m_up(ctx, m_goal.m_up_state, *this) {
|
||||
m_cc(ctx, m_goal.m_cc_state, this) {
|
||||
}
|
||||
|
||||
smt::~smt() {
|
||||
|
|
@ -47,9 +46,6 @@ void smt::propagated(unsigned n, expr const * p) {
|
|||
format r;
|
||||
for (unsigned i = 0; i < n; i++) { if (i > 0) r += comma() + line(); r += fmt(p[i]); }
|
||||
tout() << group(format("new facts:") + line() + bracket("{", r, "}")) << "\n";);
|
||||
for (unsigned i = 0; i < n; i++) {
|
||||
m_up.assigned(p[i]);
|
||||
}
|
||||
}
|
||||
|
||||
lbool smt::get_value_core(expr const & e) {
|
||||
|
|
|
|||
|
|
@ -7,7 +7,6 @@ Author: Leonardo de Moura
|
|||
#pragma once
|
||||
#include "library/discr_tree.h"
|
||||
#include "library/tactic/simp_lemmas.h"
|
||||
#include "library/tactic/smt/unit_propagation.h"
|
||||
#include "library/tactic/smt/congruence_closure.h"
|
||||
#include "library/tactic/smt/ematch.h"
|
||||
|
||||
|
|
@ -25,7 +24,6 @@ class smt_goal {
|
|||
friend class smt;
|
||||
cc_state m_cc_state;
|
||||
ematch_state m_em_state;
|
||||
up_state m_up_state;
|
||||
simp_lemmas m_simp_lemmas;
|
||||
public:
|
||||
smt_goal(smt_config const & cfg);
|
||||
|
|
@ -33,16 +31,16 @@ public:
|
|||
simp_lemmas const & get_simp_lemmas() const { return m_simp_lemmas; }
|
||||
};
|
||||
|
||||
class smt : public cc_propagation_handler, public up_assignment {
|
||||
class smt : public cc_propagation_handler {
|
||||
private:
|
||||
type_context & m_ctx;
|
||||
smt_goal & m_goal;
|
||||
congruence_closure m_cc;
|
||||
unit_propagation m_up;
|
||||
|
||||
lbool get_value_core(expr const & e);
|
||||
lbool get_value(expr const & e);
|
||||
virtual void propagated(unsigned n, expr const * p) override;
|
||||
virtual lbool get_value(expr const & e) override;
|
||||
|
||||
public:
|
||||
smt(type_context & ctx, smt_goal & g);
|
||||
virtual ~smt();
|
||||
|
|
@ -50,7 +48,7 @@ public:
|
|||
void internalize(expr const & e);
|
||||
void add(expr const & type, expr const & proof);
|
||||
|
||||
virtual optional<expr> get_proof(expr const & e) override;
|
||||
optional<expr> get_proof(expr const & e);
|
||||
bool inconsistent() const { return m_cc.inconsistent(); }
|
||||
optional<expr> get_inconsistency_proof() const { return m_cc.get_inconsistency_proof(); }
|
||||
optional<expr> get_eq_proof(expr const & lhs, expr const & rhs) const {
|
||||
|
|
|
|||
|
|
@ -478,7 +478,7 @@ void theory_ac::process() {
|
|||
|
||||
/* Propagate new equality to congruence closure module */
|
||||
if (!is_ac_app(lhs) && !is_ac_app(rhs) && m_cc.get_root(lhs) != m_cc.get_root(rhs)) {
|
||||
m_cc.push_new_eq(lhs, rhs, mark_cc_theory_proof(H));
|
||||
m_cc.push_eq(lhs, rhs, mark_cc_theory_proof(H));
|
||||
}
|
||||
|
||||
/* Orient */
|
||||
|
|
|
|||
|
|
@ -1,125 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include "library/util.h"
|
||||
#include "library/trace.h"
|
||||
#include "library/tactic/smt/unit_propagation.h"
|
||||
|
||||
namespace lean {
|
||||
static bool is_lemma(type_context & ctx, expr e) {
|
||||
if (!ctx.is_prop(e)) return false;
|
||||
bool arrow = false;
|
||||
while (is_arrow(e) && !is_not(e)) {
|
||||
arrow = true;
|
||||
if (!ctx.is_prop(binding_domain(e))) return false;
|
||||
e = binding_body(e);
|
||||
}
|
||||
return arrow || is_or(e);
|
||||
}
|
||||
|
||||
/** \brief e is a dependent lemma when
|
||||
- e is a proposition
|
||||
- e is of the form (Pi (x : A), B)
|
||||
- A is a proposition
|
||||
- B depends on x */
|
||||
static bool is_dep_lemma(type_context & ctx, expr const & e) {
|
||||
return
|
||||
is_pi(e) &&
|
||||
ctx.is_prop(e) &&
|
||||
ctx.is_prop(binding_domain(e)) &&
|
||||
!closed(binding_body(e));
|
||||
}
|
||||
|
||||
static bool is_fact(type_context & ctx, expr const & e) {
|
||||
return ctx.is_prop(e) && !is_lemma(ctx, e) && !is_dep_lemma(ctx, e);
|
||||
}
|
||||
|
||||
unit_propagation::unit_propagation(type_context & ctx, state & s, assignment & assignment):
|
||||
m_ctx(ctx), m_state(s), m_assignment(assignment) {}
|
||||
|
||||
static expr get_var(expr const & e) {
|
||||
expr arg;
|
||||
if (is_not(e, arg))
|
||||
return arg;
|
||||
else
|
||||
return e;
|
||||
}
|
||||
|
||||
void unit_propagation::visit_lemma(expr const & e) {
|
||||
lean_assert(is_lemma(ctx, e));
|
||||
expr it = e;
|
||||
unsigned i = 0;
|
||||
expr watches[2];
|
||||
|
||||
/* Traverse A_i */
|
||||
while (is_arrow(it) && !is_not(it) && i < 2) {
|
||||
expr const & p = binding_domain(it);
|
||||
switch (get_value(p)) {
|
||||
case l_true: break;
|
||||
case l_false: case l_undef:
|
||||
watches[i] = get_var(p);
|
||||
i++;
|
||||
break;
|
||||
}
|
||||
it = binding_body(it);
|
||||
}
|
||||
|
||||
/* Traverse B_j */
|
||||
bool done = false;
|
||||
while (!done && i < 2) {
|
||||
expr p, next_it;
|
||||
if (is_or(it, p, next_it)) {
|
||||
it = next_it;
|
||||
} else {
|
||||
p = it;
|
||||
done = true;
|
||||
}
|
||||
switch (get_value(p)) {
|
||||
case l_false: break;
|
||||
case l_true: case l_undef:
|
||||
watches[i] = get_var(p);
|
||||
i++;
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
if (i == 2) {
|
||||
m_state.m_facts_to_lemmas.insert(watches[0], e);
|
||||
m_state.m_facts_to_lemmas.insert(watches[1], e);
|
||||
return;
|
||||
}
|
||||
|
||||
if (i == 0) return;
|
||||
|
||||
/* TODO(Leo): */
|
||||
}
|
||||
|
||||
void unit_propagation::visit_dep_lemma(expr const & /* e */) {
|
||||
/* TODO(Leo): */
|
||||
}
|
||||
|
||||
void unit_propagation::propagate(expr const & e) {
|
||||
if (list<expr> const * lemmas = m_state.m_facts_to_lemmas.find(e)) {
|
||||
for (expr const & lemma : *lemmas)
|
||||
visit_lemma(lemma);
|
||||
}
|
||||
|
||||
if (list<expr> const * lemmas = m_state.m_facts_to_dep_lemmas.find(e)) {
|
||||
for (expr const & lemma : *lemmas)
|
||||
visit_dep_lemma(lemma);
|
||||
}
|
||||
}
|
||||
|
||||
void unit_propagation::assigned(expr const & e) {
|
||||
if (is_lemma(m_ctx, e) && m_assignment.get_value(e) == l_true) {
|
||||
visit_lemma(e);
|
||||
} else if (is_dep_lemma(m_ctx, e) && m_assignment.get_value(e) == l_true) {
|
||||
visit_dep_lemma(e);
|
||||
} else if (is_fact(m_ctx, e)) {
|
||||
propagate(e);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1,57 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include "util/rb_multi_map.h"
|
||||
#include "library/type_context.h"
|
||||
|
||||
namespace lean {
|
||||
/**
|
||||
The unit propagation module can handle lemmas of the form:
|
||||
|
||||
A_1 -> ... -> A_n -> B_1 \/ ... \/ B_m
|
||||
|
||||
and "propagates" if one of the following conditions hold:
|
||||
|
||||
- We have all A_i, and the negations of all but one B_j.
|
||||
- We have the negations of all B_j, and all but one A_i.
|
||||
|
||||
Each lemma watches two of its facts. */
|
||||
class unit_propagation {
|
||||
public:
|
||||
class state {
|
||||
friend class unit_propagation;
|
||||
rb_multi_map<expr, expr, expr_quick_cmp> m_facts_to_lemmas;
|
||||
rb_multi_map<expr, expr, expr_quick_cmp> m_facts_to_dep_lemmas;
|
||||
public:
|
||||
};
|
||||
|
||||
class assignment {
|
||||
public:
|
||||
virtual ~assignment() {}
|
||||
virtual lbool get_value(expr const & e) = 0;
|
||||
virtual optional<expr> get_proof(expr const & e) = 0;
|
||||
};
|
||||
|
||||
private:
|
||||
type_context & m_ctx;
|
||||
state & m_state;
|
||||
assignment & m_assignment;
|
||||
|
||||
lbool get_value(expr const & e) { return m_assignment.get_value(e); }
|
||||
optional<expr> get_proof(expr const & e) { return m_assignment.get_proof(e); }
|
||||
void visit_lemma(expr const & e);
|
||||
void visit_dep_lemma(expr const & e);
|
||||
void propagate(expr const & e);
|
||||
|
||||
public:
|
||||
unit_propagation(type_context & ctx, state & s, assignment & assignment);
|
||||
void assigned(expr const & e);
|
||||
};
|
||||
|
||||
typedef unit_propagation::state up_state;
|
||||
typedef unit_propagation::assignment up_assignment;
|
||||
}
|
||||
|
|
@ -1,13 +1,40 @@
|
|||
open smt_tactic
|
||||
|
||||
def ex1 (p q : Prop) : p → q → p :=
|
||||
example (p q : Prop) : p → q → p :=
|
||||
by using_smt $ return ()
|
||||
|
||||
def ex2 (p q : Prop) : ¬ p → q → ¬ p :=
|
||||
example (p q : Prop) : ¬ p → q → ¬ p :=
|
||||
by using_smt $ return ()
|
||||
|
||||
print ex1
|
||||
print ex2
|
||||
|
||||
example (p q : Prop) : p → (p ↔ q) → q :=
|
||||
by using_smt $ return ()
|
||||
|
||||
example (p q : Prop) : p → (p → q) → q :=
|
||||
by using_smt $ return ()
|
||||
|
||||
example (p q : Prop) : (p → q) → p → q :=
|
||||
by using_smt $ return ()
|
||||
|
||||
example (p q r : Prop) : (p → r → q) → r → p → q :=
|
||||
by using_smt $ return ()
|
||||
|
||||
example (p q r s t o : Prop) : (p ∨ t → o ∨ r → q ∧ s) → r → p → q :=
|
||||
by using_smt $ return ()
|
||||
|
||||
example (p q : Prop) (a b c : nat) : (p ∨ q → a = b ∨ a = c) → a ≠ b → p → c = a :=
|
||||
by using_smt $ return ()
|
||||
|
||||
example (p q : Prop) [decidable p] [decidable q] (a b c : nat) : (if p ∨ q then (a = b ∨ a = c) else (a = 0)) → p → a ≠ b → c = a :=
|
||||
by using_smt $ return ()
|
||||
|
||||
example (p q : Prop) : p → (p ↔ ¬q) → ¬q :=
|
||||
by using_smt $ return ()
|
||||
|
||||
example (p q r s : Prop) : (p ∨ q → not (r ∨ s)) → p → not r :=
|
||||
by using_smt $ return ()
|
||||
|
||||
example (p q r : Prop) (a b c : nat): (p → q ∧ r ∧ a = b + c) → p → (c + b = a ∧ r) :=
|
||||
by using_smt $ return ()
|
||||
|
||||
example (a b c d : nat) : b = d → c = d → (if a > 10 then b else c) = b :=
|
||||
by using_smt $ return ()
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue