From: Andrew Reynolds Date: Fri, 31 Aug 2018 22:22:04 +0000 (-0500) Subject: Refactor and document alpha equivalence. (#2402) X-Git-Tag: cvc5-1.0.0~4693 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6ecaa545fc11f35a0ae507c27cacebfd93df442f;p=cvc5.git Refactor and document alpha equivalence. (#2402) --- diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index 0f9d1acb1..577b2c31f 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -29,7 +29,12 @@ struct sortTypeOrder { } }; -Node AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ) { +Node AlphaEquivalenceNode::registerNode(Node q, Node t) +{ + AlphaEquivalenceNode* aen = this; + std::vector tt; + std::vector arg_index; + tt.push_back(t); std::map< Node, bool > visited; while( !tt.empty() ){ if( tt.size()==arg_index.size()+1 ){ @@ -62,45 +67,38 @@ Node AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersE } } } - Node lem; Trace("aeq-debug") << std::endl; if( aen->d_quant.isNull() ){ aen->d_quant = q; - }else{ - if( q.getNumChildren()==2 ){ - //lemma ( q <=> d_quant ) - Trace("alpha-eq") << "Alpha equivalent : " << std::endl; - Trace("alpha-eq") << " " << q << std::endl; - Trace("alpha-eq") << " " << aen->d_quant << std::endl; - lem = q.eqNode( aen->d_quant ); - }else{ - //do not reduce annotated quantified formulas based on alpha equivalence - } } - return lem; + return aen->d_quant; } -Node AlphaEquivalenceTypeNode::registerNode( AlphaEquivalenceTypeNode* aetn, - QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index ){ - while( index<(int)typs.size() ){ +Node AlphaEquivalenceTypeNode::registerNode(Node q, + Node t, + std::vector& typs, + std::map& typ_count) +{ + AlphaEquivalenceTypeNode* aetn = this; + unsigned index = 0; + while (index < typs.size()) + { TypeNode curr = typs[index]; Assert( typ_count.find( curr )!=typ_count.end() ); Trace("aeq-debug") << "[" << curr << " " << typ_count[curr] << "] "; aetn = &(aetn->d_children[curr][typ_count[curr]]); index = index + 1; } - std::vector< Node > tt; - std::vector< int > arg_index; - tt.push_back( t ); Trace("aeq-debug") << " : "; - return AlphaEquivalenceNode::registerNode( &(aetn->d_data), qe, q, tt, arg_index ); + return aetn->d_data.registerNode(q, t); } -Node AlphaEquivalence::reduceQuantifier( Node q ) { +Node AlphaEquivalenceDb::addTerm(Node q) +{ Assert( q.getKind()==FORALL ); Trace("aeq") << "Alpha equivalence : register " << q << std::endl; //construct canonical quantified formula - Node t = d_qe->getTermCanonize()->getCanonicalTerm(q[1], true); + Node t = d_tc->getCanonicalTerm(q[1], true); Trace("aeq") << " canonical form: " << t << std::endl; //compute variable type counts std::map< TypeNode, int > typ_count; @@ -113,10 +111,36 @@ Node AlphaEquivalence::reduceQuantifier( Node q ) { } } sortTypeOrder sto; - sto.d_tu = d_qe->getTermCanonize(); + sto.d_tu = d_tc; std::sort( typs.begin(), typs.end(), sto ); Trace("aeq-debug") << " "; - Node ret = AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count ); + Node ret = d_ae_typ_trie.registerNode(q, t, typs, typ_count); Trace("aeq") << " ...result : " << ret << std::endl; return ret; } + +AlphaEquivalence::AlphaEquivalence(QuantifiersEngine* qe) + : d_aedb(qe->getTermCanonize()) +{ +} + +Node AlphaEquivalence::reduceQuantifier(Node q) +{ + Assert(q.getKind() == FORALL); + Trace("aeq") << "Alpha equivalence : register " << q << std::endl; + Node ret = d_aedb.addTerm(q); + Node lem; + if (ret != q) + { + // do not reduce annotated quantified formulas based on alpha equivalence + if (q.getNumChildren() == 2) + { + // lemma ( q <=> d_quant ) + Trace("alpha-eq") << "Alpha equivalent : " << std::endl; + Trace("alpha-eq") << " " << q << std::endl; + Trace("alpha-eq") << " " << ret << std::endl; + lem = q.eqNode(ret); + } + } + return lem; +} 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 > 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 > 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& typs, + std::map& 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; }; }