Fix bug 670. Minor.

6 files changed, 81 insertions, 48 deletions

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 14d966458..4f5b93b39 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -385,7 +385,7 @@ public:
            tn.isTuple() || tn.isRecord();
   }
 private:
-  static Node collectRef( Node n, std::vector< Node >& sk, std::map< Node, Node >& rf, std::vector< Node >& rf_pending ){
+  static Node collectRef( Node n, std::vector< Node >& sk, std::map< Node, Node >& rf, std::vector< Node >& rf_pending, std::vector< Node >& terms ){
     Assert( n.isConst() );
     TypeNode tn = n.getType();
     if( tn.isDatatype() ){
@@ -396,7 +396,7 @@ private:
         children.push_back( n.getOperator() );
         bool childChanged = false;
         for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          Node nc = collectRef( n[i], sk, rf, rf_pending );
+          Node nc = collectRef( n[i], sk, rf, rf_pending, terms );
           if( nc.isNull() ){
             return Node::null();
           }
@@ -415,6 +415,9 @@ private:
           Assert( rf_pending.back().isNull() );
         }
         rf_pending.pop_back();
+        if( std::find( terms.begin(), terms.end(), ret )==terms.end() ){
+          terms.push_back( ret );
+        }
         return ret;
       }else{
         const Integer& i = n.getConst<UninterpretedConstant>().getIndex();
@@ -441,18 +444,43 @@ public:
     std::map< Node, Node > rf;
     std::vector< Node > sk;
     std::vector< Node > rf_pending;
-    Node s = collectRef( n, sk, rf, rf_pending );
+    std::vector< Node > terms;
+    Node s = collectRef( n, sk, rf, rf_pending, terms );
     if( !s.isNull() ){
       Trace("dt-nconst") << "...symbolic normalized is : " << s << std::endl;
       for( std::map< Node, Node >::iterator it = rf.begin(); it != rf.end(); ++it ){
         Trace("dt-nconst") << "  " << it->first << " = " << it->second << std::endl;
       }
+      Trace("dt-nconst") << "  " << terms.size() << " total subterms." << std::endl;
+      //now run bisimulations on all terms
+
       return n;
     }else{
       Trace("dt-nconst") << "...invalid." << std::endl;
       return Node::null();
     }
   }
+  //normalize constant : apply to top-level codatatype constants
+  static Node normalizeConstant( Node n ){
+    Assert( n.getType().isDatatype() );
+    const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype();
+    if( dt.isCodatatype() ){
+      return normalizeMuConstant( n );
+    }else{
+      std::vector< Node > children;
+      bool childrenChanged = false;
+      for( unsigned i = 0; i<n.getNumChildren(); i++ ){
+        Node nc = normalizeConstant( n[i] );
+        children.push_back( nc );
+        childrenChanged = childrenChanged || nc!=n[i];
+      }
+      if( childrenChanged ){
+        return NodeManager::currentNM()->mkNode( n.getKind(), children );
+      }else{
+        return n;
+      }
+    }
+  }
 };/* class DatatypesRewriter */
 
 }/* CVC4::theory::datatypes namespace */
diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp
index a4af183c5..0bcc0168e 100755
--- a/src/theory/datatypes/type_enumerator.cpp
+++ b/src/theory/datatypes/type_enumerator.cpp
@@ -100,7 +100,12 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
    Debug("dt-enum-debug") << "Get current term at " << index << " " << d_type << std::endl;
    Node ret;
    if( index<d_has_debruijn ){
-     ret = NodeManager::currentNM()->mkConst(UninterpretedConstant(d_type.toType(), d_size_limit));
+     if( d_child_enum ){
+       ret = NodeManager::currentNM()->mkConst(UninterpretedConstant(d_type.toType(), d_size_limit));
+     }else{
+       //no top-level variables
+       return Node::null();
+     }
    }else{
      Debug("dt-enum-debug") << "Look at constructor " << (index - d_has_debruijn) << std::endl;
      DatatypeConstructor ctor = d_datatype[index - d_has_debruijn];
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 );