replaced all static member data from rewrite rule triggers, added infrastructure for recognizing quantifier macros

14 files changed, 367 insertions, 316 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e1c30c6c7..16de7957a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -65,6 +65,7 @@
 #include "prop/options.h"
 #include "theory/arrays/options.h"
 #include "util/sort_inference.h"
+#include "theory/quantifiers/macros.h"
 
 using namespace std;
 using namespace CVC4;
@@ -1131,32 +1132,32 @@ void SmtEngine::defineFunction(Expr func,
 
 
 Node SmtEnginePrivate::getBVDivByZero(Kind k, unsigned width) {
-  NodeManager* nm = d_smt.d_nodeManager; 
+  NodeManager* nm = d_smt.d_nodeManager;
   if (k == kind::BITVECTOR_UDIV) {
     if (d_BVDivByZero.find(width) == d_BVDivByZero.end()) {
       // lazily create the function symbols
       std::ostringstream os;
-      os << "BVUDivByZero_" << width; 
+      os << "BVUDivByZero_" << width;
       Node divByZero = nm->mkSkolem(os.str(),
                                     nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
                                     "partial bvudiv", NodeManager::SKOLEM_EXACT_NAME);
-      d_BVDivByZero[width] = divByZero; 
+      d_BVDivByZero[width] = divByZero;
     }
-    return d_BVDivByZero[width]; 
+    return d_BVDivByZero[width];
   }
   else if (k == kind::BITVECTOR_UREM) {
     if (d_BVRemByZero.find(width) == d_BVRemByZero.end()) {
       std::ostringstream os;
-      os << "BVURemByZero_" << width; 
+      os << "BVURemByZero_" << width;
       Node divByZero = nm->mkSkolem(os.str(),
                                     nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
                                     "partial bvurem", NodeManager::SKOLEM_EXACT_NAME);
       d_BVRemByZero[width] = divByZero;
     }
-    return d_BVRemByZero[width]; 
-  } 
+    return d_BVRemByZero[width];
+  }
 
-  Unreachable(); 
+  Unreachable();
 }
 
 
@@ -1164,15 +1165,15 @@ Node SmtEnginePrivate::expandBVDivByZero(TNode n) {
   // we only deal wioth the unsigned division operators as the signed ones should have been
   // expanded in terms of the unsigned operators
   NodeManager* nm = d_smt.d_nodeManager;
-  unsigned width = n.getType().getBitVectorSize(); 
+  unsigned width = n.getType().getBitVectorSize();
   Node divByZero = getBVDivByZero(n.getKind(), width);
   TNode num = n[0], den = n[1];
-  Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(BitVector(width, Integer(0)))); 
+  Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(BitVector(width, Integer(0))));
   Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
   Node divTotalNumDen = nm->mkNode(n.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL :
                                    kind::BITVECTOR_UREM_TOTAL, num, den);
-  Node node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen); 
-  return node; 
+  Node node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
+  return node;
 }
 
 
@@ -1205,12 +1206,12 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
     node = bv::TheoryBVRewriter::eliminateBVSDiv(node);
     break;
   }
