drastic simplification of quantifiers code regarding equality queries, instantiation strategies moved from instantiators to central instantiation engine, removed instantiator objects, simplified rewrite rules candidate generator to use central equality engine, efficient e-matching now uses central equality engine

17 files changed, 1199 insertions, 263 deletions

diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am
index 371aa5543..316af7616 100644
--- a/src/theory/quantifiers/Makefile.am
+++ b/src/theory/quantifiers/Makefile.am
@@ -11,16 +11,12 @@ libquantifiers_la_SOURCES = \
 	quantifiers_rewriter.h \
 	quantifiers_rewriter.cpp \
 	theory_quantifiers.cpp \
-	theory_quantifiers_instantiator.h \
-	theory_quantifiers_instantiator.cpp \
 	instantiation_engine.h \
 	instantiation_engine.cpp \
 	trigger.h \
 	trigger.cpp \
 	candidate_generator.h \
 	candidate_generator.cpp \
-	instantiator_default.h \
-	instantiator_default.cpp \
 	inst_match.h \
 	inst_match.cpp \
 	model_engine.h \
@@ -44,7 +40,11 @@ libquantifiers_la_SOURCES = \
 	inst_match_generator.h \
 	inst_match_generator.cpp \
 	macros.h \
-	macros.cpp
+	macros.cpp \
+	inst_strategy_e_matching.h \
+	inst_strategy_e_matching.cpp \
+	inst_strategy_cbqi.h \
+	inst_strategy_cbqi.cpp
 
 EXTRA_DIST = \
 	kinds \
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
new file mode 100755
index 000000000..d79ddee31
--- /dev/null
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -0,0 +1,403 @@
+/*********************                                                        */

+/*! \file inst_strategy_cbqi.cpp

+ ** \verbatim

+ ** Original author: ajreynol

+ ** Major contributors: none

+ ** Minor contributors (to current version): bobot, mdeters

+ ** 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 Implementation of cbqi instantiation strategies

+ **/

+

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

+#include "theory/arith/theory_arith.h"

+#include "theory/theory_engine.h"

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

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

+

+using namespace std;

+using namespace CVC4;

+using namespace CVC4::kind;

+using namespace CVC4::context;

+using namespace CVC4::theory;

+using namespace CVC4::theory::quantifiers;

+using namespace CVC4::theory::arith;

+using namespace CVC4::theory::datatypes;

+

+#define ARITH_INSTANTIATOR_USE_MINUS_DELTA

+

+InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) :

+    InstStrategy( ie ), d_th( th ), d_counter( 0 ){

+  d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) );

+}

+

+bool InstStrategySimplex::calculateShouldProcess( Node f ){

+  //DO_THIS

+  return false;

+}

+

+void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ){

+  Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl;

+  d_instRows.clear();

+  d_tableaux_term.clear();

+  d_tableaux.clear();

+  d_ceTableaux.clear();

+  //search for instantiation rows in simplex tableaux

+  ArithVarToNodeMap avtnm = d_th->d_arithvarNodeMap.getArithVarToNodeMap();

+  for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){

+    ArithVar x = (*it).first;

+    if( d_th->d_partialModel.hasEitherBound( x ) ){

+      Node n = (*it).second;

+      Node f;

+      NodeBuilder<> t(kind::PLUS);

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

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

+          addTermToRow( x, n[i], f, t );

+        }

+      }else{

+        addTermToRow( x, n, f, t );

+      }

+      if( f!=Node::null() ){

+        d_instRows[f].push_back( x );

+        //this theory has constraints from f

+        Debug("quant-arith") << "Has constraints from " << f << std::endl;

+        //set that we should process it

+        d_quantActive[ f ] = true;

+        //set tableaux term

+        if( t.getNumChildren()==0 ){

+          d_tableaux_term[x] = NodeManager::currentNM()->mkConst( Rational(0) );

+        }else if( t.getNumChildren()==1 ){

+          d_tableaux_term[x] = t.getChild( 0 );

+        }else{

+          d_tableaux_term[x] = t;

+        }

+      }

+    }

+  }

+  //print debug

+  debugPrint( "quant-arith-debug" );

+  d_counter++;

+}

+

+int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){

+  if( e<2 ){

+    return STATUS_UNFINISHED;

+  }else if( e==2 ){

+    //Notice() << f << std::endl;

+    //Notice() << "Num inst rows = " << d_th->d_instRows[f].size() << std::endl;

+    //Notice() << "Num inst constants = " << d_quantEngine->getNumInstantiationConstants( f ) << std::endl;

+    Debug("quant-arith-simplex") << "InstStrategySimplex check " << f << ", rows = " << d_instRows[f].size() << std::endl;

+    for( int j=0; j<(int)d_instRows[f].size(); j++ ){

+      ArithVar x = d_instRows[f][j];

+      if( !d_ceTableaux[x].empty() ){

+        Debug("quant-arith-simplex") << "Check row " << x << std::endl;

+        //instantiation row will be A*e + B*t = beta,

+        // where e is a vector of terms , and t is vector of ground terms.

+        // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant

+        // We will construct the term ( beta - B*t)/coeff to use for e_i.

+        InstMatch m;

+        //By default, choose the first instantiation constant to be e_i.

+        Node var = d_ceTableaux[x].begin()->first;

+        if( var.getType().isInteger() ){

+          std::map< Node, Node >::iterator it = d_ceTableaux[x].begin();

+          //try to find coefficent that is +/- 1

+          while( !var.isNull() && !d_ceTableaux[x][var].isNull() && d_ceTableaux[x][var]!=d_negOne ){

+            ++it;

+            if( it==d_ceTableaux[x].end() ){

+              var = Node::null();

+            }else{

+              var = it->first;

+            }

+          }

+          //otherwise, try one that divides all ground term coefficients? DO_THIS

+        }

+        if( !var.isNull() ){

+          Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;

+          doInstantiation( f, d_tableaux_term[x], x, m, var );

+        }else{

+          Debug("quant-arith-simplex") << "Could not find var." << std::endl;

+        }

+        ////choose a new variable based on alternation strategy

+        //int index = d_counter%(int)d_th->d_ceTableaux[x].size();

+        //Node var;

+        //for( std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin(); it != d_th->d_ceTableaux[x].end(); ++it ){

+        //  if( index==0 ){

+        //    var = it->first;

+        //    break;

+        //  }

+        //  index--;

+        //}

+        //d_th->doInstantiation( f, d_th->d_tableaux_term[x], x, &m, var );

+      }

+    }

+  }

+  return STATUS_UNKNOWN;

+}

+

+

+void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t ){

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

+    if( n[1].hasAttribute(InstConstantAttribute()) ){

+      f = n[1].getAttribute(InstConstantAttribute());

+      if( n[1].getKind()==INST_CONSTANT ){

+        d_ceTableaux[x][ n[1] ] = n[0];

+      }else{

+        d_tableaux_ce_term[x][ n[1] ] = n[0];

+      }

+    }else{

+      d_tableaux[x][ n[1] ] = n[0];

+      t << n;

+    }

+  }else{

+    if( n.hasAttribute(InstConstantAttribute()) ){

+      f = n.getAttribute(InstConstantAttribute());

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

+        d_ceTableaux[x][ n ] = Node::null();

+      }else{

+        d_tableaux_ce_term[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );

+      }

+    }else{

+      d_tableaux[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );

+      t << n;

+    }

+  }

+}

+

