Add options --qcf-all-conflict, --ite-dtt-split-quant, refactor --ite-lift-quant. Minor bug fixes for internalReps, alpha equivalence. Update casc 25 FOF script.

7 files changed, 232 insertions, 55 deletions

diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index 47cb62715..97ad3e8ea 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -143,6 +143,14 @@ typedef enum {
   TERM_DB_RELEVANT,
 } TermDbMode;
 
+typedef enum {
+  /** do not lift ITEs in quantified formulas */
+  ITE_LIFT_QUANT_MODE_NONE,
+  /** only lift ITEs in quantified formulas if reduces the term size */
+  ITE_LIFT_QUANT_MODE_SIMPLE,
+  /** lift ITEs  */
+  ITE_LIFT_QUANT_MODE_ALL,
+} IteLiftQuantMode;
 
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index e34465d9b..231392a9a 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -19,7 +19,7 @@ option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write
  disable miniscope quantifiers for ground subformulas
 # Whether to prenex (nested universal) quantifiers
 option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToPrenexQuantMode :handler-include "theory/quantifiers/options_handlers.h"
- disable prenexing of quantified formulas
+ prenex mode for quantified formulas
 # Whether to variable-eliminate quantifiers.
 # For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to
 #   forall y. P( c, y )
@@ -27,13 +27,16 @@ option varElimQuant --var-elim-quant bool :default true
  disable simple variable elimination for quantified formulas
 option dtVarExpandQuant --dt-var-exp-quant bool :default true
  expand datatype variables bound to one constructor in quantifiers
+#ite lift mode for quantified formulas
+option iteLiftQuant --ite-lift-quant=MODE CVC4::theory::quantifiers::IteLiftQuantMode :default CVC4::theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToIteLiftQuantMode :handler-include "theory/quantifiers/options_handlers.h"
+ ite lifting mode for quantified formulas
 option iteCondVarSplitQuant --ite-cond-var-split-quant bool :default true
  split variables occurring as conditions of ITE in quantifiers
-option simpleIteLiftQuant --ite-lift-quant bool :default true
- disable simple ite lifting for quantified formulas
+option iteDtTesterSplitQuant --ite-dtt-split-quant bool :default false
+ split ites with dt testers as conditions
 # Whether to CNF quantifier bodies
-option cnfQuant --cnf-quant bool :default false
- apply CNF conversion to quantified formulas
+# option cnfQuant --cnf-quant bool :default false
+#  apply CNF conversion to quantified formulas
 # Whether to NNF quantifier bodies
 option nnfQuant --nnf-quant bool :default true
  apply NNF conversion to quantified formulas
@@ -159,6 +162,8 @@ option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :
  when to invoke conflict find mechanism for quantifiers
 option qcfTConstraint --qcf-tconstraint bool :read-write :default false
  enable entailment checks for t-constraints in qcf algorithm
+option qcfAllConflict --qcf-all-conflict bool :read-write :default false
+ add all available conflicting instances during conflict-based instantiation
 
 option instNoEntail --inst-no-entail bool :read-write :default true
  do not consider instances of quantified formulas that are currently entailed
@@ -191,7 +196,7 @@ option conjectureFilterCanonical --conjecture-filter-canonical bool :read-write
  filter based on canonicity
 option conjectureFilterModel --conjecture-filter-model bool :read-write :default true
  filter based on model
-option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 0
+option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 50
  number of ground terms to generate for model filtering
 option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false
  more aggressive merging for universal equality engine, introduces terms
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 9fb5dd69d..c518813a0 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -204,6 +204,19 @@ relevant \n\
 + Quantifiers module considers only ground terms connected to current assertions. \n\
 \n\
 ";
+static const std::string iteLiftQuantHelp = "\
+Modes for term database, supported by --ite-lift-quant:\n\
+\n\
+all  \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\
++ Lift if-then-else in quantified formulas. \n\
+\n\
+";
 
 inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
   if(optarg == "pre-full") {
@@ -414,6 +427,22 @@ inline TermDbMode stringToTermDbMode(std::string option, std::string optarg, Smt
   }
 }
 
