Fix bug 670. Minor.

1 files changed, 39 insertions, 39 deletions

diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index e4dcccdff..84bf2ec14 100755
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -29,54 +29,54 @@ struct sortTypeOrder {
   }
 };
 
-bool AlphaEquivalenceNode::registerNode( QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ) {
-  if( tt.size()==arg_index.size()+1 ){
-    Node t = tt.back();
-    Node op = t.hasOperator() ? t.getOperator() : t;
-    arg_index.push_back( 0 );
-    Trace("aeq-debug") << op << " ";
-    return d_children[op][t.getNumChildren()].registerNode( qe, q, tt, arg_index );
-  }else if( tt.empty() ){
-    //we are finished
-    Trace("aeq-debug") << std::endl;
-    if( d_quant.isNull() ){
-      d_quant = q;
-      return true;
+bool AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ) {
+  while( !tt.empty() ){
+    if( tt.size()==arg_index.size()+1 ){
+      Node t = tt.back();
+      Node op = t.hasOperator() ? t.getOperator() : t;
+      arg_index.push_back( 0 );
+      Trace("aeq-debug") << op << " ";
+      aen = &(aen->d_children[op][t.getNumChildren()]);
     }else{
-      //lemma ( q <=> d_quant )
-      Trace("alpha-eq") << "Alpha equivalent : " << std::endl;
-      Trace("alpha-eq") << "  " << q << std::endl;
-      Trace("alpha-eq") << "  " << d_quant << std::endl;
-      qe->getOutputChannel().lemma( q.iffNode( d_quant ) );
-      return false;
+      Node t = tt.back();
+      int i = arg_index.back();
+      if( i==(int)t.getNumChildren() ){
+        tt.pop_back();
+        arg_index.pop_back();
+      }else{
+        tt.push_back( t[i] );
+        arg_index[arg_index.size()-1]++;
+      }
     }
+  }
+  Trace("aeq-debug") << std::endl;
+  if( aen->d_quant.isNull() ){
+    aen->d_quant = q;
+    return true;
   }else{
-    Node t = tt.back();
-    int i = arg_index.back();
-    if( i==(int)t.getNumChildren() ){
-      tt.pop_back();
-      arg_index.pop_back();
-    }else{
-      tt.push_back( t[i] );
-      arg_index[arg_index.size()-1]++;
-    }
-    return registerNode( qe, q, tt, arg_index );
+    //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;
+    qe->getOutputChannel().lemma( q.iffNode( aen->d_quant ) );
+    return false;
   }
 }
 
-bool AlphaEquivalenceTypeNode::registerNode( QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index ){
-  if( index==(int)typs.size() ){
-    std::vector< Node > tt;
-    std::vector< int > arg_index;
-    tt.push_back( t );
-    Trace("aeq-debug") << " : ";
-    return d_data.registerNode( qe, q, tt, arg_index );
-  }else{
+bool 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() ){
     TypeNode curr = typs[index];
     Assert( typ_count.find( curr )!=typ_count.end() );
     Trace("aeq-debug") << "[" << curr << " " << typ_count[curr] << "] ";
-    return d_children[curr][typ_count[curr]].registerNode( qe, q, t, typs, typ_count, index+1 );
+    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 );
 }
 
 bool AlphaEquivalence::registerQuantifier( Node q ) {
@@ -99,7 +99,7 @@ bool AlphaEquivalence::registerQuantifier( Node q ) {
   sto.d_tdb = d_qe->getTermDatabase();
   std::sort( typs.begin(), typs.end(), sto );
   Trace("aeq-debug") << "  ";
-  bool ret = d_ae_typ_trie.registerNode( d_qe, q, t, typs, typ_count );
+  bool ret = AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count );
   Trace("aeq") << "  ...result : " << ret << std::endl;
   return ret;
 }