Improvements to --macros-quant. Enable --clause-split by default. Bug fix for cbqi regarding instantiations with free skolems, extend to boolean quantification. Infrastructure for congruence closure with free variables.

19 files changed, 595 insertions, 106 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index b0d97754d..0cd4cff44 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -336,7 +336,9 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/fun_def_process.h \
 	theory/quantifiers/fun_def_process.cpp \
 	theory/quantifiers/fun_def_engine.h \
-	theory/quantifiers/fun_def_engine.cpp \
+  theory/quantifiers/fun_def_engine.cpp \
+  theory/quantifiers/quant_equality_engine.h \
+  theory/quantifiers/quant_equality_engine.cpp \
 	theory/quantifiers/options_handlers.h \
 	theory/arith/theory_arith_type_rules.h \
 	theory/arith/type_enumerator.h \
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1e0c63ce8..87cd815e9 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3125,6 +3125,7 @@ void SmtEnginePrivate::processAssertions() {
   // Dump the assertions
   dumpAssertions("pre-everything", d_assertions);
 
+  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() begin" << endl;
   Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl;
 
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
@@ -3149,6 +3150,7 @@ void SmtEnginePrivate::processAssertions() {
 
   // Assertions are NOT guaranteed to be rewritten by this point
 
+  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-definition-expansion" << endl;
   dumpAssertions("pre-definition-expansion", d_assertions);
   {
     Chat() << "expanding definitions..." << endl;
@@ -3159,6 +3161,7 @@ void SmtEnginePrivate::processAssertions() {
       d_assertions.replace(i, expandDefinitions(d_assertions[i], cache));
     }
   }
+  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-definition-expansion" << endl;
   dumpAssertions("post-definition-expansion", d_assertions);
 
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
@@ -3212,12 +3215,14 @@ void SmtEnginePrivate::processAssertions() {
 
   // Unconstrained simplification
   if(options::unconstrainedSimp()) {
+    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-unconstrained-simp" << endl;
     dumpAssertions("pre-unconstrained-simp", d_assertions);
     Chat() << "...doing unconstrained simplification..." << endl;
     for (unsigned i = 0; i < d_assertions.size(); ++ i) {
       d_assertions.replace(i, Rewriter::rewrite(d_assertions[i]));
     }
     unconstrainedSimp();
+    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-unconstrained-simp" << endl;
     dumpAssertions("post-unconstrained-simp", d_assertions);
   }
 
@@ -3225,6 +3230,7 @@ void SmtEnginePrivate::processAssertions() {
     theory::bv::BVIntroducePow2::pow2Rewrite(d_assertions.ref());
   }
 
+  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-substitution" << endl;
   dumpAssertions("pre-substitution", d_assertions);
 
   if(options::unsatCores()) {
@@ -3240,13 +3246,13 @@ void SmtEnginePrivate::processAssertions() {
                         << "applying substitutions" << endl;
       for (unsigned i = 0; i < d_assertions.size(); ++ i) {
         Trace("simplify") << "applying to " << d_assertions[i] << endl;
-         spendResource(options::preprocessStep());
+        spendResource(options::preprocessStep());
         d_assertions.replace(i, Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertions[i])));
         Trace("simplify") << "  got " << d_assertions[i] << endl;
       }
     }
   }
-
+  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-substitution" << endl;
   dumpAssertions("post-substitution", d_assertions);
 
   // Assertions ARE guaranteed to be rewritten by this point
@@ -3261,15 +3267,18 @@ void SmtEnginePrivate::processAssertions() {
   }
 
   if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
+    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-strings-preprocess" << endl;
     dumpAssertions("pre-strings-pp", d_assertions);
     CVC4::theory::strings::StringsPreprocess sp;
     sp.simplify( d_assertions.ref() );
     //for (unsigned i = 0; i < d_assertions.size(); ++ i) {
     //  d_assertions.replace( i, Rewriter::rewrite( d_assertions[i] ) );
     //}
+    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-strings-preprocess" << endl;
     dumpAssertions("post-strings-pp", d_assertions);
   }
   if( d_smt.d_logic.isQuantified() ){
+    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl;
     //remove rewrite rules
     for( unsigned i=0; i < d_assertions.size(); i++ ) {
       if( d_assertions[i].getKind() == kind::REWRITE_RULE ){
@@ -3300,11 +3309,13 @@ void SmtEnginePrivate::processAssertions() {
     dumpAssertions("post-skolem-quant", d_assertions);
     if( options::macrosQuant() ){
       //quantifiers macro expansion
+      quantifiers::QuantifierMacros qm;
       bool success;
       do{
-        quantifiers::QuantifierMacros qm;
         success = qm.simplify( d_assertions.ref(), true );
       }while( success );
+      //finalize the definitions
+      qm.finalizeDefinitions();
     }
 
     //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF
@@ -3334,6 +3345,7 @@ void SmtEnginePrivate::processAssertions() {
         d_smt.d_fmfRecFunctionsConcrete->insert( f, cl );
       }
     }
+    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << endl;
   }
 
   if( options::sortInference() ){
@@ -3353,27 +3365,32 @@ void SmtEnginePrivate::processAssertions() {
     }
   }
 
+  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-simplify" << endl;
   dumpAssertions("pre-simplify", d_assertions);
   Chat() << "simplifying assertions..." << endl;
   noConflict = simplifyAssertions();
   if(!noConflict){
     ++(d_smt.d_stats->d_simplifiedToFalse);
   }
+  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-simplify" << endl;
   dumpAssertions("post-simplify", d_assertions);
 
   dumpAssertions("pre-static-learning", d_assertions);
   if(options::doStaticLearning()) {
+    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-static-learning" << endl;
     // Perform static learning
     Chat() << "doing static learning..." << endl;
     Trace("simplify") << "SmtEnginePrivate::simplify(): "
                       << "performing static learning" << endl;
     staticLearning();
+    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-static-learning" << endl;
   }
   dumpAssertions("post-static-learning", d_assertions);
 
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
 
+  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-ite-removal" << endl;
   dumpAssertions("pre-ite-removal", d_assertions);
   {
     Chat() << "removing term ITEs..." << endl;
@@ -3383,10 +3400,12 @@ void SmtEnginePrivate::processAssertions() {
     removeITEs();
     d_smt.d_stats->d_numAssertionsPost += d_assertions.size();
   }
+  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-ite-removal" << endl;
   dumpAssertions("post-ite-removal", d_assertions);
 
   dumpAssertions("pre-repeat-simplify", d_assertions);
   if(options::repeatSimp()) {
+    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-repeat-simplify" << endl;
     Chat() << "re-simplifying assertions..." << endl;
     ScopeCounter depth(d_simplifyAssertionsDepth);
     noConflict &= simplifyAssertions();
@@ -3452,6 +3471,7 @@ void SmtEnginePrivate::processAssertions() {
       removeITEs();
       //      Assert(iteRewriteAssertionsEnd == d_assertions.size());
     }
+    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl;
   }
   dumpAssertions("post-repeat-simplify", d_assertions);
 
@@ -3476,6 +3496,7 @@ void SmtEnginePrivate::processAssertions() {
   Debug("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl;
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
+  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-theory-preprocessing" << endl;
   dumpAssertions("pre-theory-preprocessing", d_assertions);
   {
     Chat() << "theory preprocessing..." << endl;
@@ -3486,6 +3507,7 @@ void SmtEnginePrivate::processAssertions() {
       d_assertions.replace(i, d_smt.d_theoryEngine->preprocess(d_assertions[i]));
     }
   }
+  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-theory-preprocessing" << endl;
   dumpAssertions("post-theory-preprocessing", d_assertions);
 
   // If we are using eager bit-blasting wrap assertions in fake atom so that
@@ -3511,6 +3533,7 @@ void SmtEnginePrivate::processAssertions() {
   // end: INVARIANT to maintain: no reordering of assertions or
   // introducing new ones
 
+  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl;
   dumpAssertions("post-everything", d_assertions);
 
   //set instantiation level of everything to zero
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 20bd71b45..d9ac190dc 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -1130,7 +1130,7 @@ bool InstStrategyCegqi::addLemma( Node lem ) {
 }
 
 bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) {
-  if( n.getKind()==INST_CONSTANT ){
+  if( n.getKind()==INST_CONSTANT || n.getKind()==SKOLEM ){
     //only legal if current quantified formula contains n
     return TermDb::containsTerm( d_curr_quant, n );
   }else{
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 631216507..b686ddb3b 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -164,6 +164,14 @@ bool InstantiationEngine::needsCheck( Theory::Effort e ){
   return d_quantEngine->getInstWhenNeedsCheck( e );
 }
 
+unsigned InstantiationEngine::needsModel( Theory::Effort e ) {
+  if( options::cbqiModel() && options::cbqi() ){
+    return QuantifiersEngine::QEFFORT_STANDARD;
+  }else{
+    return QuantifiersEngine::QEFFORT_NONE;
+  }
+}
+
 void InstantiationEngine::reset_round( Theory::Effort e ) {
   d_cbqi_set_quant_inactive = false;
   if( options::cbqi() ){
@@ -288,7 +296,7 @@ bool InstantiationEngine::hasApplyUf( Node f ){
 bool InstantiationEngine::hasNonArithmeticVariable( Node f ){
   for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
     TypeNode tn = f[0][i].getType();
-    if( !tn.isInteger() && !tn.isReal() ){
+    if( !tn.isInteger() && !tn.isReal() && !tn.isBoolean() ){
       return true;
     }
   }
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 5d46a9815..44612a85c 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -98,6 +98,7 @@ public:
   void finishInit();
 
   bool needsCheck( Theory::Effort e );
+  unsigned needsModel( Theory::Effort e );
   void reset_round( Theory::Effort e );
   void check( Theory::Effort e, unsigned quant_e );
   bool checkComplete();
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index e46f115a4..c26aea465 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -20,6 +20,8 @@
 #include "theory/rewriter.h"
 #include "proof/proof_manager.h"
 #include "smt/smt_engine_scope.h"
+#include "theory/quantifiers/modes.h"
+#include "theory/quantifiers/options.h"
 
 using namespace CVC4;
 using namespace std;
@@ -29,56 +31,84 @@ using namespace CVC4::kind;
 
 
 bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){
-  Trace("macros") << "Find macros..." << std::endl;
-  //first, collect macro definitions
-  for( size_t i=0; i<assertions.size(); i++ ){
-    processAssertion( assertions[i] );
-  }
-  bool retVal = false;
-  if( doRewrite && !d_macro_defs.empty() ){
-    //now, rewrite based on macro definitions
-    for( size_t i=0; i<assertions.size(); i++ ){
-      Node curr = simplify( assertions[i] );
-      if( curr!=assertions[i] ){
+  unsigned rmax = options::macrosQuantMode()==MACROS_QUANT_MODE_GROUND ? 1 : 2;
+  for( unsigned r=0; r<rmax; r++ ){
+    d_ground_macros = (r==0);
+    Trace("macros") << "Find macros, ground=" << d_ground_macros << "..." << std::endl;
+    //first, collect macro definitions
+    std::map< unsigned, Node > simp_assertions;
+    int last_macro = -1;
+    for( int i=0; i<(int)assertions.size(); i++ ){
+      Trace("macros-debug") << "  process assertion " << assertions[i] << std::endl;
+      Node curr = assertions[i];
+      //do simplification before process
+      if( doRewrite && !d_macro_defs_new.empty() ){
+        curr = simplify( assertions[i] );
         curr = Rewriter::rewrite( curr );
-        Trace("macros-rewrite") << "Rewrite " << assertions[i] << " to " << curr << std::endl;
-        PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); );
-        assertions[i] = curr;
-        retVal = true;
+        if( curr!=assertions[i] ){
+          simp_assertions[i] = curr;
+        }
+      }
+      if( processAssertion( curr ) ){
+        last_macro = i;
+        //process this assertion again
+        i--;
       }
     }
-    //also store as defined functions
-    for( std::map< Node, Node >::iterator it = d_macro_defs.begin(); it != d_macro_defs.end(); ++it ){
-      Trace("macros-def") << "Macro definition for " << it->first << " : " << it->second << std::endl;
-      Trace("macros-def") << "  basis is : ";
-      std::vector< Node > nargs;
-      std::vector< Expr > args;
-      for( unsigned i=0; i<d_macro_basis[it->first].size(); i++ ){
-        Node bv = NodeManager::currentNM()->mkBoundVar( d_macro_basis[it->first][i].getType() );
-        Trace("macros-def") << d_macro_basis[it->first][i] << " ";
-        nargs.push_back( bv );
-        args.push_back( bv.toExpr() );
+    Trace("macros") << "...finished process, #new def = " << d_macro_defs_new.size() << std::endl;
+    if( doRewrite && !d_macro_defs_new.empty() ){
+      bool retVal = false;
+      Trace("macros") << "Do simplifications..." << std::endl;
+      //now, rewrite based on macro definitions
+      for( unsigned i=0; i<assertions.size(); i++ ){
+        Node curr = assertions[i];
+        std::map< unsigned, Node >::iterator it = simp_assertions.find( i );
+        if( it!=simp_assertions.end() ){
+          curr = it->second;
+        }
+        //simplify again if before last macro
+        if( (int)i<last_macro ){
+          curr = simplify( curr );
+        }
+        if( curr!=assertions[i] ){
+          curr = Rewriter::rewrite( curr );
+          Trace("macros-rewrite") << "Rewrite " << assertions[i] << " to " << curr << std::endl;
+          PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); );
+          assertions[i] = curr;
+          retVal = true;
+        }
       }
-      Trace("macros-def") << std::endl;
-      Node sbody = it->second.substitute( d_macro_basis[it->first].begin(), d_macro_basis[it->first].end(), nargs.begin(), nargs.end() );
-      smt::currentSmtEngine()->defineFunction( it->first.toExpr(), args, sbody.toExpr() );
+      d_macro_defs_new.clear();
+      if( retVal ){
+        return true;
+      }
+    }
+  }
+  for( int i=0; i<(int)assertions.size(); i++ ){
+    if( Trace.isOn("macros-warn") ){
+      debugMacroDefinition( assertions[i], assertions[i] );
     }
   }
-  return retVal;
+  return false;
 }
 
-void QuantifierMacros::processAssertion( Node n ) {
+bool QuantifierMacros::processAssertion( Node n ) {
   if( n.getKind()==AND ){
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      processAssertion( n[i] );
+      if( processAssertion( n[i] ) ){
+        return true;
+      }
     }
+    return false;
   }else if( n.getKind()==FORALL ){
     std::vector< Node > args;
     for( size_t j=0; j<n[0].getNumChildren(); j++ ){
       args.push_back( n[0][j] );
     }
     //look at the body of the quantifier for macro definition
-    process( n[1], true, args, n );
+    return process( n[1], true, args, n );
+  }else{
+    return false;
   }
 }
 
@@ -95,15 +125,20 @@ bool QuantifierMacros::contains( Node n, Node n_s ){
   }
 }
 
-bool QuantifierMacros::containsBadOp( Node n, Node op ){
+bool QuantifierMacros::containsBadOp( Node n, Node op, std::vector< Node >& opc ){
   if( n.getKind()==APPLY_UF ){
     Node nop = n.getOperator();
     if( nop==op || d_macro_defs.find( nop )!=d_macro_defs.end()  ){
       return true;
     }
+    if( std::find( opc.begin(), opc.end(), nop )==opc.end() ){
+      opc.push_back( nop );
+    }
+  }else if( d_ground_macros && n.getKind()==FORALL ){
+    return true;
   }
   for( size_t i=0; i<n.getNumChildren(); i++ ){
-    if( containsBadOp( n[i], op ) ){
+    if( containsBadOp( n[i], op, opc ) ){
       return true;
     }
   }
@@ -147,6 +182,8 @@ void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidat
     if( n.getNumChildren()==2 && n[0].isConst() ){
       getMacroCandidates( n[1], candidates );
     }
+  }else if( n.getKind()==NOT ){
+    getMacroCandidates( n[0], candidates );
   }
 }
 
@@ -155,7 +192,9 @@ Node QuantifierMacros::solveInEquality( Node n, Node lit ){
     //return the opposite side of the equality if defined that way
     for( int i=0; i<2; i++ ){
       if( lit[i]==n ){
-        return lit[ i==0 ? 1 : 0];
+        return lit[i==0 ? 1 : 0];
+      }else if( lit[i].getKind()==NOT && lit[i][0]==n ){
+        return lit[i==0 ? 1 : 0].negate();
       }
     }
     //must solve for term n in the literal lit
@@ -235,9 +274,10 @@ bool QuantifierMacros::getSubstitution( std::vector< Node >& v_quant, std::map<
   return success;
 }
 
-void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){
+bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){
+  Trace("macros-debug") << "  process " << n << std::endl;
   if( n.getKind()==NOT ){
-    process( n[0], !pol, args, f );
+    return process( n[0], !pol, args, f );
   }else if( n.getKind()==AND || n.getKind()==OR ){
     //bool favorPol = (n.getKind()==AND)==pol;
     //conditional?
@@ -246,10 +286,21 @@ void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod
   }else if( n.getKind()==APPLY_UF ){
     //predicate case
     if( isBoundVarApplyUf( n ) ){
-      Node n_def = NodeManager::currentNM()->mkConst( pol );
-      Trace("macros-quant") << "Macro found for " << f << std::endl;
-      Trace("macros") << "* " << n_def << " is a macro for " << n.getOperator() << std::endl;
-      d_macro_defs[ n.getOperator() ] = n_def;
+      Node op = n.getOperator();
+      if( d_macro_defs.find( op )==d_macro_defs.end() ){
+        Node n_def = NodeManager::currentNM()->mkConst( pol );
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          std::stringstream ss;
+          ss << "mda_" << op << "";
+          Node v = NodeManager::currentNM()->mkSkolem( ss.str(), n[i].getType(), "created during macro definition recognition" );
+          d_macro_basis[op].push_back( v );
+        }
+        //contains no ops
+        std::vector< Node > op_contains;
+        //add the macro
+        addMacro( op, n_def, op_contains );
+        return true;
+      }
     }
   }else{
     //literal case
@@ -266,8 +317,9 @@ void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod
           getFreeVariables( m, args, fvs, false );
           //get definition and condition
           Node n_def = solveInEquality( m, n ); //definition for the macro
-          //definition must exist and not contain any free variables apart from fvs
-          if( !n_def.isNull() && !getFreeVariables( n_def, args, fvs, true )  && !containsBadOp( n_def, op ) ){
+          //definition must exist and not contain any free variables apart from fvs, opc is list of functions it contains
+          std::vector< Node > opc;
+          if( !n_def.isNull() && !getFreeVariables( n_def, args, fvs, true )  && !containsBadOp( n_def, op, opc ) ){
             Node n_cond;  //condition when this definition holds
             //conditional must not contain any free variables apart from fvs
             if( n_cond.isNull() || !getFreeVariables( n_cond, args, fvs, true ) ){
@@ -290,10 +342,8 @@ void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod
               std::vector< Node > subs;
               if( getSubstitution( fvs, solved, vars, subs, true ) ){
                 n_def = n_def.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
-                Trace("macros-quant") << "Macro found for " << f << std::endl;
-                Trace("macros") << "* " << n_def << " is a macro for " << op << std::endl;
-                d_macro_defs[op] = n_def;
-                return;
+                addMacro( op, n_def, opc );
+                return true;
               }
             }
           }
@@ -301,35 +351,123 @@ void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod
       }
     }
   }
+  return false;
 }
 
 Node QuantifierMacros::simplify( Node n ){
-  Trace("macros-debug") << "simplify " << n << std::endl;
-  std::vector< Node > children;
-  bool childChanged = false;
-  for( size_t i=0; i<n.getNumChildren(); i++ ){
-    Node nn = simplify( n[i] );
-    children.push_back( nn );
-    childChanged = childChanged || nn!=n[i];
+  if( n.getNumChildren()==0 ){
+    return n;
+  }else{
+    std::map< Node, Node >::iterator itn = d_simplify_cache.find( n );
+    if( itn!=d_simplify_cache.end() ){
+      return itn->second;
+    }else{
+      Node ret = n;
+      Trace("macros-debug") << "  simplify " << n << std::endl;
+      std::vector< Node > children;
+      bool childChanged = false;
+      for( size_t i=0; i<n.getNumChildren(); i++ ){
+        Node nn = simplify( n[i] );
+        children.push_back( nn );
+        childChanged = childChanged || nn!=n[i];
+      }
+      bool retSet = false;
+      if( n.getKind()==APPLY_UF ){
+        Node op = n.getOperator();
+        std::map< Node, Node >::iterator it = d_macro_defs.find( op );
+        if( it!=d_macro_defs.end() && !it->second.isNull() ){
+          //do substitution if necessary
+          ret = it->second;
+          std::map< Node, std::vector< Node > >::iterator itb = d_macro_basis.find( op );
+          if( itb!=d_macro_basis.end() ){
+            ret = ret.substitute( itb->second.begin(), itb->second.end(), children.begin(), children.end() );
+          }
+          retSet = true;
+        }
+      }
+      if( !retSet && childChanged ){
+        if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+          children.insert( children.begin(), n.getOperator() );
+        }
+        ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+      }
+      d_simplify_cache[n] = ret;
+      return ret;
+    }
   }
+}
+
+void QuantifierMacros::debugMacroDefinition( Node oo, Node n ) {
+  //for debugging, ensure that all previous definitions have been eliminated
   if( n.getKind()==APPLY_UF ){
     Node op = n.getOperator();
-    if( d_macro_defs.find( op )!=d_macro_defs.end() && !d_macro_defs[op].isNull() ){
-      //do substitution if necessary
-      std::map< Node, std::vector< Node > >::iterator it = d_macro_basis.find( op );
-      Node ret = d_macro_defs[op];
-      if( it!=d_macro_basis.end() ){
-        ret = ret.substitute( it->second.begin(), it->second.end(), children.begin(), children.end() );
+    if( d_macro_defs.find( op )!=d_macro_defs.end() ){
+      if( d_macro_defs.find( oo )!=d_macro_defs.end() ){
+        Trace("macros-warn") << "BAD DEFINITION for macro " << oo << " : " << d_macro_defs[oo] << std::endl;
+      }else{
+        Trace("macros-warn") << "BAD ASSERTION " << oo << std::endl;
       }
-      return ret;
+      Trace("macros-warn") << "  contains defined function " << op << "!!!" << std::endl;
     }
   }
-  if( childChanged ){
-    if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-      children.insert( children.begin(), n.getOperator() );
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){
+    debugMacroDefinition( oo, n[i] );
+  }
+}
+
+void QuantifierMacros::finalizeDefinitions() {
+  if( options::incrementalSolving() || options::produceModels() || Trace.isOn("macros-warn") ){
+    Trace("macros") << "Store as defined functions..." << std::endl;
+    //also store as defined functions
+    for( std::map< Node, Node >::iterator it = d_macro_defs.begin(); it != d_macro_defs.end(); ++it ){
+      Trace("macros-def") << "Macro definition for " << it->first << " : " << it->second << std::endl;
+      Trace("macros-def") << "  basis is : ";
+      std::vector< Node > nargs;
+      std::vector< Expr > args;
+      for( unsigned i=0; i<d_macro_basis[it->first].size(); i++ ){
+        Node bv = NodeManager::currentNM()->mkBoundVar( d_macro_basis[it->first][i].getType() );
+        Trace("macros-def") << d_macro_basis[it->first][i] << " ";
+        nargs.push_back( bv );
+        args.push_back( bv.toExpr() );
+      }
+      Trace("macros-def") << std::endl;
+      Node sbody = it->second.substitute( d_macro_basis[it->first].begin(), d_macro_basis[it->first].end(), nargs.begin(), nargs.end() );
+      smt::currentSmtEngine()->defineFunction( it->first.toExpr(), args, sbody.toExpr() );
+
+      if( Trace.isOn("macros-warn") ){
+        debugMacroDefinition( it->first, sbody );
+      }
     }
-    return NodeManager::currentNM()->mkNode( n.getKind(), children );
-  }else{
-    return n;
+    Trace("macros") << "done." << std::endl;
   }
 }
+
+void QuantifierMacros::addMacro( Node op, Node n, std::vector< Node >& opc ) {
+  Trace("macros") << "* " << n << " is a macro for " << op << ", #op contain = " << opc.size() << std::endl;
+  d_simplify_cache.clear();
+  d_macro_defs[op] = n;
+  d_macro_defs_new[op] = n;
+  //substitute into all previous
+  std::vector< Node > dep_ops;
+  dep_ops.push_back( op );
+  Trace("macros-debug") << "...substitute into " << d_macro_def_contains[op].size() << " previous definitions." << std::endl;
+  for( unsigned i=0; i<d_macro_def_contains[op].size(); i++ ){
+    Node cop = d_macro_def_contains[op][i];
+    Node def = d_macro_defs[cop];
+    def = simplify( def );
+    d_macro_defs[cop] = def;
+    if( d_macro_defs_new.find( cop )!=d_macro_defs_new.end() ){
+      d_macro_defs_new[cop] = def;
+    }
+    dep_ops.push_back( cop );
+  }
+  //store the contains op information
+  for( unsigned i=0; i<opc.size(); i++ ){
+    for( unsigned j=0; j<dep_ops.size(); j++ ){
+      Node dop = dep_ops[j];
+      if( std::find( d_macro_def_contains[opc[i]].begin(), d_macro_def_contains[opc[i]].end(), dop )==d_macro_def_contains[opc[i]].end() ){
+        d_macro_def_contains[opc[i]].push_back( dop );
+      }
+    }
+  }
+}
\ No newline at end of file
diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h
index 57f4abe4e..74fb0f47b 100644
--- a/src/theory/quantifiers/macros.h
+++ b/src/theory/quantifiers/macros.h
@@ -30,11 +30,12 @@ namespace quantifiers {
 
 class QuantifierMacros{
 private:
-  void processAssertion( Node n );
+  bool d_ground_macros;
+  bool processAssertion( Node n );
   bool isBoundVarApplyUf( Node n );
-  void process( Node n, bool pol, std::vector< Node >& args, Node f );
+  bool process( Node n, bool pol, std::vector< Node >& args, Node f );
   bool contains( Node n, Node n_s );
-  bool containsBadOp( Node n, Node op );
+  bool containsBadOp( Node n, Node op, std::vector< Node >& opc );
   bool isMacroLiteral( Node n, bool pol );
   void getMacroCandidates( Node n, std::vector< Node >& candidates );
   Node solveInEquality( Node n, Node lit );
@@ -45,13 +46,21 @@ private:
   std::map< Node, std::vector< Node > > d_macro_basis;
   //map from operators to macro definition
   std::map< Node, Node > d_macro_defs;
+  std::map< Node, Node > d_macro_defs_new;
+  //operators to macro ops that contain them
+  std::map< Node, std::vector< Node > > d_macro_def_contains;
+  //simplify cache
+  std::map< Node, Node > d_simplify_cache;
 private:
   Node simplify( Node n );
+  void addMacro( Node op, Node n, std::vector< Node >& opc );
+  void debugMacroDefinition( Node oo, Node n );
 public:
   QuantifierMacros(){}
   ~QuantifierMacros(){}
 
   bool simplify( std::vector< Node >& assertions, bool doRewrite = false );
+  void finalizeDefinitions();
 };
 
 }
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index af2d88e94..75e75637f 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -161,6 +161,13 @@ typedef enum {
   SYGUS_INV_TEMPL_MODE_POST,
 } SygusInvTemplMode;
 
+typedef enum {
+  /** infer all definitions */
+  MACROS_QUANT_MODE_ALL,
+  /** infer ground definitions */
+  MACROS_QUANT_MODE_GROUND,
+} MacrosQuantMode;
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 5cb9062e4..0edd3f1ea 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -40,7 +40,7 @@ option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default fal
 # Whether to NNF quantifier bodies
 option nnfQuant --nnf-quant bool :default true
  apply NNF conversion to quantified formulas
-option clauseSplit --clause-split bool :default false
+option clauseSplit --clause-split bool :default true
  apply clause splitting to quantified formulas
 # Whether to pre-skolemize quantifier bodies.
 # For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to
@@ -54,9 +54,6 @@ option preSkolemQuantAgg --pre-skolem-quant-agg bool :read-write :default true
 # Whether to perform agressive miniscoping
 option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
  perform aggressive miniscoping for quantifiers
-# Whether to perform quantifier macro expansion
-option macrosQuant --macros-quant bool :default false
- perform quantifiers macro expansions
 # Whether to CNF quantifier bodies
 option elimTautQuant --elim-taut-quant bool :default true
  eliminate tautological disjuncts of quantified formulas
@@ -65,17 +62,14 @@ option elimTautQuant --elim-taut-quant bool :default true
  
 option eMatching --e-matching bool :read-write :default true
  whether to do heuristic E-matching
- 
+
 option termDbMode --term-db-mode CVC4::theory::quantifiers::TermDbMode :default CVC4::theory::quantifiers::TERM_DB_ALL :read-write :include "theory/quantifiers/modes.h" :handler  CVC4::theory::quantifiers::stringToTermDbMode :handler-include "theory/quantifiers/options_handlers.h"
  which ground terms to consider for instantiation
-# Whether to consider terms in the bodies of quantifiers for matching
 option registerQuantBodyTerms --register-quant-body-terms bool :default false
  consider ground terms within bodies of quantified formulas for matching
  
-# Whether to use smart triggers
 option smartTriggers --smart-triggers bool :default true
  disable smart triggers
-# Whether to use relevent triggers
 option relevantTriggers --relevant-triggers bool :default false
  prefer triggers that are more relevant based on SInE style analysis
 option relationalTriggers --relational-triggers bool :default false
@@ -96,11 +90,12 @@ option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :d
  selection mode for triggers
 option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToUserPatMode :handler-include "theory/quantifiers/options_handlers.h"
  policy for handling user-provided patterns for quantifier instantiation
+option incrementTriggers --increment-triggers bool :default true
+ generate additional triggers as needed during search
  
 option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h"
  when to apply instantiation
  
- 
 option instMaxLevel --inst-max-level=N int :read-write :default -1
  maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)
 option instLevelInputOnly --inst-level-input-only bool :default true
@@ -108,8 +103,6 @@ option instLevelInputOnly --inst-level-input-only bool :default true
 option internalReps --quant-internal-reps bool :default true
  instantiate with representatives chosen by quantifiers engine
  
-option incrementTriggers --increment-triggers bool :default true
- generate additional triggers as needed during search
 option eagerInstQuant --eager-inst-quant bool :default false
  apply quantifier instantiation eagerly
 
@@ -124,7 +117,6 @@ option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::Liter
 option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h"
  policy for instantiating axioms
 
- 
 ### finite model finding options
  
 option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write
@@ -252,6 +244,8 @@ option recurseCbqi --cbqi-recurse bool :default false
  turns on recursive counterexample-based quantifier instantiation
 option cbqiSat --cbqi-sat bool :read-write :default true
  answer sat when quantifiers are asserted with counterexample-based quantifier instantiation
+option cbqiModel --cbqi-model bool :read-write :default true
+ guide instantiations by model values for counterexample-based quantifier instantiation
  
 ### local theory extensions options 
 
@@ -266,10 +260,19 @@ option lteRestrictInstClosure --lte-restrict-inst-closure bool :default false
 
 option quantAlphaEquiv --quant-alpha-equiv bool :default true
   infer alpha equivalence between quantified formulas
+option macrosQuant --macros-quant bool :default false
+ perform quantifiers macro expansion
+option macrosQuantMode --macros-quant-mode=MODE CVC4::theory::quantifiers::MacrosQuantMode :default CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMacrosQuantMode :handler-include "theory/quantifiers/options_handlers.h"
+ mode for quantifiers macro expansion
 
 ### recursive function options
 
 #option funDefs --fun-defs bool :default false
 #  enable specialized techniques for recursive function definitions
  
+### e-unification options
+
+option quantEqualityEngine --quant-ee bool :default false
+  maintain congrunce closure over universal equalities
+ 
 endmodule
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 4d2276621..699dd0296 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -230,6 +230,16 @@ post \n\
 + Synthesize invariant based on strengthening of postcondition. \n\
 \n\
 ";
+static const std::string macrosQuantHelp = "\
+Template modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\
+\n\
+all \n\
++ Infer definitions for functions, including those containing quantified formulas.\n\
+\n\
+ground (default) \n\
++ Only infer ground definitions for functions.\n\
+\n\
+";
 
 inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
   if(optarg == "pre-full") {
@@ -472,6 +482,20 @@ inline SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::stri
   }
 }
 
+inline MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg == "all" ) {
+    return MACROS_QUANT_MODE_ALL;
+  } else if(optarg == "ground") {
+    return MACROS_QUANT_MODE_GROUND;
+  } else if(optarg ==  "help") {
+    puts(macrosQuantHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --macros-quant-mode: `") +
+                          optarg + "'.  Try --macros-quant-mode help.");
+  }
+}
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/quant_equality_engine.cpp b/src/theory/quantifiers/quant_equality_engine.cpp
new file mode 100755
index 000000000..8e683f660
--- /dev/null
+++ b/src/theory/quantifiers/quant_equality_engine.cpp
@@ -0,0 +1,139 @@
+/*********************                                                        */
+/*! \file quant_equality_engine.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
+ **
+ ** Congruence closure with free variables
+ **/
+
+#include <vector>
+
+#include "theory/quantifiers/quant_equality_engine.h"
+#include "theory/rewriter.h"
+#include "theory/quantifiers/term_database.h"
+
+using namespace CVC4;
+using namespace std;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace CVC4::kind;
+
+QuantEqualityEngine::QuantEqualityEngine( QuantifiersEngine * qe, context::Context* c ) :
+QuantifiersModule( qe ),
+d_notify( *this ),
+d_uequalityEngine(d_notify, c, "theory::quantifiers::QuantEqualityEngine", true),
+d_conflict(c, false),
+d_quant_red(c),
+d_quant_unproc(c){
+  d_uequalityEngine.addFunctionKind( kind::APPLY_UF );
+}
+
+void QuantEqualityEngine::conflict(TNode t1, TNode t2) {
+  //report conflict through quantifiers engine output channel
+  std::vector<TNode> assumptions;
+  d_uequalityEngine.explainEquality(t1, t2, true, assumptions, NULL);
+  Node conflict;
+  if( assumptions.size()==1 ){
+    conflict = assumptions[0];
+  }else{
+    conflict = NodeManager::currentNM()->mkNode( AND, assumptions );
+  }
+  d_conflict = true;
+  Trace("qee-conflict") << "Quantifier equality engine conflict : " << conflict << std::endl;
+  d_quantEngine->getOutputChannel().conflict( conflict );
+}
+
+void QuantEqualityEngine::eqNotifyNewClass(TNode t){
+
+}
+void QuantEqualityEngine::eqNotifyPreMerge(TNode t1, TNode t2){
+
+}
+void QuantEqualityEngine::eqNotifyPostMerge(TNode t1, TNode t2){
+
+}
+void QuantEqualityEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
+
+}
+
+/* whether this module needs to check this round */
+bool QuantEqualityEngine::needsCheck( Theory::Effort e ) {
+  return e>=Theory::EFFORT_LAST_CALL;
+}
+
+/* reset at a round */
+void QuantEqualityEngine::reset_round( Theory::Effort e ){
+  //TODO
+}
+
+/* Call during quantifier engine's check */
+void QuantEqualityEngine::check( Theory::Effort e, unsigned quant_e ) {
+  //TODO
+}
+
+/* Called for new quantifiers */
+void QuantEqualityEngine::registerQuantifier( Node q ) {
+  //TODO
+}
+
+/** called for everything that gets asserted */
+void QuantEqualityEngine::assertNode( Node n ) {
+  Assert( n.getKind()==FORALL );
+  Trace("qee-debug") << "QEE assert : " << n << std::endl;
+  Node lit = n[1].getKind()==NOT ? n[1][0] : n[1];
+  bool pol = n[1].getKind()!=NOT;
+  if( lit.getKind()==APPLY_UF || lit.getKind()==EQUAL ){
+    lit = getTermDatabase()->getCanonicalTerm( lit );
+    Trace("qee-debug") << "Canonical :  " << lit << ", pol = " << pol << std::endl;
+    Node t1 = lit.getKind()==APPLY_UF ? lit : lit[0];
+    Node t2;
+    if( lit.getKind()==APPLY_UF ){
+      t2 = pol ? getTermDatabase()->d_true : getTermDatabase()->d_false;
+      pol = true;
+    }else{
+      t2 = lit[1];
+    }
+    bool alreadyHolds = false;
+    if( pol && areUnivEqual( t1, t2 ) ){
+      alreadyHolds = true;
+    }else if( !pol && areUnivDisequal( t1, t2 ) ){
+      alreadyHolds = true;
+    }
+
+    if( alreadyHolds ){
+      d_quant_red.push_back( n );
+      Trace("qee-debug") << "...add to redundant" << std::endl;
+    }else{
+      if( lit.getKind()==APPLY_UF ){
+        d_uequalityEngine.assertPredicate(lit, pol, n);
+      }else{
+        d_uequalityEngine.assertEquality(lit, pol, n);
+      }
+    }
+  }else{
+    d_quant_unproc[n] = true;
+    Trace("qee-debug") << "...add to unprocessed (" << lit.getKind() << ")" << std::endl;
+  }
+}
+
+bool QuantEqualityEngine::areUnivDisequal( TNode n1, TNode n2 ) {
+  return n1!=n2 && d_uequalityEngine.hasTerm( n1 ) && d_uequalityEngine.hasTerm( n2 ) && d_uequalityEngine.areDisequal( n1, n2, false );
+}
+
+bool QuantEqualityEngine::areUnivEqual( TNode n1, TNode n2 ) {
+  return n1==n2 || ( d_uequalityEngine.hasTerm( n1 ) && d_uequalityEngine.hasTerm( n2 ) && d_uequalityEngine.areEqual( n1, n2 ) );
+}
+
+TNode QuantEqualityEngine::getUnivRepresentative( TNode n ) {
+  if( d_uequalityEngine.hasTerm( n ) ){
+    return d_uequalityEngine.getRepresentative( n );
+  }else{
+    return n;
+  }
+}
\ No newline at end of file
diff --git a/src/theory/quantifiers/quant_equality_engine.h b/src/theory/quantifiers/quant_equality_engine.h
new file mode 100755
index 000000000..0de6341cb
--- /dev/null
+++ b/src/theory/quantifiers/quant_equality_engine.h
@@ -0,0 +1,92 @@
+/*********************                                                        */
+/*! \file quant_equality_engine.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 Congruence closure with free variables
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__QUANTIFIERS_EQUALITY_ENGINE_H
+#define __CVC4__QUANTIFIERS_EQUALITY_ENGINE_H
+
+#include <iostream>
+#include <string>
+#include <vector>
+#include <map>
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class QuantEqualityEngine : public QuantifiersModule {
+  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
+private:
+  //notification class for equality engine
+  class NotifyClass : public eq::EqualityEngineNotify {
+    QuantEqualityEngine& d_qee;
+  public:
+    NotifyClass(QuantEqualityEngine& qee): d_qee(qee) {}
+    bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; }
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; }
+    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { return true; }
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2) { d_qee.conflict(t1, t2); }
+    void eqNotifyNewClass(TNode t) { d_qee.eqNotifyNewClass(t); }
+    void eqNotifyPreMerge(TNode t1, TNode t2) { d_qee.eqNotifyPreMerge(t1, t2); }
+    void eqNotifyPostMerge(TNode t1, TNode t2) { d_qee.eqNotifyPostMerge(t1, t2); }
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {d_qee.eqNotifyDisequal(t1, t2, reason); }
+  };/* class ConjectureGenerator::NotifyClass */
+  /** The notify class */
+  NotifyClass d_notify;
+  /** (universal) equaltity engine */
+  eq::EqualityEngine d_uequalityEngine;
+  /** Are we in conflict */
+  context::CDO<bool> d_conflict;
+  /** list of redundant quantifiers in current context */
+  context::CDList<Node> d_quant_red;
+  /** unprocessed quantifiers in current context */
+  NodeBoolMap d_quant_unproc;
+private:
+  void conflict(TNode t1, TNode t2);
+  void eqNotifyNewClass(TNode t);
+  void eqNotifyPreMerge(TNode t1, TNode t2);
+  void eqNotifyPostMerge(TNode t1, TNode t2);
+  void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
+public:
+  QuantEqualityEngine( QuantifiersEngine * qe, context::Context* c );
+  ~QuantEqualityEngine(){}
+
+  /* whether this module needs to check this round */
+  bool needsCheck( Theory::Effort e );
+  /* reset at a round */
+  void reset_round( 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 );
+  /** called for everything that gets asserted */
+  void assertNode( Node n );
+  /** Identify this module (for debugging, dynamic configuration, etc..) */
+  std::string identify() const { return "QuantEqualityEngine"; }
+  /** queries */
+  bool areUnivDisequal( TNode n1, TNode n2 );
+  bool areUnivEqual( TNode n1, TNode n2 );
+  TNode getUnivRepresentative( TNode n );
+};
+
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 6a95e243d..d6cbe386c 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -109,7 +109,7 @@ void QuantifiersRewriter::computeArgVec( std::vector< Node >& args, std::vector<
   std::map< Node, bool > activeMap;
   computeArgs( args, activeMap, n );
   for( unsigned i=0; i<args.size(); i++ ){
-    if( activeMap[args[i]] ){
+    if( activeMap.find( args[i] )!=activeMap.end() ){
       activeArgs.push_back( args[i] );
     }
   }
@@ -119,10 +119,13 @@ void QuantifiersRewriter::computeArgVec2( std::vector< Node >& args, std::vector
   Assert( activeArgs.empty() );
   std::map< Node, bool > activeMap;
   computeArgs( args, activeMap, n );
-  computeArgs( args, activeMap, ipl );
-  for( unsigned i=0; i<args.size(); i++ ){
-    if( activeMap[args[i]] ){
-      activeArgs.push_back( args[i] );
+  if( !activeMap.empty() ){
+    //collect variables in inst pattern list only if we cannot eliminate quantifier
+    computeArgs( args, activeMap, ipl );
+    for( unsigned i=0; i<args.size(); i++ ){
+      if( activeMap.find( args[i] )!=activeMap.end() ){
+        activeArgs.push_back( args[i] );
+      }
     }
   }
 }
@@ -341,7 +344,7 @@ Node QuantifiersRewriter::computeNNF( Node body ){
 }
 
 
-void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, 
+void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons,
                                                    std::vector< Node >& conj ){
   if( n.getKind()==ITE && n[0].getKind()==APPLY_TESTER && n[1].getType().isBoolean() ){
   Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl;
@@ -375,7 +378,7 @@ void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node
     std::vector< Node > children;
     children.push_back( n );
     std::vector< Node > vars;
-    //add all positive testers 
+    //add all positive testers
     for( std::map< Node, Node >::iterator it = pcons.begin(); it != pcons.end(); ++it ){
       children.push_back( it->second.negate() );
       vars.push_back( it->first );
@@ -797,7 +800,7 @@ Node QuantifiersRewriter::computeElimTaut( Node body ) {
   }
   return body;
 }
-  
+
 Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >& vars ) {
   if( body.getKind()==OR ){
     size_t var_found_count = 0;
@@ -905,7 +908,7 @@ Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >&
 
 Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node ipl ){
   std::vector< Node > activeArgs;
-  //if cegqi is on, may be synthesis conjecture, in which case we want to keep all variables 
+  //if cegqi is on, may be synthesis conjecture, in which case we want to keep all variables
   if( options::ceGuidedInst() && !ipl.isNull() ){
     for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
       Trace("quant-attr-debug") << "Check : " << ipl[i] << " " << ipl[i].getKind() << std::endl;
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 380ee19fd..7616e770a 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1458,7 +1458,7 @@ bool TermDb::isAssoc( Kind k ) {
 }
 
 bool TermDb::isComm( Kind k ) {
-  return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
+  return k==EQUAL || k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
          k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR;
 }
 
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 06fc8898b..f034b3212 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -38,6 +38,7 @@
 #include "theory/quantifiers/full_model_check.h"
 #include "theory/quantifiers/ambqi_builder.h"
 #include "theory/quantifiers/fun_def_engine.h"
+#include "theory/quantifiers/quant_equality_engine.h"
 
 using namespace std;
 using namespace CVC4;
@@ -129,6 +130,9 @@ d_lemmas_produced_c(u){
   if( !options::finiteModelFind() || options::fmfInstEngine() ){
     d_inst_engine = new quantifiers::InstantiationEngine( this );
     d_modules.push_back(  d_inst_engine );
+    if( options::cbqi() && options::cbqiModel() ){
+      needsBuilder = true;
+    }
   }else{
     d_inst_engine = NULL;
   }
@@ -176,6 +180,13 @@ d_lemmas_produced_c(u){
   //}else{
   d_fun_def_engine = NULL;
   //}
+  if( options::quantEqualityEngine() ){
+    d_uee = new quantifiers::QuantEqualityEngine( this, c );
+    d_modules.push_back( d_uee );
+  }else{
+    d_uee = NULL;
+  }
+
 
   if( needsBuilder ){
     Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl;
@@ -216,6 +227,7 @@ QuantifiersEngine::~QuantifiersEngine(){
   delete d_ceg_inst;
   delete d_lte_part_inst;
   delete d_fun_def_engine;
+  delete d_uee;
   for(std::map< Node, QuantPhaseReq* >::iterator i = d_phase_reqs.begin(); i != d_phase_reqs.end(); ++i) {
     delete (*i).second;
   }
@@ -378,7 +390,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
       if( d_hasAddedLemma ){
         break;
       //otherwise, complete the model generation if necessary
-      }else if( quant_e==QEFFORT_MODEL && needsModelE<=quant_e && options::produceModels() ){
+      }else if( quant_e==QEFFORT_MODEL && needsModelE<=quant_e && options::produceModels() && e==Theory::EFFORT_LAST_CALL ){
         Trace("quant-engine-debug") << "Build completed model..." << std::endl;
         d_builder->buildModel( d_model, true );
       }
@@ -441,10 +453,10 @@ bool QuantifiersEngine::reduceQuantifier( Node q ) {
   std::map< Node, bool >::iterator it = d_quants_red.find( q );
   if( it==d_quants_red.end() ){
     if( d_alpha_equiv ){
-      Trace("quant-engine-debug") << "Alpha equivalence " << q << "?" << std::endl;
+      Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl;
       //add equivalence with another quantified formula
       if( !d_alpha_equiv->registerQuantifier( q ) ){
-        Trace("quant-engine-debug") << "...alpha equivalence success." << std::endl;
+        Trace("quant-engine-red") << "...alpha equivalence success." << std::endl;
         ++(d_statistics.d_red_alpha_equiv);
         d_quants_red[q] = true;
         return true;
@@ -452,9 +464,9 @@ bool QuantifiersEngine::reduceQuantifier( Node q ) {
     }
     if( d_lte_part_inst && !q.getAttribute(LtePartialInstAttribute()) ){
       //will partially instantiate
-      Trace("quant-engine-debug") << "LTE: Partially instantiate " << q << "?" << std::endl;
+      Trace("quant-engine-red") << "LTE: Partially instantiate " << q << "?" << std::endl;
       if( d_lte_part_inst->addQuantifier( q ) ){
-        Trace("quant-engine-debug") << "...LTE partially instantiate success." << std::endl;
+        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);
@@ -795,7 +807,7 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache ){
       //d_curr_out->lemma( lem, false, true );
       d_lemmas_produced_c[ lem ] = true;
       d_lemmas_waiting.push_back( lem );
-      Trace("inst-add-debug2") << "Added lemma : " << lem << std::endl;
+      Trace("inst-add-debug2") << "Added lemma" << std::endl;
       return true;
     }else{
       Trace("inst-add-debug2") << "Duplicate." << std::endl;
@@ -980,7 +992,9 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
 }
 
 void QuantifiersEngine::printInstantiations( std::ostream& out ) {
+  bool printed = false;
   for( std::map< Node, bool >::iterator it = d_skolemized.begin(); it != d_skolemized.end(); ++it ){
+    printed = true;
     out << "Skolem constants of " << it->first << " : " << std::endl;
     out << "  ( ";
     for( unsigned i=0; i<d_term_db->d_skolem_constants[it->first].size(); i++ ){
@@ -992,16 +1006,21 @@ void QuantifiersEngine::printInstantiations( std::ostream& out ) {
   }
   if( options::incrementalSolving() ){
     for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
+      printed = true;
       out << "Instantiations of " << it->first << " : " << std::endl;
       it->second->print( out, it->first );
     }
   }else{
     for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
+      printed = true;
       out << "Instantiations of " << it->first << " : " << std::endl;
       it->second.print( out, it->first );
       out << std::endl;
     }
   }
+  if( !printed ){
+    out << "No instantiations." << std::endl;
+  }
 }
 
 void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index c9a3a8027..101aa43cd 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -94,6 +94,7 @@ namespace quantifiers {
   class LtePartialInst;
   class AlphaEquivalence;
   class FunDefEngine;
+  class QuantEqualityEngine;
 }/* CVC4::theory::quantifiers */
 
 namespace inst {
@@ -145,6 +146,8 @@ private:
   quantifiers::LtePartialInst * d_lte_part_inst;
   /** function definitions engine */
   quantifiers::FunDefEngine * d_fun_def_engine;
+  /** quantifiers equality engine */
+  quantifiers::QuantEqualityEngine * d_uee;
 public: //effort levels
   enum {
     QEFFORT_CONFLICT,
@@ -233,6 +236,8 @@ public:  //modules
   quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; }
   /** function definition engine */
   quantifiers::FunDefEngine * getFunDefEngine() { return d_fun_def_engine; }
+  /** quantifiers equality engine */
+  quantifiers::QuantEqualityEngine * getQuantEqualityEngine() { return d_uee; }
 private:
   /** owner of quantified formulas */
   std::map< Node, QuantifiersModule * > d_owner;
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 09ca6710d..eb004c184 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -49,7 +49,11 @@ TESTS =	\
 	simp-len.smt2 \
 	is-even.smt2 \
 	is-even-pred.smt2 \
-	delta-simp.smt2
+	delta-simp.smt2  \
+	nested-delta.smt2 \
+	nested-inf.smt2
+
+
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
 # set3.smt2
diff --git a/test/regress/regress0/quantifiers/nested-delta.smt2 b/test/regress/regress0/quantifiers/nested-delta.smt2
new file mode 100644
index 000000000..9352f0410
--- /dev/null
+++ b/test/regress/regress0/quantifiers/nested-delta.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --cbqi-recurse
+; EXPECT: sat
+(set-logic LRA)
+(set-info :status sat)
+(assert (forall ((x Real)) (or (exists ((y Real)) (and (< y 0) (< y x))) (<= x 0))))
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/quantifiers/nested-inf.smt2 b/test/regress/regress0/quantifiers/nested-inf.smt2
new file mode 100644
index 000000000..f27a876db
--- /dev/null
+++ b/test/regress/regress0/quantifiers/nested-inf.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --cbqi-recurse
+; EXPECT: sat
+(set-logic LRA)
+(set-info :status sat)
+(assert (forall ((x Real)) (exists ((y Real)) (> y x))))
+(check-sat)
\ No newline at end of file