-    
+
  case kind::BITVECTOR_UDIV:
  case kind::BITVECTOR_UREM: {
-   node = expandBVDivByZero(node); 
-    break; 
-  }    
+   node = expandBVDivByZero(node);
+    break;
+  }
   case kind::DIVISION: {
     // partial function: division
     if(d_smt.d_logic.isLinear()) {
@@ -2060,9 +2061,14 @@ void SmtEnginePrivate::processAssertions() {
   }
   dumpAssertions("post-skolem-quant", d_assertionsToPreprocess);
 
+  if( options::macrosQuant() ){
+    //quantifiers macro expansion
+    QuantifierMacros qm;
+    qm.simplify( d_assertionsToPreprocess );
+  }
+
   if( options::sortInference() ){
     //sort inference technique
-    //TODO: use this as a rewrite technique here?
     SortInference si;
     si.simplify( d_assertionsToPreprocess );
   }
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 8bd151f31..e06cf0d12 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -985,7 +985,7 @@ Node TheoryArith::axiomIteForTotalDivision(Node div_tot){
   Comparison invEq = Comparison::mkComparison(EQUAL, n, d * div_tot_p);
   Comparison zeroEq = Comparison::mkComparison(EQUAL, div_tot_p, Polynomial::mkZero());
   Node dEq0 = (d.getNode()).eqNode(mkRationalNode(0));
-  Node ite = dEq0.iteNode(zeroEq.getNode(), invEq.getNode()); 
+  Node ite = dEq0.iteNode(zeroEq.getNode(), invEq.getNode());
 
   return ite;
 }
diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am
index ed60e77a9..371aa5543 100644
--- a/src/theory/quantifiers/Makefile.am
+++ b/src/theory/quantifiers/Makefile.am
@@ -42,7 +42,9 @@ libquantifiers_la_SOURCES = \
 	quant_util.h \
 	quant_util.cpp \
 	inst_match_generator.h \
-	inst_match_generator.cpp
+	inst_match_generator.cpp \
+	macros.h \
+	macros.cpp
 
 EXTRA_DIST = \
 	kinds \
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
new file mode 100755
index 000000000..10db57184
--- /dev/null
+++ b/src/theory/quantifiers/macros.cpp
@@ -0,0 +1,128 @@
+/*********************                                                        */

+/*! \file macros.cpp

+ ** \verbatim

+ ** Original author: ajreynol

+ ** Major contributors: none

+ ** Minor contributors (to current version): none

+ ** This file is part of the CVC4 prototype.

+ ** Copyright (c) 2009-2012  New York University and The University of Iowa

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

+ **

+ ** \brief Sort inference module

+ **

+ ** This class implements quantifiers macro definitions.

+ **/

+

+#include <vector>

+

+#include "theory/quantifiers/macros.h"

+

+using namespace CVC4;

+using namespace std;

+using namespace CVC4::theory;

+using namespace CVC4::theory::quantifiers;

+using namespace CVC4::kind;

+using namespace CVC4::context;

+

+void QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){

+  //first, collect macro definitions

+  for( size_t i=0; i<assertions.size(); i++ ){

+    if( assertions[i].getKind()==FORALL ){

+      std::vector< Node > args;

+      for( size_t j=0; j<assertions[i][0].getNumChildren(); j++ ){

+        args.push_back( assertions[i][0][j] );

+      }

+      //look at the body of the quantifier for macro definition

+      process( assertions[i][1], true, args, assertions[i] );

+    }

+  }

+  //now, rewrite based on macro definitions

+  for( size_t i=0; i<assertions.size(); i++ ){

+    assertions[i] = simplify( assertions[i] );

+  }

+}

+

+bool QuantifierMacros::containsOp( Node n, Node op ){

+  if( n.getKind()==APPLY_UF ){

+    if( n.getOperator()==op ){

+      return true;

+    }

+  }

+  for( size_t i=0; i<n.getNumChildren(); i++ ){

+    if( containsOp( n[i], op ) ){

+      return true;

+    }

+  }

+  return false;

+}

+

+bool QuantifierMacros::isMacroKind( Node n, bool pol ){

+  return pol && ( n.getKind()==EQUAL || n.getKind()==IFF );

+}

+

+void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){

+  if( n.getKind()==NOT ){

+    process( n[0], !pol, args, f );

+  }else if( n.getKind()==AND || n.getKind()==OR || n.getKind()==IMPLIES ){

+    //bool favorPol = (n.getKind()==AND)==pol;

+    //conditional?

+  }else if( n.getKind()==ITE ){

+    //can not do anything

+  }else{

+    //literal case

+    //only care about literals in form of (basis, definition)

+    if( isMacroKind( n, pol ) ){

+      for( int i=0; i<2; i++ ){

+        int j = i==0 ? 1 : 0;

+        //check if n[i] is the basis for a macro

+        if( n[i].getKind()==APPLY_UF ){

+          //make sure it doesn't occur in the potential definition

+          if( !containsOp( n[j], n[i].getOperator() ) ){

+            //bool usable = true;

+            //for( size_j a=0; a<n[i].getNumChildren(); a++ )

+            //  if( std::find( args.begin(), args.end(), n[i][a] )==args.end() ){

+            //  }

+            //}

+            Trace("macros") << n << " is possible macro in " << f << std::endl;

+          }

+        }

+      }

+    }

+  }

+}

+

