Implement dynamic splitting for quantified formulas. Minor refactoring of reductions in quantifiers engine.

20 files changed, 365 insertions, 124 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 4f2998e7a..068e30256 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -350,6 +350,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/quant_equality_engine.cpp \
 	theory/quantifiers/ceg_instantiator.h \
 	theory/quantifiers/ceg_instantiator.cpp \
+	theory/quantifiers/quant_split.h \
+	theory/quantifiers/quant_split.cpp \
 	theory/arith/theory_arith_type_rules.h \
 	theory/arith/type_enumerator.h \
 	theory/arith/arithvar.h \
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 99698df99..45a7447aa 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -199,20 +199,24 @@ Cardinality Datatype::computeCardinality( std::vector< Type >& processing ) cons
 bool Datatype::isRecursiveSingleton() const throw(IllegalArgumentException) {
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
   if( d_card_rec_singleton==0 ){
-    Assert( d_card_u_assume.empty() );
-    std::vector< Type > processing;
-    if( computeCardinalityRecSingleton( processing, d_card_u_assume ) ){
-      d_card_rec_singleton = 1;
+    if( isCodatatype() ){
+      Assert( d_card_u_assume.empty() );
+      std::vector< Type > processing;
+      if( computeCardinalityRecSingleton( processing, d_card_u_assume ) ){
+        d_card_rec_singleton = 1;
+      }else{
+        d_card_rec_singleton = -1;
+      }
+      if( d_card_rec_singleton==1 ){
+        Trace("dt-card") << "Datatype " << getName() << " is recursive singleton, dependent upon " << d_card_u_assume.size() << " uninterpreted sorts: " << std::endl;
+        for( unsigned i=0; i<d_card_u_assume.size(); i++ ){
+          Trace("dt-card") << "  " << d_card_u_assume [i] << std::endl;
+        }
+        Trace("dt-card") << std::endl;
+      }
     }else{
       d_card_rec_singleton = -1;
     }
-    if( d_card_rec_singleton==1 ){
-      Trace("dt-card") << "Datatype " << getName() << " is recursive singleton, dependent upon " << d_card_u_assume.size() << " uninterpreted sorts: " << std::endl;
-      for( unsigned i=0; i<d_card_u_assume.size(); i++ ){
-        Trace("dt-card") << "  " << d_card_u_assume [i] << std::endl;
-      }
-      Trace("dt-card") << std::endl;
-    }
   }
   return d_card_rec_singleton==1;
 }
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 1c48f4bb1..f214b032c 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -441,6 +441,20 @@ ground-uf \n\
 \n\
 ";
 
+const std::string OptionsHandler::s_quantDSplitHelp = "\
+Template modes for quantifiers splitting, supported by --quant-split:\n\
+\n\
+none \n\
++ Never split quantified formulas.\n\
+\n\
+default \n\
++ Split quantified formulas over some finite datatypes when finite model finding is enabled.\n\
+\n\
+agg \n\
++ Aggressively split quantified formulas.\n\
+\n\
+";
+
 theory::quantifiers::InstWhenMode OptionsHandler::stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException) {
   if(optarg == "pre-full") {
     return theory::quantifiers::INST_WHEN_PRE_FULL;
@@ -686,6 +700,21 @@ theory::quantifiers::MacrosQuantMode OptionsHandler::stringToMacrosQuantMode(std
   }
 }
 
+theory::quantifiers::QuantDSplitMode OptionsHandler::stringToQuantDSplitMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "none" ) {
+    return theory::quantifiers::QUANT_DSPLIT_MODE_NONE;
+  } else if(optarg == "default") {
+    return theory::quantifiers::QUANT_DSPLIT_MODE_DEFAULT;
+  } else if(optarg == "agg") {
+    return theory::quantifiers::QUANT_DSPLIT_MODE_AGG;
+  } else if(optarg ==  "help") {
+    puts(s_quantDSplitHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --quant-dsplit-mode: `") +
+                          optarg + "'.  Try --quant-dsplit-mode help.");
+  }
+}
 
 // theory/bv/options_handlers.h
 void OptionsHandler::abcEnabledBuild(std::string option, bool value) throw(OptionException) {
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 9aa037004..a2d67be60 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
  ** 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
@@ -100,6 +100,7 @@ public:
   theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException);
+  theory::quantifiers::QuantDSplitMode stringToQuantDSplitMode(std::string option, std::string optarg) throw(OptionException);
 
   // theory/bv/options_handlers.h
   void abcEnabledBuild(std::string option, bool value) throw(OptionException);
@@ -199,6 +200,7 @@ public:
   static const std::string s_iteLiftQuantHelp;
   static const std::string s_literalMatchHelp;
   static const std::string s_macrosQuantHelp;
+  static const std::string s_quantDSplitHelp;
   static const std::string s_mbqiModeHelp;
   static const std::string s_modelFormatHelp;
   static const std::string s_prenexQuantModeHelp;
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 540db38ec..7395a9a30 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -163,6 +163,16 @@ enum MacrosQuantMode {
   MACROS_QUANT_MODE_GROUND_UF,
 };
 
+enum QuantDSplitMode {
+  /** never do quantifiers splitting */
+  QUANT_DSPLIT_MODE_NONE,
+  /** default */
+  QUANT_DSPLIT_MODE_DEFAULT,
+  /** do quantifiers splitting aggressively */
+  QUANT_DSPLIT_MODE_AGG,
+};
+
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index f5a6ee843..cba1423a0 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -283,6 +283,8 @@ option macrosQuant --macros-quant bool :read-write :default false
  perform quantifiers macro expansion
 option macrosQuantMode --macros-quant-mode=MODE CVC4::theory::quantifiers::MacrosQuantMode :default CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF :include "options/quantifiers_modes.h" :handler stringToMacrosQuantMode
  mode for quantifiers macro expansion
+option quantDynamicSplit --quant-dsplit-mode=MODE CVC4::theory::quantifiers::QuantDSplitMode :read-write :default CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_DEFAULT :include "options/quantifiers_modes.h" :handler stringToQuantDSplitMode
+ mode for dynamic quantifiers splitting
 
 ### recursive function options
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 95995a765..d37cbf12d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1882,6 +1882,9 @@ void SmtEngine::setDefaults() {
       options::preSkolemQuantNested.set( false );
     }
   }
+  if( !d_logic.isTheoryEnabled(THEORY_DATATYPES) ){
+    options::quantDynamicSplit.set( quantifiers::QUANT_DSPLIT_MODE_NONE );
+  }
 
   //until bugs 371,431 are fixed
   if( ! options::minisatUseElim.wasSetByUser()){
diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index b72f15a01..d49b37e4c 100644
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -79,7 +79,7 @@ bool AlphaEquivalenceTypeNode::registerNode( AlphaEquivalenceTypeNode* aetn,
   return AlphaEquivalenceNode::registerNode( &(aetn->d_data), qe, q, tt, arg_index );
 }
 
-bool AlphaEquivalence::registerQuantifier( Node q ) {
+bool AlphaEquivalence::reduceQuantifier( Node q ) {
   Assert( q.getKind()==FORALL );
   Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
   //construct canonical quantified formula
@@ -99,7 +99,7 @@ bool AlphaEquivalence::registerQuantifier( Node q ) {
   sto.d_tdb = d_qe->getTermDatabase();
   std::sort( typs.begin(), typs.end(), sto );
   Trace("aeq-debug") << "  ";
-  bool ret = AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count );
+  bool ret = !AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count );
   Trace("aeq") << "  ...result : " << ret << std::endl;
   return ret;
 }
diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h
index 99517fd2a..18a700842 100644
--- a/src/theory/quantifiers/alpha_equivalence.h
+++ b/src/theory/quantifiers/alpha_equivalence.h
@@ -48,7 +48,7 @@ public:
   AlphaEquivalence( QuantifiersEngine* qe ) : d_qe( qe ){}
   ~AlphaEquivalence(){}
 
-  bool registerQuantifier( Node q );
+  bool reduceQuantifier( Node q );
 };
 
 }
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 272f16be8..6c912cdab 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -36,18 +36,11 @@ d_qe( qe ), d_forall_asserts( c ), d_isModelSet( c, false ){
 
 }
 
-void FirstOrderModel::assertQuantifier( Node n, bool reduced ){
-  if( !reduced ){
-    if( n.getKind()==FORALL ){
-      d_forall_asserts.push_back( n );
-    }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;
+void FirstOrderModel::assertQuantifier( Node n ){
+  if( n.getKind()==FORALL ){
+    d_forall_asserts.push_back( n );
+  }else if( n.getKind()==NOT ){
+    Assert( n[0].getKind()==FORALL );
   }
 }
 
@@ -122,20 +115,17 @@ Node FirstOrderModel::getSomeDomainElement(TypeNode tn){
 
 /** 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;
+  return d_forall_asserts.size()>0;
 }
 
 void FirstOrderModel::reset_round() {
   d_quant_active.clear();
 }
 
+//bool FirstOrderModel::isQuantifierAsserted( TNode q ) {
+//  return d_forall_asserts.find( q )!=d_forall_asserts.end();
+//}
+
 void FirstOrderModel::setQuantifierActive( TNode q, bool active ) {
   d_quant_active[q] = active;
 }
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index d42eb61e3..d5dc62667 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -49,8 +49,6 @@ protected:
   QuantifiersEngine * d_qe;
   /** 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,13 +57,11 @@ protected:
   virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0;
 public: //for Theory Quantifiers:
   /** assert quantifier */
-  void assertQuantifier( Node n, bool reduced = false );
+  void assertQuantifier( Node n );
   /** 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(); }
   /** initialize model for term */
   void initializeModelForTerm( Node n, std::map< Node, bool >& visited );
   virtual void processInitializeModelForTerm( Node n ) = 0;
@@ -94,14 +90,14 @@ public:
   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;
 public:
   /** reset round */
   void reset_round();
+  /** is quantified formula asserted */
+  //bool isQuantifierAsserted( TNode q );
   /** set quantified formula active/inactive 
    * a quantified formula may be set inactive if for instance:
    *   - it is entailed by other quantified formulas
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index ad400413e..e6c9b9e6b 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -169,13 +169,15 @@ void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){
 bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visited ){
   if( visited.find( n )==visited.end() ){
     visited[n] = true;
-    if( n.getKind()!=INST_CONSTANT && TermDb::hasInstConstAttr( n ) ){
+    if( n.getKind()!=BOUND_VARIABLE && TermDb::hasBoundVarAttr( n ) ){
       if( !inst::Trigger::isCbqiKind( n.getKind() ) ){
         Trace("cbqi-debug2") << "Non-cbqi kind : " << n.getKind() << " in " << n  << std::endl;
         return true;
       }else if( n.getKind()==MULT && ( n.getNumChildren()!=2 || !n[0].isConst() ) ){
         Trace("cbqi-debug2") << "Non-linear arithmetic : " << n << std::endl;
         return true;
+      }else if( n.getKind()==FORALL ){
+        return hasNonCbqiOperator( n[1], visited );
       }else{
         for( unsigned i=0; i<n.getNumChildren(); i++ ){
           if( hasNonCbqiOperator( n[i], visited ) ){
@@ -220,9 +222,9 @@ bool InstStrategyCbqi::doCbqi( Node q ){
         }else{
           //if quantifier has a non-arithmetic variable, then do not use cbqi
           //if quantifier has an APPLY_UF term, then do not use cbqi
-          Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
+          //Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
           std::map< Node, bool > visited;
-          ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( cb, visited );
+          ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( q[1], visited );
         }
       }
     }
diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp
index 794032c87..86fbdc7f7 100644
--- a/src/theory/quantifiers/local_theory_ext.cpp
+++ b/src/theory/quantifiers/local_theory_ext.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file quant_util.cpp
+/*! \file local_theory_ext.cpp
  ** \verbatim
  ** Original author: Andrew Reynolds
  ** Major contributors: none
@@ -31,69 +31,69 @@ 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;
+void LtePartialInst::preRegisterQuantifier( Node q ) {
+  if( !q.getAttribute(LtePartialInstAttribute()) ){
+    if( d_do_inst.find( q )!=d_do_inst.end() ){
+      if( d_do_inst[q] ){
+        d_lte_asserts.push_back( q );
+        d_quantEngine->setOwner( q, this );
+      }
     }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]] = false;
-    }
-    getEligibleInstVars( q[1], vars );
-
-    //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;
+      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]] = false;
       }
-    }
-    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;
+      getEligibleInstVars( q[1], vars );
+
+      //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 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;
         }
-      }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;
+        d_quantEngine->setOwner( q, this );
       }
     }
-    
-    
-    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;
   }
 }
 
@@ -188,7 +188,6 @@ void LtePartialInst::getInstantiations( std::vector< Node >& lemmas ) {
       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 );
     }
   }
 }
diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h
index 6e2ee34af..d802c2cf7 100644
--- a/src/theory/quantifiers/local_theory_ext.h
+++ b/src/theory/quantifiers/local_theory_ext.h
@@ -55,8 +55,8 @@ private:
   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 );
+  /** determine whether this quantified formula will be reduced */
+  void preRegisterQuantifier( Node q );
   /** was invoked */
   bool wasInvoked() { return d_wasInvoked; }
   
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
new file mode 100644
index 000000000..e874ee5b8
--- /dev/null
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -0,0 +1,129 @@
+/*********************                                                        */
+/*! \file quant_split.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/quant_split.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "options/quantifiers_options.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+
+QuantDSplit::QuantDSplit( QuantifiersEngine * qe, context::Context* c ) :
+QuantifiersModule( qe ), d_added_split( qe->getUserContext() ){
+
+}
+
+/** pre register quantifier */
+void QuantDSplit::preRegisterQuantifier( Node q ) {
+  int max_index = -1;
+  int max_score = -1;
+  if( q.getNumChildren()==3 ){
+    return;
+  }
+  Trace("quant-dsplit-debug") << "Check split quantified formula : " << q << std::endl;
+  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+    TypeNode tn = q[0][i].getType();
+    if( tn.isDatatype() ){
+      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+      if( dt.isRecursiveSingleton() ){
+        Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is recursive singleton." << std::endl;
+      }else{
+        int score = -1;
+        if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){
+          score = dt.isFinite() ? 1 : -1;
+        }else if(  options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){
+          score = dt.isUFinite() ? 1 : -1;
+        }
+        Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << std::endl;
+        if( score>max_score ){
+          max_index = i;
+          max_score = score;
+        }
+      }
+    }
+  }
+
+  if( max_index!=-1 ){
+    Trace("quant-dsplit-debug") << "Will split at index " << max_index << "." << std::endl;
+    d_quant_to_reduce[q] = max_index;
+    d_quantEngine->setOwner( q, this );
+  }
+}
+
+/* whether this module needs to check this round */
+bool QuantDSplit::needsCheck( Theory::Effort e ) {
+  return e>=Theory::EFFORT_FULL;
+}
+/* Call during quantifier engine's check */
+void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) {
+  //flush lemmas ASAP (they are a reduction)
+  if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){
+    std::vector< Node > lemmas;
+    for(std::map< Node, int >::iterator it = d_quant_to_reduce.begin(); it != d_quant_to_reduce.end(); ++it) {
+      Node q = it->first;
+      if( d_added_split.find( q )==d_added_split.end() ){
+        d_added_split.insert( q );
+        std::vector< Node > bvs;
+        for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+          if( (int)i!=it->second ){
+            bvs.push_back( q[0][i] );
+          }
+        }
+        std::vector< Node > disj;
+        disj.push_back( q.negate() );
+        TNode svar = q[0][it->second];
+        TypeNode tn = svar.getType();
+        if( tn.isDatatype() ){
+          const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+          for( unsigned j=0; j<dt.getNumConstructors(); j++ ){
+            std::vector< Node > vars;
+            for( unsigned k=0; k<dt[j].getNumArgs(); k++ ){
+              TypeNode tns = TypeNode::fromType( dt[j][k].getRangeType() );
+              Node v = NodeManager::currentNM()->mkBoundVar( tns );
+              vars.push_back( v );
+            }
+            std::vector< Node > bvs_cmb;
+            bvs_cmb.insert( bvs_cmb.end(), bvs.begin(), bvs.end() );
+            bvs_cmb.insert( bvs_cmb.end(), vars.begin(), vars.end() );
+            vars.insert( vars.begin(), Node::fromExpr( dt[j].getConstructor() ) );
+            Node c = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, vars );
+            TNode ct = c;
+            Node body = q[1].substitute( svar, ct );
+            if( !bvs_cmb.empty() ){
+              body = NodeManager::currentNM()->mkNode( kind::FORALL, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, bvs_cmb ), body );
+            }
+            disj.push_back( body );
+          }
+        }else{
+          Assert( false );
+        }
+        lemmas.push_back( disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj ) );
+      }
+    }
+
+    //add lemmas to quantifiers engine
+    for( unsigned i=0; i<lemmas.size(); i++ ){
+      Trace("quant-dsplit") << "QuantDSplit lemma : " << lemmas[i] << std::endl;
+      d_quantEngine->addLemma( lemmas[i], false );
+    }
+  }
+}
+
diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h
new file mode 100644
index 000000000..f40acc2fd
--- /dev/null
+++ b/src/theory/quantifiers/quant_split.h
@@ -0,0 +1,54 @@
+/*********************                                                        */
+/*! \file quant_split.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 dynamic quantifiers splitting
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANT_SPLIT_H
+#define __CVC4__THEORY__QUANT_SPLIT_H
+
+#include "theory/quantifiers_engine.h"
+#include "context/cdo.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class QuantDSplit : public QuantifiersModule {
+  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+private:
+  /** list of relevant quantifiers asserted in the current context */
+  std::map< Node, int > d_quant_to_reduce;
+  /** whether we have instantiated quantified formulas */
+  NodeSet d_added_split;
+public:
+  QuantDSplit( QuantifiersEngine * qe, context::Context* c );
+  /** determine whether this quantified formula will be reduced */
+  void preRegisterQuantifier( Node q );
+  
+  /* 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 "QuantDSplit"; }
+};
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index ce6c929b2..cfb3fda94 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -39,6 +39,7 @@
 #include "theory/quantifiers/rewrite_engine.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/trigger.h"
+#include "theory/quantifiers/quant_split.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
@@ -121,6 +122,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
   d_sg_gen = NULL;
   d_inst_engine = NULL;
   d_i_cbqi = NULL;
+  d_qsplit = NULL;
   d_model_engine = NULL;
   d_bint = NULL;
   d_rr_engine = NULL;
@@ -161,6 +163,7 @@ QuantifiersEngine::~QuantifiersEngine(){
   delete d_uee;
   delete d_fs;
   delete d_i_cbqi;
+  delete d_qsplit;
 }
 
 EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() {
@@ -237,6 +240,11 @@ void QuantifiersEngine::finishInit(){
     d_lte_part_inst = new quantifiers::LtePartialInst( this, c );
     d_modules.push_back( d_lte_part_inst );
   }
+  if( ( options::finiteModelFind() && options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ) || 
+      options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_AGG ){
+    d_qsplit = new quantifiers::QuantDSplit( this, c );
+    d_modules.push_back( d_qsplit );
+  }
   if( options::quantAlphaEquiv() ){
     d_alpha_equiv = new quantifiers::AlphaEquivalence( this );
   }
@@ -367,9 +375,9 @@ void QuantifiersEngine::check( Theory::Effort e ){
       }
       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_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;
       }
@@ -513,25 +521,13 @@ bool QuantifiersEngine::reduceQuantifier( Node q ) {
     if( d_alpha_equiv ){
       Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl;
       //add equivalence with another quantified formula
-      if( !d_alpha_equiv->registerQuantifier( q ) ){
+      if( d_alpha_equiv->reduceQuantifier( q ) ){
         Trace("quant-engine-red") << "...alpha equivalence success." << std::endl;
         ++(d_statistics.d_red_alpha_equiv);
         d_quants_red[q] = true;
         return true;
       }
     }
-    if( d_lte_part_inst && !q.getAttribute(LtePartialInstAttribute()) ){
-      //will partially instantiate
-      Trace("quant-engine-red") << "LTE: Partially instantiate " << q << "?" << std::endl;
-      if( d_lte_part_inst->addQuantifier( q ) ){
-        Trace("quant-engine-red") << "...LTE partially instantiate success." << std::endl;
-        //delayed reduction : assert to model
-        d_model->assertQuantifier( q, true );
-        ++(d_statistics.d_red_lte_partial_inst);
-        d_quants_red[q] = true;
-        return true;
-      }
-    }
     d_quants_red[q] = false;
     return false;
   }else{
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 28fcbbc85..c5c88487b 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -64,8 +64,8 @@ public:
   virtual void check( Theory::Effort e, unsigned quant_e ) = 0;
   /* check was complete (e.g. no lemmas implies a model) */
   virtual bool checkComplete() { return true; }
-  /* Called for new quantifiers */
-  virtual void preRegisterQuantifier( Node q ) {}
+  /* Called for new quantified formulas */
+  virtual void preRegisterQuantifier( Node q ) { }
   /* Called for new quantifiers after owners are finalized */
   virtual void registerQuantifier( Node q ) = 0;
   virtual void assertNode( Node n ) {}
@@ -99,6 +99,7 @@ namespace quantifiers {
   class QuantEqualityEngine;
   class FullSaturation;
   class InstStrategyCbqi;
+  class QuantDSplit;
 }/* CVC4::theory::quantifiers */
 
 namespace inst {
@@ -157,6 +158,8 @@ private:
   quantifiers::FullSaturation * d_fs;
   /** counterexample-based quantifier instantiation */
   quantifiers::InstStrategyCbqi * d_i_cbqi;
+  /** quantifiers splitting */
+  quantifiers::QuantDSplit * d_qsplit;
 public: //effort levels
   enum {
     QEFFORT_CONFLICT,
@@ -253,6 +256,8 @@ public:  //modules
   quantifiers::FullSaturation * getFullSaturation() { return d_fs; }
   /** get inst strategy cbqi */
   quantifiers::InstStrategyCbqi * getInstStrategyCbqi() { return d_i_cbqi; }
+  /** get quantifiers splitting */
+  quantifiers::QuantDSplit * getQuantDSplit() { return d_qsplit; }
 private:
   /** owner of quantified formulas */
   std::map< Node, QuantifiersModule * > d_owner;
@@ -281,7 +286,7 @@ public:
   /** get next decision request */
   Node getNextDecisionRequest();
 private:
-  /** reduce quantifier */
+  /** reduceQuantifier, return true if reduced */
   bool reduceQuantifier( Node q );
   /** compute term vector */
   void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms );
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index 8cff980a5..a3ff2fcc7 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -50,7 +50,8 @@ TESTS =	\
 	loopy_coda.smt2 \
 	fmc_unsound_model.smt2 \
 	am-bad-model.cvc \
-	nun-0208-to.smt2
+	nun-0208-to.smt2 \
+	datatypes-ufinite.smt2
 
 
 EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/fmf/datatypes-ufinite.smt2 b/test/regress/regress0/fmf/datatypes-ufinite.smt2
new file mode 100644
index 000000000..d802930fd
--- /dev/null
+++ b/test/regress/regress0/fmf/datatypes-ufinite.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(declare-sort U 0)
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+(declare-fun d () U)
+(assert (distinct a b c))
+(declare-sort V 0)
+(declare-datatypes () ((ufin1 (cons1 (s11 U) (s12 U) (s13 U))) (ufin2 (cons2 (s21 V) (s22 U)) (cons3))))
+(declare-fun P (ufin1 ufin2) Bool)
+(declare-fun Q (ufin1 ufin1) Bool)
+(assert (forall ((x ufin1) (y ufin2) (z ufin1)) (or (P x y) (Q x z))))
+(assert (not (P (cons1 a a a) cons3)))
+(assert (not (Q (cons1 a d a) (cons1 a b c))))
+(check-sat)