Refactor and document alpha equivalence. (#2402)

1 files changed, 48 insertions, 24 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;
+}