+void InstStrategySimplex::debugPrint( const char* c ){

+  ArithVarToNodeMap avtnm = d_th->d_arithvarNodeMap.getArithVarToNodeMap();

+  for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){

+    ArithVar x = (*it).first;

+    Node n = (*it).second;

+    //if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){

+      Debug(c) << x << " : " << n << ", bounds = ";

+      if( d_th->d_partialModel.hasLowerBound( x ) ){

+        Debug(c) << d_th->d_partialModel.getLowerBound( x );

+      }else{

+        Debug(c) << "-infty";

+      }

+      Debug(c) << " <= ";

+      Debug(c) << d_th->d_partialModel.getAssignment( x );

+      Debug(c) << " <= ";

+      if( d_th->d_partialModel.hasUpperBound( x ) ){

+        Debug(c) << d_th->d_partialModel.getUpperBound( x );

+      }else{

+        Debug(c) << "+infty";

+      }

+      Debug(c) << std::endl;

+      //Debug(c) << "   Term = " << d_tableaux_term[x] << std::endl;

+      //Debug(c) << "   ";

+      //for( std::map< Node, Node >::iterator it2 = d_tableaux[x].begin(); it2 != d_tableaux[x].end(); ++it2 ){

+      //  Debug(c) << "( " << it2->first << ", " << it2->second << " ) ";

+      //}

+      //for( std::map< Node, Node >::iterator it2 = d_ceTableaux[x].begin(); it2 != d_ceTableaux[x].end(); ++it2 ){

+      //  Debug(c) << "(CE)( " << it2->first << ", " << it2->second << " ) ";

+      //}

+      //for( std::map< Node, Node >::iterator it2 = d_tableaux_ce_term[x].begin(); it2 != d_tableaux_ce_term[x].end(); ++it2 ){

+      //  Debug(c) << "(CE-term)( " << it2->first << ", " << it2->second << " ) ";

+      //}

+      //Debug(c) << std::endl;

+    //}

+  }

+  Debug(c) << std::endl;

+

+  for( int q=0; q<d_quantEngine->getNumQuantifiers(); q++ ){

+    Node f = d_quantEngine->getQuantifier( q );

+    Debug(c) << f << std::endl;

+    Debug(c) << "   Inst constants: ";

+    for( int i=0; i<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){

+      if( i>0 ){

+        Debug( c ) << ", ";

+      }

+      Debug( c ) << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );

+    }

+    Debug(c) << std::endl;

+    Debug(c) << "   Instantiation rows: ";

+    for( int i=0; i<(int)d_instRows[f].size(); i++ ){

+      if( i>0 ){

+        Debug(c) << ", ";

+      }

+      Debug(c) << d_instRows[f][i];

+    }

+    Debug(c) << std::endl;

+  }

+}

+

+//say instantiation row x for quantifier f is coeff*var + A*t[e] + term = beta,

+// where var is an instantiation constant from f,

+// t[e] is a vector of terms containing instantiation constants from f,

+// and term is a ground term (c1*t1 + ... + cn*tn).

+// We construct the term ( beta - term )/coeff to use as an instantiation for var.

+bool InstStrategySimplex::doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node var ){

+  //first try +delta

+  if( doInstantiation2( f, term, x, m, var ) ){

+    ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith);

+    return true;

+  }else{

+#ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA

+    //otherwise try -delta

+    if( doInstantiation2( f, term, x, m, var, true ) ){

+      ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith_minus);

+      return true;

+    }else{

+      return false;

+    }

+#else

+    return false;

+#endif

+  }

+}

+

+bool InstStrategySimplex::doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){

+  // make term ( beta - term )/coeff

+  Node beta = getTableauxValue( x, minus_delta );

+  Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term );

+  if( !d_ceTableaux[x][var].isNull() ){

+    if( var.getType().isInteger() ){

+      Assert( d_ceTableaux[x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) );

+      instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[x][var], instVal );

+    }else{

+      Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[x][var].getConst<Rational>() );

+      instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal );

+    }

+  }

+  instVal = Rewriter::rewrite( instVal );

+  //use as instantiation value for var

+  m.set(var, instVal);

+  Debug("quant-arith") << "Add instantiation " << m << std::endl;

+  return d_quantEngine->addInstantiation( f, m );

+}

+

+Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){

+  if( d_th->d_arithvarNodeMap.hasArithVar(n) ){

+    ArithVar v = d_th->d_arithvarNodeMap.asArithVar( n );

+    return getTableauxValue( v, minus_delta );

+  }else{

+    return NodeManager::currentNM()->mkConst( Rational(0) );

+  }

+}

+

+Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){

+  const Rational& delta = d_th->d_partialModel.getDelta();

+  DeltaRational drv = d_th->d_partialModel.getAssignment( v );

+  Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta );

+  return mkRationalNode(qmodel);

+}

+

+

+InstStrategyDatatypesValue::InstStrategyDatatypesValue( TheoryDatatypes* th, QuantifiersEngine* qe ) :

+  InstStrategy( qe ), d_th( th ){

+

+}

+

+bool InstStrategyDatatypesValue::calculateShouldProcess( Node f ){

+  //DO_THIS

+  return false;

+}

+

+void InstStrategyDatatypesValue::processResetInstantiationRound( Theory::Effort effort ){

+

+}

+

+int InstStrategyDatatypesValue::process( Node f, Theory::Effort effort, int e ){

+  Debug("quant-datatypes") << "Datatypes: Try to solve (" << e << ") for " << f << "... " << std::endl;

+  if( e<2 ){

+    return InstStrategy::STATUS_UNFINISHED;

+  }else if( e==2 ){

+    InstMatch m;

+    for( int j = 0; j<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){

+      Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );

+      if( i.getType().isDatatype() ){

+        Node n = getValueFor( i );

+        Debug("quant-datatypes-debug") << "Value for " << i << " is " << n << std::endl;

+        m.set(i,n);

+      }

+    }

+    //d_quantEngine->addInstantiation( f, m );

+  }

+  return InstStrategy::STATUS_UNKNOWN;

+}

+