+Node QuantifierMacros::simplify( Node n ){

+#if 0

+  std::vector< Node > children;

+  bool childChanged = false;

+  for( size_t i=0; i<n.getNumChildren(); i++ ){

+    Node nn = simplify( n[i] );

+    children.push_back( nn );

+    childChanged = childChanged || nn!=n[i];

+  }

+  if( n.getKind()==APPLY_UF ){

+    Node op = n.getOperator();

+    if( d_macro_defs.find( op )!=d_macro_defs.end() ){

+      //do subsitutition

+      Node ns = d_macro_defs[op].second;

+      std::vector< Node > vars;

+      for( size_t i = 0; i<d_macro_defs[op].first.getNumChildren(); i++ ){

+        vars.push_back( d_macro_defs[op].first[i] );

+      }

+      ns = ns.substitute( vars.begin(), vars.end(), children.begin(), children.end() );

+      return ns;

+    }

+  }

+  if( childChanged ){

+    if( n.isParameterized() ){

+      std::insert( children.begin(), n.getOperator() );

+    }

+    return NodeManager::currentNM()->mkNode( n.getKind(), children );

+  }else{

+    return n;

+  }

+#else

+  return n;

+#endif

+}

diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h
new file mode 100755
index 000000000..d93070481
--- /dev/null
+++ b/src/theory/quantifiers/macros.h
@@ -0,0 +1,51 @@
+/*********************                                                        */

+/*! \file macros.h

+ ** \verbatim

+ ** Original author: ajreynol

+ ** Major contributors: none

+ ** Minor contributors (to current version): none

+ ** This file is part of the CVC4 prototype.

+ ** Copyright (c) 2009-2012  New York University and The University of Iowa

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

+ **

+ ** \brief Pre-process step for detecting quantifier macro definitions

+ **/

+

+#include "cvc4_private.h"

+

+#ifndef __CVC4__QUANTIFIERS_MACROS_H

+#define __CVC4__QUANTIFIERS_MACROS_H

+

+#include <iostream>

+#include <string>

+#include <vector>

+#include <map>

+#include "expr/node.h"

+#include "expr/type_node.h"

+

+namespace CVC4 {

+namespace theory {

+namespace quantifiers {

+

+class QuantifierMacros{

+private:

+  void process( Node n, bool pol, std::vector< Node >& args, Node f );

+  bool containsOp( Node n, Node op );

+  bool isMacroKind( Node n, bool pol );

+  //map from operators to macro definition ( basis, definition )

+  std::map< Node, std::pair< Node, Node > > d_macro_defs;

+private:

+  Node simplify( Node n );

+public:

+  QuantifierMacros(){}

+  ~QuantifierMacros(){}

+

+  void simplify( std::vector< Node >& assertions, bool doRewrite = false );

+};

+

+}

+}

+}

+

+#endif

diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 2c36520e4..24d0c4047 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -37,6 +37,10 @@ option cnfQuant --cnf-quant bool :default false
 option preSkolemQuant --pre-skolem-quant bool :default false
  apply skolemization eagerly to bodies of quantified formulas
 
+# Whether to perform quantifier macro expansion
+option macrosQuant --macros-quant bool :default false
+ perform quantifiers macro expansions
+
 # Whether to use smart triggers
 option smartTriggers /--disable-smart-triggers bool :default true
  disable smart triggers
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index b55e8abdf..2c2ee0bfe 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -468,6 +468,77 @@ void TermDb::getVarContainsNode( Node f, Node n, std::vector< Node >& varContain
   }
 }
 
