Restrict LtePartialInst instantiations based on E-matching, promote to quantifiers module. Refactor QuantifiersEngine registration and check.

11 files changed, 451 insertions, 248 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index c72e11809..184ef5d56 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -327,6 +327,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/conjecture_generator.cpp \
 	theory/quantifiers/ce_guided_instantiation.h \
 	theory/quantifiers/ce_guided_instantiation.cpp \
+	theory/quantifiers/local_theory_ext.h \
+	theory/quantifiers/local_theory_ext.cpp \
 	theory/quantifiers/fun_def_process.h \
 	theory/quantifiers/fun_def_process.cpp \
 	theory/quantifiers/options_handlers.h \
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index d4f32becc..eef354e75 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -36,14 +36,21 @@ d_qe( qe ), d_axiom_asserted( c, false ), d_forall_asserts( c ), d_isModelSet( c
 
 }
 
-void FirstOrderModel::assertQuantifier( Node n ){
-  if( n.getKind()==FORALL ){
-    d_forall_asserts.push_back( n );
-    if( n.getAttribute(AxiomAttribute()) ){
-      d_axiom_asserted = true;
+void FirstOrderModel::assertQuantifier( Node n, bool reduced ){
+  if( !reduced ){
+    if( n.getKind()==FORALL ){
+      d_forall_asserts.push_back( n );
+      if( n.getAttribute(AxiomAttribute()) ){
+        d_axiom_asserted = true;
+      }
+    }else if( n.getKind()==NOT ){
+      Assert( n[0].getKind()==FORALL );
     }
-  }else if( n.getKind()==NOT ){
-    Assert( n[0].getKind()==FORALL );
+  }else{
+    Assert( n.getKind()==FORALL );
+    Assert( d_forall_to_reduce.find( n )==d_forall_to_reduce.end() );
+    d_forall_to_reduce[n] = true;
+    Trace("quant") << "Mark to reduce : " << n << std::endl;
   }
 }
 
@@ -112,6 +119,18 @@ Node FirstOrderModel::getSomeDomainElement(TypeNode tn){
   return d_rep_set.d_type_reps[tn][0];
 }
 
+/** needs check */
+bool FirstOrderModel::checkNeeded() {
+  return d_forall_asserts.size()>0 || !d_forall_to_reduce.empty();
+}
+
+/** mark reduced */
+void FirstOrderModel::markQuantifierReduced( Node q ) {
+  Assert( d_forall_to_reduce.find( q )!=d_forall_to_reduce.end() );
+  d_forall_to_reduce.erase( q );
+  Trace("quant") << "Mark reduced : " << q << std::endl;
+}
+
 void FirstOrderModel::reset_round() {
   d_quant_active.clear();
 }
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 77ccad247..c2cd88e17 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -51,6 +51,8 @@ protected:
   context::CDO< bool > d_axiom_asserted;
   /** list of quantifiers asserted in the current context */
   context::CDList<Node> d_forall_asserts;
+  /** list of quantifiers that have been marked to reduce */
+  std::map< Node, bool > d_forall_to_reduce;
   /** is model set */
   context::CDO< bool > d_isModelSet;
   /** get variable id */
@@ -59,11 +61,13 @@ protected:
   virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0;
 public: //for Theory Quantifiers:
   /** assert quantifier */
-  void assertQuantifier( Node n );
+  void assertQuantifier( Node n, bool reduced = false );
   /** get number of asserted quantifiers */
   int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); }
   /** get asserted quantifier */
   Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; }
+  /** get number to reduce quantifiers */
+  unsigned getNumToReduceQuantifiers() { return d_forall_to_reduce.size(); }
   /** bool axiom asserted */
   bool isAxiomAsserted() { return d_axiom_asserted; }
   /** initialize model for term */
@@ -92,6 +96,10 @@ public:
   }
   /** get some domain element */
   Node getSomeDomainElement(TypeNode tn);
+  /** do we need to do any work? */
+  bool checkNeeded();
+  /** mark reduced */
+  void markQuantifierReduced( Node q );
 private:
   //list of inactive quantified formulas
   std::map< TNode, bool > d_quant_active;
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 6a2bd5e2e..f378b4913 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -19,6 +19,7 @@
 #include "theory/theory_engine.h"
 #include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/first_order_model.h"
 
 using namespace std;
 using namespace CVC4;
