lean2/src/library/blast/congruence_closure.h

/*
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 {
struct ext_congr_lemma;
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<expr> m_target;
        optional<expr> m_proof;
        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_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.
        // The basic idea is to introduce a counter gmt that records the number of heuristic instantiation that have
        // occurred in the current branch. It is incremented after each round of heuristic instantiation.
        // The field m_mt records the last time any proper descendant of of thie entry was involved in a merge.
    };

    /* 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) const {
            int r = quick_cmp(k1.m_R, k2.m_R);
            if (r != 0) return r;
            else return expr_quick_cmp()(k1.m_expr, k2.m_expr);
        }
    };

    /* Key for the congruence set */
    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:1; // true if m_expr is another symmetric relation.
        congr_key() { m_eq = 0; m_iff = 0; m_symm_rel = 0; }
    };

    struct congr_key_cmp {
        int operator()(congr_key const & k1, congr_key const & k2) const;
    };

    typedef rb_tree<expr, expr_quick_cmp>                    expr_set;
    typedef rb_map<eqc_key, entry, eqc_key_cmp>              entries;
    typedef eqc_key     child_key;
    typedef eqc_key_cmp child_key_cmp;
    typedef eqc_key     parent_occ;
    typedef eqc_key_cmp parent_occ_cmp;
    typedef rb_tree<parent_occ, parent_occ_cmp>              parent_occ_set;
    typedef rb_map<child_key, parent_occ_set, child_key_cmp> parents;
    typedef rb_tree<congr_key, congr_key_cmp>                congruences;

    entries     m_entries;
    parents     m_parents;
    congruences m_congruences;
    list<name>  m_non_eq_relations;
    /** The congruence closure module has a mode where the root of
        each equivalence class is marked as an interpreted/abstract
        value. Moreover, in this mode proof production is disabled.
        This capability is useful for heuristic instantiation. */
    short       m_froze_partitions{false};
    short       m_inconsistent{false};
    unsigned    m_gmt{0};
    void update_non_eq_relations(name const & R);

    void register_to_propagate(expr const & e);
    void internalize_core(name const & R, expr const & e, bool toplevel, bool to_propagate);
    void process_todo();

    int compare_symm(name const & R, expr lhs1, expr rhs1, expr lhs2, expr rhs2) const;
    int compare_root(name const & R, expr e1, expr e2) const;
    unsigned symm_hash(name const & R, expr const & lhs, expr const & rhs) const;
    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(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);
    void invert_trans(name const & R, expr const & e, optional<expr> new_target, optional<expr> new_proof);
    void invert_trans(name const & R, expr const & e);
    void remove_parents(name const & R, expr const & e);
    void reinsert_parents(name const & R, expr const & e);
    void update_mt(name const & R, expr const & e);
    expr mk_iff_false_intro(expr const & proof);
    expr mk_iff_true_intro(expr const & proof);
    void add_eqv_step(name const & R, expr e1, expr e2, expr const & H);
    void add_eqv_core(name const & R, expr const & lhs, expr const & rhs, expr const & H);

    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;
    expr mk_proof(name const & R, expr const & lhs, expr const & rhs, expr const & H) const;

    void display_eqc(name const & R, expr const & e) const;
public:
    void initialize();

    /** \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.
       6- Sorts (Type and Prop). */
    void internalize(name const & R, expr const & e, bool toplevel = false);
    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);
    void add(expr const & type, expr const & proof);
    /** \brief Similar to \c add but asserts the given type without proof
        \pre It can only be used after \c freeze_partitions has been invoked (i.e., proof extraction has been disabled). */
    void assume(expr const & type);

    /** \brief Assert the equivalence (R a b) with proof H. */
    void add_eqv(name const & R, expr const & a, expr const & b, expr const & H);

    /** \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<expr> get_inconsistency_proof() const;

    /** \brief Return true iff 'e1' and 'e2' are in the same equivalence class for relation \c R. */
    bool is_eqv(name const & R, expr const & e1, expr const & e2) const;
    optional<expr> get_eqv_proof(name const & R, 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 & R, expr const & e1, expr const & e2) const;
    optional<expr> get_uneqv_proof(name const & R, expr const & e1, expr const & e2) const;

    /** \brief Return true iff \c e has been proved by this module. That is, the proposition \c e is inhabited */
    bool proved(expr const & e) const;
    optional<expr> get_proof(expr const & e) const;

    /** \brief Return true iff \c (not e) has been proved by this module. That is, the proposition \c (not e) is inhabited */
    bool disproved(expr const & e) const;
    optional<expr> get_disproof(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 Mark the root of each equivalence class as an "abstract value"
        After this method is invoked, proof production is disabled. Moreover,
        merging two different partitions will trigger an inconsistency. */
    void freeze_partitions();

    void inc_gmt() { m_gmt++; }

    /** \brief dump for debugging purposes. */
    void display() const;
    void display_eqcs() const;
    void display_parents() const;
    bool check_eqc(name const & R, expr const & e) 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();
};

/** \brief Return the congruence closure object associated with the current state */
congruence_closure & get_cc();

void initialize_congruence_closure();
void finalize_congruence_closure();
}}