+/** is n1 an instance of n2 or vice versa? */
+int TermDb::isInstanceOf( Node n1, Node n2 ){
+  if( n1==n2 ){
+    return 1;
+  }else if( n1.getKind()==n2.getKind() ){
+    if( n1.getKind()==APPLY_UF ){
+      if( n1.getOperator()==n2.getOperator() ){
+        int result = 0;
+        for( int i=0; i<(int)n1.getNumChildren(); i++ ){
+          if( n1[i]!=n2[i] ){
+            int cResult = isInstanceOf( n1[i], n2[i] );
+            if( cResult==0 ){
+              return 0;
+            }else if( cResult!=result ){
+              if( result!=0 ){
+                return 0;
+              }else{
+                result = cResult;
+              }
+            }
+          }
+        }
+        return result;
+      }
+    }
+    return 0;
+  }else if( n2.getKind()==INST_CONSTANT ){
+    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 ){
+      return 1;
+    }
+  }else if( n1.getKind()==INST_CONSTANT ){
+    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 ){
+      return 1;
+    }
+  }
+  return 0;
+}
+
+void TermDb::filterInstances( 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] );
+        if( result==1 ){
+          active[j] = false;
+        }else if( result==-1 ){
+          active[i] = false;
+        }
+      }
+    }
+  }
+  std::vector< Node > temp;
+  for( int i=0; i<(int)nodes.size(); i++ ){
+    if( active[i] ){
+      temp.push_back( nodes[i] );
+    }
+  }
+  nodes.clear();
+  nodes.insert( nodes.begin(), temp.begin(), temp.end() );
+}
+
 void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){
   if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){
     d_op_triggers[op].push_back( tr );
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 2bae5a043..a1f1de1dc 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -65,6 +65,10 @@ class QuantifiersEngine;
 namespace inst{
   class Trigger;
 }
+namespace rrinst{
+  class Trigger;
+}
+
 
 namespace quantifiers {
 
@@ -82,6 +86,7 @@ public:
 class TermDb {
   friend class ::CVC4::theory::QuantifiersEngine;
   friend class ::CVC4::theory::inst::Trigger;
+  friend class ::CVC4::theory::rrinst::Trigger;
 private:
   /** reference to the quantifiers engine */
   QuantifiersEngine* d_quantEngine;
@@ -218,6 +223,10 @@ public:
   void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains );
   /** register trigger (for eager quantifier instantiation) */
   void registerTrigger( inst::Trigger* tr, Node op );
+  /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
+  int isInstanceOf( Node n1, Node n2 );
+  /** filter all nodes that have instances */
+  void filterInstances( std::vector< Node >& nodes );
 };/* class TermDb */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 67b2e6bd8..a9c5e8b96 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -250,32 +250,6 @@ bool Trigger::isSimpleTrigger( Node n ){
   }
 }
 