@@ -255,9 +256,9 @@ void InstStrategySimplex::debugPrint( const char* c ){
     //}
   }
   Debug(c) << std::endl;
-
-  for( int q=0; q<d_quantEngine->getNumQuantifiers(); q++ ){
-    Node f = d_quantEngine->getQuantifier( q );
+  
+  for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+    Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
     Debug(c) << f << std::endl;
     Debug(c) << "   Inst constants: ";
     for( int i=0; i<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index b53919aaf..518921433 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -64,11 +64,11 @@ void InstantiationEngine::finishInit(){
     d_instStrategies.push_back( d_i_ag );
   }
   
-  //local theory extensions
-  if( options::localTheoryExt() ){
-    d_i_lte = new InstStrategyLocalTheoryExt( d_quantEngine );
-    d_instStrategies.push_back( d_i_lte );
-  }
+  //local theory extensions TODO?
+  //if( options::localTheoryExt() ){
+  //  d_i_lte = new InstStrategyLocalTheoryExt( d_quantEngine );
+  //  d_instStrategies.push_back( d_i_lte );
+  //}
   
   //full saturation : instantiate from relevant domain, then arbitrary terms
   if( options::fullSaturateQuant() ){
diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp
new file mode 100644
index 000000000..d62fa02c2
--- /dev/null
+++ b/src/theory/quantifiers/local_theory_ext.cpp
@@ -0,0 +1,249 @@
+/*********************                                                        */
+/*! \file quant_util.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  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 local theory ext utilities
+ **/
+
+#include "theory/quantifiers/local_theory_ext.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/first_order_model.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+
+LtePartialInst::LtePartialInst( QuantifiersEngine * qe, context::Context* c ) : 
+QuantifiersModule( qe ), d_wasInvoked( false ), d_needsCheck( false ){
+
+}
+
+/** add quantifier */
+bool LtePartialInst::addQuantifier( Node q ) {
+  if( d_do_inst.find( q )!=d_do_inst.end() ){
+    if( d_do_inst[q] ){
+      d_lte_asserts.push_back( q );
+      return true;
+    }else{
+      return false;
+    }
+  }else{
+    d_vars[q].clear();
+    d_pat_var_order[q].clear();
+    //check if this quantified formula is eligible for partial instantiation
+    std::map< Node, bool > vars;
+    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+      vars[q[0][i]] = true;
+    }
+    getEligibleInstVars( q[1], vars );
+
+    //TODO : instantiate only if we would force ground instances?
+    std::map< Node, int > var_order;
+    bool doInst = true;
+    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+      if( vars[q[0][i]] ){
+        d_vars[q].push_back( q[0][i] );
+        var_order[q[0][i]] = i;
+      }else{
+        Trace("lte-partial-inst-debug") << "...do not consider, variable " << q[0][i] << " was not found in correct position in body." << std::endl;
+        doInst = false;
+        break;
+      }
+    }
+    if( doInst ){
+      //also needs patterns
+      if( q.getNumChildren()==3 && q[2].getNumChildren()==1 ){
+        for( unsigned i=0; i<q[2][0].getNumChildren(); i++ ){
+          Node pat = q[2][0][i];
+          if( pat.getKind()==APPLY_UF ){
+            for( unsigned j=0; j<pat.getNumChildren(); j++ ){
+              if( !addVariableToPatternList( pat[j], d_pat_var_order[q], var_order ) ){
+                doInst = false;
+              }
+            }
+          }else if( !addVariableToPatternList( pat, d_pat_var_order[q], var_order ) ){
+            doInst = false;
+          }
+          if( !doInst ){
+            Trace("lte-partial-inst-debug") << "...do not consider, cannot resolve pattern : " << pat << std::endl;
+            break;
+          }
+        }
+      }else{
+        Trace("lte-partial-inst-debug") << "...do not consider (must have exactly one pattern)." << std::endl;
+      }
+    }
+    
+    
+    Trace("lte-partial-inst") << "LTE: ...will " << ( doInst ? "" : "not ") << "instantiate " << q << std::endl;
+    d_do_inst[q] = doInst;
+    if( doInst ){
+      d_lte_asserts.push_back( q );
+      d_needsCheck = true;
+    }
+    return doInst;
+  }
+}
+
+bool LtePartialInst::addVariableToPatternList( Node v, std::vector< int >& pat_var_order, std::map< Node, int >& var_order ) {
+  std::map< Node, int >::iterator it = var_order.find( v );
+  if( it==var_order.end() ){
+    return false;
+  }else if( std::find( pat_var_order.begin(), pat_var_order.end(), it->second )!=pat_var_order.end() ){
+    return false;
+  }else{
+    pat_var_order.push_back( it->second );
+    return true;
+  }
+}
+
+void LtePartialInst::getEligibleInstVars( Node n, std::map< Node, bool >& vars ) {
+  if( n.getKind()!=APPLY_UF || n.getType().isBoolean() ){
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      if( vars.find( n[i] )!=vars.end() ){
+        vars[n[i]] = false;
+      }
+    }
+  }
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){
+    getEligibleInstVars( n[i], vars );
+  }
+}
+
+/* whether this module needs to check this round */
+bool LtePartialInst::needsCheck( Theory::Effort e ) {
+  return e>=Theory::EFFORT_FULL && d_needsCheck;
+}
+/* Call during quantifier engine's check */
+void LtePartialInst::check( Theory::Effort e, unsigned quant_e ) {
+  //flush lemmas ASAP (they are a reduction)
+  if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT && d_needsCheck ){
+    std::vector< Node > lemmas;
+    getInstantiations( lemmas );
+    //add lemmas to quantifiers engine
+    for( unsigned i=0; i<lemmas.size(); i++ ){
+      d_quantEngine->addLemma( lemmas[i], false );
+    }
+    d_needsCheck = false;
+  }
+}
+
+
+void LtePartialInst::reset() {
+  d_reps.clear();
+  eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
+  while( !eqcs_i.isFinished() ){
+    TNode r = (*eqcs_i);
+    TypeNode tn = r.getType();
+    d_reps[tn].push_back( r );
+    ++eqcs_i;
+  }
+}
+
+
+/** get instantiations */
+void LtePartialInst::getInstantiations( std::vector< Node >& lemmas ) {
+  Trace("lte-partial-inst") << "LTE : get instantiations, # quant = " << d_lte_asserts.size() << std::endl;
+  reset();
+  for( unsigned i=0; i<d_lte_asserts.size(); i++ ){
+    Node q = d_lte_asserts[i];
+    Assert( d_do_inst.find( q )!=d_do_inst.end() && d_do_inst[q] );
+    if( d_inst.find( q )==d_inst.end() ){
+      Trace("lte-partial-inst") << "LTE : Get partial instantiations for " << q << "..." << std::endl;
+      d_inst[q] = true;
+      Assert( !d_vars[q].empty() );
+      //make bound list
+      Node bvl;
+      std::vector< Node > bvs;
+      for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
+        if( std::find( d_vars[q].begin(), d_vars[q].end(), q[0][j] )==d_vars[q].end() ){
+          bvs.push_back( q[0][j] );
+        }
+      }
+      if( !bvs.empty() ){
+        bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs );
+      }
+      std::vector< Node > conj;
+      std::vector< Node > terms;
+      std::vector< TypeNode > types;
+      for( unsigned j=0; j<d_vars[q].size(); j++ ){
+        types.push_back( d_vars[q][j].getType() );
+        terms.push_back( Node::null() );
+      }
+
+      getPartialInstantiations( conj, q, bvl, d_vars[q], terms, types, NULL, 0, 0, 0 );
+      Assert( !conj.empty() );
+      lemmas.push_back( NodeManager::currentNM()->mkNode( OR, q.negate(), conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ) ) );
+      d_wasInvoked = true;
+      d_quantEngine->getModel()->markQuantifierReduced( q );
+    }
+  }
+}
+
+void LtePartialInst::getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl,
+                                               std::vector< Node >& vars, std::vector< Node >& terms, std::vector< TypeNode >& types, TermArgTrie * curr,
+                                               unsigned pindex, unsigned paindex, unsigned iindex ){
+  if( iindex==vars.size() ){
+    Node body = q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+    if( bvl.isNull() ){
+      conj.push_back( body );
+      Trace("lte-partial-inst") << " - ground conjunct : " << body << std::endl;
+    }else{
+      Node nq;
+      if( q.getNumChildren()==3 ){
+        Node ipl = q[2].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+        nq = NodeManager::currentNM()->mkNode( FORALL, bvl, body, ipl );
+      }else{
+        nq = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
+      }
+      Trace("lte-partial-inst") << " - quantified conjunct : " << nq << std::endl;
+      LtePartialInstAttribute ltpia;
+      nq.setAttribute(ltpia,true);
+      conj.push_back( nq );
+    }
+  }else{
+    Assert( pindex<q[2][0].getNumChildren() );
+    Node pat = q[2][0][pindex];
+    Assert( pat.getNumChildren()==0 || paindex<=pat.getNumChildren() );
+    if( pat.getKind()==APPLY_UF ){
+      Assert( paindex<=pat.getNumChildren() );
+      if( paindex==pat.getNumChildren() ){
+        getPartialInstantiations( conj, q, bvl, vars, terms, types, NULL, pindex+1, 0, iindex );
+      }else{
+        if( !curr ){
+          Assert( paindex==0 );
+          //start traversing term index for the operator
+          curr = d_quantEngine->getTermDatabase()->getTermArgTrie( pat.getOperator() );
+        }
+        for( std::map< TNode, TermArgTrie >::iterator it = curr->d_data.begin(); it != curr->d_data.end(); ++it ){
+          terms[d_pat_var_order[q][iindex]] = it->first;
+          getPartialInstantiations( conj, q, bvl, vars, terms, types, &it->second, pindex, paindex+1, iindex+1 );
+        }
+      }
+    }else{
+      std::map< TypeNode, std::vector< Node > >::iterator it = d_reps.find( types[iindex] );
+      if( it!=d_reps.end() ){
+        Trace("lte-partial-inst-debug") << it->second.size() << " reps of type " << types[iindex] << std::endl;
+        for( unsigned i=0; i<it->second.size(); i++ ){
+          terms[d_pat_var_order[q][iindex]] = it->second[i];
+          getPartialInstantiations( conj, q, bvl, vars, terms, types, NULL, pindex+1, 0, iindex+1 );
+        }
+      }else{
+        Trace("lte-partial-inst-debug") << "No reps found of type " << types[iindex] << std::endl;
+      }
+    }
+  }
+}
diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h
new file mode 100644
index 000000000..6e2ee34af
--- /dev/null
+++ b/src/theory/quantifiers/local_theory_ext.h
@@ -0,0 +1,79 @@
+/*********************                                                        */
+/*! \file local_theory_ext.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief local theory extensions util
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__LOCAL_THEORY_EXT_H
+#define __CVC4__THEORY__LOCAL_THEORY_EXT_H
+
+#include "theory/quantifiers_engine.h"
+#include "context/cdo.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class TermArgTrie;  
+
+class LtePartialInst : public QuantifiersModule {
+private:
+  // was this module invoked
+  bool d_wasInvoked;
+  // needs check
+  bool d_needsCheck;
+  //representatives per type
+  std::map< TypeNode, std::vector< Node > > d_reps;
+  // should we instantiate quantifier
+  std::map< Node, bool > d_do_inst;
+  // have we instantiated quantifier
+  std::map< Node, bool > d_inst;
+  std::map< Node, std::vector< Node > > d_vars;
+  std::map< Node, std::vector< int > > d_pat_var_order;
+  /** list of relevant quantifiers asserted in the current context */
+  std::vector< Node > d_lte_asserts;
+  /** reset */
+  void reset();
+  /** get instantiations */
+  void getInstantiations( std::vector< Node >& lemmas );
+  void getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl,
+                                 std::vector< Node >& vars, std::vector< Node >& inst, std::vector< TypeNode >& types, TermArgTrie * curr,
+                                 unsigned pindex, unsigned paindex, unsigned iindex );
+  /** get eligible inst variables */
+  void getEligibleInstVars( Node n, std::map< Node, bool >& vars );
+  
+  bool addVariableToPatternList( Node v, std::vector< int >& pat_var_order, std::map< Node, int >& var_order );
+public:
+  LtePartialInst( QuantifiersEngine * qe, context::Context* c );
+  /** add quantifier : special form of registration */
+  bool addQuantifier( Node q );
+  /** was invoked */
+  bool wasInvoked() { return d_wasInvoked; }
+  
+  /* whether this module needs to check this round */
+  bool needsCheck( Theory::Effort e );
+  /* Call during quantifier engine's check */
+  void check( Theory::Effort e, unsigned quant_e );
+  /* Called for new quantifiers */
+  void registerQuantifier( Node q ) {}
+  void assertNode( Node n ) {}
+  /** Identify this module (for debugging, dynamic configuration, etc..) */
+  std::string identify() const { return "LtePartialInst"; }
+  
+};
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 088ba093f..f73bc7bb2 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -255,142 +255,3 @@ void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool&
     }
   }
 }
