Fix bug 670. Minor.

4 files changed, 44 insertions, 44 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;
 }
diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h
index fa2109ccc..99517fd2a 100755
--- a/src/theory/quantifiers/alpha_equivalence.h
+++ b/src/theory/quantifiers/alpha_equivalence.h
@@ -28,14 +28,15 @@ class AlphaEquivalenceNode {
 public:
   std::map< Node, std::map< int, AlphaEquivalenceNode > > d_children;
   Node d_quant;
-  bool registerNode( QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index );
+  static bool registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index );
 };
 
 class AlphaEquivalenceTypeNode {
 public:
   std::map< TypeNode, std::map< int, AlphaEquivalenceTypeNode > > d_children;
   AlphaEquivalenceNode d_data;
-  bool registerNode( QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index = 0 );
+  static bool registerNode( AlphaEquivalenceTypeNode* aetn,
+                            QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index = 0 );
 };
 
 class AlphaEquivalence {
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 791ad6e90..e5e484625 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -207,13 +207,13 @@ relevant \n\
 static const std::string iteLiftQuantHelp = "\
 Modes for term database, supported by --ite-lift-quant:\n\
 \n\
-all  \n\
+none  \n\
 + Do not lift if-then-else in quantified formulas.\n\
 \n\
 simple  \n\
 + Lift if-then-else in quantified formulas if results in smaller term size.\n\
 \n\
-none \n\
+all \n\
 + Lift if-then-else in quantified formulas. \n\
 \n\
 ";
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 0f477b828..828099984 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -62,7 +62,6 @@ private:
     COMPUTE_VAR_ELIMINATION,
     //COMPUTE_FLATTEN_ARGS_UF,
     //COMPUTE_CNF,
-    COMPUTE_SPLIT,
     COMPUTE_LAST
   };
   static Node computeOperation( Node f, bool isNested, int computeOption );