More optimizations to --macros-quant, add --macros-quant-mode=ground-uf. Cleanup varContains caches in term db. Fix bug related to macros in non-tracing builds.

9 files changed, 229 insertions, 216 deletions

diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index c26aea465..163005806 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -22,6 +22,8 @@
 #include "smt/smt_engine_scope.h"
 #include "theory/quantifiers/modes.h"
 #include "theory/quantifiers/options.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/trigger.h"
 
 using namespace CVC4;
 using namespace std;
@@ -31,26 +33,14 @@ using namespace CVC4::kind;
 
 
 bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){
-  unsigned rmax = options::macrosQuantMode()==MACROS_QUANT_MODE_GROUND ? 1 : 2;
+  unsigned rmax = options::macrosQuantMode()==MACROS_QUANT_MODE_ALL ? 2 : 1;
   for( unsigned r=0; r<rmax; r++ ){
     d_ground_macros = (r==0);
     Trace("macros") << "Find macros, ground=" << d_ground_macros << "..." << std::endl;
     //first, collect macro definitions
-    std::map< unsigned, Node > simp_assertions;
-    int last_macro = -1;
     for( int i=0; i<(int)assertions.size(); i++ ){
       Trace("macros-debug") << "  process assertion " << assertions[i] << std::endl;
-      Node curr = assertions[i];
-      //do simplification before process
-      if( doRewrite && !d_macro_defs_new.empty() ){
-        curr = simplify( assertions[i] );
-        curr = Rewriter::rewrite( curr );
-        if( curr!=assertions[i] ){
-          simp_assertions[i] = curr;
-        }
-      }
-      if( processAssertion( curr ) ){
-        last_macro = i;
+      if( processAssertion( assertions[i] ) ){
         //process this assertion again
         i--;
       }
@@ -61,15 +51,7 @@ bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite
       Trace("macros") << "Do simplifications..." << std::endl;
       //now, rewrite based on macro definitions
       for( unsigned i=0; i<assertions.size(); i++ ){
-        Node curr = assertions[i];
-        std::map< unsigned, Node >::iterator it = simp_assertions.find( i );
-        if( it!=simp_assertions.end() ){
-          curr = it->second;
-        }
-        //simplify again if before last macro
-        if( (int)i<last_macro ){
-          curr = simplify( curr );
-        }
+        Node curr = simplify( assertions[i] );
         if( curr!=assertions[i] ){
           curr = Rewriter::rewrite( curr );
           Trace("macros-rewrite") << "Rewrite " << assertions[i] << " to " << curr << std::endl;
@@ -84,8 +66,8 @@ bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite
       }
     }
   }
-  for( int i=0; i<(int)assertions.size(); i++ ){
-    if( Trace.isOn("macros-warn") ){
+  if( Trace.isOn("macros-warn") ){
+    for( int i=0; i<(int)assertions.size(); i++ ){
       debugMacroDefinition( assertions[i], assertions[i] );
     }
   }
@@ -99,47 +81,45 @@ bool QuantifierMacros::processAssertion( Node n ) {
         return true;
       }
     }
-    return false;
-  }else if( n.getKind()==FORALL ){
+  }else if( n.getKind()==FORALL && d_quant_macros.find( n )==d_quant_macros.end() ){
     std::vector< Node > args;
     for( size_t j=0; j<n[0].getNumChildren(); j++ ){
       args.push_back( n[0][j] );
     }
+    Node nproc = n[1];
+    if( !d_macro_defs_new.empty() ){
+      nproc = simplify( nproc );
+      if( nproc!=n[1] ){
+        nproc = Rewriter::rewrite( nproc );
+      }
+    }
     //look at the body of the quantifier for macro definition
-    return process( n[1], true, args, n );
-  }else{
-    return false;
+    if( process( nproc, true, args, n ) ){
+      d_quant_macros[n] = true;
+      return true;
+    }
   }
+  return false;
 }
 
-bool QuantifierMacros::contains( Node n, Node n_s ){
-  if( n==n_s ){
-    return true;
-  }else{
-    for( size_t i=0; i<n.getNumChildren(); i++ ){
-      if( contains( n[i], n_s ) ){
+bool QuantifierMacros::containsBadOp( Node n, Node op, std::vector< Node >& opc, std::map< Node, bool >& visited ){
+  if( visited.find( n )==visited.end() ){
+    visited[n] = true;
+    if( n.getKind()==APPLY_UF ){
+      Node nop = n.getOperator();
+      if( nop==op || d_macro_defs.find( nop )!=d_macro_defs.end()  ){
         return true;
       }
-    }
-    return false;
-  }
-}
-
-bool QuantifierMacros::containsBadOp( Node n, Node op, std::vector< Node >& opc ){
-  if( n.getKind()==APPLY_UF ){
-    Node nop = n.getOperator();
-    if( nop==op || d_macro_defs.find( nop )!=d_macro_defs.end()  ){
+      if( std::find( opc.begin(), opc.end(), nop )==opc.end() ){
+        opc.push_back( nop );
+      }
+    }else if( d_ground_macros && n.getKind()==FORALL ){
       return true;
     }
-    if( std::find( opc.begin(), opc.end(), nop )==opc.end() ){
-      opc.push_back( nop );
-    }
-  }else if( d_ground_macros && n.getKind()==FORALL ){
-    return true;
-  }
-  for( size_t i=0; i<n.getNumChildren(); i++ ){
-    if( containsBadOp( n[i], op, opc ) ){
-      return true;
+    for( size_t i=0; i<n.getNumChildren(); i++ ){
+      if( containsBadOp( n[i], op, opc, visited ) ){
+        return true;
+      }
     }
   }
   return false;
@@ -149,6 +129,19 @@ bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){
   return pol && ( n.getKind()==EQUAL || n.getKind()==IFF );
 }
 
+bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) {
+  Node icn = d_qe->getTermDatabase()->getInstConstantNode( n, f );
+  Trace("macros-debug2") << "Get free variables in " << icn << std::endl;
+  std::vector< Node > var;
+  d_qe->getTermDatabase()->getVarContainsNode( f, icn, var );
+  Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl;
+  std::vector< Node > trigger_var;
+  inst::Trigger::getTriggerVariables( d_qe, icn, f, trigger_var );
+  Trace("macros-debug2") << "Done." << std::endl;
+  //only if all variables are also trigger variables
+  return trigger_var.size()>=var.size();
+}
+
 bool QuantifierMacros::isBoundVarApplyUf( Node n ) {
   Assert( n.getKind()==APPLY_UF );
   TypeNode tn = n.getOperator().getType();
@@ -168,22 +161,25 @@ bool QuantifierMacros::isBoundVarApplyUf( Node n ) {
   return true;
 }
 
-void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidates ){
-  if( n.getKind()==APPLY_UF ){
-    if( isBoundVarApplyUf( n ) ){
-      candidates.push_back( n );
-    }
-  }else if( n.getKind()==PLUS ){
-    for( size_t i=0; i<n.getNumChildren(); i++ ){
-      getMacroCandidates( n[i], candidates );
-    }
-  }else if( n.getKind()==MULT ){
-    //if the LHS is a constant
-    if( n.getNumChildren()==2 && n[0].isConst() ){
-      getMacroCandidates( n[1], candidates );
+void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidates, std::map< Node, bool >& visited ){
+  if( visited.find( n )==visited.end() ){
+    visited[n] = true;
+    if( n.getKind()==APPLY_UF ){
+      if( isBoundVarApplyUf( n ) ){
+        candidates.push_back( n );
+      }
+    }else if( n.getKind()==PLUS ){
+      for( size_t i=0; i<n.getNumChildren(); i++ ){
+        getMacroCandidates( n[i], candidates, visited );
+      }
+    }else if( n.getKind()==MULT ){
+      //if the LHS is a constant
+      if( n.getNumChildren()==2 && n[0].isConst() ){
+        getMacroCandidates( n[1], candidates, visited );
+      }
+    }else if( n.getKind()==NOT ){
+      getMacroCandidates( n[0], candidates, visited );
     }
-  }else if( n.getKind()==NOT ){
-    getMacroCandidates( n[0], candidates );
   }
 }
 
@@ -239,19 +235,22 @@ Node QuantifierMacros::solveInEquality( Node n, Node lit ){
   return Node::null();
 }
 
-bool QuantifierMacros::getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly ){
-  if( std::find( v_quant.begin(), v_quant.end(), n )!=v_quant.end() ){
-    if( std::find( vars.begin(), vars.end(), n )==vars.end() ){
-      if( retOnly ){
-        return true;
-      }else{
-        vars.push_back( n );
+bool QuantifierMacros::getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly, std::map< Node, bool >& visited ){
+  if( visited.find( n )==visited.end() ){
+    visited[n] = true;
+    if( std::find( v_quant.begin(), v_quant.end(), n )!=v_quant.end() ){
+      if( std::find( vars.begin(), vars.end(), n )==vars.end() ){
+        if( retOnly ){
+          return true;
+        }else{
+          vars.push_back( n );
+        }
       }
     }
-  }
-  for( size_t i=0; i<n.getNumChildren(); i++ ){
-    if( getFreeVariables( n[i], v_quant, vars, retOnly ) ){
-      return true;
+    for( size_t i=0; i<n.getNumChildren(); i++ ){
+      if( getFreeVariables( n[i], v_quant, vars, retOnly, visited ) ){
+        return true;
+      }
     }
   }
   return false;
@@ -305,46 +304,58 @@ bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod
   }else{
     //literal case
     if( isMacroLiteral( n, pol ) ){
+      std::map< Node, bool > visited;
       std::vector< Node > candidates;
       for( size_t i=0; i<n.getNumChildren(); i++ ){
-        getMacroCandidates( n[i], candidates );
+        getMacroCandidates( n[i], candidates, visited );
       }
       for( size_t i=0; i<candidates.size(); i++ ){
         Node m = candidates[i];
         Node op = m.getOperator();
         if( d_macro_defs.find( op )==d_macro_defs.end() ){
           std::vector< Node > fvs;
-          getFreeVariables( m, args, fvs, false );
+          visited.clear();
+          getFreeVariables( m, args, fvs, false, visited );
           //get definition and condition
           Node n_def = solveInEquality( m, n ); //definition for the macro
-          //definition must exist and not contain any free variables apart from fvs, opc is list of functions it contains
-          std::vector< Node > opc;
-          if( !n_def.isNull() && !getFreeVariables( n_def, args, fvs, true )  && !containsBadOp( n_def, op, opc ) ){
-            Node n_cond;  //condition when this definition holds
-            //conditional must not contain any free variables apart from fvs
-            if( n_cond.isNull() || !getFreeVariables( n_cond, args, fvs, true ) ){
-              Trace("macros-debug") << m << " is possible macro in " << f << std::endl;
-              //now we must rewrite candidates[i] to a term of form g( x1, ..., xn ) where
-              // x1 ... xn are distinct variables
-              if( d_macro_basis[op].empty() ){
-                for( size_t a=0; a<m.getNumChildren(); a++ ){
-                  std::stringstream ss;
-                  ss << "mda_" << op << "";
-                  Node v = NodeManager::currentNM()->mkSkolem( ss.str(), m[a].getType(), "created during macro definition recognition" );
-                  d_macro_basis[op].push_back( v );
+          if( !n_def.isNull() ){
+            Trace("macros-debug") << m << " is possible macro in " << f << std::endl;
+            Trace("macros-debug") << "  corresponding definition is : " << n_def << std::endl;
+            visited.clear();
+            //definition must exist and not contain any free variables apart from fvs
+            if( !getFreeVariables( n_def, args, fvs, true, visited ) ){
+              Trace("macros-debug") << "...free variables are contained." << std::endl;
+              visited.clear();
+              //cannot contain a defined operator, opc is list of functions it contains
+              std::vector< Node > opc;
+              if( !containsBadOp( n_def, op, opc, visited ) ){
+                Trace("macros-debug") << "...does not contain bad (recursive) operator." << std::endl;
+                //must be ground UF term if mode is GROUND_UF
+                if( options::macrosQuantMode()!=MACROS_QUANT_MODE_GROUND_UF || isGroundUfTerm( f, n_def ) ){
+                  Trace("macros-debug") << "...respects ground-uf constraint." << std::endl;
+                  //now we must rewrite candidates[i] to a term of form g( x1, ..., xn ) where
+                  // x1 ... xn are distinct variables
+                  if( d_macro_basis[op].empty() ){
+                    for( size_t a=0; a<m.getNumChildren(); a++ ){
+                      std::stringstream ss;
+                      ss << "mda_" << op << "";
+                      Node v = NodeManager::currentNM()->mkSkolem( ss.str(), m[a].getType(), "created during macro definition recognition" );
+                      d_macro_basis[op].push_back( v );
+                    }
+                  }
+                  std::map< Node, Node > solved;
+                  for( size_t a=0; a<m.getNumChildren(); a++ ){
+                    solved[m[a]] = d_macro_basis[op][a];
+                  }
+                  std::vector< Node > vars;
+                  std::vector< Node > subs;
+                  if( getSubstitution( fvs, solved, vars, subs, true ) ){
+                    n_def = n_def.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+                    addMacro( op, n_def, opc );
+                    return true;
+                  }
                 }
               }
-              std::map< Node, Node > solved;
-              for( size_t a=0; a<m.getNumChildren(); a++ ){
-                solved[m[a]] = d_macro_basis[op][a];
-              }
-              std::vector< Node > vars;
-              std::vector< Node > subs;
-              if( getSubstitution( fvs, solved, vars, subs, true ) ){
-                n_def = n_def.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
-                addMacro( op, n_def, opc );
-                return true;
-              }
             }
           }
         }
@@ -416,7 +427,11 @@ void QuantifierMacros::debugMacroDefinition( Node oo, Node n ) {
 }
 
 void QuantifierMacros::finalizeDefinitions() {
-  if( options::incrementalSolving() || options::produceModels() || Trace.isOn("macros-warn") ){
+  bool doDefs = false;
+  if( Trace.isOn("macros-warn") ){
+    doDefs = true;
+  }
+  if( options::incrementalSolving() || options::produceModels() || doDefs ){
     Trace("macros") << "Store as defined functions..." << std::endl;
     //also store as defined functions
     for( std::map< Node, Node >::iterator it = d_macro_defs.begin(); it != d_macro_defs.end(); ++it ){
diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h
index 74fb0f47b..06e2d652a 100644
--- a/src/theory/quantifiers/macros.h
+++ b/src/theory/quantifiers/macros.h
@@ -23,6 +23,7 @@
 #include <map>
 #include "expr/node.h"
 #include "expr/type_node.h"
+#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {
@@ -30,16 +31,18 @@ namespace quantifiers {
 
 class QuantifierMacros{
 private:
+  QuantifiersEngine * d_qe;
+private:
   bool d_ground_macros;
   bool processAssertion( Node n );
   bool isBoundVarApplyUf( Node n );
   bool process( Node n, bool pol, std::vector< Node >& args, Node f );
-  bool contains( Node n, Node n_s );
-  bool containsBadOp( Node n, Node op, std::vector< Node >& opc );
+  bool containsBadOp( Node n, Node op, std::vector< Node >& opc, std::map< Node, bool >& visited );
   bool isMacroLiteral( Node n, bool pol );
-  void getMacroCandidates( Node n, std::vector< Node >& candidates );
+  bool isGroundUfTerm( Node f, Node n );
+  void getMacroCandidates( Node n, std::vector< Node >& candidates, std::map< Node, bool >& visited );
   Node solveInEquality( Node n, Node lit );
-  bool getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly );
+  bool getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly, std::map< Node, bool >& visited );
   bool getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved,
                         std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete );
   //map from operators to macro basis terms
@@ -49,14 +52,15 @@ private:
   std::map< Node, Node > d_macro_defs_new;
   //operators to macro ops that contain them
   std::map< Node, std::vector< Node > > d_macro_def_contains;
-  //simplify cache
+  //simplify caches
   std::map< Node, Node > d_simplify_cache;
+  std::map< Node, bool > d_quant_macros;
 private:
   Node simplify( Node n );
   void addMacro( Node op, Node n, std::vector< Node >& opc );
   void debugMacroDefinition( Node oo, Node n );
 public:
-  QuantifierMacros(){}
+  QuantifierMacros( QuantifiersEngine * qe ) : d_qe( qe ){}
   ~QuantifierMacros(){}
 
   bool simplify( std::vector< Node >& assertions, bool doRewrite = false );
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index 75e75637f..94ba7daaf 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -166,6 +166,8 @@ typedef enum {
   MACROS_QUANT_MODE_ALL,
   /** infer ground definitions */
   MACROS_QUANT_MODE_GROUND,
+  /** infer ground uf definitions */
+  MACROS_QUANT_MODE_GROUND_UF,
 } MacrosQuantMode;
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 0edd3f1ea..48a9fdea2 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -260,9 +260,9 @@ option lteRestrictInstClosure --lte-restrict-inst-closure bool :default false
 
 option quantAlphaEquiv --quant-alpha-equiv bool :default true
   infer alpha equivalence between quantified formulas
-option macrosQuant --macros-quant bool :default false
+option macrosQuant --macros-quant bool :read-write :default false
  perform quantifiers macro expansion
-option macrosQuantMode --macros-quant-mode=MODE CVC4::theory::quantifiers::MacrosQuantMode :default CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMacrosQuantMode :handler-include "theory/quantifiers/options_handlers.h"
+option macrosQuantMode --macros-quant-mode=MODE CVC4::theory::quantifiers::MacrosQuantMode :default CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMacrosQuantMode :handler-include "theory/quantifiers/options_handlers.h"
  mode for quantifiers macro expansion
 
 ### recursive function options
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 699dd0296..791ad6e90 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -239,6 +239,9 @@ all \n\
 ground (default) \n\
 + Only infer ground definitions for functions.\n\
 \n\
+ground-uf \n\
++ Only infer ground definitions for functions that result in triggers for all free variables.\n\
+\n\
 ";
 
 inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
@@ -487,6 +490,8 @@ inline MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string o
     return MACROS_QUANT_MODE_ALL;
   } else if(optarg == "ground") {
     return MACROS_QUANT_MODE_GROUND;
+  } else if(optarg == "ground-uf") {
+    return MACROS_QUANT_MODE_GROUND_UF;
   } else if(optarg ==  "help") {
     puts(macrosQuantHelp.c_str());
     exit(1);
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 7616e770a..7973abcc6 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -753,7 +753,6 @@ int TermDb::getNumInstantiationConstants( Node f ) const {
 Node TermDb::getInstConstantBody( Node f ){
   std::map< Node, Node >::iterator it = d_inst_const_body.find( f );
   if( it==d_inst_const_body.end() ){
-    makeInstantiationConstantsFor( f );
     Node n = getInstConstantNode( f[1], f );
     d_inst_const_body[ f ] = n;
     return n;
@@ -783,15 +782,9 @@ Node TermDb::getCounterexampleLiteral( Node f ){
 }
 
 Node TermDb::getInstConstantNode( Node n, Node f ){
-  Assert( d_inst_constants.find( f )!=d_inst_constants.end() );
-  return convertNodeToPattern(n,f,d_vars[f],d_inst_constants[ f ]);
-}
-
-Node TermDb::convertNodeToPattern( Node n, Node f, const std::vector<Node> & vars,
-                                              const std::vector<Node> & inst_constants){
-  Node n2 = n.substitute( vars.begin(), vars.end(),
-                          inst_constants.begin(),
-                          inst_constants.end() );
+  makeInstantiationConstantsFor( f );
+  Node n2 = n.substitute( d_vars[f].begin(), d_vars[f].end(),
+                          d_inst_constants[f].begin(), d_inst_constants[f].end() );
   return n2;
 }
 
@@ -1001,66 +994,47 @@ Node TermDb::getFreeVariableForType( TypeNode tn ) {
   return d_free_vars[tn];
 }
 
-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::computeVarContains( Node n, std::vector< Node >& varContains ) {
+  std::map< Node, bool > visited;
+  computeVarContains2( n, varContains, visited );
 }
 
-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;
+void TermDb::computeVarContains2( Node n, std::vector< Node >& varContains, std::map< Node, bool >& visited ){
+  if( visited.find( n )==visited.end() ){
+    visited[n] = true;
+    if( n.getKind()==INST_CONSTANT ){
+      if( std::find( varContains.begin(), varContains.end(), n )==varContains.end() ){
+        varContains.push_back( n );
+      }
+    }else{
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        computeVarContains2( n[i], varContains, visited );
       }
     }
-    //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] );
+  for( unsigned i=0; i<pats.size(); 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] );
-      }
-    }
+    getVarContainsNode( f, pats[i], varContains[ pats[i] ] );
   }
 }
 
 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] );
+  std::vector< Node > vars;
+  computeVarContains( n, vars );  
+  for( unsigned j=0; j<vars.size(); j++ ){
+    Node v = vars[j];
+    if( v.getAttribute(InstConstantAttribute())==f ){
+      if( std::find( varContains.begin(), varContains.end(), v )==varContains.end() ){
+        varContains.push_back( v );
+      }
     }
   }
 }
 
-/** is n1 an instance of n2 or vice versa? */
-int TermDb::isInstanceOf( Node n1, Node n2 ){
+int TermDb::isInstanceOf2( Node n1, Node n2, std::vector< Node >& varContains1, std::vector< Node >& varContains2 ){
   if( n1==n2 ){
     return 1;
   }else if( n1.getKind()==n2.getKind() ){
@@ -1069,7 +1043,7 @@ int TermDb::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 = isInstanceOf2( n1[i], n2[i], varContains1, varContains2 );
             if( cResult==0 ){
               return 0;
             }else if( cResult!=result ){
@@ -1086,25 +1060,31 @@ int TermDb::isInstanceOf( Node n1, Node n2 ){
     }
     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 ){
+    if( varContains1.size()==1 && varContains1[ 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 ){
+    if( varContains2.size()==1 && varContains2[ 0 ]==n1 ){
       return 1;
     }
   }
   return 0;
 }
 
+int TermDb::isInstanceOf( Node n1, Node n2 ){
+  std::vector< Node > varContains1;
+  std::vector< Node > varContains2;
+  computeVarContains( n1, varContains1 );
+  computeVarContains( n1, varContains2 );
+  return isInstanceOf2( n1, n2, varContains1, varContains2 );
+}
+
 bool TermDb::isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs ){
   if( n1==n2 ){
     return true;
@@ -1136,10 +1116,14 @@ bool TermDb::isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& su
 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++ ){
+  std::map< int, std::vector< Node > > varContains;
+  for( unsigned i=0; i<nodes.size(); i++ ){
+    computeVarContains( nodes[i], varContains[i] );
+  }   
+  for( unsigned i=0; i<nodes.size(); i++ ){
+    for( unsigned j=i+1; j<nodes.size(); j++ ){
       if( active[i] && active[j] ){
-        int result = isInstanceOf( nodes[i], nodes[j] );
+        int result = isInstanceOf2( nodes[i], nodes[j], varContains[i], varContains[j] );
         if( result==1 ){
           Trace("filter-instances") << nodes[j] << " is an instance of " << nodes[i] << std::endl;
           active[j] = false;
@@ -1151,7 +1135,7 @@ void TermDb::filterInstances( std::vector< Node >& nodes ){
     }
   }
   std::vector< Node > temp;
-  for( int i=0; i<(int)nodes.size(); i++ ){
+  for( unsigned i=0; i<nodes.size(); i++ ){
     if( active[i] ){
       temp.push_back( nodes[i] );
     }
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 23594d49a..416761ce8 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -248,14 +248,6 @@ public:
       instantiation.
    */
   Node getInstConstantNode( Node n, Node f );
-  /** same as before but node f is just linked to the new pattern by the
-      applied attribute
-      vars the bind variable
-      nvars the same variable but with an attribute
-  */
-  Node convertNodeToPattern( Node n, Node f,
-                             const std::vector<Node> & vars,
-                             const std::vector<Node> & nvars);
 
   static Node getInstConstAttr( Node n );
   static bool hasInstConstAttr( Node n );
@@ -306,18 +298,16 @@ public:
 //for triggers
 private:
   /** helper function for compute var contains */
-  void computeVarContains2( Node n, Node parent );
-  /** var contains */
-  std::map< TNode, std::vector< TNode > > d_var_contains;
+  void computeVarContains2( Node n, std::vector< Node >& varContains, std::map< Node, bool >& visited );
   /** triggers for each operator */
   std::map< Node, std::vector< inst::Trigger* > > d_op_triggers;
   /** helper for is instance of */
   bool isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs );
+  /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
+  int isInstanceOf2( Node n1, Node n2, std::vector< Node >& varContains1, std::vector< Node >& varContains2 );
 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 );
+  void computeVarContains( Node n, std::vector< Node >& varContains );
   /** 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 */
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index e4d9a2730..0085177cc 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -121,23 +121,23 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
     std::map< Node, bool > vars;
     std::map< Node, std::vector< Node > > patterns;
     size_t varCount = 0;
-    for( int i=0; i<(int)temp.size(); i++ ){
+    std::map< Node, std::vector< Node > > varContains;
+    qe->getTermDatabase()->getVarContains( f, temp, varContains );
+    for( unsigned i=0; i<temp.size(); i++ ){
       bool foundVar = false;
-      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( quantifiers::TermDb::getInstConstAttr(v)==f ){
-          if( vars.find( v )==vars.end() ){
-            varCount++;
-            vars[ v ] = true;
-            foundVar = true;
-          }
+      for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){
+        Node v = varContains[ temp[i] ][j];
+        Assert( quantifiers::TermDb::getInstConstAttr(v)==f );
+        if( vars.find( v )==vars.end() ){
+          varCount++;
+          vars[ v ] = true;
+          foundVar = true;
         }
       }
       if( foundVar ){
         trNodes.push_back( 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];
+        for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){
+          Node v = varContains[ temp[i] ][j];
           patterns[ v ].push_back( temp[i] );
         }
       }
@@ -156,11 +156,11 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
       return NULL;
     }else{
       //now, minimize the trigger
-      for( int i=0; i<(int)trNodes.size(); i++ ){
+      for( unsigned i=0; i<trNodes.size(); i++ ){
         bool keepPattern = false;
         Node n = trNodes[i];
-        for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){
-          Node v = qe->getTermDatabase()->d_var_contains[ n ][j];
+        for( unsigned j=0; j<varContains[ n ].size(); j++ ){
+          Node v = varContains[ n ][j];
           if( patterns[v].size()==1 ){
             keepPattern = true;
             break;
@@ -168,9 +168,9 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
         }
         if( !keepPattern ){
           //remove from pattern vector
-          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++ ){
+          for( unsigned j=0; j<varContains[ n ].size(); j++ ){
+            Node v = varContains[ n ][j];
+            for( unsigned k=0; k<patterns[v].size(); k++ ){
               if( patterns[v][k]==n ){
                 patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 );
                 break;
@@ -335,7 +335,7 @@ bool Trigger::isSimpleTrigger( Node n ){
 }
 
 
-bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ){
+bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ){
   if( patMap.find( n )==patMap.end() ){
     patMap[ n ] = false;
     bool newHasPol = n.getKind()==IFF ? false : hasPol;
@@ -347,7 +347,7 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map<
         bool retVal = false;
         for( int i=0; i<(int)n.getNumChildren(); i++ ){
           bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol;
-          if( collectPatTerms2( qe, f, n[i], patMap, tstrt, exclude, newPol, newHasPol2 ) ){
+          if( collectPatTerms2( f, n[i], patMap, tstrt, exclude, newPol, newHasPol2 ) ){
             retVal = true;
           }
         }
@@ -383,7 +383,7 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map<
       if( n.getKind()!=FORALL ){
         for( int i=0; i<(int)n.getNumChildren(); i++ ){
           bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol;
-          if( collectPatTerms2( qe, f, n[i], patMap, tstrt, exclude, newPol, newHasPol2 ) ){
+          if( collectPatTerms2( f, n[i], patMap, tstrt, exclude, newPol, newHasPol2 ) ){
             retVal = true;
           }
         }
@@ -491,7 +491,7 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto
       }
     }
   }
-  collectPatTerms2( qe, f, n, patMap, tstrt, exclude, true, true );
+  collectPatTerms2( f, n, patMap, tstrt, exclude, true, true );
   for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){
     if( it->second ){
       patTerms.push_back( it->first );
@@ -568,6 +568,17 @@ Node Trigger::getInversion( Node n, Node x ) {
   return Node::null();
 }
 
+void Trigger::getTriggerVariables( QuantifiersEngine* qe, Node icn, Node f, std::vector< Node >& t_vars ) {
+  std::vector< Node > patTerms;
+  //collect all patterns from icn
+  std::vector< Node > exclude;
+  collectPatTerms( qe, f, icn, patTerms, TS_ALL, exclude );
+  //collect all variables from all patterns in patTerms, add to t_vars
+  for( unsigned i=0; i<patTerms.size(); i++ ){
+    qe->getTermDatabase()->getVarContainsNode( f, patTerms[i], t_vars );
+  }
+}
+
 InstMatchGenerator* Trigger::getInstMatchGenerator( Node q, Node n ) {
   if( n.getKind()==INST_CONSTANT ){
     return NULL;
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 60e268a4f..f601a02ab 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -94,7 +94,7 @@ private:
   static bool isUsable( Node n, Node f );
   static Node getIsUsableTrigger( Node n, Node f, bool pol = true, bool hasPol = false );
   /** collect all APPLY_UF pattern terms for f in n */
-  static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol );
+  static bool collectPatTerms2( Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol );
 public:
   //different strategies for choosing trigger terms
   enum {
@@ -116,6 +116,8 @@ public:
   static InstMatchGenerator* getInstMatchGenerator( Node q, Node n );
   static Node getInversionVariable( Node n );
   static Node getInversion( Node n, Node x );
+  /** get all variables that E-matching can possibly handle */
+  static void getTriggerVariables( QuantifiersEngine* qe, Node icn, Node f, std::vector< Node >& t_vars );
 
   inline void toStream(std::ostream& out) const {
     /*