-
-
-QuantLtePartialInst::QuantLtePartialInst( QuantifiersEngine * qe, context::Context* c ) : d_wasInvoked( false ), d_qe( qe ), d_lte_asserts( c ){
-
-}
-
-/** add quantifier */
-bool QuantLtePartialInst::addQuantifier( Node q ) {
-  if( d_do_inst.find( q )!=d_do_inst.end() ){
-    if( d_do_inst[q] ){
-      d_lte_asserts.push_back( q );
-      return true;
-    }else{
-      return false;
-    }
-  }else{
-    d_vars[q].clear();
-    //check if this quantified formula is eligible for partial instantiation
-    std::map< Node, bool > vars;
-    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-      vars[q[0][i]] = true;
-    }
-    getEligibleInstVars( q[1], vars );
-
-    //TODO : instantiate only if we would force ground instances?
-    bool doInst = true;
-    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-      if( vars[q[0][i]] ){
-        d_vars[q].push_back( q[0][i] );
-      }else{
-        doInst = false;
-        break;
-      }
-    }
-    Trace("lte-partial-inst") << "LTE: ...will " << ( doInst ? "" : "not ") << "instantiate " << q << std::endl;
-    d_do_inst[q] = doInst;
-    if( doInst ){
-      d_lte_asserts.push_back( q );
-    }
-    return doInst;
-  }
-}
-
-void QuantLtePartialInst::getEligibleInstVars( Node n, std::map< Node, bool >& vars ) {
-  if( n.getKind()!=APPLY_UF || n.getType().isBoolean() ){
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( vars.find( n[i] )!=vars.end() ){
-        vars[n[i]] = false;
-      }
-    }
-  }
-  for( unsigned i=0; i<n.getNumChildren(); i++ ){
-    getEligibleInstVars( n[i], vars );
-  }
-}
-
-void QuantLtePartialInst::reset() {
-  d_reps.clear();
-  eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine();
-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
-  while( !eqcs_i.isFinished() ){
-    TNode r = (*eqcs_i);
-    TypeNode tn = r.getType();
-    d_reps[tn].push_back( r );
-    ++eqcs_i;
-  }
-}
-
-/** get instantiations */
-void QuantLtePartialInst::getInstantiations( std::vector< Node >& lemmas ) {
-  Trace("lte-partial-inst") << "LTE : get instantiations, # quant = " << d_lte_asserts.size() << std::endl;
-  reset();
-  for( unsigned i=0; i<d_lte_asserts.size(); i++ ){
-    Node q = d_lte_asserts[i];
-    Assert( d_do_inst.find( q )!=d_do_inst.end() && d_do_inst[q] );
-    if( d_inst.find( q )==d_inst.end() ){
-      Trace("lte-partial-inst") << "LTE : Get partial instantiations for " << q << "..." << std::endl;
-      d_inst[q] = true;
-      Assert( !d_vars[q].empty() );
-      //make bound list
-      Node bvl;
-      std::vector< Node > bvs;
-      for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
-        if( std::find( d_vars[q].begin(), d_vars[q].end(), q[0][j] )==d_vars[q].end() ){
-          bvs.push_back( q[0][j] );
-        }
-      }
-      if( !bvs.empty() ){
-        bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs );
-      }
-      std::vector< Node > conj;
-      std::vector< Node > terms;
-      std::vector< TypeNode > types;
-      for( unsigned j=0; j<d_vars[q].size(); j++ ){
-        types.push_back( d_vars[q][j].getType() );
-      }
-      getPartialInstantiations( conj, q, bvl, d_vars[q], terms, types, 0 );
-      Assert( !conj.empty() );
-      lemmas.push_back( NodeManager::currentNM()->mkNode( OR, q.negate(), conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ) ) );
-      d_wasInvoked = true;
-    }
-  }
-}
-
-void QuantLtePartialInst::getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl,
-                                                    std::vector< Node >& vars, std::vector< Node >& terms, std::vector< TypeNode >& types, unsigned index ){
-  if( index==vars.size() ){
-    Node body = q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
-    if( bvl.isNull() ){
-      conj.push_back( body );
-      Trace("lte-partial-inst") << " - ground conjunct : " << body << std::endl;
-    }else{
-      Node nq;
-      if( q.getNumChildren()==3 ){
-        Node ipl = q[2].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
-        nq = NodeManager::currentNM()->mkNode( FORALL, bvl, body, ipl );
-      }else{
-        nq = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
-      }
-      Trace("lte-partial-inst") << " - quantified conjunct : " << nq << std::endl;
-      LtePartialInstAttribute ltpia;
-      nq.setAttribute(ltpia,true);
-      conj.push_back( nq );
-    }
-  }else{
-    std::map< TypeNode, std::vector< Node > >::iterator it = d_reps.find( types[index] );
-    if( it!=d_reps.end() ){
-      terms.push_back( Node::null() );
-      Trace("lte-partial-inst-debug") << it->second.size() << " reps of type " << types[index] << std::endl;
-      for( unsigned i=0; i<it->second.size(); i++ ){
-        terms[index] = it->second[i];
-        getPartialInstantiations( conj, q, bvl, vars, terms, types, index+1 );
-      }
-      terms.pop_back();
-    }else{
-      Trace("lte-partial-inst-debug") << "No reps found of type " << types[index] << std::endl;
-    }
-  }
-}
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 116211bfb..d7e220b2e 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -110,38 +110,6 @@ public:
   virtual void setLiberal( bool l ) = 0;
 };/* class EqualityQuery */
 
