Merge branch 'master' of https://github.com/CVC4/CVC4

9 files changed, 220 insertions, 419 deletions

diff --git a/src/theory/quantifiers/equality_infer.cpp b/src/theory/quantifiers/equality_infer.cpp
index c3064116f..5190025ee 100644
--- a/src/theory/quantifiers/equality_infer.cpp
+++ b/src/theory/quantifiers/equality_infer.cpp
@@ -53,10 +53,10 @@ void EqualityInference::addToExplanation( std::vector< Node >& exp, Node e ) {
 }
 
 void EqualityInference::addToExplanationEqc( std::vector< Node >& exp, Node eqc ) {
-  NodeListMap::iterator re_i = d_rep_exp.find( eqc );
+  NodeIntMap::iterator re_i = d_rep_exp.find( eqc );
   if( re_i!=d_rep_exp.end() ){
-    for( unsigned i=0; i<(*re_i).second->size(); i++ ){
-      addToExplanation( exp, (*(*re_i).second)[i] );
+    for( int i=0; i<(*re_i).second; i++ ){
+      addToExplanation( exp, d_rep_exp_data[eqc][i] );
     }
   }
   //for( unsigned i=0; i<d_eqci[n]->d_rep_exp.size(); i++ ){
@@ -65,16 +65,19 @@ void EqualityInference::addToExplanationEqc( std::vector< Node >& exp, Node eqc
 }
 
 void EqualityInference::addToExplanationEqc( Node eqc, std::vector< Node >& exp_to_add ) {
-  NodeListMap::iterator re_i = d_rep_exp.find( eqc );
-  NodeList* re;
+  NodeIntMap::iterator re_i = d_rep_exp.find( eqc );
+  int n_re = 0;
   if( re_i != d_rep_exp.end() ){
-    re = (*re_i).second;
-  }else{
-    re = new(d_c->getCMM()) NodeList( true, d_c, false, context::ContextMemoryAllocator<TNode>(d_c->getCMM()) );
-    d_rep_exp.insertDataFromContextMemory( eqc, re );
+    n_re = (*re_i).second;
   }
+  d_rep_exp[eqc] = n_re + exp_to_add.size();
   for( unsigned i=0; i<exp_to_add.size(); i++ ){
-    re->push_back( exp_to_add[i] );
+    if( n_re<(int)d_rep_exp_data[eqc].size() ){
+      d_rep_exp_data[eqc][n_re] = exp_to_add[i];
+    }else{
+      d_rep_exp_data[eqc].push_back( exp_to_add[i] );
+    }
+    n_re++;
   }
   //for( unsigned i=0; i<exp_to_add.size(); i++ ){
   //  eqci->d_rep_exp.push_back( exp_to_add[i] );
@@ -204,16 +207,18 @@ void EqualityInference::eqNotifyNewClass(TNode t) {
 
 void EqualityInference::addToUseList( Node used, Node eqc ) {
 #if 1
-  NodeListMap::iterator ul_i = d_uselist.find( used );
-  NodeList* ul;
+  NodeIntMap::iterator ul_i = d_uselist.find( used );
+  int n_ul = 0;
   if( ul_i != d_uselist.end() ){
-    ul = (*ul_i).second;
-  }else{
-    ul = new(d_c->getCMM()) NodeList( true, d_c, false, context::ContextMemoryAllocator<TNode>(d_c->getCMM()) );
-    d_uselist.insertDataFromContextMemory( used, ul );
+    n_ul = (*ul_i).second;
   }
+  d_uselist[ used ] = n_ul + 1;
   Trace("eq-infer-debug") << "      add to use list : " << used << " -> " << eqc << std::endl;
-  (*ul).push_back( eqc );  
+  if( n_ul<(int)d_uselist_data[used].size() ){
+    d_uselist_data[used][n_ul] = eqc;
+  }else{
+    d_uselist_data[used].push_back( eqc );  
+  }
 #else
   std::map< Node, EqcInfo * >::iterator itu = d_eqci.find( used );
   EqcInfo * eqci_used;
@@ -356,12 +361,12 @@ void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) {
               //go through all equivalence classes that may refer to v_solve
               std::map< Node, bool > processed;
               processed[v_solve] = true;
-              NodeListMap::iterator ul_i = d_uselist.find( v_solve );
+              NodeIntMap::iterator ul_i = d_uselist.find( v_solve );
               if( ul_i != d_uselist.end() ){
-                NodeList* ul = (*ul_i).second;
-                Trace("eq-infer-debug") << "      use list size = " << ul->size() << std::endl;
-                for( unsigned j=0; j<ul->size(); j++ ){
-                  Node r = (*ul)[j];
+                int n_ul = (*ul_i).second;
+                Trace("eq-infer-debug") << "      use list size = " << n_ul << std::endl;
+                for( int j=0; j<n_ul; j++ ){
+                  Node r = d_uselist_data[v_solve][j];
                 //Trace("eq-infer-debug") << "      use list size = " << eqci_solved->d_uselist.size() << std::endl;
                 //for( unsigned j=0; j<eqci_solved->d_uselist.size(); j++ ){
                 //  Node r = eqci_solved->d_uselist[j];
diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h
index 93c7bd080..80d6ef98b 100644
--- a/src/theory/quantifiers/equality_infer.h
+++ b/src/theory/quantifiers/equality_infer.h
@@ -39,7 +39,7 @@ class EqualityInference
   typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
   typedef context::CDChunkList<Node> NodeList;
-  typedef context::CDHashMap< Node, NodeList *, NodeHashFunction > NodeListMap;
+  typedef context::CDHashMap< Node, int, NodeHashFunction > NodeIntMap;
 private:
   context::Context * d_c;
   Node d_one;
@@ -67,11 +67,13 @@ private:
   BoolMap d_elim_vars;
   std::map< Node, EqcInfo * > d_eqci;
   NodeMap d_rep_to_eqc;
-  NodeListMap d_rep_exp;
+  NodeIntMap d_rep_exp;
+  std::map< Node, std::vector< Node > > d_rep_exp_data;
   /** set eqc rep */
   void setEqcRep( Node t, Node r, std::vector< Node >& exp_to_add, EqcInfo * eqci );
   /** use list */
-  NodeListMap d_uselist;
+  NodeIntMap d_uselist;
+  std::map< Node, std::vector< Node > > d_uselist_data;
   void addToUseList( Node used, Node eqc );
   /** pending merges */
   NodeList d_pending_merges;
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index bd5100a2e..2d3bf76f6 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -32,6 +32,7 @@ namespace theory {
 namespace inst {
 
 InstMatchGenerator::InstMatchGenerator( Node pat ){
+  d_cg = NULL;
   d_needsReset = true;
   d_active_add = false;
   Assert( quantifiers::TermDb::hasInstConstAttr(pat) );
@@ -43,12 +44,20 @@ InstMatchGenerator::InstMatchGenerator( Node pat ){
 }
 
 InstMatchGenerator::InstMatchGenerator() {
+  d_cg = NULL;
   d_needsReset = true;
   d_active_add = false;
   d_next = NULL;
   d_matchPolicy = MATCH_GEN_DEFAULT;
 }
 
+InstMatchGenerator::~InstMatchGenerator() throw() {
+  for( unsigned i=0; i<d_children.size(); i++ ){
+    delete d_children[i];
+  }
+  delete d_cg;
+}
+
 void InstMatchGenerator::setActiveAdd(bool val){
   d_active_add = val;
   if( d_next!=NULL ){
@@ -249,7 +258,7 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi
       Trace("matching-debug2") << "Reset children..." << std::endl;
       //now, fit children into match
       //we will be requesting candidates for matching terms for each child
-      for( int i=0; i<(int)d_children.size(); i++ ){
+      for( unsigned i=0; i<d_children.size(); i++ ){
         d_children[i]->reset( t[ d_children_index[i] ], qe );
       }
       Trace("matching-debug2") << "Continue next " << d_next << std::endl;
@@ -484,7 +493,7 @@ d_f( q ){
     }
     Debug("smart-multi-trigger") << std::endl;
   }
-  for( int i=0; i<(int)pats.size(); i++ ){
+  for( unsigned i=0; i<pats.size(); i++ ){
     Node n = pats[i];
     //make the match generator
     d_children.push_back( InstMatchGenerator::mkInstMatchGenerator(q, n, qe ) );
@@ -492,7 +501,7 @@ d_f( q ){
     std::vector< int > unique_vars;
     std::map< int, bool > shared_vars;
     int numSharedVars = 0;
-    for( int j=0; j<(int)d_var_contains[n].size(); j++ ){
+    for( unsigned j=0; j<d_var_contains[n].size(); j++ ){
       if( d_var_to_node[ d_var_contains[n][j] ].size()==1 ){
         Debug("smart-multi-trigger") << "Var " << d_var_contains[n][j] << " is unique to " << pats[i] << std::endl;
         unique_vars.push_back( d_var_contains[n][j] );
@@ -503,7 +512,7 @@ d_f( q ){
     }
     //we use the latest shared variables, then unique variables
     std::vector< int > vars;
-    int index = i==0 ? (int)(pats.size()-1) : (i-1);
+    unsigned index = i==0 ? pats.size()-1 : (i-1);
     while( numSharedVars>0 && index!=i ){
       for( std::map< int, bool >::iterator it = shared_vars.begin(); it != shared_vars.end(); ++it ){
         if( it->second ){
@@ -519,16 +528,24 @@ d_f( q ){
     }
     vars.insert( vars.end(), unique_vars.begin(), unique_vars.end() );
     Debug("smart-multi-trigger") << "   Index[" << i << "]: ";
-    for( int i=0; i<(int)vars.size(); i++ ){
-      Debug("smart-multi-trigger") << vars[i] << " ";
+    for( unsigned j=0; j<vars.size(); j++ ){
+      Debug("smart-multi-trigger") << vars[j] << " ";
     }
     Debug("smart-multi-trigger") << std::endl;
     //make ordered inst match trie
-    InstMatchTrie::ImtIndexOrder* imtio = new InstMatchTrie::ImtIndexOrder;
-    imtio->d_order.insert( imtio->d_order.begin(), vars.begin(), vars.end() );
-    d_children_trie.push_back( InstMatchTrieOrdered( imtio ) );
+    d_imtio[i] = new InstMatchTrie::ImtIndexOrder;
+    d_imtio[i]->d_order.insert( d_imtio[i]->d_order.begin(), vars.begin(), vars.end() );
+    d_children_trie.push_back( InstMatchTrieOrdered( d_imtio[i] ) );
   }
+}
 
+InstMatchGeneratorMulti::~InstMatchGeneratorMulti() throw() {
+  for( unsigned i=0; i<d_children.size(); i++ ){
+    delete d_children[i];
+  }
+  for( std::map< unsigned, InstMatchTrie::ImtIndexOrder* >::iterator it = d_imtio.begin(); it != d_imtio.end(); ++it ){
+    delete it->second;
+  }
 }
 
 /** reset instantiation round (call this whenever equivalence classes have changed) */
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index 49e3c1ec5..096774c51 100644
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -91,7 +91,7 @@ public:
   InstMatchGenerator( Node pat );
   InstMatchGenerator();
   /** destructor */
-  ~InstMatchGenerator() throw() {}
+  virtual ~InstMatchGenerator() throw();
   /** The pattern we are producing matches for.
       If null, this is a multi trigger that is merging matches from d_children.
   */
@@ -125,7 +125,7 @@ public:
 class VarMatchGeneratorBooleanTerm : public InstMatchGenerator {
 public:
   VarMatchGeneratorBooleanTerm( Node var, Node comp );
-  ~VarMatchGeneratorBooleanTerm() throw() {}
+  virtual ~VarMatchGeneratorBooleanTerm() throw() {}
   Node d_comp;
   bool d_rm_prev;
   /** reset instantiation round (call this at beginning of instantiation round) */
@@ -142,7 +142,7 @@ public:
 class VarMatchGeneratorTermSubs : public InstMatchGenerator {
 public:
   VarMatchGeneratorTermSubs( Node var, Node subs );
-  ~VarMatchGeneratorTermSubs() throw() {}
+  virtual ~VarMatchGeneratorTermSubs() throw() {}
   TNode d_var;
   TypeNode d_var_type;
   Node d_subs;
@@ -183,6 +183,8 @@ private:
   int d_matchPolicy;
   /** children generators */
   std::vector< InstMatchGenerator* > d_children;
+  /** order */
+  std::map< unsigned, InstMatchTrie::ImtIndexOrder* > d_imtio;
   /** inst match tries for each child */
   std::vector< InstMatchTrieOrdered > d_children_trie;
   /** calculate matches */
@@ -191,7 +193,7 @@ public:
   /** constructors */
   InstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe );
   /** destructor */
-  ~InstMatchGeneratorMulti() throw() {}
+  virtual ~InstMatchGeneratorMulti() throw();
   /** reset instantiation round (call this whenever equivalence classes have changed) */
   void resetInstantiationRound( QuantifiersEngine* qe );
   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 511337b40..68f824c57 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -48,7 +48,7 @@ bool QuantifiersRewriter::isClause( Node n ){
 bool QuantifiersRewriter::isLiteral( Node n ){
   switch( n.getKind() ){
   case NOT:
-    return isLiteral( n[0] );
+    return n[0].getKind()!=NOT && isLiteral( n[0] );
     break;
   case OR:
   case AND:
@@ -59,7 +59,8 @@ bool QuantifiersRewriter::isLiteral( Node n ){
     return false;
     break;
   case EQUAL:
-    return n[0].getType()!=NodeManager::currentNM()->booleanType();
+    //for boolean terms
+    return !n[0].getType().isBoolean();
     break;
   default:
     break;
@@ -259,121 +260,98 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
   return RewriteResponse( status, ret );
 }
 
-Node QuantifiersRewriter::computeElimSymbols( Node body ) {
-  if( isLiteral( body ) ){
-    return body;
-  }else{
-    bool childrenChanged = false;
-    Kind k = body.getKind();
-    if( body.getKind()==IMPLIES ){
-      k = OR;
-      childrenChanged = true;
-    }else if( body.getKind()==XOR ){
-      k = IFF;
+bool QuantifiersRewriter::addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged ){
+  if( ( k==OR || k==AND ) && options::elimTautQuant() ){
+    Node lit = c.getKind()==NOT ? c[0] : c;
+    bool pol = c.getKind()!=NOT;
+    std::map< Node, bool >::iterator it = lit_pol.find( lit );
+    if( it==lit_pol.end() ){
+      lit_pol[lit] = pol;
+      children.push_back( c );
+    }else{
       childrenChanged = true;
-    }
-    std::vector< Node > children;
-    std::map< Node, bool > lit_pol;
-    for( unsigned i=0; i<body.getNumChildren(); i++ ){
-      Node c = computeElimSymbols( body[i] );
-      if( i==0 && ( body.getKind()==IMPLIES || body.getKind()==XOR ) ){
-        c = c.negate();
-      }
-      if( ( k==OR || k==AND ) && options::elimTautQuant() ){
-        Node lit = c.getKind()==NOT ? c[0] : c;
-        bool pol = c.getKind()!=NOT;
-        std::map< Node, bool >::iterator it = lit_pol.find( lit );
-        if( it==lit_pol.end() ){
-          lit_pol[lit] = pol;
-          children.push_back( c );
-        }else{
-          childrenChanged = true;
-          if( it->second!=pol ){
-            return NodeManager::currentNM()->mkConst( k==OR );
-          }
-        }
-      }else{
-        children.push_back( c );
+      if( it->second!=pol ){
+        return false;
       }
-      childrenChanged = childrenChanged || c!=body[i];
-    }
-    //if( body.getKind()==ITE && isLiteral( body[0] ) ){
-    //  ret = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] ), 
-    //                                               NodeManager::currentNM()->mkNode( OR, body[0], body[2] ) );
-    //}
-    if( childrenChanged ){
-      return ( children.size()==1 && k!=NOT ) ? children[0] : NodeManager::currentNM()->mkNode( k, children );
-    }else{
-      return body;
     }
+  }else{
+    children.push_back( c );
   }
+  return true;
 }
 
-Node QuantifiersRewriter::computeNNF( Node body ){
-  if( body.getKind()==NOT ){
+// eliminates IMPLIES/XOR, removes duplicates/infers tautologies of AND/OR, and computes NNF
+Node QuantifiersRewriter::computeElimSymbols( Node body ) {
+  Kind ok = body.getKind();
+  Kind k = ok;
+  bool negAllCh = false;
+  bool negCh1 = false;
+  if( ok==IMPLIES ){
+    k = OR;
+    negCh1 = true;
+  }else if( ok==XOR ){
+    k = IFF;
+    negCh1 = true;
+  }else if( ok==NOT ){
     if( body[0].getKind()==NOT ){
-      return computeNNF( body[0][0] );
-    }else if( isLiteral( body[0] ) ){
-      return body;
+      return computeElimSymbols( body[0][0] );
+    }else if( body[0].getKind()==OR || body[0].getKind()==IMPLIES ){
+      k = AND;   
+      negAllCh = true;
+      negCh1 = body[0].getKind()==IMPLIES;
+      body = body[0];
+    }else if( body[0].getKind()==AND ){
+      k = OR;
+      negAllCh = true;
+      body = body[0];
+    }else if( body[0].getKind()==XOR || body[0].getKind()==IFF ){
+      k = IFF;
+      negCh1 = ( body[0].getKind()==IFF );
+      body = body[0];
+    }else if( body[0].getKind()==ITE ){
+      k = body[0].getKind();
+      negAllCh = true;
+      negCh1 = true;
+      body = body[0];
     }else{
-      std::vector< Node > children; 
-      Kind k = body[0].getKind();
-
-      if( body[0].getKind()==OR || body[0].getKind()==AND ){
-        k = body[0].getKind()==AND ? OR : AND;
-        for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
-          Node nc = computeNNF( body[0][i].notNode() );
-          if( nc.getKind()==k ){
-            for( unsigned j=0; j<nc.getNumChildren(); j++ ){
-              children.push_back( nc[j] );
-            }
-          }else{
-            children.push_back( nc );
-          }
-        }
-      }else if( body[0].getKind()==IFF ){
-        for( int i=0; i<2; i++ ){
-          Node nn = i==0 ? body[0][i] : body[0][i].notNode();
-          children.push_back( computeNNF( nn ) );
-        }
-      }else if( body[0].getKind()==ITE ){
-        for( int i=0; i<3; i++ ){
-          Node nn = i==0 ? body[0][i] : body[0][i].notNode();
-          children.push_back( computeNNF( nn ) );
-        }
-      }else{
-        Notice() << "Unhandled Quantifiers NNF: " << body << std::endl;
-        return body;
-      }
-      return NodeManager::currentNM()->mkNode( k, children );
+      return body;
     }
-  }else if( isLiteral( body ) ){
+  }else if( ok!=IFF && ok!=ITE && ok!=AND && ok!=OR ){
+    //a literal
     return body;
-  }else{
-    std::vector< Node > children;
-    bool childrenChanged = false;
-    bool isAssoc = body.getKind()==AND || body.getKind()==OR;
-    for( int i=0; i<(int)body.getNumChildren(); i++ ){
-      Node nc = computeNNF( body[i] );
-      if( isAssoc && nc.getKind()==body.getKind() ){
-        for( unsigned j=0; j<nc.getNumChildren(); j++ ){
-          children.push_back( nc[j] );
+  }
+  bool childrenChanged = false;
+  std::vector< Node > children;
+  std::map< Node, bool > lit_pol;
+  for( unsigned i=0; i<body.getNumChildren(); i++ ){
+    Node c = computeElimSymbols( ( i==0 && negCh1 )!=negAllCh ? body[i].negate() : body[i] );
+    bool success = true;
+    if( c.getKind()==k && ( k==OR || k==AND ) ){
+      //flatten
+      childrenChanged = true;
+      for( unsigned j=0; j<c.getNumChildren(); j++ ){
+        if( !addCheckElimChild( children, c[j], k, lit_pol, childrenChanged ) ){
+          success = false;
+          break;
         }
-        childrenChanged = true;
-      }else{
-        children.push_back( nc );
-        childrenChanged = childrenChanged || nc!=body[i];
       }
-    }
-    if( childrenChanged ){
-      return NodeManager::currentNM()->mkNode( body.getKind(), children );
     }else{
-      return body;
+      success = addCheckElimChild( children, c, k, lit_pol, childrenChanged );
+    }
+    if( !success ){
+      // tautology
+      Assert( k==OR || k==AND );
+      return NodeManager::currentNM()->mkConst( k==OR );
     }
+    childrenChanged = childrenChanged || c!=body[i];
+  }
+  if( childrenChanged || k!=ok ){
+    return ( children.size()==1 && k!=NOT ) ? children[0] : NodeManager::currentNM()->mkNode( k, children );
+  }else{
+    return 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() ){
@@ -1036,144 +1014,6 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >&
   return body;
 }
 
-Node QuantifiersRewriter::computeClause( Node n ){
-  Assert( isClause( n ) );
-  if( isLiteral( n ) ){
-    return n;
-  }else{
-    NodeBuilder<> t(OR);
-    if( n.getKind()==NOT ){
-      if( n[0].getKind()==NOT ){
-        return computeClause( n[0][0] );
-      }else{
-        //De-Morgan's law
-        Assert( n[0].getKind()==AND );
-        for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
-          Node nn = computeClause( n[0][i].notNode() );
-          addNodeToOrBuilder( nn, t );
-        }
-      }
-    }else{
-      for( int i=0; i<(int)n.getNumChildren(); i++ ){
-        Node nn = computeClause( n[i] );
-        addNodeToOrBuilder( nn, t );
-      }
-    }
-    return t.constructNode();
-  }
-}
-
-Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ){
-  if( isLiteral( n ) ){
-    return n;
-  }else if( !forcePred && isClause( n ) ){
-    return computeClause( n );
-  }else{
-    Kind k = n.getKind();
-    NodeBuilder<> t(k);
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      Node nc = n[i];
-      Node ncnf = computeCNF( nc, args, defs, k!=OR );
-      if( k==OR ){
-        addNodeToOrBuilder( ncnf, t );
-      }else{
-        t << ncnf;
-      }
-    }
-    if( !forcePred && k==OR ){
-      return t.constructNode();
-    }else{
-      //compute the free variables
-      Node nt = t;
-      std::vector< Node > activeArgs;
-      computeArgVec( args, activeArgs, nt );
-      std::vector< TypeNode > argTypes;
-      for( int i=0; i<(int)activeArgs.size(); i++ ){
-        argTypes.push_back( activeArgs[i].getType() );
-      }
-      //create the predicate
-      Assert( argTypes.size()>0 );
-      TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, NodeManager::currentNM()->booleanType() );
-      std::stringstream ss;
-      ss << "cnf_" << n.getKind() << "_" << n.getId();
-      Node op = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "was created by the quantifiers rewriter" );
-      std::vector< Node > predArgs;
-      predArgs.push_back( op );
-      predArgs.insert( predArgs.end(), activeArgs.begin(), activeArgs.end() );
-      Node pred = NodeManager::currentNM()->mkNode( APPLY_UF, predArgs );
-      Trace("quantifiers-rewrite-cnf-debug") << "Made predicate " << pred << " for " << nt << std::endl;
-      //create the bound var list
-      Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, activeArgs );
-      //now, look at the structure of nt
-      if( nt.getKind()==NOT ){
-        //case for NOT
-        for( int i=0; i<2; i++ ){
-          NodeBuilder<> tt(OR);
-          tt << ( i==0 ? nt[0].notNode() : nt[0] );
-          tt << ( i==0 ? pred.notNode() : pred );
-          defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
-        }
-      }else if( nt.getKind()==OR ){
-        //case for OR
-        for( int i=0; i<(int)nt.getNumChildren(); i++ ){
-          NodeBuilder<> tt(OR);
-          tt << nt[i].notNode() << pred;
-          defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
-        }
-        NodeBuilder<> tt(OR);
-        for( int i=0; i<(int)nt.getNumChildren(); i++ ){
-          tt << nt[i];
-        }
-        tt << pred.notNode();
-        defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
-      }else if( nt.getKind()==AND ){
-        //case for AND
-        for( int i=0; i<(int)nt.getNumChildren(); i++ ){
-          NodeBuilder<> tt(OR);
-          tt << nt[i] << pred.notNode();
-          defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
-        }
-        NodeBuilder<> tt(OR);
-        for( int i=0; i<(int)nt.getNumChildren(); i++ ){
-          tt << nt[i].notNode();
-        }
-        tt << pred;
-        defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
-      }else if( nt.getKind()==IFF ){
-        //case for IFF
-        for( int i=0; i<4; i++ ){
-          NodeBuilder<> tt(OR);
-          tt << ( ( i==0 || i==3 ) ? nt[0].notNode() : nt[0] );
-          tt << ( ( i==1 || i==3 ) ? nt[1].notNode() : nt[1] );
-          tt << ( ( i==0 || i==1 ) ? pred.notNode() : pred );
-          defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
-        }
-      }else if( nt.getKind()==ITE ){
-        //case for ITE
-        for( int j=1; j<=2; j++ ){
-          for( int i=0; i<2; i++ ){
-            NodeBuilder<> tt(OR);
-            tt << ( ( j==1 ) ? nt[0].notNode() : nt[0] );
-            tt << ( ( i==1 ) ? nt[j].notNode() : nt[j] );
-            tt << ( ( i==0 ) ? pred.notNode() : pred );
-            defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
-          }
-        }
-        for( int i=0; i<2; i++ ){
-          NodeBuilder<> tt(OR);
-          tt << ( i==0 ? nt[1].notNode() : nt[1] );
-          tt << ( i==0 ? nt[2].notNode() : nt[2] );
-          tt << ( i==1 ? pred.notNode() : pred );
-          defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
-        }
-      }else{
-        Notice() << "Unhandled Quantifiers CNF: " << nt << std::endl;
-      }
-      return pred;
-    }
-  }
-}
-
 Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, bool pol ){
   if( body.getKind()==FORALL ){
     if( pol && ( options::prenexQuant()==PRENEX_ALL || body.getNumChildren()==2 ) ){
@@ -1181,15 +1021,13 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
       std::vector< Node > subs;
       //for doing prenexing of same-signed quantifiers
       //must rename each variable that already exists
-      for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
-        //if( std::find( args.begin(), args.end(), body[0][i] )!=args.end() ){
+      for( unsigned i=0; i<body[0].getNumChildren(); i++ ){
         terms.push_back( body[0][i] );
         subs.push_back( NodeManager::currentNM()->mkBoundVar( body[0][i].getType() ) );
       }
       args.insert( args.end(), subs.begin(), subs.end() );
       Node newBody = body[1];
       newBody = newBody.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
-      Debug("quantifiers-substitute-debug") << "Did substitute have an effect" << (body[1] != newBody) << body[1] << " became " << newBody << endl;
       return newBody;
     }else{
       return body;
@@ -1198,7 +1036,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
     Assert( body.getKind()!=EXISTS );
     bool childrenChanged = false;
     std::vector< Node > newChildren;
-    for( int i=0; i<(int)body.getNumChildren(); i++ ){
+    for( unsigned i=0; i<body.getNumChildren(); i++ ){
       bool newHasPol;
       bool newPol;
       QuantPhaseReq::getPolarity( body, i, true, pol, newHasPol, newPol );
@@ -1224,7 +1062,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
   }
 }
 
-Node QuantifiersRewriter::computeSplit( Node f, std::vector< Node >& args, Node body ) {
+Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ) {
   Assert( body.getKind()==OR );
   size_t var_found_count = 0;
   size_t eqc_count = 0;
@@ -1240,8 +1078,8 @@ Node QuantifiersRewriter::computeSplit( Node f, std::vector< Node >& args, Node
     Node n = body[i];
     std::vector< Node > lit_args;
     computeArgVec( args, lit_args, n );
-    if (lit_args.empty()) {
-      lits.push_back(n);
+    if( lit_args.empty() ){
+      lits.push_back( n );
     }else {
       //collect the equivalence classes this literal belongs to, and the new variables it contributes
       std::vector< int > eqcs;
@@ -1293,8 +1131,8 @@ Node QuantifiersRewriter::computeSplit( Node f, std::vector< Node >& args, Node
       eqc_to_lit[eqcz].push_back(n);
     }
   }
-  if ( eqc_active>1 || !lits.empty() ){
-    Trace("clause-split-debug") << "Split clause " << f << std::endl;
+  if ( eqc_active>1 || !lits.empty() || var_to_eqc.size()!=args.size() ){
+    Trace("clause-split-debug") << "Split quantified formula with body " << body << std::endl;
     Trace("clause-split-debug") << "   Ground literals: " << std::endl;
     for( size_t i=0; i<lits.size(); i++) {
       Trace("clause-split-debug") << "      " << lits[i] << std::endl;
@@ -1317,27 +1155,21 @@ Node QuantifiersRewriter::computeSplit( Node f, std::vector< Node >& args, Node
       Node fa = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
       lits.push_back(fa);
     }
-    Assert( lits.size()>1 );
-    Node nf = NodeManager::currentNM()->mkNode(OR,lits);
+    Assert( !lits.empty() );
+    Node nf = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode(OR,lits);
     Trace("clause-split-debug") << "Made node : " << nf << std::endl;
     return nf;
+  }else{
+    return mkForAll( args, body, qa );
   }
-  return f;
 }
 
 Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, QAttributes& qa ){
-  std::vector< Node > activeArgs;
-  //if cegqi is on, may be synthesis conjecture, in which case we want to keep all variables
-  if( options::ceGuidedInst() && qa.d_sygus ){
-    activeArgs.insert( activeArgs.end(), args.begin(), args.end() );
-  }else{
-    computeArgVec2( args, activeArgs, body, qa.d_ipl );
-  }
-  if( activeArgs.empty() ){
+  if( args.empty() ){
     return body;
   }else{
     std::vector< Node > children;
-    children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, activeArgs ) );
+    children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) );
     children.push_back( body );
     if( !qa.d_ipl.isNull() ){
       children.push_back( qa.d_ipl );
@@ -1346,82 +1178,59 @@ Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, QAttri
   }
 }
 
-Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, Node body, QAttributes& qa ){
+//computes miniscoping, also eliminates variables that do not occur free in body
+Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa ){
   if( body.getKind()==FORALL ){
-    //combine arguments
+    //combine prenex
     std::vector< Node > newArgs;
-    for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
+    newArgs.insert( newArgs.end(), args.begin(), args.end() );
+    for( unsigned i=0; i<body[0].getNumChildren(); i++ ){
       newArgs.push_back( body[0][i] );
     }
-    newArgs.insert( newArgs.end(), args.begin(), args.end() );
-    return mkForAll( newArgs, body[ 1 ], qa );
-  }else{
-    if( body.getKind()==NOT ){
-      //push not downwards
-      if( body[0].getKind()==NOT ){
-        return computeMiniscoping( f, args, body[0][0], qa );
-      }else if( body[0].getKind()==AND ){
-        if( options::miniscopeQuantFreeVar() ){
-          NodeBuilder<> t(kind::OR);
-          for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
-            t <<  ( body[0][i].getKind()==NOT ? body[0][i][0] : body[0][i].notNode() );
-          }
-          return computeMiniscoping( f, args, t.constructNode(), qa );
-        }
-      }else if( body[0].getKind()==OR ){
-        if( options::miniscopeQuant() ){
-          NodeBuilder<> t(kind::AND);
-          for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
-            Node trm = body[0][i].negate();
-            t << computeMiniscoping( f, args, trm, qa );
-          }
-          return t.constructNode();
+    return mkForAll( newArgs, body[1], qa );
+  }else if( body.getKind()==AND ){
+    if( options::miniscopeQuant() ){
+      //break apart
+      NodeBuilder<> t(kind::AND);
+      for( unsigned i=0; i<body.getNumChildren(); i++ ){
+        t << computeMiniscoping( args, body[i], qa );
+      }
+      Node retVal = t;
+      return retVal;
+    }
+  }else if( body.getKind()==OR ){
+    if( options::quantSplit() ){
+      //splitting subsumes free variable miniscoping, apply it with higher priority
+      return computeSplit( args, body, qa );
+    }else if( options::miniscopeQuantFreeVar() ){
+      Node newBody = body;
+      NodeBuilder<> body_split(kind::OR);
+      NodeBuilder<> tb(kind::OR);
+      for( unsigned i=0; i<body.getNumChildren(); i++ ){
+        Node trm = body[i];
+        if( TermDb::containsTerms( body[i], args ) ){
+          tb << trm;
+        }else{
+          body_split << trm;
         }
       }
-    }else if( body.getKind()==AND ){
-      if( options::miniscopeQuant() ){
-        //break apart
-        NodeBuilder<> t(kind::AND);
-        for( unsigned i=0; i<body.getNumChildren(); i++ ){
-          t << computeMiniscoping( f, args, body[i], qa );
-        }
-        Node retVal = t;
-        return retVal;
-      }
-    }else if( body.getKind()==OR ){
-      if( options::quantSplit() ){
-        //splitting subsumes free variable miniscoping, apply it with higher priority
-        Node nf = computeSplit( f, args, body );
-        if( nf!=f ){
-          return nf;
-        }
-      }else if( options::miniscopeQuantFreeVar() ){
-        Node newBody = body;
-        NodeBuilder<> body_split(kind::OR);
-        NodeBuilder<> tb(kind::OR);
-        for( unsigned i=0; i<body.getNumChildren(); i++ ){
-          Node trm = body[i];
-          if( TermDb::containsTerms( body[i], args ) ){
-            tb << trm;
-          }else{
-            body_split << trm;
-          }
-        }
-        if( tb.getNumChildren()==0 ){
-          return body_split;
-        }else if( body_split.getNumChildren()>0 ){
-          newBody = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb;
-          body_split << mkForAll( args, newBody, qa );
-          return body_split.getNumChildren()==1 ? body_split.getChild( 0 ) : body_split;
-        }
+      if( tb.getNumChildren()==0 ){
+        return body_split;
+      }else if( body_split.getNumChildren()>0 ){
+        newBody = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb;
+        std::vector< Node > activeArgs;
+        computeArgVec2( args, activeArgs, newBody, qa.d_ipl );
+        body_split << mkForAll( activeArgs, newBody, qa );
+        return body_split.getNumChildren()==1 ? body_split.getChild( 0 ) : body_split;
       }
     }
+  }else if( body.getKind()==NOT ){
+    Assert( isLiteral( body[0] ) );
   }
-  //if( body==f[1] ){
-  //  return f;
-  //}else{
-  return mkForAll( args, body, qa );
-  //}
+  //remove variables that don't occur
+  std::vector< Node > activeArgs;
+  computeArgVec2( args, activeArgs, body, qa.d_ipl );
+  return mkForAll( activeArgs, body, qa );
 }
 
 Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& args, Node body ){
@@ -1539,8 +1348,6 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q
     return is_std;
   }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
     return options::aggressiveMiniscopeQuant() && is_std;
-  }else if( computeOption==COMPUTE_NNF ){
-    return true;
   }else if( computeOption==COMPUTE_PROCESS_TERMS ){
     return options::condRewriteQuant();
   }else if( computeOption==COMPUTE_COND_SPLIT ){
@@ -1549,8 +1356,6 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q
     return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant() && is_std;
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
     return ( options::varElimQuant() || options::dtVarExpandQuant() || options::purifyQuant() ) && is_std;
-  //}else if( computeOption==COMPUTE_CNF ){
-  //  return options::cnfQuant();
   }else if( computeOption==COMPUTE_PURIFY_EXPAND ){
     return options::purifyQuant() && is_std;
   }else{
@@ -1570,11 +1375,9 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut
     n = computeElimSymbols( n );
   }else if( computeOption==COMPUTE_MINISCOPING ){
     //return directly
-    return computeMiniscoping( f, args, n, qa );
+    return computeMiniscoping( args, n, qa );
   }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
     return computeAggressiveMiniscoping( args, n );
-  }else if( computeOption==COMPUTE_NNF ){
-    n = computeNNF( n );
   }else if( computeOption==COMPUTE_PROCESS_TERMS ){
     std::vector< Node > new_conds;
     n = computeProcessTerms( n, args, new_conds, f, qa );
@@ -1588,9 +1391,6 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut
     n = computePrenex( n, args, true );
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
     n = computeVarElimination( n, args, qa );
-  //}else if( computeOption==COMPUTE_CNF ){
-    //n = computeCNF( n, args, defs, false );
-    //ipl = Node::null();
   }else if( computeOption==COMPUTE_PURIFY_EXPAND ){
     std::vector< Node > conj;
     computePurifyExpand( n, conj, args, qa );
@@ -1724,15 +1524,15 @@ struct ContainsQuantAttributeId {};
 typedef expr::Attribute<ContainsQuantAttributeId, uint64_t> ContainsQuantAttribute;
 
 // check if the given node contains a universal quantifier
-bool QuantifiersRewriter::containsQuantifiers(Node n) {
+bool QuantifiersRewriter::containsQuantifiers( Node n ){
   if( n.hasAttribute(ContainsQuantAttribute()) ){
     return n.getAttribute(ContainsQuantAttribute())==1;
-  } else if(n.getKind() == kind::FORALL) {
+  }else if( n.getKind() == kind::FORALL ){
     return true;
-  } else {
+  }else{
     bool cq = false;
     for( unsigned i = 0; i < n.getNumChildren(); ++i ){
-      if( containsQuantifiers(n[i]) ){
+      if( containsQuantifiers( n[i] ) ){
         cq = true;
         break;
       }
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 2071d1793..776517109 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -38,6 +38,7 @@ public:
   static int getPurifyId( Node n );
   static int getPurifyIdLit( Node n );
 private:
+  static bool addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged );
   static void addNodeToOrBuilder( Node n, NodeBuilder<>& t );
   static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa );
   static void computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n, std::map< Node, bool >& visited );
@@ -46,7 +47,6 @@ private:
   static Node computeProcessTerms2( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond,
                                     std::map< Node, Node >& cache, std::map< Node, Node >& icache,
                                     std::vector< Node >& new_vars, std::vector< Node >& new_conds );
-  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 );
   static bool isConditionalVariableElim( Node n, int pol=0 );
   static bool isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent );
@@ -57,15 +57,13 @@ private:
   static Node computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa, std::map< Node, std::vector< int > >& var_parent );
 private:
   static Node computeElimSymbols( Node body );
-  static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, QAttributes& qa );
+  static Node computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa );
   static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body );
-  static Node computeNNF( Node body );
   //cache is dependent upon currCond, icache is not, new_conds are negated conditions
   static Node computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa );
   static Node computeCondSplit( Node body, QAttributes& qa );
-  static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred );
   static Node computePrenex( Node body, std::vector< Node >& args, bool pol );
-  static Node computeSplit( Node f, std::vector< Node >& args, Node body );
+  static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa );
   static Node computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa );
   static Node computePurify( Node body, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent );
   static void computePurifyExpand( Node body, std::vector< Node >& conj, std::vector< Node >& args, QAttributes& qa );
@@ -74,7 +72,6 @@ private:
     COMPUTE_ELIM_SYMBOLS = 0,
     COMPUTE_MINISCOPING,
     COMPUTE_AGGRESSIVE_MINISCOPING,
-    COMPUTE_NNF,
     COMPUTE_PROCESS_TERMS,
     COMPUTE_PRENEX,
     COMPUTE_VAR_ELIMINATION,
diff --git a/src/theory/quantifiers/symmetry_breaking.h b/src/theory/quantifiers/symmetry_breaking.h
index 38fea4f45..e682955e7 100644
--- a/src/theory/quantifiers/symmetry_breaking.h
+++ b/src/theory/quantifiers/symmetry_breaking.h
@@ -42,9 +42,7 @@ class SubsortSymmetryBreaker {
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
-  //typedef context::CDChunkList<int> IntList;
   typedef context::CDList<Node> NodeList;
-  typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap;
 private:
   /** quantifiers engine */
   QuantifiersEngine* d_qe;
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 5645c3401..c34d86497 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -238,10 +238,15 @@ void TermDb::computeUfTerms( TNode f ) {
     if( it!=d_op_map.end() ){
       eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
       Trace("term-db-debug") << "Adding terms for operator " << f << std::endl;
+      unsigned congruentCount = 0;
+      unsigned nonCongruentCount = 0;
+      unsigned alreadyCongruentCount = 0;
+      unsigned relevantCount = 0;
       for( unsigned i=0; i<it->second.size(); i++ ){
         Node n = it->second[i];
         //to be added to term index, term must be relevant, and exist in EE
         if( hasTermCurrent( n ) && ee->hasTerm( n ) ){
+          relevantCount++;
           if( isTermActive( n ) ){
             computeArgReps( n );
 
@@ -260,7 +265,7 @@ void TermDb::computeUfTerms( TNode f ) {
             if( at!=n && ee->areEqual( at, n ) ){
               setTermInactive( n );
               Trace("term-db-debug") << n << " is redundant." << std::endl;
-              //congruentCount++;
+              congruentCount++;
             }else{
               if( at!=n && ee->areDisequal( at, n, false ) ){
                 std::vector< Node > lits;
@@ -282,29 +287,22 @@ void TermDb::computeUfTerms( TNode f ) {
                 d_consistent_ee = false;
                 return;
               }
-              //nonCongruentCount++;
+              nonCongruentCount++;
               d_op_nonred_count[ f ]++;
             }
           }else{
             Trace("term-db-debug") << n << " is already redundant." << std::endl;
-            //congruentCount++;
-            //alreadyCongruentCount++;
+            alreadyCongruentCount++;
           }
         }else{
           Trace("term-db-debug") << n << " is not relevant." << std::endl;
-          //nonRelevantCount++;
         }
       }
-      
-      /*
-      if( Trace.isOn("term-db-index") ){
-        Trace("term-db-index") << "Term index for " << f << " : " << std::endl;
-        Trace("term-db-index") << "- " << it->first << std::endl;
-        d_func_map_trie[ f ].debugPrint("term-db-index", it->second[0]);
-        Trace("term-db-index") << "Non-Congruent/Congruent/Non-Relevant = ";
-        Trace("term-db-index") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl; 
+      if( Trace.isOn("tdb") ){
+        Trace("tdb") << "Term db size [" << f << "] : " << nonCongruentCount << " / ";
+        Trace("tdb") << ( nonCongruentCount + congruentCount ) << " / " << ( nonCongruentCount + congruentCount + alreadyCongruentCount ) << " / ";
+        Trace("tdb") << relevantCount << " / " << it->second.size() << std::endl;
       }
-      */
     }
   }
 }
@@ -676,10 +674,6 @@ void TermDb::presolve() {
 }
 
 bool TermDb::reset( Theory::Effort effort ){
-  //int nonCongruentCount = 0;
-  //int congruentCount = 0;
-  //int alreadyCongruentCount = 0;
-  //int nonRelevantCount = 0;
   d_op_nonred_count.clear();
   d_arg_reps.clear();
   d_func_map_trie.clear();
@@ -743,20 +737,6 @@ bool TermDb::reset( Theory::Effort effort ){
     }
   }
 */  
-  /*
-  Trace("term-db-stats") << "TermDb: Reset" << std::endl;
-  Trace("term-db-stats") << "Non-Congruent/Congruent/Non-Relevant = ";
-  Trace("term-db-stats") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl;
-  if( Trace.isOn("term-db-index") ){
-    Trace("term-db-index") << "functions : " << std::endl;
-    for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
-      if( it->second.size()>0 ){
-        Trace("term-db-index") << "- " << it->first << std::endl;
-        d_func_map_trie[ it->first ].debugPrint("term-db-index", it->second[0]);
-      }
-    }
-  }
-  */
   return true;
 }
 
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 214a4d055..802acc089 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -86,7 +86,7 @@ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes )
 }
 
 Trigger::~Trigger() {
-  if(d_mg != NULL) { delete d_mg; }
+  delete d_mg;
 }
 
 void Trigger::resetInstantiationRound(){