-/** filter all nodes that have instances */
-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( qe, nodes[i], nodes[j] );
-        if( result==1 ){
-          active[j] = false;
-        }else if( result==-1 ){
-          active[i] = false;
-        }
-      }
-    }
-  }
-  std::vector< Node > temp;
-  for( int i=0; i<(int)nodes.size(); i++ ){
-    if( active[i] ){
-      temp.push_back( nodes[i] );
-    }
-  }
-  nodes.clear();
-  nodes.insert( nodes.begin(), temp.begin(), temp.end() );
-}
-
 
 bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ){
   if( patMap.find( n )==patMap.end() ){
@@ -345,7 +319,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( qe, temp );
+    qe->getTermDatabase()->filterInstances( temp );
     if( temp.size()!=patTerms2.size() ){
       Debug("trigger-filter-instance") << "Filtered an instance: " << std::endl;
       Debug("trigger-filter-instance") << "Old: ";
@@ -378,54 +352,6 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto
   }
 }
 
-/** is n1 an instance of n2 or vice versa? */
-int Trigger::isInstanceOf( QuantifiersEngine* qe, Node n1, Node n2 ){
-  if( n1==n2 ){
-    return 1;
-  }else if( n1.getKind()==n2.getKind() ){
-    if( n1.getKind()==APPLY_UF ){
-      if( n1.getOperator()==n2.getOperator() ){
-        int result = 0;
-        for( int i=0; i<(int)n1.getNumChildren(); i++ ){
-          if( n1[i]!=n2[i] ){
-            int cResult = isInstanceOf( qe, n1[i], n2[i] );
-            if( cResult==0 ){
-              return 0;
-            }else if( cResult!=result ){
-              if( result!=0 ){
-                return 0;
-              }else{
-                result = cResult;
-              }
-            }
-          }
-        }
-        return result;
-      }
-    }
-    return 0;
-  }else if( n2.getKind()==INST_CONSTANT ){
-    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( qe->getTermDatabase()->d_var_contains[ n1 ].size()==1 &&
-        qe->getTermDatabase()->d_var_contains[ n1 ][ 0 ]==n2 ){
-      return 1;
-    }
-  }else if( n1.getKind()==INST_CONSTANT ){
-    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( qe->getTermDatabase()->d_var_contains[ n2 ].size()==1 &&
-        qe->getTermDatabase()->d_var_contains[ n2 ][ 0 ]==n1 ){
-      return 1;
-    }
-  }
-  return 0;
-}
-
 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 267debb02..6fcd316f4 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -108,10 +108,6 @@ public:
   static bool isUsableTrigger( Node n, Node f );
   static bool isAtomicTrigger( Node n );
   static bool isSimpleTrigger( Node n );
-  /** filter all nodes that have instances */
-  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( 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/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 3f6ba8a0f..b4e046506 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -26,6 +26,7 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/rewriterules/efficient_e_matching.h"
+#include "theory/rewriterules/rr_trigger.h"
 
 using namespace std;
 using namespace CVC4;
@@ -40,6 +41,7 @@ d_quant_rel( false ){ //currently do not care about relevance
   d_eq_query = new EqualityQueryQuantifiersEngine( this );
   d_term_db = new quantifiers::TermDb( this );
   d_tr_trie = new inst::TriggerTrie;
+  d_rr_tr_trie = new rrinst::TriggerTrie;
   d_eem = new EfficientEMatcher( this );
   d_hasAddedLemma = false;
 
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 8fc6253ac..20972a6a1 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -68,6 +68,10 @@ namespace inst {
   class TriggerTrie;
 }/* CVC4::theory::inst */
 
+namespace rrinst {
+  class TriggerTrie;
+}/* CVC4::theory::inst */
+
 class EfficientEMatcher;
 class EqualityQueryQuantifiersEngine;
 
@@ -108,6 +112,8 @@ private:
   quantifiers::TermDb* d_term_db;
   /** all triggers will be stored in this trie */
   inst::TriggerTrie* d_tr_trie;
+  /** all triggers for rewrite rules will be stored in this trie */
+  rrinst::TriggerTrie* d_rr_tr_trie;
   /** extended model object */
   quantifiers::FirstOrderModel* d_model;
 private:
@@ -193,6 +199,8 @@ public:
   quantifiers::TermDb* getTermDatabase() { return d_term_db; }
   /** get trigger database */
   inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
+  /** get rewrite trigger database */
+  rrinst::TriggerTrie* getRRTriggerDatabase() { return d_rr_tr_trie; }
   /** add term to database */
   void addTermToDatabase( Node n, bool withinQuant = false );
 public:
diff --git a/src/theory/rewriterules/rr_trigger.cpp b/src/theory/rewriterules/rr_trigger.cpp
index 545c47bcd..ad77f0bcb 100644
--- a/src/theory/rewriterules/rr_trigger.cpp
+++ b/src/theory/rewriterules/rr_trigger.cpp
@@ -26,43 +26,9 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::rrinst;
 
-//#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< Node, std::vector< Node > > Trigger::d_var_contains;
-int Trigger::trCount = 0;
-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 ){
-  trCount++;
   d_nodes.insert( d_nodes.begin(), nodes.begin(), nodes.end() );
   Debug("trigger") << "Trigger for " << f << ": " << d_nodes << std::endl;
   if(matchOption == MATCH_GEN_DEFAULT) d_mg = mkPatterns( d_nodes, qe );
@@ -80,24 +46,6 @@ d_quantEngine( qe ), d_f( f ){
     ++(qe->d_statistics.d_multi_triggers);
   }
 }
-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 );
@@ -141,9 +89,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;
@@ -153,8 +101,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] );
         }
       }
@@ -163,8 +111,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;
@@ -172,8 +120,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 );
@@ -194,7 +142,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->getTriggerDatabase()->getTrigger( trNodes );
     //if( t ){
     //  trOld++;
     //}else{
