From 39ec756331e8a4f81aa593711f9b990c2758e300 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 16 Nov 2015 16:07:00 -0800 Subject: [PATCH] feat(library/blast): add congruence closure skeleton --- src/library/blast/CMakeLists.txt | 2 +- src/library/blast/congruence_closure.cpp | 14 +++ src/library/blast/congruence_closure.h | 143 +++++++++++++++++++++++ 3 files changed, 158 insertions(+), 1 deletion(-) create mode 100644 src/library/blast/congruence_closure.cpp create mode 100644 src/library/blast/congruence_closure.h diff --git a/src/library/blast/CMakeLists.txt b/src/library/blast/CMakeLists.txt index 2f0cc3ae7..1c8b52ff8 100644 --- a/src/library/blast/CMakeLists.txt +++ b/src/library/blast/CMakeLists.txt @@ -2,4 +2,4 @@ add_library(blast OBJECT expr.cpp state.cpp blast.cpp blast_tactic.cpp init_module.cpp simplifier.cpp simple_actions.cpp intros_action.cpp proof_expr.cpp options.cpp choice_point.cpp simple_strategy.cpp backward_action.cpp util.cpp gexpr.cpp revert_action.cpp subst_action.cpp no_confusion_action.cpp - simplify_actions.cpp strategy.cpp recursor_action.cpp) + simplify_actions.cpp strategy.cpp recursor_action.cpp congruence_closure.cpp) diff --git a/src/library/blast/congruence_closure.cpp b/src/library/blast/congruence_closure.cpp new file mode 100644 index 000000000..e6eedcea8 --- /dev/null +++ b/src/library/blast/congruence_closure.cpp @@ -0,0 +1,14 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/blast/congruence_closure.h" + +namespace lean { +namespace blast { +void congruence_closure::display() const { + // TODO(Leo): +} +}} diff --git a/src/library/blast/congruence_closure.h b/src/library/blast/congruence_closure.h new file mode 100644 index 000000000..f941ff212 --- /dev/null +++ b/src/library/blast/congruence_closure.h @@ -0,0 +1,143 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "kernel/expr.h" +#include "library/expr_lt.h" +#include "library/blast/hypothesis.h" + +namespace lean { +namespace blast { +class congruence_closure { + /* + We maintain several equivalence relations. + Any relation tagged as [refl], [symm] and [trans] is handled by this module. + + We use a union-find based data-structure for storing the equivalence relations. + Each equivalence class contains one or more expressions. + We store the additional information for each expression in the 'entry' structure. + We use a mapping from (R, e) to 'entry', where 'R' is the equivalence relation name, and + 'e' is an expression. + + To find the equivalence class for expression 'e' with respect to equivalence relation 'R', + we create a key (R, e) and get the associated entry. The entry has a 'm_next' field, + that is the next element in the equivalence class containing 'e'. + + We used functional-datastructures because we must be able to create copies efficiently. + It will be part of the blast::state object. + + Remark: only a subset of use-defined congruence rules are considered. + We ignore user-defined congruence rules that have hypotheses and/or are contextual. + */ + + /* Equivalence class data associated with an expression 'e' */ + struct entry { + expr m_next; // next element in the equivalence class. + expr m_root; // root (aka canonical) representative of the equivalence class. + expr m_cg_root; // root of the congruence class, it is meaningless if 'e' is not an application. + // When 'e' was added to this equivalence class because of an equality (H : e ~ target), then we + // store 'target' at 'm_target', and 'H' at 'm_proof'. Both fields are none if 'e' == m_root + optional m_target; + optional 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 */ + struct eqc_key { + name m_R; + expr m_expr; + eqc_key() {} + eqc_key(name const & n, expr const & e):m_R(n), m_expr(e) {} + }; + + struct eqc_key_cmp { + int operator()(eqc_key const & k1, eqc_key const & k2) { + 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); + } + }; + + /* Key for the congruence set */ + struct congr_key { + name m_R; + expr m_expr; + /* 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. + }; + + struct congr_key_cmp { + int operator()(congr_key const & k1, congr_key const & k2); + }; + + typedef rb_tree expr_set; + typedef rb_map entries; + typedef rb_map parents; + typedef rb_tree congruences; + + entries m_entries; + parents m_parents; + congruences m_congruences; + +public: + /** \brief Register expression \c e in this data-structure. + It creates entries for each sub-expression in \c e. + It also updates the m_parents mapping. + + We ignore the following subterms of \c e. + 1- and, or and not-applications are not inserted into the data-structures, but + their arguments are visited. + 2- (Pi (x : A), B), the subterms A and B are not visited if B depends on x. + 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. */ + void internalize(expr const & e); + + /** \brief Given a hypothesis H, this method will do the following based on the type of H + 1- (H : a ~ b): merge equivalence classes of 'a' and 'b', and propagate congruences. + + 2- (H : not a ~ b): add the equivalence ((a ~ b) <-> false) + + 3- (H : P), if P is a proposition, add the equivalence (P <-> true) + + 4- (H : not P), add the equivalence (P <-> false) + + If H is none of the forms above, this method does nothing. */ + void add(hypothesis_idx hidx); + + /** \brief Return true if an inconsistency has been detected, i.e., true and false are in the same equivalence class */ + bool is_inconsistent() const; + /** \brief Return the proof of inconsistency */ + optional 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; + optional 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 get_uneqv_proof(name const & rel_name, 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; + + /** \brief dump for debugging purposes. */ + void display() const; +}; +}}