+Node InstStrategyDatatypesValue::getValueFor( Node n ){

+  //simply get the ground value for n in the current model, if it exists,

+  //  or return an arbitrary ground term otherwise

+  if( !n.hasAttribute(InstConstantAttribute()) ){

+    return n;

+  }else{

+    return n;

+  }

+  /*  FIXME

+

+  Debug("quant-datatypes-debug")  << "get value for " << n << std::endl;

+  if( !n.hasAttribute(InstConstantAttribute()) ){

+    return n;

+  }else{

+    Assert( n.getType().isDatatype() );

+    //check if in equivalence class with ground term

+    Node rep = getRepresentative( n );

+    Debug("quant-datatypes-debug") << "Rep is " << rep << std::endl;

+    if( !rep.hasAttribute(InstConstantAttribute()) ){

+      return rep;

+    }else{

+      if( !n.getType().isDatatype() ){

+        return n.getType().mkGroundTerm();

+      }else{

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

+          std::vector< Node > children;

+          children.push_back( n.getOperator() );

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

+            children.push_back( getValueFor( n[i] ) );

+          }

+          return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );

+        }else{

+          const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype();

+          TheoryDatatypes::EqLists* labels = &((TheoryDatatypes*)d_th)->d_labels;

+          //otherwise, use which constructor the inst constant is current chosen to be

+          if( labels->find( n )!=labels->end() ){

+            TheoryDatatypes::EqList* lbl = (*labels->find( n )).second;

+            int tIndex = -1;

+            if( !lbl->empty() && (*lbl)[ lbl->size()-1 ].getKind()==APPLY_TESTER ){

+              Debug("quant-datatypes-debug") << n << " tester is " << (*lbl)[ lbl->size()-1 ] << std::endl;

+              tIndex = Datatype::indexOf((*lbl)[ lbl->size()-1 ].getOperator().toExpr());

+            }else{

+              Debug("quant-datatypes-debug") << "find possible tester choice" << std::endl;

+              //must find a possible choice

+              vector< bool > possibleCons;

+              possibleCons.resize( dt.getNumConstructors(), true );

+              for( TheoryDatatypes::EqList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ) {

+                Node leqn = (*j);

+                possibleCons[ Datatype::indexOf( leqn[0].getOperator().toExpr() ) ] = false;

+              }

+              for( unsigned int j=0; j<possibleCons.size(); j++ ) {

+                if( possibleCons[j] ){

+                  tIndex = j;

+                  break;

+                }

+              }

+            }

+            Assert( tIndex!=-1 );

+            Node cons = Node::fromExpr( dt[ tIndex ].getConstructor() );

+            Debug("quant-datatypes-debug") << n << " cons is " << cons << std::endl;

+            std::vector< Node > children;

+            children.push_back( cons );

+            for( int i=0; i<(int)dt[ tIndex ].getNumArgs(); i++ ) {

+              Node sn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[tIndex][i].getSelector() ), n );

+              if( n.hasAttribute(InstConstantAttribute()) ){

+                InstConstantAttribute ica;

+                sn.setAttribute(ica,n.getAttribute(InstConstantAttribute()) );

+              }

+              Node snn = getValueFor( sn );

+              children.push_back( snn );

+            }

+            return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );

+          }else{

+            return n.getType().mkGroundTerm();

+          }

+        }

+      }

+    }

+  }

+  */

+}

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
new file mode 100755
index 000000000..3ee423fe7
--- /dev/null
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -0,0 +1,110 @@
+/*********************                                                        */

+/*! \file inst_strategy_cbqi.h

+ ** \verbatim

+ ** Original author: ajreynol

+ ** Major contributors: none

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

+ ** 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 instantiator_arith_instantiator

+ **/

+

+

+#include "cvc4_private.h"

+

+#ifndef __CVC4__INST_STRATEGT_CBQI_H

+#define __CVC4__INST_STRATEGT_CBQI_H

+

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

+#include "theory/arith/arithvar_node_map.h"

+

+#include "util/statistics_registry.h"

+

+namespace CVC4 {

+namespace theory {

+

+namespace arith {

+  class TheoryArith;

+}

+

+namespace datatypes {

+  class TheoryDatatypes;

+}

+

+namespace quantifiers {

+

+

+class InstStrategySimplex : public InstStrategy{

+protected:

+  /** calculate if we should process this quantifier */

+  bool calculateShouldProcess( Node f );

+private:

+  /** reference to theory arithmetic */

+  arith::TheoryArith* d_th;

+  /** delta */

+  std::map< TypeNode, Node > d_deltas;

+  /** for each quantifier, simplex rows */

+  std::map< Node, std::vector< arith::ArithVar > > d_instRows;

+  /** tableaux */

+  std::map< arith::ArithVar, Node > d_tableaux_term;

+  std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux_ce_term;

+  std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux;

+  /** ce tableaux */

+  std::map< arith::ArithVar, std::map< Node, Node > > d_ceTableaux;

+  /** get value */

+  Node getTableauxValue( Node n, bool minus_delta = false );

+  Node getTableauxValue( arith::ArithVar v, bool minus_delta = false );

+  /** do instantiation */

+  bool doInstantiation( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var );

+  bool doInstantiation2( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var, bool minus_delta = false );

+  /** add term to row */

+  void addTermToRow( arith::ArithVar x, Node n, Node& f, NodeBuilder<>& t );

+  /** print debug */

+  void debugPrint( const char* c );

+private:

+  /** */

+  int d_counter;

+  /** negative one */

+  Node d_negOne;

+  /** process functions */

+  void processResetInstantiationRound( Theory::Effort effort );

+  int process( Node f, Theory::Effort effort, int e );

+public:

+  InstStrategySimplex( arith::TheoryArith* th, QuantifiersEngine* ie );

+  ~InstStrategySimplex(){}

+  /** identify */

+  std::string identify() const { return std::string("Simplex"); }

+};

+

+

+class InstStrategyDatatypesValue : public InstStrategy

+{

+protected:

+  /** calculate if we should process this quantifier */

+  bool calculateShouldProcess( Node f );

+private:

+  /** reference to theory datatypes */

+  datatypes::TheoryDatatypes* d_th;

+  /** get value function */

+  Node getValueFor( Node n );

+public:

+  //constructor

+  InstStrategyDatatypesValue( datatypes::TheoryDatatypes* th, QuantifiersEngine* qe );

+  ~InstStrategyDatatypesValue(){}

+  /** reset instantiation */

+  void processResetInstantiationRound( Theory::Effort effort );

+  /** process method, returns a status */

+  int process( Node f, Theory::Effort effort, int e );

+  /** identify */

+  std::string identify() const { return std::string("InstStrategyDatatypesValue"); }

+

+};/* class InstStrategy */

+

+}

+}

+}

+

+#endif
\ No newline at end of file
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
new file mode 100755
index 000000000..48af334ff
--- /dev/null
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -0,0 +1,379 @@
+/*********************                                                        */

+/*! \file inst_strategy_e_matching.cpp

+ ** \verbatim

+ ** Original author: ajreynol

+ ** Major contributors: mdeters

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

+ ** 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 Implementation of e matching instantiation strategies

+ **/

+

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

+

+#include "theory/theory_engine.h"

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

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

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

+

+using namespace std;

+using namespace CVC4;

+using namespace CVC4::kind;

+using namespace CVC4::context;

+using namespace CVC4::theory;

+using namespace CVC4::theory::inst;

+using namespace CVC4::theory::quantifiers;

+

+#define USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER

+//#define MULTI_TRIGGER_FULL_EFFORT_HALF

+#define MULTI_MULTI_TRIGGERS

+

+struct sortQuantifiersForSymbol {

+  QuantifiersEngine* d_qe;

+  bool operator() (Node i, Node j) {

+    int nqfsi = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( i.getOperator() );

+    int nqfsj = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( j.getOperator() );

+    if( nqfsi<nqfsj ){

+      return true;

+    }else if( nqfsi>nqfsj ){

+      return false;

+    }else{

+      return false;

+    }

+  }

+};

+

+void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){

+  //reset triggers

+  for( std::map< Node, std::vector< Trigger* > >::iterator it = d_user_gen.begin(); it != d_user_gen.end(); ++it ){

+    for( int i=0; i<(int)it->second.size(); i++ ){

+      it->second[i]->resetInstantiationRound();

+      it->second[i]->reset( Node::null() );

+    }

+  }

+}

+