-class QuantLtePartialInst {
-private:
-  // was this module invoked
-  bool d_wasInvoked;
-  //representatives per type
-  std::map< TypeNode, std::vector< Node > > d_reps;
-  // should we instantiate quantifier
-  std::map< Node, bool > d_do_inst;
-  // have we instantiated quantifier
-  std::map< Node, bool > d_inst;
-  std::map< Node, std::vector< Node > > d_vars;
-  /** pointer to quant engine */
-  QuantifiersEngine * d_qe;
-  /** list of relevant quantifiers asserted in the current context */
-  context::CDList<Node> d_lte_asserts;
-  /** reset */
-  void reset();
-  /** get instantiations */
-  void getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl,
-                                 std::vector< Node >& vars, std::vector< Node >& inst, std::vector< TypeNode >& types, unsigned index );
-  /** get eligible inst variables */
-  void getEligibleInstVars( Node n, std::map< Node, bool >& vars );
-public:
-  QuantLtePartialInst( QuantifiersEngine * qe, context::Context* c );
-  /** add quantifier */
-  bool addQuantifier( Node q );
-  /** get instantiations */
-  void getInstantiations( std::vector< Node >& lemmas );
-  /** was invoked */
-  bool wasInvoked() { return d_wasInvoked; }
-};
-
 
 }
 }
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 7fb6c0bb7..a1a6dcefc 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -30,6 +30,7 @@
 #include "theory/quantifiers/quant_conflict_find.h"
 #include "theory/quantifiers/conjecture_generator.h"
 #include "theory/quantifiers/ce_guided_instantiation.h"
