diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-31 17:22:04 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-31 17:22:04 -0500 |
commit | 6ecaa545fc11f35a0ae507c27cacebfd93df442f (patch) | |
tree | 2076ddfe7072c87961d72316ec67dc45da69135d /src/theory/quantifiers/alpha_equivalence.h | |
parent | 0b48be52459c358267ca19f4e134fe22b850f425 (diff) |
Refactor and document alpha equivalence. (#2402)
Diffstat (limited to 'src/theory/quantifiers/alpha_equivalence.h')
-rw-r--r-- | src/theory/quantifiers/alpha_equivalence.h | 94 |
1 files changed, 80 insertions, 14 deletions
diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h index 0e48bb349..4ab45b015 100644 --- a/src/theory/quantifiers/alpha_equivalence.h +++ b/src/theory/quantifiers/alpha_equivalence.h @@ -24,31 +24,97 @@ namespace CVC4 { namespace theory { namespace quantifiers { +/** + * This is a discrimination tree index for terms. It handles variadic + * operators by indexing based on operator arity, and flattens multiple + * occurrences of subterms. + * + * For example, the term + * +( f( x ), +( a, f(x), b ) ) + * is stored at: + * d_children[+][2].d_children[f][1]. + * d_children[x][0].d_children[+][3]. + * d_children[a][0].d_children[f(x)][0]. + * d_children[b][0] + * Notice that the second occurrence of f(x) is flattened. + */ class AlphaEquivalenceNode { public: - std::map< Node, std::map< int, AlphaEquivalenceNode > > d_children; - Node d_quant; - static Node registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ); + /** children of this node */ + std::map<Node, std::map<int, AlphaEquivalenceNode> > d_children; + /** the data at this node */ + Node d_quant; + /** Registers term q to this trie. The term t is the canonical form of q. */ + Node registerNode(Node q, Node t); }; +/** + * This trie stores a trie of the above form for each multi-set of types. For + * each term t registered to this node, we store t in the appropriate + * AlphaEquivalenceNode trie. For example, if t contains 2 free variables + * of type T1 and 3 free variables of type T2, then it is stored at + * d_children[T1][2].d_children[T2][3]. + */ class AlphaEquivalenceTypeNode { public: - std::map< TypeNode, std::map< int, AlphaEquivalenceTypeNode > > d_children; - AlphaEquivalenceNode d_data; - static Node registerNode( AlphaEquivalenceTypeNode* aetn, - QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index = 0 ); + /** children of this node */ + std::map<TypeNode, std::map<int, AlphaEquivalenceTypeNode> > d_children; + /** the database of terms at this node */ + AlphaEquivalenceNode d_data; + /** register node + * + * This registers term q to this trie. The term t is the canonical form of + * q, typs/typ_count represent a multi-set of types of free variables in t. + */ + Node registerNode(Node q, + Node t, + std::vector<TypeNode>& typs, + std::map<TypeNode, int>& typ_count); }; -class AlphaEquivalence { -private: - QuantifiersEngine* d_qe; - //per # of variables per type +/** + * Stores a database of quantified formulas, which computes alpha-equivalence. + */ +class AlphaEquivalenceDb +{ + public: + AlphaEquivalenceDb(TermCanonize* tc) : d_tc(tc) {} + /** adds quantified formula q to this database + * + * This function returns a quantified formula q' that is alpha-equivalent to + * q. If q' != q, then q' was previously added to this database via a call + * to addTerm. + */ + Node addTerm(Node q); + + private: + /** a trie per # of variables per type */ AlphaEquivalenceTypeNode d_ae_typ_trie; -public: - AlphaEquivalence( QuantifiersEngine* qe ) : d_qe( qe ){} + /** pointer to the term canonize utility */ + TermCanonize* d_tc; +}; + +/** + * A quantifiers module that computes reductions based on alpha-equivalence, + * using the above utilities. + */ +class AlphaEquivalence +{ + public: + AlphaEquivalence(QuantifiersEngine* qe); ~AlphaEquivalence(){} - /** reduce quantifier, return value (if non-null) is lemma justifying why q ia reducible. */ + /** reduce quantifier + * + * If non-null, its return value is lemma justifying why q is reducible. + * This is of the form ( q = q' ) where q' is a quantified formula that + * was previously registered to this class via a call to reduceQuantifier, + * and q and q' are alpha-equivalent. + */ Node reduceQuantifier( Node q ); + + private: + /** the database of quantified formulas registered to this class */ + AlphaEquivalenceDb d_aedb; }; } |