+int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){

+  if( e==0 ){

+    return STATUS_UNFINISHED;

+  }else if( e==1 ){

+    d_counter[f]++;

+    Debug("quant-uf-strategy") << "Try user-provided patterns..." << std::endl;

+    //Notice() << "Try user-provided patterns..." << std::endl;

+    for( int i=0; i<(int)d_user_gen[f].size(); i++ ){

+      bool processTrigger = true;

+      if( effort!=Theory::EFFORT_LAST_CALL && d_user_gen[f][i]->isMultiTrigger() ){

+//#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF

+//        processTrigger = d_counter[f]%2==0;

+//#endif

+      }

+      if( processTrigger ){

+        //if( d_user_gen[f][i]->isMultiTrigger() )

+          //Notice() << "  Process (user) " << (*d_user_gen[f][i]) << " for " << f << "..." << std::endl;

+        InstMatch baseMatch;

+        int numInst = d_user_gen[f][i]->addInstantiations( baseMatch );

+        //if( d_user_gen[f][i]->isMultiTrigger() )

+          //Notice() << "  Done, numInst = " << numInst << "." << std::endl;

+        d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_user_patterns += numInst;

+        if( d_user_gen[f][i]->isMultiTrigger() ){

+          d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;

+        }

+        //d_quantEngine->d_hasInstantiated[f] = true;

+      }

+    }

+    Debug("quant-uf-strategy") << "done." << std::endl;

+    //Notice() << "done" << std::endl;

+  }

+  return STATUS_UNKNOWN;

+}

+

+void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){

+  //add to generators

+  std::vector< Node > nodes;

+  for( int i=0; i<(int)pat.getNumChildren(); i++ ){

+    nodes.push_back( pat[i] );

+  }

+  if( Trigger::isUsableTrigger( nodes, f ) ){

+    //extend to literal matching

+    d_quantEngine->getPhaseReqTerms( f, nodes );

+    //check match option

+    int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0;

+    d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW,

+                                                 options::smartTriggers() ) );

+  }

+}

+/*

+InstStrategyUserPatterns::Statistics::Statistics():

+  d_instantiations("InstStrategyUserPatterns::Instantiations", 0)

+{

+  StatisticsRegistry::registerStat(&d_instantiations);

+}

+

+InstStrategyUserPatterns::Statistics::~Statistics(){

+  StatisticsRegistry::unregisterStat(&d_instantiations);

+}

+*/

+

+void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){

+  //reset triggers

+  for( std::map< Node, std::map< Trigger*, bool > >::iterator it = d_auto_gen_trigger.begin(); it != d_auto_gen_trigger.end(); ++it ){

+    for( std::map< Trigger*, bool >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){

+      itt->first->resetInstantiationRound();

+      itt->first->reset( Node::null() );

+    }

+  }

+}

+

+int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){

+  int peffort = f.getNumChildren()==3 ? 2 : 1;

+  //int peffort = f.getNumChildren()==3 ? 2 : 1;

+  //int peffort = 1;

+  if( e<peffort ){

+    return STATUS_UNFINISHED;

+  }else{

+    bool gen = false;

+    if( e==peffort ){

+      if( d_counter.find( f )==d_counter.end() ){

+        d_counter[f] = 0;

+        gen = true;

+      }else{

+        d_counter[f]++;

+        gen = d_regenerate && d_counter[f]%d_regenerate_frequency==0;

+      }

+    }else{

+      gen = true;

+    }

+    if( gen ){

+      generateTriggers( f );

+    }

+    Debug("quant-uf-strategy")  << "Try auto-generated triggers... " << d_tr_strategy << " " << e << std::endl;

+    //Notice() << "Try auto-generated triggers..." << std::endl;

+    for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[f].begin(); itt != d_auto_gen_trigger[f].end(); ++itt ){

+      Trigger* tr = itt->first;

+      if( tr ){

+        bool processTrigger = itt->second;

+        if( effort!=Theory::EFFORT_LAST_CALL && tr->isMultiTrigger() ){

+#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF

+          processTrigger = d_counter[f]%2==0;

+#endif

+        }

+        if( processTrigger ){

+          //if( tr->isMultiTrigger() )

+            Debug("quant-uf-strategy-auto-gen-triggers") << "  Process " << (*tr) << "..." << std::endl;

+          InstMatch baseMatch;

+          int numInst = tr->addInstantiations( baseMatch );

+          //if( tr->isMultiTrigger() )

+            Debug("quant-uf-strategy-auto-gen-triggers") << "  Done, numInst = " << numInst << "." << std::endl;

+          if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){

+            d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen_min += numInst;

+          }else{

+            d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen += numInst;

+          }

+          if( tr->isMultiTrigger() ){

+            d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;

+          }

+          //d_quantEngine->d_hasInstantiated[f] = true;

+        }

+      }

+    }

+    Debug("quant-uf-strategy") << "done." << std::endl;

+    //Notice() << "done" << std::endl;

+  }

+  return STATUS_UNKNOWN;

+}

+

+void InstStrategyAutoGenTriggers::generateTriggers( Node f ){

+  Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl;

+  if( d_patTerms[0].find( f )==d_patTerms[0].end() ){

+    //determine all possible pattern terms based on trigger term selection strategy d_tr_strategy

+    d_patTerms[0][f].clear();

+    d_patTerms[1][f].clear();

+    std::vector< Node > patTermsF;

+    Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getInstConstantBody( f ), patTermsF, d_tr_strategy, true );

+    Debug("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << std::endl;

+    Debug("auto-gen-trigger") << "   ";

+    for( int i=0; i<(int)patTermsF.size(); i++ ){

+      Debug("auto-gen-trigger") << patTermsF[i] << " ";

+    }

+    Debug("auto-gen-trigger") << std::endl;

+    //extend to literal matching (if applicable)

+    d_quantEngine->getPhaseReqTerms( f, patTermsF );

+    //sort into single/multi triggers

+    std::map< Node, std::vector< Node > > 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 );

+        d_is_single_trigger[ it->first ] = true;

+      }else{

+        d_patTerms[1][f].push_back( it->first );

+        d_is_single_trigger[ it->first ] = false;

+      }

+    }

+    d_made_multi_trigger[f] = false;

+    Debug("auto-gen-trigger") << "Single triggers for " << f << " : " << std::endl;

+    Debug("auto-gen-trigger") << "   ";

+    for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){

+      Debug("auto-gen-trigger") << d_patTerms[0][f][i] << " ";

+    }

+    Debug("auto-gen-trigger") << std::endl;

+    Debug("auto-gen-trigger") << "Multi-trigger term pool for " << f << " : " << std::endl;

+    Debug("auto-gen-trigger") << "   ";

+    for( int i=0; i<(int)d_patTerms[1][f].size(); i++ ){

+      Debug("auto-gen-trigger") << d_patTerms[1][f][i] << " ";

+    }

+    Debug("auto-gen-trigger") << std::endl;

+  }

+

+  //populate candidate pattern term vector for the current trigger

+  std::vector< Node > patTerms;

+#ifdef USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER

+  //try to add single triggers first

+  for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){

+    if( !d_single_trigger_gen[d_patTerms[0][f][i]] ){

+      patTerms.push_back( d_patTerms[0][f][i] );

+    }

+  }

+  //if no single triggers exist, add multi trigger terms

+  if( patTerms.empty() ){

+    patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );

+  }

+#else

+  patTerms.insert( patTerms.begin(), d_patTerms[0][f].begin(), d_patTerms[0][f].end() );

+  patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );

+#endif

+

