From 651e3834baaffb96f384e92246bb4879b654e198 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 24 Nov 2015 18:32:20 -0800 Subject: [PATCH] feat(library/blast/congruence_closure): allow meta-variables in the congruence closure module after partitions have been frozen --- src/library/blast/assert_cc_action.cpp | 2 ++ src/library/blast/congruence_closure.cpp | 6 ++++-- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/library/blast/assert_cc_action.cpp b/src/library/blast/assert_cc_action.cpp index 47f78d8f3c..a21c0e7dfd 100644 --- a/src/library/blast/assert_cc_action.cpp +++ b/src/library/blast/assert_cc_action.cpp @@ -16,6 +16,8 @@ action_result assert_cc_action(hypothesis_idx hidx) { if (!get_config().m_cc) return action_result::failed(); congruence_closure & cc = get_cc(); + if (has_expr_metavar(curr_state().get_hypothesis_decl(hidx).get_type())) + return action_result::failed(); cc.add(hidx); // cc.display(); if (cc.is_inconsistent()) { diff --git a/src/library/blast/congruence_closure.cpp b/src/library/blast/congruence_closure.cpp index 31904c71a8..12dea69ab0 100644 --- a/src/library/blast/congruence_closure.cpp +++ b/src/library/blast/congruence_closure.cpp @@ -566,17 +566,19 @@ static bool is_logical_app(expr const & n) { void congruence_closure::internalize_core(name const & R, expr const & e, bool toplevel, bool to_propagate) { lean_assert(closed(e)); - if (has_expr_metavar(e)) + // we allow metavariables after partitions have been frozen + if (has_expr_metavar(e) && !m_froze_partitions) return; if (m_entries.find(eqc_key(R, e))) return; // e has already been internalized update_non_eq_relations(R); switch (e.kind()) { - case expr_kind::Var: case expr_kind::Meta: + case expr_kind::Var: lean_unreachable(); case expr_kind::Sort: return; case expr_kind::Constant: case expr_kind::Local: + case expr_kind::Meta: mk_entry_core(R, e, to_propagate, false); return; case expr_kind::Lambda: