cleanup up some static data members in the quantifiers code

8 files changed, 190 insertions, 171 deletions

diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index d2083ef3d..5f24a3dfa 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -610,7 +610,7 @@ InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node f, std::vector< Node >& p
 d_f( f ){
   Debug("smart-multi-trigger") << "Making smart multi-trigger for " << f << std::endl;
   std::map< Node, std::vector< Node > > var_contains;
-  Trigger::getVarContains( f, pats, var_contains );
+  qe->getTermDatabase()->getVarContains( f, pats, var_contains );
   //convert to indicies
   for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){
     Debug("smart-multi-trigger") << "Pattern " << it->first << " contains: ";
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 727f568c5..fb3098e24 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -30,7 +30,7 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
 InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) :
-QuantifiersModule( qe ), d_setIncomplete( setIncomplete ){
+QuantifiersModule( qe ), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ){
 
 }
 
@@ -144,25 +144,23 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
   }
 }
 
-static int ierCounter = 0;
-
 void InstantiationEngine::check( Theory::Effort e ){
   if( e==Theory::EFFORT_FULL ){
-    ierCounter++;
+    d_ierCounter++;
   }
   //determine if we should perform check, based on instWhenMode
   bool performCheck = false;
   if( options::instWhenMode()==INST_WHEN_FULL ){
     performCheck = ( e >= Theory::EFFORT_FULL );
   }else if( options::instWhenMode()==INST_WHEN_FULL_LAST_CALL ){
-    performCheck = ( ( e==Theory::EFFORT_FULL  && ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL );
+    performCheck = ( ( e==Theory::EFFORT_FULL  && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL );
   }else if( options::instWhenMode()==INST_WHEN_LAST_CALL ){
     performCheck = ( e >= Theory::EFFORT_LAST_CALL );
   }else{
     performCheck = true;
   }
   if( performCheck ){
-    Debug("inst-engine") << "IE: Check " << e << " " << ierCounter << std::endl;
+    Debug("inst-engine") << "IE: Check " << e << " " << d_ierCounter << std::endl;
     double clSet = 0;
     if( Trace.isOn("inst-engine") ){
       clSet = double(clock())/double(CLOCKS_PER_SEC);
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 19dac736c..7721552c5 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -36,6 +36,8 @@ private:
   std::map< Node, Node > d_ce_lit;
   /** whether the instantiation engine should set incomplete if it cannot answer SAT */
   bool d_setIncomplete;
+  /** inst round counter */
+  int d_ierCounter;
 private:
   bool hasAddedCbqiLemma( Node f );
   void addCbqiLemma( Node f );
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 7b5d9e6e2..b41770b7e 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -28,26 +28,54 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
 using namespace CVC4::theory::inst;
- bool TermArgTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){
-   if( argIndex<(int)n.getNumChildren() ){
-     Node r = qe->getEqualityQuery()->getRepresentative( n[ argIndex ] );
-     std::map< Node, TermArgTrie >::iterator it = d_data.find( r );
-     if( it==d_data.end() ){
-       d_data[r].addTerm2( qe, n, argIndex+1 );
-       return true;
-     }else{
-       return it->second.addTerm2( qe, n, argIndex+1 );
-     }
-   }else{
-     //store n in d_data (this should be interpretted as the "data" and not as a reference to a child)
-     d_data[n].d_data.clear();
-     return false;
-   }
- }
+
+bool TermArgTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){
+  if( argIndex<(int)n.getNumChildren() ){
+    Node r = qe->getEqualityQuery()->getRepresentative( n[ argIndex ] );
+    std::map< Node, TermArgTrie >::iterator it = d_data.find( r );
+    if( it==d_data.end() ){
+      d_data[r].addTerm2( qe, n, argIndex+1 );
+      return true;
+    }else{
+      return it->second.addTerm2( qe, n, argIndex+1 );
+    }
+  }else{
+    //store n in d_data (this should be interpretted as the "data" and not as a reference to a child)
+    d_data[n].d_data.clear();
+    return false;
+  }
+}
+
+Trigger* TrTrie::getTrigger2( std::vector< Node >& nodes ){
+  if( nodes.empty() ){
+    return d_tr;
+  }else{
+    Node n = nodes.back();
+    nodes.pop_back();
+    if( d_children.find( n )!=d_children.end() ){
+      return d_children[n]->getTrigger2( nodes );
+    }else{
+      return NULL;
+    }
+  }
+}
+
+void TrTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){
+  if( nodes.empty() ){
+    d_tr = t;
+  }else{
+    Node n = nodes.back();
+    nodes.pop_back();
+    if( d_children.find( n )==d_children.end() ){
+      d_children[n] = new TrTrie;
+    }
+    d_children[n]->addTrigger2( nodes, t );
+  }
+}
 
 void TermDb::addTermEfficient( Node n, std::set< Node >& added){
   static AvailableInTermDb aitdi;
-  if (Trigger::isAtomicTrigger( n ) && !n.getAttribute(aitdi)){
+  if (inst::Trigger::isAtomicTrigger( n ) && !n.getAttribute(aitdi)){
     //Already processed but new in this branch
     n.setAttribute(aitdi,true);
     added.insert( n );
@@ -71,7 +99,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
     n.setAttribute(AvailableInTermDb(),true);
     //if this is an atomic trigger, consider adding it
     //Call the children?
-    if( Trigger::isAtomicTrigger( n ) ){
+    if( inst::Trigger::isAtomicTrigger( n ) ){
       if( !n.hasAttribute(InstConstantAttribute()) ){
         Debug("term-db") << "register trigger term " << n << std::endl;
         //std::cout << "register trigger term " << n << std::endl;
@@ -370,3 +398,61 @@ const std::vector<Node> & TermDb::getParents(TNode n, TNode f, int arg){
   static std::vector<Node> empty;
   return empty;
 }
+
+void TermDb::computeVarContains( Node n ) {
+  if( d_var_contains.find( n )==d_var_contains.end() ){
+    d_var_contains[n].clear();
+    computeVarContains2( n, n );
+  }
+}
+
+void TermDb::computeVarContains2( Node n, Node parent ){
+  if( n.getKind()==INST_CONSTANT ){
+    if( std::find( d_var_contains[parent].begin(), d_var_contains[parent].end(), n )==d_var_contains[parent].end() ){
+      d_var_contains[parent].push_back( n );
+    }
+  }else{
+    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      computeVarContains2( n[i], parent );
+    }
+  }
+}
+
+bool TermDb::isVariableSubsume( Node n1, Node n2 ){
+  if( n1==n2 ){
+    return true;
+  }else{
+    //Notice() << "is variable subsume ? " << n1 << " " << n2 << std::endl;
+    computeVarContains( n1 );
+    computeVarContains( n2 );
+    for( int i=0; i<(int)d_var_contains[n2].size(); i++ ){
+      if( std::find( d_var_contains[n1].begin(), d_var_contains[n1].end(), d_var_contains[n2][i] )==d_var_contains[n1].end() ){
+        //Notice() << "no" << std::endl;
+        return false;
+      }
+    }
+    //Notice() << "yes" << std::endl;
+    return true;
+  }
+}
+
+void TermDb::getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ){
+  for( int i=0; i<(int)pats.size(); i++ ){
+    computeVarContains( pats[i] );
+    varContains[ pats[i] ].clear();
+    for( int j=0; j<(int)d_var_contains[pats[i]].size(); j++ ){
+      if( d_var_contains[pats[i]][j].getAttribute(InstConstantAttribute())==f ){
+        varContains[ pats[i] ].push_back( d_var_contains[pats[i]][j] );
+      }
+    }
+  }
+}
+
+void TermDb::getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ){
+  computeVarContains( n );
+  for( int j=0; j<(int)d_var_contains[n].size(); j++ ){
+    if( d_var_contains[n][j].getAttribute(InstConstantAttribute())==f ){
+      varContains.push_back( d_var_contains[n][j] );
+    }
+  }
+}
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 8106b5715..8e3b5b085 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -28,6 +28,10 @@ namespace theory {
 
 class QuantifiersEngine;
 
+namespace inst{
+  class Trigger;
+}
+
 namespace quantifiers {
 
 class TermArgTrie {
@@ -40,8 +44,34 @@ public:
   bool addTerm( QuantifiersEngine* qe, Node n ) { return addTerm2( qe, n, 0 ); }
 };/* class TermArgTrie */
 
+
+/** a trie of triggers */
+class TrTrie {
+private:
+  inst::Trigger* getTrigger2( std::vector< Node >& nodes );
+  void addTrigger2( std::vector< Node >& nodes, inst::Trigger* t );
+public:
+  TrTrie() : d_tr( NULL ){}
+  inst::Trigger* d_tr;
+  std::map< TNode, TrTrie* > d_children;
+  inst::Trigger* getTrigger( std::vector< Node >& nodes ){
+    std::vector< Node > temp;
+    temp.insert( temp.begin(), nodes.begin(), nodes.end() );
+    std::sort( temp.begin(), temp.end() );
+    return getTrigger2( temp );
+  }
+  void addTrigger( std::vector< Node >& nodes, inst::Trigger* t ){
+    std::vector< Node > temp;
+    temp.insert( temp.begin(), nodes.begin(), nodes.end() );
+    std::sort( temp.begin(), temp.end() );
+    return addTrigger2( temp, t );
+  }
+};/* class inst::Trigger::TrTrie */
+
+
 class TermDb {
   friend class ::CVC4::theory::QuantifiersEngine;
+  friend class ::CVC4::theory::inst::Trigger;
 private:
   /** reference to the quantifiers engine */
   QuantifiersEngine* d_quantEngine;
@@ -147,6 +177,28 @@ public:
                              const std::vector<Node> & nvars);
   /** get free variable for instantiation constant */
   Node getFreeVariableForInstConstant( Node n );
+
+//for triggers
+private:
+  /** helper function for compute var contains */
+  void computeVarContains2( Node n, Node parent );
+  /** all triggers will be stored in this trie */
+  TrTrie d_tr_trie;
+  /** var contains */
+  std::map< TNode, std::vector< TNode > > d_var_contains;
+public:
+  /** compute var contains */
+  void computeVarContains( Node n );
+  /** variables subsume, return true if n1 contains all free variables in n2 */
+  bool isVariableSubsume( Node n1, Node n2 );
+  /** get var contains for each of the patterns in pats */
+  void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains );
+  /** get var contains for node n */
+  void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains );
+  /** get trigger */
+  inst::Trigger* getTrigger( std::vector< Node >& nodes ){ return d_tr_trie.getTrigger( nodes ); }
+  /** add trigger */
+  void addTrigger( std::vector< Node >& nodes, inst::Trigger* t ){ d_tr_trie.addTrigger( nodes, t ); }
 };/* class TermDb */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 49a1f8332..f197c0885 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -21,6 +21,7 @@
 #include "theory/quantifiers/candidate_generator.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/quantifiers/options.h"
+#include "theory/quantifiers/term_database.h"
 
 using namespace std;
 using namespace CVC4;
@@ -31,36 +32,6 @@ using namespace CVC4::theory::inst;
 
 //#define NESTED_PATTERN_SELECTION
 
-Trigger* Trigger::TrTrie::getTrigger2( std::vector< Node >& nodes ){
-  if( nodes.empty() ){
-    return d_tr;
-  }else{
-    Node n = nodes.back();
-    nodes.pop_back();
-    if( d_children.find( n )!=d_children.end() ){
-      return d_children[n]->getTrigger2( nodes );
-    }else{
-      return NULL;
-    }
-  }
-}
-void Trigger::TrTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){
-  if( nodes.empty() ){
-    d_tr = t;
-  }else{
-    Node n = nodes.back();
-    nodes.pop_back();
-    if( d_children.find( n )==d_children.end() ){
-      d_children[n] = new TrTrie;
-    }
-    d_children[n]->addTrigger2( nodes, t );
-  }
-}
-
-/** trigger static members */
-std::map< TNode, std::vector< TNode > > Trigger::d_var_contains;
-Trigger::TrTrie Trigger::d_tr_trie;
-
 /** trigger class constructor */
 Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool smartTriggers ) :
 d_quantEngine( qe ), d_f( f ){
@@ -104,24 +75,6 @@ d_quantEngine( qe ), d_f( f ){
     }
   }
 }
-void Trigger::computeVarContains( Node n ) {
-  if( d_var_contains.find( n )==d_var_contains.end() ){
-    d_var_contains[n].clear();
-    computeVarContains2( n, n );
-  }
-}
-
-void Trigger::computeVarContains2( Node n, Node parent ){
-  if( n.getKind()==INST_CONSTANT ){
-    if( std::find( d_var_contains[parent].begin(), d_var_contains[parent].end(), n )==d_var_contains[parent].end() ){
-      d_var_contains[parent].push_back( n );
-    }
-  }else{
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      computeVarContains2( n[i], parent );
-    }
-  }
-}
 
 void Trigger::resetInstantiationRound(){
   d_mg->resetInstantiationRound( d_quantEngine );
@@ -169,9 +122,9 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
     std::map< Node, std::vector< Node > > patterns;
     for( int i=0; i<(int)temp.size(); i++ ){
       bool foundVar = false;
-      computeVarContains( temp[i] );
-      for( int j=0; j<(int)d_var_contains[ temp[i] ].size(); j++ ){
-        Node v = d_var_contains[ temp[i] ][j];
+      qe->getTermDatabase()->computeVarContains( temp[i] );
+      for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ temp[i] ].size(); j++ ){
+        Node v = qe->getTermDatabase()->d_var_contains[ temp[i] ][j];
         if( v.getAttribute(InstConstantAttribute())==f ){
           if( vars.find( v )==vars.end() ){
             vars[ v ] = true;
@@ -181,8 +134,8 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
       }
       if( foundVar ){
         trNodes.push_back( temp[i] );
-        for( int j=0; j<(int)d_var_contains[ temp[i] ].size(); j++ ){
-          Node v = d_var_contains[ temp[i] ][j];
+        for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ temp[i] ].size(); j++ ){
+          Node v = qe->getTermDatabase()->d_var_contains[ temp[i] ][j];
           patterns[ v ].push_back( temp[i] );
         }
       }
@@ -191,8 +144,8 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
     for( int i=0; i<(int)trNodes.size(); i++ ){
       bool keepPattern = false;
       Node n = trNodes[i];
-      for( int j=0; j<(int)d_var_contains[ n ].size(); j++ ){
-        Node v = d_var_contains[ n ][j];
+      for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){
+        Node v = qe->getTermDatabase()->d_var_contains[ n ][j];
         if( patterns[v].size()==1 ){
           keepPattern = true;
           break;
@@ -200,8 +153,8 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
       }
       if( !keepPattern ){
         //remove from pattern vector
-        for( int j=0; j<(int)d_var_contains[ n ].size(); j++ ){
-          Node v = d_var_contains[ n ][j];
+        for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){
+          Node v = qe->getTermDatabase()->d_var_contains[ n ][j];
           for( int k=0; k<(int)patterns[v].size(); k++ ){
             if( patterns[v][k]==n ){
               patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 );
@@ -222,7 +175,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
   if( trOption==TR_MAKE_NEW ){
     //static int trNew = 0;
     //static int trOld = 0;
-    //Trigger* t = d_tr_trie.getTrigger( trNodes );
+    //Trigger* t = qe->getTermDatabase()->getTrigger( trNodes );
     //if( t ){
     //  trOld++;
     //}else{
@@ -232,7 +185,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
     //  Notice() << "Trigger new old = " << trNew << " " << trOld << std::endl;
     //}
   }else{
-    Trigger* t = d_tr_trie.getTrigger( trNodes );
+    Trigger* t = qe->getTermDatabase()->getTrigger( trNodes );
     if( t ){
       if( trOption==TR_GET_OLD ){
         //just return old trigger
@@ -243,7 +196,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
     }
   }
   Trigger* t = new Trigger( qe, f, trNodes, matchOption, smartTriggers );
-  d_tr_trie.addTrigger( trNodes, t );
+  qe->getTermDatabase()->addTrigger( trNodes, t );
   return t;
 }
 Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption, bool smartTriggers ){
@@ -302,13 +255,13 @@ bool Trigger::isSimpleTrigger( Node n ){
 }
 
 /** filter all nodes that have instances */
-void Trigger::filterInstances( std::vector< Node >& nodes ){
+void Trigger::filterInstances( QuantifiersEngine* qe, std::vector< Node >& nodes ){
   std::vector< bool > active;
   active.resize( nodes.size(), true );
   for( int i=0; i<(int)nodes.size(); i++ ){
     for( int j=i+1; j<(int)nodes.size(); j++ ){
       if( active[i] && active[j] ){
-        int result = isInstanceOf( nodes[i], nodes[j] );
+        int result = isInstanceOf( qe, nodes[i], nodes[j] );
         if( result==1 ){
           active[j] = false;
         }else if( result==-1 ){
@@ -396,7 +349,7 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto
     collectPatTerms( qe, f, n, patTerms2, TS_ALL, false );
     std::vector< Node > temp;
     temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() );
-    filterInstances( temp );
+    filterInstances( qe, temp );
     if( temp.size()!=patTerms2.size() ){
       Debug("trigger-filter-instance") << "Filtered an instance: " << std::endl;
       Debug("trigger-filter-instance") << "Old: ";
@@ -430,7 +383,7 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto
 }
 
 /** is n1 an instance of n2 or vice versa? */
-int Trigger::isInstanceOf( Node n1, Node n2 ){
+int Trigger::isInstanceOf( QuantifiersEngine* qe, Node n1, Node n2 ){
   if( n1==n2 ){
     return 1;
   }else if( n1.getKind()==n2.getKind() ){
@@ -439,7 +392,7 @@ int Trigger::isInstanceOf( Node n1, Node n2 ){
         int result = 0;
         for( int i=0; i<(int)n1.getNumChildren(); i++ ){
           if( n1[i]!=n2[i] ){
-            int cResult = isInstanceOf( n1[i], n2[i] );
+            int cResult = isInstanceOf( qe, n1[i], n2[i] );
             if( cResult==0 ){
               return 0;
             }else if( cResult!=result ){
@@ -456,64 +409,27 @@ int Trigger::isInstanceOf( Node n1, Node n2 ){
     }
     return 0;
   }else if( n2.getKind()==INST_CONSTANT ){
-    computeVarContains( n1 );
+    qe->getTermDatabase()->computeVarContains( n1 );
     //if( std::find( d_var_contains[ n1 ].begin(), d_var_contains[ n1 ].end(), n2 )!=d_var_contains[ n1 ].end() ){
     //  return 1;
     //}
-    if( d_var_contains[ n1 ].size()==1 && d_var_contains[ n1 ][ 0 ]==n2 ){
+    if( qe->getTermDatabase()->d_var_contains[ n1 ].size()==1 &&
+        qe->getTermDatabase()->d_var_contains[ n1 ][ 0 ]==n2 ){
       return 1;
     }
   }else if( n1.getKind()==INST_CONSTANT ){
-    computeVarContains( n2 );
+    qe->getTermDatabase()->computeVarContains( n2 );
     //if( std::find( d_var_contains[ n2 ].begin(), d_var_contains[ n2 ].end(), n1 )!=d_var_contains[ n2 ].end() ){
     //  return -1;
     //}
-    if( d_var_contains[ n2 ].size()==1 && d_var_contains[ n2 ][ 0 ]==n1 ){
+    if( qe->getTermDatabase()->d_var_contains[ n2 ].size()==1 &&
+        qe->getTermDatabase()->d_var_contains[ n2 ][ 0 ]==n1 ){
       return 1;
     }
   }
   return 0;
 }
 
-bool Trigger::isVariableSubsume( Node n1, Node n2 ){
-  if( n1==n2 ){
-    return true;
-  }else{
-    //Notice() << "is variable subsume ? " << n1 << " " << n2 << std::endl;
-    computeVarContains( n1 );
-    computeVarContains( n2 );
-    for( int i=0; i<(int)d_var_contains[n2].size(); i++ ){
-      if( std::find( d_var_contains[n1].begin(), d_var_contains[n1].end(), d_var_contains[n2][i] )==d_var_contains[n1].end() ){
-        //Notice() << "no" << std::endl;
-        return false;
-      }
-    }
-    //Notice() << "yes" << std::endl;
-    return true;
-  }
-}
-
-void Trigger::getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ){
-  for( int i=0; i<(int)pats.size(); i++ ){
-    computeVarContains( pats[i] );
-    varContains[ pats[i] ].clear();
-    for( int j=0; j<(int)d_var_contains[pats[i]].size(); j++ ){
-      if( d_var_contains[pats[i]][j].getAttribute(InstConstantAttribute())==f ){
-        varContains[ pats[i] ].push_back( d_var_contains[pats[i]][j] );
-      }
-    }
-  }
-}
-
-void Trigger::getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ){
-  computeVarContains( n );
-  for( int j=0; j<(int)d_var_contains[n].size(); j++ ){
-    if( d_var_contains[n][j].getAttribute(InstConstantAttribute())==f ){
-      varContains.push_back( d_var_contains[n][j] );
-    }
-  }
-}
-
 bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs ){
   if( n.getKind()==PLUS ){
     Assert( coeffs.empty() );
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 207cef5d9..686fda241 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -28,11 +28,6 @@ namespace inst {
 //a collect of nodes representing a trigger
 class Trigger {
 private:
-  /** computation of variable contains */
-  static std::map< TNode, std::vector< TNode > > d_var_contains;
-  static void computeVarContains( Node n );
-  static void computeVarContains2( Node n, Node parent );
-private:
   /** the quantifiers engine */
   QuantifiersEngine* d_quantEngine;
   /** the quantifier this trigger is for */
@@ -40,31 +35,6 @@ private:
   /** match generators */
   IMGenerator* d_mg;
 private:
-  /** a trie of triggers */
-  class TrTrie {
-  private:
-    Trigger* getTrigger2( std::vector< Node >& nodes );
-    void addTrigger2( std::vector< Node >& nodes, Trigger* t );
-  public:
-    TrTrie() : d_tr( NULL ){}
-    Trigger* d_tr;
-    std::map< TNode, TrTrie* > d_children;
-    Trigger* getTrigger( std::vector< Node >& nodes ){
-      std::vector< Node > temp;
-      temp.insert( temp.begin(), nodes.begin(), nodes.end() );
-      std::sort( temp.begin(), temp.end() );
-      return getTrigger2( temp );
-    }
-    void addTrigger( std::vector< Node >& nodes, Trigger* t ){
-      std::vector< Node > temp;
-      temp.insert( temp.begin(), nodes.begin(), nodes.end() );
-      std::sort( temp.begin(), temp.end() );
-      return addTrigger2( temp, t );
-    }
-  };/* class Trigger::TrTrie */
-  /** all triggers will be stored in this trie */
-  static TrTrie d_tr_trie;
-private:
   /** trigger constructor */
   Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes, int matchOption = 0, bool smartTriggers = false );
 public:
@@ -138,14 +108,9 @@ public:
   static bool isAtomicTrigger( Node n );
   static bool isSimpleTrigger( Node n );
   /** filter all nodes that have instances */
-  static void filterInstances( std::vector< Node >& nodes );
+  static void filterInstances( QuantifiersEngine* qe, std::vector< Node >& nodes );
   /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
-  static int isInstanceOf( Node n1, Node n2 );
-  /** variables subsume, return true if n1 contains all free variables in n2 */
-  static bool isVariableSubsume( Node n1, Node n2 );
-  /** get var contains */
-  static void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains );
-  static void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains );
+  static int isInstanceOf( QuantifiersEngine* qe, Node n1, Node n2 );
   /** get pattern arithmetic */
   static bool getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs );
 
diff --git a/src/theory/uf/inst_strategy.cpp b/src/theory/uf/inst_strategy.cpp
index 9d644ae8d..5ce88177a 100644
--- a/src/theory/uf/inst_strategy.cpp
+++ b/src/theory/uf/inst_strategy.cpp
@@ -236,7 +236,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
     d_quantEngine->getPhaseReqTerms( f, patTermsF );
     //sort into single/multi triggers
     std::map< Node, std::vector< Node > > varContains;
-    Trigger::getVarContains( f, patTermsF, varContains );
+    d_quantEngine->getTermDatabase()->getVarContains( f, patTermsF, varContains );
     for( std::map< Node, std::vector< Node > >::iterator it = varContains.begin(); it != varContains.end(); ++it ){
       if( it->second.size()==f[0].getNumChildren() ){
         d_patTerms[0][f].push_back( it->first );