+  if( !patTerms.empty() ){

+    Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl;

+    //sort terms based on relevance

+    if( d_rlv_strategy==RELEVANCE_DEFAULT ){

+      sortQuantifiersForSymbol sqfs;

+      sqfs.d_qe = d_quantEngine;

+      //sort based on # occurrences (this will cause Trigger to select rarer symbols)

+      std::sort( patTerms.begin(), patTerms.end(), sqfs );

+      Debug("relevant-trigger") << "Terms based on relevance: " << std::endl;

+      for( int i=0; i<(int)patTerms.size(); i++ ){

+        Debug("relevant-trigger") << "   " << patTerms[i] << " (";

+        Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;

+      }

+      //Notice() << "Terms based on relevance: " << std::endl;

+      //for( int i=0; i<(int)patTerms.size(); i++ ){

+      //  Notice() << "   " << patTerms[i] << " (";

+      //  Notice() << d_quantEngine->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;

+      //}

+    }

+    //now, generate the trigger...

+    int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0;

+    Trigger* tr = NULL;

+    if( d_is_single_trigger[ patTerms[0] ] ){

+      tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL,

+                               options::smartTriggers() );

+      d_single_trigger_gen[ patTerms[0] ] = true;

+    }else{

+      //if we are re-generating triggers, shuffle based on some method

+      if( d_made_multi_trigger[f] ){

+#ifndef MULTI_MULTI_TRIGGERS

+        return;

+#endif

+        std::random_shuffle( patTerms.begin(), patTerms.end() ); //shuffle randomly

+      }else{

+        d_made_multi_trigger[f] = true;

+      }

+      //will possibly want to get an old trigger

+      tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD,

+                               options::smartTriggers() );

+    }

+    if( tr ){

+      if( tr->isMultiTrigger() ){

+        //disable all other multi triggers

+        for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[f].begin(); it != d_auto_gen_trigger[f].end(); ++it ){

+          if( it->first->isMultiTrigger() ){

+            d_auto_gen_trigger[f][ it->first ] = false;

+          }

+        }

+      }

+      //making it during an instantiation round, so must reset

+      if( d_auto_gen_trigger[f].find( tr )==d_auto_gen_trigger[f].end() ){

+        tr->resetInstantiationRound();

+        tr->reset( Node::null() );

+      }

+      d_auto_gen_trigger[f][tr] = true;

+      //if we are generating additional triggers...

+      if( d_generate_additional && d_is_single_trigger[ patTerms[0] ] ){

+        int index = 0;

+        if( index<(int)patTerms.size() ){

+          //Notice() << "check add additional" << std::endl;

+          //check if similar patterns exist, and if so, add them additionally

+          int nqfs_curr = d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[0].getOperator() );

+          index++;

+          bool success = true;

+          while( success && index<(int)patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){

+            success = false;

+            if( d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){

+              d_single_trigger_gen[ patTerms[index] ] = true;

+              Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL,

+                                                 options::smartTriggers() );

+              if( tr2 ){

+                //Notice() << "Add additional trigger " << patTerms[index] << std::endl;

+                tr2->resetInstantiationRound();

+                tr2->reset( Node::null() );

+                d_auto_gen_trigger[f][tr2] = true;

+              }

+              success = true;

+            }

+            index++;

+          }

+          //Notice() << "done check add additional" << std::endl;

+        }

+      }

+    }

+  }

+}

+/*

+InstStrategyAutoGenTriggers::Statistics::Statistics():

+  d_instantiations("InstStrategyAutoGenTriggers::Instantiations", 0),

+  d_instantiations_min("InstStrategyAutoGenTriggers::Instantiations_min", 0)

+{

+  StatisticsRegistry::registerStat(&d_instantiations);

+  StatisticsRegistry::registerStat(&d_instantiations_min);

+}

+

+InstStrategyAutoGenTriggers::Statistics::~Statistics(){

+  StatisticsRegistry::unregisterStat(&d_instantiations);

+  StatisticsRegistry::unregisterStat(&d_instantiations_min);

+}

+*/

+

+void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){

+}

+

+int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){

+  if( e<5 ){

+    return STATUS_UNFINISHED;

+  }else{

+    if( d_guessed.find( f )==d_guessed.end() ){

+      d_guessed[f] = true;

+      Debug("quant-uf-alg") << "Add guessed instantiation" << std::endl;

+      InstMatch m;

+      if( d_quantEngine->addInstantiation( f, m ) ){

+        ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);

+        //d_quantEngine->d_hasInstantiated[f] = true;

+      }

+    }

+    return STATUS_UNKNOWN;

+  }

+}

+/*

+InstStrategyFreeVariable::Statistics::Statistics():

+  d_instantiations("InstStrategyGuess::Instantiations", 0)

+{

+  StatisticsRegistry::registerStat(&d_instantiations);

+}

+

+InstStrategyFreeVariable::Statistics::~Statistics(){

+  StatisticsRegistry::unregisterStat(&d_instantiations);

+}

+*/

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

+/*! \file inst_strategy_e_matching.h

+ ** \verbatim

+ ** Original author: ajreynol

+ ** Major contributors: none

+ ** Minor contributors (to current version): bobot, mdeters

+ ** 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 E matching instantiation strategies

+ **/

+

+#include "cvc4_private.h"

+

+#ifndef __CVC4__INST_STRATEGY_E_MATCHING_H

+#define __CVC4__INST_STRATEGY_E_MATCHING_H

+

+#include "theory/quantifiers_engine.h"

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

+

+#include "context/context.h"

+#include "context/context_mm.h"

+

+#include "util/statistics_registry.h"

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

+

+namespace CVC4 {

+namespace theory {

+namespace quantifiers {

+

+//instantiation strategies

+

+class InstStrategyUserPatterns : public InstStrategy{

+private:

+  /** explicitly provided patterns */

+  std::map< Node, std::vector< inst::Trigger* > > d_user_gen;

+  /** counter for quantifiers */

+  std::map< Node, int > d_counter;

+  /** process functions */

+  void processResetInstantiationRound( Theory::Effort effort );

+  int process( Node f, Theory::Effort effort, int e );

+public:

+  InstStrategyUserPatterns( QuantifiersEngine* ie ) :

+      InstStrategy( ie ){}

+  ~InstStrategyUserPatterns(){}

+public:

+  /** add pattern */

+  void addUserPattern( Node f, Node pat );

+  /** get num patterns */

+  int getNumUserGenerators( Node f ) { return (int)d_user_gen[f].size(); }

+  /** get user pattern */

+  inst::Trigger* getUserGenerator( Node f, int i ) { return d_user_gen[f][ i ]; }

+  /** identify */

+  std::string identify() const { return std::string("UserPatterns"); }

+};/* class InstStrategyUserPatterns */

+

+class InstStrategyAutoGenTriggers : public InstStrategy{

+public:

+  enum {

+    RELEVANCE_NONE,

+    RELEVANCE_DEFAULT,

+  };

+private:

+  /** trigger generation strategy */

+  int d_tr_strategy;

+  /** relevance strategy */

+  int d_rlv_strategy;

+  /** regeneration */

+  bool d_regenerate;

+  int d_regenerate_frequency;

+  /** generate additional triggers */

+  bool d_generate_additional;

+  /** triggers for each quantifier */

+  std::map< Node, std::map< inst::Trigger*, bool > > d_auto_gen_trigger;

+  std::map< Node, int > d_counter;

+  /** single, multi triggers for each quantifier */

+  std::map< Node, std::vector< Node > > d_patTerms[2];

+  std::map< Node, bool > d_is_single_trigger;

+  std::map< Node, bool > d_single_trigger_gen;

+  std::map< Node, bool > d_made_multi_trigger;

+private:

+  /** process functions */

+  void processResetInstantiationRound( Theory::Effort effort );

+  int process( Node f, Theory::Effort effort, int e );

+  /** generate triggers */

+  void generateTriggers( Node f );

+public:

+  InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt, int rstrt, int rgfr = -1 ) :

+      InstStrategy( qe ), d_tr_strategy( tstrt ), d_rlv_strategy( rstrt ), d_generate_additional( false ){

+    setRegenerateFrequency( rgfr );

+  }

+  ~InstStrategyAutoGenTriggers(){}

+public:

+  /** get auto-generated trigger */

+  inst::Trigger* getAutoGenTrigger( Node f );

+  /** identify */

+  std::string identify() const { return std::string("AutoGenTriggers"); }

+  /** set regenerate frequency, if fr<0, turn off regenerate */

+  void setRegenerateFrequency( int fr ){

+    if( fr<0 ){

+      d_regenerate = false;

+    }else{

+      d_regenerate_frequency = fr;

+      d_regenerate = true;

+    }

+  }

+  /** set generate additional */

+  void setGenerateAdditional( bool val ) { d_generate_additional = val; }

+};/* class InstStrategyAutoGenTriggers */

+

+class InstStrategyFreeVariable : public InstStrategy{

+private:

+  /** guessed instantiations */

+  std::map< Node, bool > d_guessed;

+  /** process functions */

+  void processResetInstantiationRound( Theory::Effort effort );

+  int process( Node f, Theory::Effort effort, int e );

+public:

+  InstStrategyFreeVariable( QuantifiersEngine* qe ) :

+      InstStrategy( qe ){}

+  ~InstStrategyFreeVariable(){}

+  /** identify */

+  std::string identify() const { return std::string("FreeVariable"); }

+};/* class InstStrategyFreeVariable */

+

+}

+}/* CVC4::theory namespace */