@@ -204,7 +152,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
     //  std::cout << "Trigger new old = " << trNew << " " << trOld << std::endl;
     //}
   }else{
-    Trigger* t = d_tr_trie.getTrigger( trNodes );
+    Trigger* t = qe->getRRTriggerDatabase()->getTrigger( trNodes );
     if( t ){
       if( trOption==TR_GET_OLD ){
         //just return old trigger
@@ -215,7 +163,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->getRRTriggerDatabase()->addTrigger( trNodes, t );
   return t;
 }
 Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption, bool smartTriggers ){
@@ -264,32 +212,6 @@ bool Trigger::isSimpleTrigger( Node n ){
   }
 }
 
-/** filter all nodes that have instances */
-void Trigger::filterInstances( 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] );
-        if( result==1 ){
-          active[j] = false;
-        }else if( result==-1 ){
-          active[i] = false;
-        }
-      }
-    }
-  }
-  std::vector< Node > temp;
-  for( int i=0; i<(int)nodes.size(); i++ ){
-    if( active[i] ){
-      temp.push_back( nodes[i] );
-    }
-  }
-  nodes.clear();
-  nodes.insert( nodes.begin(), temp.begin(), temp.end() );
-}
-
 
 bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ){
   if( patMap.find( n )==patMap.end() ){
@@ -359,7 +281,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 );
+    qe->getTermDatabase()->filterInstances( temp );
     if( temp.size()!=patTerms2.size() ){
       Debug("trigger-filter-instance") << "Filtered an instance: " << std::endl;
       Debug("trigger-filter-instance") << "Old: ";
@@ -392,91 +314,6 @@ 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 ){
-  if( n1==n2 ){
-    return 1;
-  }else if( n1.getKind()==n2.getKind() ){
-    if( n1.getKind()==APPLY_UF ){
-      if( n1.getOperator()==n2.getOperator() ){
-        int result = 0;
-        for( int i=0; i<(int)n1.getNumChildren(); i++ ){
-          if( n1[i]!=n2[i] ){
-            int cResult = isInstanceOf( n1[i], n2[i] );
-            if( cResult==0 ){
-              return 0;
-            }else if( cResult!=result ){
-              if( result!=0 ){
-                return 0;
-              }else{
-                result = cResult;
-              }
-            }
-          }
-        }
-        return result;
-      }
-    }
-    return 0;
-  }else if( n2.getKind()==INST_CONSTANT ){
-    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 ){
-      return 1;
-    }
-  }else if( n1.getKind()==INST_CONSTANT ){
-    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 ){
-      return 1;
-    }
-  }
-  return 0;
-}
-
-bool Trigger::isVariableSubsume( Node n1, Node n2 ){
-  if( n1==n2 ){
-    return true;
-  }else{
-    //std::cout << "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() ){
-        //std::cout << "no" << std::endl;
-        return false;
-      }
-    }
-    //std::cout << "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() );
@@ -519,3 +356,31 @@ bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coef
   }
   return false;
 }
+
+
+
+Trigger* TriggerTrie::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 TriggerTrie::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 TriggerTrie;
+    }
+    d_children[n]->addTrigger2( nodes, t );
+  }
+}
diff --git a/src/theory/rewriterules/rr_trigger.h b/src/theory/rewriterules/rr_trigger.h
index 99e7bf3d3..7be5d1507 100644
--- a/src/theory/rewriterules/rr_trigger.h
+++ b/src/theory/rewriterules/rr_trigger.h
@@ -25,13 +25,6 @@ namespace rrinst {
 
 //a collect of nodes representing a trigger
 class Trigger {
-public:
-  static int trCount;
-private:
-  /** computation of variable contains */
-  static std::map< Node, std::vector< Node > > d_var_contains;
-  static void computeVarContains( Node n );
-  static void computeVarContains2( Node n, Node parent );
 private:
   /** the quantifiers engine */
   QuantifiersEngine* d_quantEngine;
@@ -40,32 +33,6 @@ private:
   /** match generators */
   PatsMatcher * 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< Node, 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 );
-    }
-  };
-  /** 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,15 +105,6 @@ public:
   }
   static bool isUsableTrigger( std::vector< Node >& nodes, Node f );
   static bool isSimpleTrigger( Node n );
-  /** filter all nodes that have instances */
-  static void filterInstances( 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 );
   /** get pattern arithmetic */
   static bool getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs );
 
@@ -165,6 +123,31 @@ inline std::ostream& operator<<(std::ostream& out, const Trigger & tr) {
   return out;
 }
 
+/** a trie of triggers */
+class TriggerTrie
+{
+private:
+  Trigger* getTrigger2( std::vector< Node >& nodes );
+  void addTrigger2( std::vector< Node >& nodes, Trigger* t );
+public:
+  TriggerTrie() : d_tr( NULL ){}
+  Trigger* d_tr;
+  std::map< Node, TriggerTrie* > 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 );
+  }
+};
+
+
 }/* CVC4::theory::rrinst namespace */
 
 }/* CVC4::theory namespace */