+inline IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg == "all" ) {
+    return ITE_LIFT_QUANT_MODE_ALL;
+  } else if(optarg == "simple") {
+    return ITE_LIFT_QUANT_MODE_SIMPLE;
+  } else if(optarg == "none") {
+    return ITE_LIFT_QUANT_MODE_NONE;
+  } else if(optarg ==  "help") {
+    puts(iteLiftQuantHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --ite-lift-quant: `") +
+                          optarg + "'.  Try --ite-lift-quant help.");
+  }
+}
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 18bffe908..47c2e1c5b 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1971,6 +1971,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
         Trace("qcf-debug") << std::endl;
       }
       short end_e = getMaxQcfEffort();
+      bool isConflict = false;
       for( short e = effort_conflict; e<=end_e; e++ ){
         d_effort = e;
         Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl;
@@ -2014,8 +2015,12 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
                       ++addedLemmas;
                       if( e==effort_conflict ){
                         d_quant_order.insert( d_quant_order.begin(), q );
-                        d_conflict.set( true );
                         ++(d_statistics.d_conflict_inst);
+                        if( options::qcfAllConflict() ){
+                          isConflict = true;
+                        }else{
+                          d_conflict.set( true );
+                        }
                         break;
                       }else if( e==effort_prop_eq ){
                         ++(d_statistics.d_prop_inst);
@@ -2044,6 +2049,9 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
           break;
         }
       }
+      if( isConflict ){
+        d_conflict.set( true );
+      }
       if( Trace.isOn("qcf-engine") ){
         double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
         Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet);
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 0afdece82..07aa89ece 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -340,64 +340,141 @@ Node QuantifiersRewriter::computeNNF( Node body ){
   }
 }
 
+
+void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, 
+                                                   std::vector< Node >& conj ){
+  if( n.getKind()==ITE && n[0].getKind()==APPLY_TESTER && n[1].getType().isBoolean() ){
+  Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl;
+    Node x = n[0][0];
+    std::map< Node, Node >::iterator itp = pcons.find( x );
+    if( itp!=pcons.end() ){
+      Trace("quantifiers-rewrite-ite-debug") << "...condition already set " << itp->second << std::endl;
+      computeDtTesterIteSplit( n[ itp->second==n[0] ? 1 : 2 ], pcons, ncons, conj );
+    }else{
+      Expr testerExpr = n[0].getOperator().toExpr();
+      int index = Datatype::indexOf( testerExpr );
+      std::map< int, Node >::iterator itn = ncons[x].find( index );
+      if( itn!=ncons[x].end() ){
+        Trace("quantifiers-rewrite-ite-debug") << "...condition negated " << itn->second << std::endl;
+        computeDtTesterIteSplit( n[ 2 ], pcons, ncons, conj );
+      }else{
+        for( unsigned i=0; i<2; i++ ){
+          if( i==0 ){
+            pcons[x] = n[0];
+          }else{
+            pcons.erase( x );
+            ncons[x][index] = n[0].negate();
+          }
+          computeDtTesterIteSplit( n[i+1], pcons, ncons, conj );
+        }
+        ncons[x].erase( index );
+      }
+    }
+  }else{
+    Trace("quantifiers-rewrite-ite-debug") << "Return value : " << n << std::endl;
+    std::vector< Node > children;
+    children.push_back( n );
+    std::vector< Node > vars;
+    //add all positive testers 
+    for( std::map< Node, Node >::iterator it = pcons.begin(); it != pcons.end(); ++it ){
+      children.push_back( it->second.negate() );
+      vars.push_back( it->first );
+    }
+    //add all negative testers
+    for( std::map< Node, std::map< int, Node > >::iterator it = ncons.begin(); it != ncons.end(); ++it ){
+      Node x = it->first;
+      //only if we haven't settled on a positive tester
+      if( std::find( vars.begin(), vars.end(), x )==vars.end() ){
+        //check if we have exhausted all options but one
+        const Datatype& dt = DatatypeType(x.getType().toType()).getDatatype();
+        std::vector< Node > nchildren;
+        int pos_cons = -1;
+        for( int i=0; i<(int)dt.getNumConstructors(); i++ ){
+          std::map< int, Node >::iterator itt = it->second.find( i );
+          if( itt==it->second.end() ){
+            pos_cons = pos_cons==-1 ? i : -2;
+          }else{
+            nchildren.push_back( itt->second.negate() );
+          }
+        }
+        if( pos_cons>=0 ){
+          const DatatypeConstructor& c = dt[pos_cons];
+          Expr tester = c.getTester();
+          children.push_back( NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), x ).negate() );
+        }else{
+          children.insert( children.end(), nchildren.begin(), nchildren.end() );
+        }
+      }
+    }
+    //make condition/output pair
+    Node c = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children );
+    conj.push_back( c );
+  }
+}
+
 Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol ) {
   if( body.getType().isBoolean() ){
-    if( body.getKind()==EQUAL && options::simpleIteLiftQuant() ){
+    if( body.getKind()==EQUAL && options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE ){
       for( size_t i=0; i<2; i++ ){
         if( body[i].getKind()==ITE ){
           Node no = i==0 ? body[1] : body[0];
-          bool doRewrite = false;
-          std::vector< Node > children;
-          children.push_back( body[i][0] );
-          for( size_t j=1; j<=2; j++ ){
-            //check if it rewrites to a constant
-            Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, body[i][j] );
-            nn = Rewriter::rewrite( nn );
-            children.push_back( nn );
-            if( nn.isConst() ){
-              doRewrite = true;
+          if( no.getKind()!=ITE ){
+            bool doRewrite = options::iteLiftQuant()==ITE_LIFT_QUANT_MODE_ALL;
+            std::vector< Node > children;
+            children.push_back( body[i][0] );
+            for( size_t j=1; j<=2; j++ ){
+              //check if it rewrites to a constant
+              Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, body[i][j] );
+              nn = Rewriter::rewrite( nn );
+              children.push_back( nn );
+              if( nn.isConst() ){
+                doRewrite = true;
+              }
+            }
+            if( doRewrite ){
+              return NodeManager::currentNM()->mkNode( ITE, children );
             }
-          }
-          if( doRewrite ){
-            return NodeManager::currentNM()->mkNode( ITE, children );
           }
         }
       }
-    }else if( body.getKind()==ITE && hasPol && options::iteCondVarSplitQuant() ){
-      for( unsigned r=0; r<2; r++ ){
-        //check if there is a variable elimination
-        Node b = r==0 ? body[0] : body[0].negate();
-        QuantPhaseReq qpr( b );
-        std::vector< Node > vars;
-        std::vector< Node > subs;
-        Trace("ite-var-split-quant") << "phase req " << body[0] << " #: " << qpr.d_phase_reqs.size() << std::endl;
-        for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
-          Trace("ite-var-split-quant") << "phase req " << it->first << " -> " << it->second << std::endl;
-          if( it->second ){
-            if( it->first.getKind()==EQUAL ){
-              for( unsigned i=0; i<2; i++ ){
-                if( it->first[i].getKind()==BOUND_VARIABLE ){
-                  unsigned j = i==0 ? 1 : 0;
-                  if( !hasArg1( it->first[i], it->first[j] ) ){
-                    vars.push_back( it->first[i] );
-                    subs.push_back( it->first[j] );
-                    break;
+    }else if( body.getKind()==ITE && hasPol ){
+      if( options::iteCondVarSplitQuant() ){
+        Trace("quantifiers-rewrite-ite-debug") << "Conditional var eq split " << body << std::endl;
+        for( unsigned r=0; r<2; r++ ){
+          //check if there is a variable elimination
+          Node b = r==0 ? body[0] : body[0].negate();
+          QuantPhaseReq qpr( b );
+          std::vector< Node > vars;
+          std::vector< Node > subs;
+          Trace("quantifiers-rewrite-ite-debug") << "phase req " << body[0] << " #: " << qpr.d_phase_reqs.size() << std::endl;
+          for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
+            Trace("quantifiers-rewrite-ite-debug") << "phase req " << it->first << " -> " << it->second << std::endl;
+            if( it->second ){
+              if( it->first.getKind()==EQUAL ){
+                for( unsigned i=0; i<2; i++ ){
+                  if( it->first[i].getKind()==BOUND_VARIABLE ){
+                    unsigned j = i==0 ? 1 : 0;
+                    if( !hasArg1( it->first[i], it->first[j] ) ){
+                      vars.push_back( it->first[i] );
+                      subs.push_back( it->first[j] );
+                      break;
+                    }
                   }
                 }
               }
             }
           }
-        }
-        if( !vars.empty() ){
-          //bool cpol = (r==1);
-          Node pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] );
-          //pos = pos.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
-          //pos = Rewriter::rewrite( pos );
-          Node neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] );
-          //Trace("ite-var-split-quant") << "Split ITE " << body << " into : " << std::endl;
-          //Trace("ite-var-split-quant") << "   " << pos << std::endl;
-          //Trace("ite-var-split-quant") << "   " << neg << std::endl;
-          return NodeManager::currentNM()->mkNode( AND, pos, neg );
+          if( !vars.empty() ){
+            //bool cpol = (r==1);
+            Node pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] );
+            //pos = pos.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+            //pos = Rewriter::rewrite( pos );
+            Node neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] );
+            Trace("quantifiers-rewrite-ite") << "*** Split ITE (conditional variable eq) " << body << " into : " << std::endl;
+            Trace("quantifiers-rewrite-ite") << "   " << pos << std::endl;
+            Trace("quantifiers-rewrite-ite") << "   " << neg << std::endl;
+            return NodeManager::currentNM()->mkNode( AND, pos, neg );
+          }
         }
       }
     }
@@ -420,6 +497,26 @@ Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol )
   return body;
 }
 
+Node QuantifiersRewriter::computeProcessIte2( Node body ){
+  if( body.getKind()==ITE ){
+    if( options::iteDtTesterSplitQuant() ){
+      Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body << std::endl;
+      std::map< Node, Node > pcons;
+      std::map< Node, std::map< int, Node > > ncons;
+      std::vector< Node > conj;
+      computeDtTesterIteSplit( body, pcons, ncons, conj );
+      Assert( !conj.empty() );
+      if( conj.size()>1 ){
+        Trace("quantifiers-rewrite-ite") << "*** Split ITE (datatype tester) " << body << " into : " << std::endl;
+        for( unsigned i=0; i<conj.size(); i++ ){
+          Trace("quantifiers-rewrite-ite") << "   " << conj[i] << std::endl;
+        }
+        return NodeManager::currentNM()->mkNode( AND, conj );
+      }
+    }
+  }
+  return body;
+}
 
 
 Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){
@@ -1002,7 +1099,9 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption
   }else if( computeOption==COMPUTE_NNF ){
     return options::nnfQuant();
   }else if( computeOption==COMPUTE_PROCESS_ITE ){
-    return options::iteCondVarSplitQuant() || options::simpleIteLiftQuant();
+    return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant();
+  }else if( computeOption==COMPUTE_PROCESS_ITE_2 ){
+    return options::iteDtTesterSplitQuant();
   }else if( computeOption==COMPUTE_PRENEX ){
     return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant();
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
@@ -1041,6 +1140,8 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp
       n = computeNNF( n );
     }else if( computeOption==COMPUTE_PROCESS_ITE ){
       n = computeProcessIte( n, true, true );
+    }else if( computeOption==COMPUTE_PROCESS_ITE_2 ){
+      n = computeProcessIte2( n );
     }else if( computeOption==COMPUTE_PRENEX ){
       n = computePrenex( n, args, true );
     }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 838eff57b..201a03737 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -40,12 +40,14 @@ private:
   static bool hasArg( std::vector< Node >& args, Node n );
   static bool hasArg1( Node a, Node n );
   static Node computeClause( Node n );
+  static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj );
 private:
   static Node computeElimSymbols( Node body );
   static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl );
   static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body );
   static Node computeNNF( Node body );
   static Node computeProcessIte( Node body, bool hasPol, bool pol );
+  static Node computeProcessIte2( Node body );
   static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl );
   static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred );
   static Node computePrenex( Node body, std::vector< Node >& args, bool pol );
@@ -57,6 +59,7 @@ private:
     COMPUTE_AGGRESSIVE_MINISCOPING,
     COMPUTE_NNF,
     COMPUTE_PROCESS_ITE,
+    COMPUTE_PROCESS_ITE_2,
     COMPUTE_PRENEX,
     COMPUTE_VAR_ELIMINATION,
     //COMPUTE_FLATTEN_ARGS_UF,
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 84cb63617..8c99881d6 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1189,7 +1189,7 @@ bool TermDb::getTermOrder( Node a, Node b ) {
     Trace("aeq-debug2") << a << "...op..." << aop << std::endl;
     Trace("aeq-debug2") << b << "...op..." << bop << std::endl;
     if( aop==bop ){
-      if( aop.getNumChildren()==bop.getNumChildren() ){
+      if( a.getNumChildren()==b.getNumChildren() ){
         for( unsigned i=0; i<a.getNumChildren(); i++ ){
           if( a[i]!=b[i] ){
             //first distinct child determines the ordering
@@ -1229,7 +1229,19 @@ Node TermDb::getCanonicalFreeVar( TypeNode tn, unsigned i ) {
 
 struct sortTermOrder {
   TermDb* d_tdb;
+  //std::map< Node, std::map< Node, bool > > d_cache;
   bool operator() (Node i, Node j) {
+    /*
+    //must consult cache since term order is partial?
+    std::map< Node, bool >::iterator it = d_cache[j].find( i );
+    if( it!=d_cache[j].end() && it->second ){
+      return false;
+    }else{
+      bool ret = d_tdb->getTermOrder( i, j );
+      d_cache[i][j] = ret;
+      return ret;
+    }
+    */
     return d_tdb->getTermOrder( i, j );
   }
 };
@@ -1238,6 +1250,7 @@ struct sortTermOrder {
 //  - orders variables left to right
 //  - if apply_torder, then sort direct subterms of commutative operators
 Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder ) {
+  Trace("canon-term-debug") << "Get canonical term for " << n << std::endl;
   if( n.getKind()==BOUND_VARIABLE ){
     std::map< TNode, TNode >::iterator it = subs.find( n );
     if( it==subs.end() ){
@@ -1246,31 +1259,41 @@ Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_coun
       unsigned vn = var_count[tn];
       var_count[tn]++;
       subs[n] = getCanonicalFreeVar( tn, vn );
+      Trace("canon-term-debug") << "...allocate variable." << std::endl;
       return subs[n];
     }else{
+      Trace("canon-term-debug") << "...return variable in subs." << std::endl;
       return it->second;
     }
   }else if( n.getNumChildren()>0 ){
     //collect children
+    Trace("canon-term-debug") << "Collect children" << std::endl;
     std::vector< Node > cchildren;
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
       cchildren.push_back( n[i] );
     }
     //if applicable, first sort by term order
     if( apply_torder && isComm( n.getKind() ) ){
+      Trace("canon-term-debug") << "Sort based on commutative operator " << n.getKind() << std::endl;
       sortTermOrder sto;
       sto.d_tdb = this;
       std::sort( cchildren.begin(), cchildren.end(), sto );
     }
     //now make canonical
+    Trace("canon-term-debug") << "Make canonical children" << std::endl;
     for( unsigned i=0; i<cchildren.size(); i++ ){
       cchildren[i] = getCanonicalTerm( cchildren[i], var_count, subs, apply_torder );
     }
-    if( n.hasOperator() ){
+    if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+      Trace("canon-term-debug") << "Insert operator " << n.getOperator() << std::endl;
       cchildren.insert( cchildren.begin(), n.getOperator() );
     }
-    return NodeManager::currentNM()->mkNode( n.getKind(), cchildren );
+    Trace("canon-term-debug") << "...constructing for " << n << "." << std::endl;
+    Node ret = NodeManager::currentNM()->mkNode( n.getKind(), cchildren );
+    Trace("canon-term-debug") << "...constructed " << ret << " for " << n << "." << std::endl;
+    return ret;
   }else{
+    Trace("canon-term-debug") << "...return 0-child term." << std::endl;
     return n;
   }
 }