+}/* CVC4 namespace */

+

+#endif

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 8d935a323..579c53665 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -15,10 +15,12 @@
 #include "theory/quantifiers/instantiation_engine.h"
 
 #include "theory/theory_engine.h"
-#include "theory/uf/theory_uf_instantiator.h"
 #include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/inst_strategy_e_matching.h"
+#include "theory/quantifiers/inst_strategy_cbqi.h"
+#include "theory/quantifiers/trigger.h"
 
 using namespace std;
 using namespace CVC4;
@@ -26,12 +28,49 @@ using namespace CVC4::kind;
 using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
+using namespace CVC4::theory::inst;
 
 InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) :
 QuantifiersModule( qe ), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ), d_performCheck( false ){
 
 }
 
+void InstantiationEngine::finishInit(){
+  //for UF terms
+  if( !options::finiteModelFind() || options::fmfInstEngine() ){
+    //if( options::cbqi() ){
+    //  addInstStrategy( new InstStrategyCheckCESolved( this, d_quantEngine ) );
+    //}
+    //these are the instantiation strategies for basic E-matching
+    if( options::userPatternsQuant() ){
+      d_isup = new InstStrategyUserPatterns( d_quantEngine );
+      addInstStrategy( d_isup );
+    }else{
+      d_isup = NULL;
+    }
+    InstStrategyAutoGenTriggers* i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, Trigger::TS_ALL,
+                                                                         InstStrategyAutoGenTriggers::RELEVANCE_DEFAULT, 3 );
+    i_ag->setGenerateAdditional( true );
+    addInstStrategy( i_ag );
+    //addInstStrategy( new InstStrategyAddFailSplits( this, ie ) );
+    if( !options::finiteModelFind() ){
+      addInstStrategy( new InstStrategyFreeVariable( d_quantEngine ) );
+    }
+    //d_isup->setPriorityOver( i_ag );
+    //d_isup->setPriorityOver( i_agm );
+    //i_ag->setPriorityOver( i_agm );
+  }
+  //CBQI: FIXME
+  //for arithmetic
+  //if( options::cbqi() ){
+  //  addInstStrategy( new InstStrategySimplex( d_quantEngine ) );
+  //}
+  //for datatypes
+  //if( options::cbqi() ){
+  //  addInstStrategy( new InstStrategyDatatypesValue( d_quantEngine ) );
+  //}
+}
+
 
 bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
   //if counterexample-based quantifier instantiation is active
@@ -68,9 +107,10 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
   //reset the quantifiers engine
   Debug("inst-engine-ctrl") << "Reset IE" << std::endl;
   //reset the instantiators
-  for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){
-    if( d_quantEngine->getInstantiator( i ) ){
-      d_quantEngine->getInstantiator( i )->resetInstantiationRound( effort );
+  for( size_t i=0; i<d_instStrategies.size(); ++i ){
+    InstStrategy* is = d_instStrategies[i];
+    if( isActiveStrategy( is ) ){
+      is->processResetInstantiationRound( effort );
     }
   }
   //iterate over an internal effort level e
@@ -90,11 +130,12 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
         //int e_use = d_quantEngine->getRelevance( f )==-1 ? e - 1 : e;
         int e_use = e;
         if( e_use>=0 ){
-          //use each theory instantiator to instantiate f
-          for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){
-            if( d_quantEngine->getInstantiator( i ) ){
-              Debug("inst-engine-debug") << "Do " << d_quantEngine->getInstantiator( i )->identify() << " " << e_use << std::endl;
-              int quantStatus = d_quantEngine->getInstantiator( i )->doInstantiation( f, effort, e_use );
+          //check each instantiation strategy
+          for( size_t i=0; i<d_instStrategies.size(); ++i ){
+            InstStrategy* is = d_instStrategies[i];
+            if( isActiveStrategy( is ) && is->shouldProcess( f ) ){
+              Debug("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl;
+              int quantStatus = is->process( f, effort, e_use );
               Debug("inst-engine-debug") << " -> status is " << quantStatus << std::endl;
               InstStrategy::updateStatus( d_inst_round_status, quantStatus );
             }
@@ -112,13 +153,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
   Debug("inst-engine") << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl;
   //Notice() << "All instantiators finished, # added lemmas = " << (int)d_lemmas_waiting.size() << std::endl;
   if( !d_quantEngine->hasAddedLemma() ){
-    Debug("inst-engine-stuck") << "No instantiations produced at this state: " << std::endl;
-    for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){
-      if( d_quantEngine->getInstantiator( i ) ){
-        d_quantEngine->getInstantiator( i )->debugPrint("inst-engine-stuck");
-        Debug("inst-engine-stuck") << std::endl;
-      }
-    }
+    Debug("inst-engine-stuck") << "No instantiations produced at this state." << std::endl;
     Debug("inst-engine-ctrl") << "---Fail." << std::endl;
     return false;
   }else{
@@ -238,9 +273,6 @@ void InstantiationEngine::registerQuantifier( Node f ){
   Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
   if( !doCbqi( f ) ){
     d_quantEngine->addTermToDatabase( ceBody, true );
-    //need to tell which instantiators will be responsible
-    //by default, just chose the UF instantiator
-    d_quantEngine->getInstantiator( theory::THEORY_UF )->setQuantifierActive( f );
   }
 
   //take into account user patterns
@@ -249,7 +281,7 @@ void InstantiationEngine::registerQuantifier( Node f ){
     //add patterns
     for( int i=0; i<(int)subsPat.getNumChildren(); i++ ){
       //Notice() << "Add pattern " << subsPat[i] << " for " << f << std::endl;
-      ((uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( theory::THEORY_UF ))->addUserPattern( f, subsPat[i] );
+      addUserPattern( f, subsPat[i] );
     }
   }
 }
@@ -359,4 +391,38 @@ Node InstantiationEngine::getNextDecisionRequest(){
     }
   }
   return Node::null();
-}
\ No newline at end of file
+}
+
+void InstantiationEngine::addUserPattern( Node f, Node pat ){
+  if( d_isup ){
+    d_isup->addUserPattern( f, pat );
+  }
+}
+
+InstantiationEngine::Statistics::Statistics():
+  d_instantiations_user_patterns("InstantiationEngine::Instantiations_User_Patterns", 0),
+  d_instantiations_auto_gen("InstantiationEngine::Instantiations_Auto_Gen", 0),
+  d_instantiations_auto_gen_min("InstantiationEngine::Instantiations_Auto_Gen_Min", 0),
+  d_instantiations_guess("InstantiationEngine::Instantiations_Guess", 0),
+  d_instantiations_cbqi_arith("InstantiationEngine::Instantiations_Cbqi_Arith", 0),
+  d_instantiations_cbqi_arith_minus("InstantiationEngine::Instantiations_Cbqi_Arith_Minus", 0),
+  d_instantiations_cbqi_datatypes("InstantiationEngine::Instantiations_Cbqi_Datatypes", 0)
+{
+  StatisticsRegistry::registerStat(&d_instantiations_user_patterns);
+  StatisticsRegistry::registerStat(&d_instantiations_auto_gen);
+  StatisticsRegistry::registerStat(&d_instantiations_auto_gen_min);
+  StatisticsRegistry::registerStat(&d_instantiations_guess);
+  StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith);
+  StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith_minus);
+  StatisticsRegistry::registerStat(&d_instantiations_cbqi_datatypes);
+}
+
+InstantiationEngine::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_instantiations_user_patterns);
+  StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen);
+  StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen_min);
+  StatisticsRegistry::unregisterStat(&d_instantiations_guess);
+  StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith);
+  StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith_minus);
+  StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_datatypes);
+}
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index b3bbbce4a..a7ae1ae8e 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -24,9 +24,71 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class InstStrategyUserPatterns;
+
+/** instantiation strategy class */
+class InstStrategy {
+public:
+  enum Status {
+    STATUS_UNFINISHED,
+    STATUS_UNKNOWN,
+    STATUS_SAT,
+  };/* enum Status */
+protected:
+  /** reference to the instantiation engine */
+  QuantifiersEngine* d_quantEngine;
+  /** should process a quantifier */
+  std::map< Node, bool > d_quantActive;
+  /** calculate should process */
+  virtual bool calculateShouldProcess( Node f ) { return true; }
+public:
+  InstStrategy( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
+  virtual ~InstStrategy(){}
+
+  /** should process quantified formula f? */
+  bool shouldProcess( Node f ) {
+    if( d_quantActive.find( f )==d_quantActive.end() ){
+      d_quantActive[f] = calculateShouldProcess( f );
+    }
+    return d_quantActive[f];
+  }
+  /** reset instantiation */
+  virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
+  /** process method, returns a status */
+  virtual int process( Node f, Theory::Effort effort, int e ) = 0;
+  /** update status */
+  static void updateStatus( int& currStatus, int addStatus ){
+    if( addStatus==STATUS_UNFINISHED ){
+      currStatus = STATUS_UNFINISHED;
+    }else if( addStatus==STATUS_UNKNOWN ){
+      if( currStatus==STATUS_SAT ){
+        currStatus = STATUS_UNKNOWN;
+      }
+    }
+  }
+  /** identify */
+  virtual std::string identify() const { return std::string("Unknown"); }
+};/* class InstStrategy */
+
 class InstantiationEngine : public QuantifiersModule
 {
 private:
+  /** instantiation strategies */
+  std::vector< InstStrategy* > d_instStrategies;
+  /** instantiation strategies active */
+  std::map< InstStrategy*, bool > d_instStrategyActive;
+  /** user-pattern instantiation strategy */
+  InstStrategyUserPatterns* d_isup;
+  /** is instantiation strategy active */
+  bool isActiveStrategy( InstStrategy* is ) {
+    return d_instStrategyActive.find( is )!=d_instStrategyActive.end() && d_instStrategyActive[is];
+  }
+  /** add inst strategy */
+  void addInstStrategy( InstStrategy* is ){
+    d_instStrategies.push_back( is );
+    d_instStrategyActive[is] = true;
+  }
+private:
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
   /** status of instantiation round (one of InstStrategy::STATUS_*) */
   int d_inst_round_status;
@@ -62,6 +124,8 @@ private:
 public:
   InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete = true );
   ~InstantiationEngine(){}
+  /** initialize */
+  void finishInit();
 
   bool needsCheck( Theory::Effort e );
   void check( Theory::Effort e );
@@ -69,6 +133,23 @@ public:
   void assertNode( Node f );
   Node explain(TNode n){ return Node::null(); }
   Node getNextDecisionRequest();
+  /** add user pattern */
+  void addUserPattern( Node f, Node pat );
+public:
+  /** statistics class */
+  class Statistics {
+  public:
+    IntStat d_instantiations_user_patterns;
+    IntStat d_instantiations_auto_gen;
+    IntStat d_instantiations_auto_gen_min;
+    IntStat d_instantiations_guess;
+    IntStat d_instantiations_cbqi_arith;
+    IntStat d_instantiations_cbqi_arith_minus;
+    IntStat d_instantiations_cbqi_datatypes;
+    Statistics();
+    ~Statistics();
+  };
+  Statistics d_statistics;
 };/* class InstantiationEngine */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/instantiator_default.cpp b/src/theory/quantifiers/instantiator_default.cpp
deleted file mode 100644
index def3c9f58..000000000
--- a/src/theory/quantifiers/instantiator_default.cpp
+++ /dev/null
@@ -1,54 +0,0 @@
-/*********************                                                        */
-/*! \file instantiator_default.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): bobot, mdeters
- ** 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 Implementation of instantiator_default class
- **/
-
-#include "theory/quantifiers/instantiator_default.h"
-#include "theory/theory_engine.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-
-InstantiatorDefault::InstantiatorDefault(context::Context* c, QuantifiersEngine* ie, Theory* th) :
-  Instantiator( c, ie, th ) {
-}
-
-void InstantiatorDefault::assertNode( Node assertion ){
-}
-
-void InstantiatorDefault::processResetInstantiationRound( Theory::Effort effort ){
-}
-
-int InstantiatorDefault::process( Node f, Theory::Effort effort, int e ){
-  /*
-  if( e < 4 ){
-    return InstStrategy::STATUS_UNFINISHED;
-  }else if( e == 4 ){
-    Debug("quant-default") << "Process " << f << " : " << std::endl;
-    InstMatch m;
-    for( int j=0; j<(int)d_quantEngine->getNumInstantiationConstants( f ); j++ ){
-      Node i = d_quantEngine->getInstantiationConstant( f, j );
-      Debug("quant-default") << "Getting value for " << i << std::endl;
-      if( d_quantEngine->getTheoryEngine()->theoryOf( i )==getTheory() ){    //if it belongs to this theory
-        Node val = d_th->getValue( i );
-        Debug("quant-default") << "Default Instantiate for " << d_th->getId() << ", setting " << i << " = " << val << std::endl;
-        m.set( i, val);
-      }
-    }
-    d_quantEngine->addInstantiation( f, m );
-  }
-  */
-  return InstStrategy::STATUS_UNKNOWN;
-}
diff --git a/src/theory/quantifiers/instantiator_default.h b/src/theory/quantifiers/instantiator_default.h
deleted file mode 100644
index d21499ae0..000000000
--- a/src/theory/quantifiers/instantiator_default.h
+++ /dev/null
@@ -1,46 +0,0 @@
-/*********************                                                        */
-/*! \file instantiator_default.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: mdeters
- ** 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 instantiator_default
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__QUANTIFIERS__INSTANTIATOR_DEFAULT_H
-#define __CVC4__THEORY__QUANTIFIERS__INSTANTIATOR_DEFAULT_H
-
-#include <string>
-#include "theory/quantifiers_engine.h"
-
-namespace CVC4 {
-namespace theory {
-
-class InstantiatorDefault : public Instantiator {
-  friend class QuantifiersEngine;
-protected:
-  /** reset instantiation round */
-  void processResetInstantiationRound(Theory::Effort effort);
-  /** process quantifier */
-  int process( Node f, Theory::Effort effort, int e );
-public:
-  InstantiatorDefault(context::Context* c, QuantifiersEngine* ie, Theory* th);
-  ~InstantiatorDefault() { }
-  /** check function, assertion is asserted to theory */
-  void assertNode( Node assertion );
-  /** identify */
-  std::string identify() const { return std::string("InstantiatorDefault"); }
-};/* class InstantiatorDefault */
-
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATOR_DEFAULT_H */
diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds
index c81816528..ab0e9d934 100644
--- a/src/theory/quantifiers/kinds
+++ b/src/theory/quantifiers/kinds
@@ -6,7 +6,6 @@
 
 theory THEORY_QUANTIFIERS ::CVC4::theory::quantifiers::TheoryQuantifiers "theory/quantifiers/theory_quantifiers.h"
 typechecker "theory/quantifiers/theory_quantifiers_type_rules.h"
-instantiator ::CVC4::theory::quantifiers::InstantiatorTheoryQuantifiers "theory/quantifiers/theory_quantifiers_instantiator.h"
 
 properties check propagate presolve getNextDecisionRequest
 
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index c7e68acb1..2f44140c2 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -17,7 +17,6 @@
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/uf/theory_uf_model.h"
-#include "theory/uf/theory_uf_instantiator.h"
 #include "theory/uf/theory_uf_strong_solver.h"
 #include "theory/arrays/theory_arrays_model.h"
 #include "theory/quantifiers/first_order_model.h"
@@ -25,6 +24,7 @@
 #include "theory/quantifiers/model_builder.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/inst_gen.h"
+#include "theory/quantifiers/trigger.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 456914818..bf6ea11f0 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -17,7 +17,6 @@
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/uf/theory_uf_strong_solver.h"
-#include "theory/uf/theory_uf_instantiator.h"
 #include "theory/quantifiers/options.h"
 #include "theory/arrays/theory_arrays_model.h"
 #include "theory/quantifiers/first_order_model.h"
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 9a26878b5..d60aa2ef4 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -106,7 +106,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
                 addedLemmas += d_op_triggers[op][i]->addTerm( n );
               }
               //Message() << "Terms, added lemmas: " << addedLemmas << std::endl;
-              d_quantEngine->flushLemmas( &d_quantEngine->getTheoryEngine()->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel() );
+              d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
             }
           }
         }
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 446c9285e..cfdb30f38 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -22,7 +22,6 @@
 #include "theory/quantifiers/model_engine.h"
 #include "expr/kind.h"
 #include "util/cvc4_assert.h"
-#include "theory/quantifiers/theory_quantifiers_instantiator.h"
 #include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
diff --git a/src/theory/quantifiers/theory_quantifiers_instantiator.cpp b/src/theory/quantifiers/theory_quantifiers_instantiator.cpp
deleted file mode 100644
index eabb4ceda..000000000
--- a/src/theory/quantifiers/theory_quantifiers_instantiator.cpp
+++ /dev/null
@@ -1,73 +0,0 @@
-/*********************                                                        */
-/*! \file theory_quantifiers_instantiator.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** 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 Implementation of theory_quantifiers_instantiator class
- **/
-
-#include "theory/quantifiers/theory_quantifiers_instantiator.h"
-#include "theory/quantifiers/theory_quantifiers.h"
-#include "theory/quantifiers/options.h"
-#include "theory/theory_engine.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-
-InstantiatorTheoryQuantifiers::InstantiatorTheoryQuantifiers(context::Context* c, QuantifiersEngine* ie, Theory* th) :
-Instantiator( c, ie, th ){
-
-}
-
-void InstantiatorTheoryQuantifiers::assertNode( Node assertion ){
-  Debug("quant-quant-assert") << "InstantiatorTheoryQuantifiers::check: " << assertion << std::endl;
-  if( options::cbqi() ){
-    if( assertion.hasAttribute(InstConstantAttribute()) ){
-      Debug("quant-quant-assert") << "   -> has constraints from " << assertion.getAttribute(InstConstantAttribute()) << std::endl;
-      setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
-    }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
-      Debug("quant-quant-assert") << "   -> has constraints from " << assertion[0].getAttribute(InstConstantAttribute()) << std::endl;
-      setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) );
-    }
-  }
-}
-
-void InstantiatorTheoryQuantifiers::processResetInstantiationRound( Theory::Effort effort ){
-
-}
-
-
-int InstantiatorTheoryQuantifiers::process( Node f, Theory::Effort effort, int e ){
-  Debug("quant-quant") << "Quant: Try to solve (" << e << ") for " << f << "... " << std::endl;
-  if( e<5 ){
-    return InstStrategy::STATUS_UNFINISHED;
-  }else if( e==5 ){
-    //add random addition
-    InstMatch m;
-    if( d_quantEngine->addInstantiation( f, m ) ){
-      ++(d_statistics.d_instantiations);
-    }
-  }
-  return InstStrategy::STATUS_UNKNOWN;
-}
-
-InstantiatorTheoryQuantifiers::Statistics::Statistics():
-  d_instantiations("InstantiatorTheoryQuantifiers::Instantiations_Total", 0)
-{
-  StatisticsRegistry::registerStat(&d_instantiations);
-}
-
-InstantiatorTheoryQuantifiers::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_instantiations);
-}
-
diff --git a/src/theory/quantifiers/theory_quantifiers_instantiator.h b/src/theory/quantifiers/theory_quantifiers_instantiator.h
deleted file mode 100644
index 5722c264f..000000000
--- a/src/theory/quantifiers/theory_quantifiers_instantiator.h
+++ /dev/null
@@ -1,58 +0,0 @@
-/*********************                                                        */
-/*! \file theory_quantifiers_instantiator.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: mdeters
- ** 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 instantiator_quantifiers_instantiator
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_INSTANTIATOR_H
-#define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_INSTANTIATOR_H
-
-#include "theory/quantifiers_engine.h"
-
-#include "util/statistics_registry.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class InstantiatorTheoryQuantifiers : public Instantiator{
-  friend class QuantifiersEngine;
-public:
-  InstantiatorTheoryQuantifiers(context::Context* c, QuantifiersEngine* ie, Theory* th);
-  ~InstantiatorTheoryQuantifiers() {}
-
-  /** check function, assertion is asserted to theory */
-  void assertNode( Node assertion );
-  /** identify */
-  std::string identify() const { return std::string("InstantiatorTheoryQuantifiers"); }
-private:
-  /**  reset instantiation */
-  void processResetInstantiationRound( Theory::Effort effort );
-  /** process at effort */
-  int process( Node f, Theory::Effort effort, int e );
-
-  class Statistics {
-  public:
-    IntStat d_instantiations;
-    Statistics();
-    ~Statistics();
-  };
-  Statistics d_statistics;
-};/* class InstantiatiorTheoryQuantifiers */
-
-}/* CVC4::theory::quantifiers namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_INSTANTIATOR_H */
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 4d5efcd8d..bc577fda6 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -15,7 +15,6 @@
 #include "theory/quantifiers/trigger.h"
 #include "theory/theory_engine.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/uf/theory_uf_instantiator.h"
 #include "theory/quantifiers/candidate_generator.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/quantifiers/options.h"