+#include "theory/quantifiers/local_theory_ext.h"
 #include "theory/quantifiers/relevant_domain.h"
 #include "theory/uf/options.h"
 #include "theory/uf/theory_uf.h"
@@ -154,7 +155,8 @@ d_lemmas_produced_c(u){
     d_ceg_inst = NULL;
   }
   if( options::ltePartialInst() ){
-    d_lte_part_inst = new QuantLtePartialInst( this, c );
+    d_lte_part_inst = new quantifiers::LtePartialInst( this, c );
+    d_modules.push_back( d_lte_part_inst );
   }else{
     d_lte_part_inst = NULL;
   }
@@ -260,10 +262,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
   }
   if( e==Theory::EFFORT_FULL ){
     d_ierCounter++;
-    //process partial instantiations for LTE
-    if( d_lte_part_inst ){
-      d_lte_part_inst->getInstantiations( d_lemmas_waiting );
-    }
   }else if( e==Theory::EFFORT_LAST_CALL ){
     d_ierCounter_lc++;
   }
@@ -271,8 +269,8 @@ void QuantifiersEngine::check( Theory::Effort e ){
   bool needsModel = false;
   bool needsFullModel = false;
   std::vector< QuantifiersModule* > qm;
-  if( d_model->getNumAssertedQuantifiers()>0 ){
-    needsCheck = e>=Theory::EFFORT_LAST_CALL;  //always need to check at or above last call
+  if( d_model->checkNeeded() ){
+    needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL;  //always need to check at or above last call
     for( int i=0; i<(int)d_modules.size(); i++ ){
       if( d_modules[i]->needsCheck( e ) ){
         qm.push_back( d_modules[i] );
@@ -288,21 +286,27 @@ void QuantifiersEngine::check( Theory::Effort e ){
   }
   if( needsCheck ){
     Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl;
-    Trace("quant-engine-debug") << "  modules to check : ";
-    for( unsigned i=0; i<qm.size(); i++ ){
-      Trace("quant-engine-debug") << qm[i]->identify() << " ";
+    if( Trace.isOn("quant-engine-debug") ){
+      Trace("quant-engine-debug") << "  modules to check : ";
+      for( unsigned i=0; i<qm.size(); i++ ){
+        Trace("quant-engine-debug") << qm[i]->identify() << " ";
+      }
+      Trace("quant-engine-debug") << std::endl;
+      Trace("quant-engine-debug") << "  # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl;
+      if( d_model->getNumToReduceQuantifiers()>0 ){
+        Trace("quant-engine-debug") << "  # quantified formulas to reduce = " << d_model->getNumToReduceQuantifiers() << std::endl;
+      }
+      if( !d_lemmas_waiting.empty() ){
+        Trace("quant-engine-debug") << "  lemmas waiting = " << d_lemmas_waiting.size() << std::endl;
+      }
+      Trace("quant-engine-debug") << "  Theory engine finished : " << !d_te->needCheck() << std::endl;
+      Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
     }
-    Trace("quant-engine-debug") << std::endl;
-    Trace("quant-engine-debug") << "  # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl;
-    if( !d_lemmas_waiting.empty() ){
-      Trace("quant-engine-debug") << "  lemmas waiting = " << d_lemmas_waiting.size() << std::endl;
+    if( Trace.isOn("quant-engine-ee") ){
+      Trace("quant-engine-ee") << "Equality engine : " << std::endl;
+      debugPrintEqualityEngine( "quant-engine-ee" );
     }
-    Trace("quant-engine-debug") << "  Theory engine finished : " << !d_te->needCheck() << std::endl;
 
-    Trace("quant-engine-ee") << "Equality engine : " << std::endl;
-    debugPrintEqualityEngine( "quant-engine-ee" );
-
-    Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
     //reset relevant information
     d_conflict = false;
     d_hasAddedLemma = false;
@@ -406,36 +410,54 @@ void QuantifiersEngine::check( Theory::Effort e ){
   }
 }
 
-void QuantifiersEngine::registerQuantifier( Node f ){
-  if( std::find( d_quants.begin(), d_quants.end(), f )==d_quants.end() ){
+bool QuantifiersEngine::registerQuantifier( Node f ){
+  std::map< Node, bool >::iterator it = d_quants.find( f );
+  if( it==d_quants.end() ){
     Trace("quant") << "QuantifiersEngine : Register quantifier ";
     Trace("quant") << " : " << f << std::endl;
-    d_quants.push_back( f );
-
     ++(d_statistics.d_num_quant);
     Assert( f.getKind()==FORALL );
-    //make instantiation constants for f
-    d_term_db->makeInstantiationConstantsFor( f );
-    d_term_db->computeAttributes( f );
-    QuantifiersModule * qm = getOwner( f );
-    if( qm!=NULL ){
-      Trace("quant") << "   Owner : " << qm->identify() << std::endl;
-    }
-    //register with quantifier relevance
-    if( d_quant_rel ){
-      d_quant_rel->registerQuantifier( f );
-    }
-    //register with each module
-    for( int i=0; i<(int)d_modules.size(); i++ ){
-      d_modules[i]->registerQuantifier( f );
+    
+    //check whether we should apply a reduction
+    bool reduced = false;
+    if( d_lte_part_inst && !f.getAttribute(LtePartialInstAttribute()) ){
+      Trace("lte-partial-inst") << "LTE: Partially instantiate " << f << "?" << std::endl;
+      if( d_lte_part_inst->addQuantifier( f ) ){
+        reduced = true;
+      }
     }
-    Node ceBody = d_term_db->getInstConstantBody( f );
-    //generate the phase requirements
-    d_phase_reqs[f] = new QuantPhaseReq( ceBody, true );
-    //also register it with the strong solver
-    if( options::finiteModelFind() ){
-      ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f );
+    if( reduced ){
+      d_model->assertQuantifier( f, true );
+      d_quants[f] = false;
+      return false;
+    }else{
+      //make instantiation constants for f
+      d_term_db->makeInstantiationConstantsFor( f );
+      d_term_db->computeAttributes( f );
+      QuantifiersModule * qm = getOwner( f );
+      if( qm!=NULL ){
+        Trace("quant") << "   Owner : " << qm->identify() << std::endl;
+      }
+      //register with quantifier relevance
+      if( d_quant_rel ){
+        d_quant_rel->registerQuantifier( f );
+      }
+      //register with each module
+      for( int i=0; i<(int)d_modules.size(); i++ ){
+        d_modules[i]->registerQuantifier( f );
+      }
+      Node ceBody = d_term_db->getInstConstantBody( f );
+      //generate the phase requirements
+      d_phase_reqs[f] = new QuantPhaseReq( ceBody, true );
+      //also register it with the strong solver
+      if( options::finiteModelFind() ){
+        ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f );
+      }
+      d_quants[f] = true;
+      return true;
     }
+  }else{
+    return it->second;
   }
 }
 
@@ -464,18 +486,14 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
   }
   //assert to modules TODO : handle !pol
   if( pol ){
-    if( d_lte_part_inst && !f.getAttribute(LtePartialInstAttribute()) ){
-      Trace("lte-partial-inst") << "LTE: Partially instantiate " << f << "?" << std::endl;
-      if( d_lte_part_inst->addQuantifier( f ) ){
-        return;
-      }
-    }
     //register the quantifier
-    registerQuantifier( f );
+    bool nreduced = registerQuantifier( f );
     //assert it to each module
-    d_model->assertQuantifier( f );
-    for( int i=0; i<(int)d_modules.size(); i++ ){
-      d_modules[i]->assertNode( f );
+    if( nreduced ){
+      d_model->assertQuantifier( f );
+      for( int i=0; i<(int)d_modules.size(); i++ ){
+        d_modules[i]->assertNode( f );
+      }
     }
   }
 }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index eb4470eec..78609914f 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -89,6 +89,7 @@ namespace quantifiers {
   class QModelBuilder;
   class ConjectureGenerator;
   class CegInstantiation;
+  class LtePartialInst;
 }/* CVC4::theory::quantifiers */
 
 namespace inst {
@@ -135,7 +136,7 @@ private:
   /** ceg instantiation */
   quantifiers::CegInstantiation * d_ceg_inst;
   /** lte partial instantiation */
-  QuantLtePartialInst * d_lte_part_inst;
+  quantifiers::LtePartialInst * d_lte_part_inst;
 public: //effort levels
   enum {
     QEFFORT_CONFLICT,
@@ -144,7 +145,7 @@ public: //effort levels
   };
 private:
   /** list of all quantifiers seen */
-  std::vector< Node > d_quants;
+  std::map< Node, bool > d_quants;
   /** list of all lemmas produced */
   //std::map< Node, bool > d_lemmas_produced;
   BoolMap d_lemmas_produced_c;
@@ -217,6 +218,8 @@ public:  //modules
   quantifiers::ConjectureGenerator * getConjectureGenerator() { return d_sg_gen; }
   /** ceg instantiation */
   quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; }
+  /** local theory ext partial inst */
+  quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; }
 private:
   /** owner of quantified formulas */
   std::map< Node, QuantifiersModule * > d_owner;
@@ -233,7 +236,7 @@ public:
   /** check at level */
   void check( Theory::Effort e );
   /** register quantifier */
-  void registerQuantifier( Node f );
+  bool registerQuantifier( Node f );
   /** register quantifier */
   void registerPattern( std::vector<Node> & pattern);
   /** assert universal quantifier */
@@ -283,11 +286,6 @@ public:
   /** set instantiation level attr */
   static void setInstantiationLevelAttr( Node n, uint64_t level );
 public:
-  /** get number of quantifiers */
-  int getNumQuantifiers() { return (int)d_quants.size(); }
-  /** get quantifier */
-  Node getQuantifier( int i ) { return d_quants[i]; }
-public:
   /** get model */
   quantifiers::FirstOrderModel* getModel() { return d_model; }
   /** get term database */