Refactor and document alpha equivalence. (#2402)

2 files changed, 128 insertions, 38 deletions

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<Node> tt;
+  std::vector<int> 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<TypeNode>& typs,
+                                            std::map<TypeNode, int>& 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<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;
 };
 
 }