39 files changed, 1310 insertions, 1685 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 64e3eb932..450bf063e 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -307,23 +307,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/quant_conflict_find.h \
 	theory/quantifiers/quant_conflict_find.cpp \
 	theory/quantifiers/options_handlers.h \
-	theory/rewriterules/theory_rewriterules_rules.h \
-	theory/rewriterules/theory_rewriterules_rules.cpp \
 	theory/rewriterules/theory_rewriterules.h \
 	theory/rewriterules/theory_rewriterules.cpp \
-	theory/rewriterules/theory_rewriterules_rewriter.h \
-	theory/rewriterules/theory_rewriterules_type_rules.h \
-	theory/rewriterules/theory_rewriterules_preprocess.h \
-	theory/rewriterules/theory_rewriterules_params.h \
-	theory/rewriterules/rr_inst_match.h \
-	theory/rewriterules/rr_inst_match_impl.h \
-	theory/rewriterules/rr_inst_match.cpp \
-	theory/rewriterules/rr_trigger.h \
-	theory/rewriterules/rr_trigger.cpp \
-	theory/rewriterules/rr_candidate_generator.h \
-	theory/rewriterules/rr_candidate_generator.cpp \
-	theory/rewriterules/efficient_e_matching.h \
-	theory/rewriterules/efficient_e_matching.cpp \
 	theory/arith/theory_arith_type_rules.h \
 	theory/arith/type_enumerator.h \
 	theory/arith/arithvar.h \
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 16528e404..8c8b5f840 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -80,8 +80,10 @@
 #include "util/sort_inference.h"
 #include "theory/quantifiers/quant_conflict_find.h"
 #include "theory/quantifiers/macros.h"
-#include "theory/datatypes/options.h"
 #include "theory/quantifiers/first_order_reasoning.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/options.h"
+#include "theory/datatypes/options.h"
 #include "theory/strings/theory_strings_preprocess.h"
 
 using namespace std;
@@ -596,11 +598,6 @@ public:
   }
 
   /**
-   * Pre-skolemize quantifiers.
-   */
-  Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector<Node>& fvs);
-
-  /**
    * Substitute away all AbstractValues in a node.
    */
   Node substituteAbstractValues(TNode n) {
@@ -1188,7 +1185,7 @@ void SmtEngine::setLogicInternal() throw() {
     //instantiate only on last call
     if( options::fmfInstEngine() ){
       Trace("smt") << "setting inst when mode to LAST_CALL" << endl;
-      options::instWhenMode.set( INST_WHEN_LAST_CALL );
+      options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
     }
   }
   if ( options::fmfBoundInt() ){
@@ -1776,120 +1773,6 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
   return result.top();
 }
 
-
-struct ContainsQuantAttributeId {};
-typedef expr::Attribute<ContainsQuantAttributeId, uint64_t> ContainsQuantAttribute;
-
-// check if the given node contains a universal quantifier
-static bool containsQuantifiers(Node n) {
-  if( n.hasAttribute(ContainsQuantAttribute()) ){
-    return n.getAttribute(ContainsQuantAttribute())==1;
-  } else if(n.getKind() == kind::FORALL) {
-    return true;
-  } else {
-    bool cq = false;
-    for( unsigned i = 0; i < n.getNumChildren(); ++i ){
-      if( containsQuantifiers(n[i]) ){
-        cq = true;
-        break;
-      }
-    }
-    ContainsQuantAttribute cqa;
-    n.setAttribute(cqa, cq ? 1 : 0);
-    return cq;
-  }
-}
-
-Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< Node >& fvs ){
-  Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << endl;
-  if( n.getKind()==kind::NOT ){
-    Node nn = preSkolemizeQuantifiers( n[0], !polarity, fvs );
-    return nn.negate();
-  }else if( n.getKind()==kind::FORALL ){
-    if( polarity ){
-      vector< Node > children;
-      children.push_back( n[0] );
-      //add children to current scope
-      vector< Node > fvss;
-      fvss.insert( fvss.begin(), fvs.begin(), fvs.end() );
-      for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
-        fvss.push_back( n[0][i] );
-      }
-      //process body
-      children.push_back( preSkolemizeQuantifiers( n[1], polarity, fvss ) );
-      if( n.getNumChildren()==3 ){
-        children.push_back( n[2] );
-      }
-      //return processed quantifier
-      return NodeManager::currentNM()->mkNode( kind::FORALL, children );
-    }else{
-      //process body
-      Node nn = preSkolemizeQuantifiers( n[1], polarity, fvs );
-      //now, substitute skolems for the variables
-      vector< TypeNode > argTypes;
-      for( int i=0; i<(int)fvs.size(); i++ ){
-        argTypes.push_back( fvs[i].getType() );
-      }
-      //calculate the variables and substitution
-      vector< Node > vars;
-      vector< Node > subs;
-      for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
-        vars.push_back( n[0][i] );
-      }
-      for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
-        //make the new function symbol
-        if( argTypes.empty() ){
-          Node s = NodeManager::currentNM()->mkSkolem( "sk_$$", n[0][i].getType(), "created during pre-skolemization" );
-          subs.push_back( s );
-        }else{
-          TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, n[0][i].getType() );
-          Node op = NodeManager::currentNM()->mkSkolem( "skop_$$", typ, "op created during pre-skolemization" );
-          //DOTHIS: set attribute on op, marking that it should not be selected as trigger
-          vector< Node > funcArgs;
-          funcArgs.push_back( op );
-          funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() );
-          subs.push_back( NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs ) );
-        }
-      }
-      //apply substitution
-      nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
-      return nn;
-    }
-  }else{
-    //check if it contains a quantifier as a subterm
-    //if so, we will write this node
-    if( containsQuantifiers( n ) ){
-      if( n.getType().isBoolean() ){
-        if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){
-          Node nn;
-          //must remove structure
-          if( n.getKind()==kind::ITE ){
-            nn = NodeManager::currentNM()->mkNode( kind::AND,
-                   NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ),
-                   NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) );
-          }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){
-            nn = NodeManager::currentNM()->mkNode( kind::AND,
-                   NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ),
-                   NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) );
-          }else if( n.getKind()==kind::IMPLIES ){
-            nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] );
-          }
-          return preSkolemizeQuantifiers( nn, polarity, fvs );
-        }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){
-          vector< Node > children;
-          for( int i=0; i<(int)n.getNumChildren(); i++ ){
-            children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvs ) );
-          }
-          return NodeManager::currentNM()->mkNode( n.getKind(), children );
-        }else{
-          //must pull ite's
-        }
-      }
-    }
-    return n;
-  }
-}
-
 void SmtEnginePrivate::removeITEs() {
   d_smt.finalOptionsAreSet();
 
@@ -3156,13 +3039,25 @@ void SmtEnginePrivate::processAssertions() {
     dumpAssertions("post-strings-pp", d_assertionsToPreprocess);
   }
   if( d_smt.d_logic.isQuantified() ){
+    //remove rewrite rules
+    for( unsigned i=0; i < d_assertionsToPreprocess.size(); i++ ) {
+      if( d_assertionsToPreprocess[i].getKind() == kind::REWRITE_RULE ){
+        Node prev = d_assertionsToPreprocess[i];
+        Trace("quantifiers-rewrite-debug") << "Rewrite rewrite rule " << prev << "..." << std::endl;
+        d_assertionsToPreprocess[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::rewriteRewriteRule( d_assertionsToPreprocess[i] ) );
+        Trace("quantifiers-rewrite") << "*** rr-rewrite " << prev << endl;
+        Trace("quantifiers-rewrite") << "   ...got " << d_assertionsToPreprocess[i] << endl;
+      }
+    }
+
     dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess);
     if( options::preSkolemQuant() ){
       //apply pre-skolemization to existential quantifiers
       for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
         Node prev = d_assertionsToPreprocess[i];
+        Trace("quantifiers-rewrite-debug") << "Pre-skolemize " << prev << "..." << std::endl;
         vector< Node > fvs;
-        d_assertionsToPreprocess[i] = Rewriter::rewrite( preSkolemizeQuantifiers( d_assertionsToPreprocess[i], true, fvs ) );
+        d_assertionsToPreprocess[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvs ) );
         if( prev!=d_assertionsToPreprocess[i] ){
           Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << endl;
           Trace("quantifiers-rewrite") << "   ...got " << d_assertionsToPreprocess[i] << endl;
@@ -3174,14 +3069,14 @@ void SmtEnginePrivate::processAssertions() {
       //quantifiers macro expansion
       bool success;
       do{
-        QuantifierMacros qm;
+        quantifiers::QuantifierMacros qm;
         success = qm.simplify( d_assertionsToPreprocess, true );
       }while( success );
     }
 
     Trace("fo-rsn-enable") << std::endl;
     if( options::foPropQuant() ){
-      FirstOrderPropagation fop;
+      quantifiers::FirstOrderPropagation fop;
       fop.simplify( d_assertionsToPreprocess );
     }
   }
@@ -3977,28 +3872,26 @@ void SmtEngine::checkModel(bool hardFailure) {
     Debug("boolean-terms") << "++ got " << n << endl;
     Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << endl;
 
-    if(Theory::theoryOf(n) != THEORY_REWRITERULES) {
+    //AJR : FIXME need to ignore quantifiers too?
+    if( n.getKind() != kind::REWRITE_RULE ){
       // In case it's a quantifier (or contains one), look up its value before
       // simplifying, or the quantifier might be irreparably altered.
       n = m->getValue(n);
-    }
-
-    // Simplify the result.
-    n = d_private->simplify(n);
-    Notice() << "SmtEngine::checkModel(): -- simplifies to  " << n << endl;
-
-    TheoryId thy = Theory::theoryOf(n);
-    if(thy == THEORY_REWRITERULES) {
+    } else {
       // Note this "skip" is done here, rather than above.  This is
       // because (1) the quantifier could in principle simplify to false,
       // which should be reported, and (2) checking for the quantifier
       // above, before simplification, doesn't catch buried quantifiers
       // anyway (those not at the top-level).
-      Notice() << "SmtEngine::checkModel(): -- skipping rewrite-rules assertion"
+      Notice() << "SmtEngine::checkModel(): -- skipping quantifiers/rewrite-rules assertion"
                << endl;
       continue;
     }
 
+    // Simplify the result.
+    n = d_private->simplify(n);
+    Notice() << "SmtEngine::checkModel(): -- simplifies to  " << n << endl;
+
     // Replace the already-known ITEs (this is important for ground ITEs under quantifiers).
     n = d_private->d_iteRemover.replace(n);
     Notice() << "SmtEngine::checkModel(): -- ite replacement gives " << n << endl;
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index d920fc8ca..37dba5e92 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -70,6 +70,8 @@
 #include "theory/theory_model.h"
 
 #include "theory/arith/options.h"
+#include "theory/quantifiers/options.h"
+
 
 #include "theory/quantifiers/bounded_integers.h"
 
@@ -1597,7 +1599,7 @@ void TheoryArithPrivate::preRegisterTerm(TNode n) {
       }
       ConstraintP c = d_constraintDatabase.lookup(n);
       Assert(c != NullConstraint);
-  
+
       Debug("arith::preregister") << "setup constraint" << c << endl;
       Assert(!c->canBePropagated());
       c->setPreregistered();
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index e59874429..bec8ea350 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -18,6 +18,7 @@
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/model_engine.h"
+#include "theory/quantifiers/term_database.h"
 
 using namespace CVC4;
 using namespace std;
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 1e89bb1ea..1b34bc118 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -18,6 +18,7 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/inst_match.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/options.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 8c00c5af4..f3203da4b 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -18,6 +18,7 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/full_model_check.h"
 #include "theory/quantifiers/qinterval_builder.h"
+#include "theory/quantifiers/options.h"
 
 #define USE_INDEX_ORDERING
 
diff --git a/src/theory/quantifiers/first_order_reasoning.cpp b/src/theory/quantifiers/first_order_reasoning.cpp
index a696af3c2..1c87dad7b 100644
--- a/src/theory/quantifiers/first_order_reasoning.cpp
+++ b/src/theory/quantifiers/first_order_reasoning.cpp
@@ -19,10 +19,11 @@
 #include "theory/rewriter.h"
 
 using namespace CVC4;
-using namespace CVC4::kind;
 using namespace std;
-
-namespace CVC4 {
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace CVC4::kind;
+using namespace CVC4::context;
 
 
 void FirstOrderPropagation::collectLits( Node n, std::vector<Node> & lits ){
@@ -167,5 +168,3 @@ Node FirstOrderPropagation::simplify( Node n ) {
     return NodeManager::currentNM()->mkNode( n.getKind(), children );
   }
 }
-
-}
diff --git a/src/theory/quantifiers/first_order_reasoning.h b/src/theory/quantifiers/first_order_reasoning.h
index 6bc5c21c1..92898eff5 100644
--- a/src/theory/quantifiers/first_order_reasoning.h
+++ b/src/theory/quantifiers/first_order_reasoning.h
@@ -25,6 +25,8 @@
 #include "expr/type_node.h"
 
 namespace CVC4 {
+namespace theory {
+namespace quantifiers {
 
 class FirstOrderPropagation {
 private:
@@ -41,5 +43,7 @@ public:
 };
 
 }
+}
+}
 
 #endif
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index d542e878c..6c889781d 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/full_model_check.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/options.h"
+#include "theory/quantifiers/term_database.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp
index 27b87e6a4..aaa65e630 100644
--- a/src/theory/quantifiers/inst_gen.cpp
+++ b/src/theory/quantifiers/inst_gen.cpp
@@ -16,6 +16,7 @@
 #include "theory/quantifiers/model_engine.h"
 #include "theory/quantifiers/model_builder.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/term_database.h"
 
 //#define CHILD_USE_CONSIDER
 
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index e1d301c09..13186c7cc 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -18,6 +18,7 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/candidate_generator.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/options.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index dee8192c1..f60e01a7d 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -97,22 +97,11 @@ void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){
     //extend to literal matching
     d_quantEngine->getPhaseReqTerms( f, nodes );
     //check match option
-    int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0;
+    int matchOption = 0;
     d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW,
                                                  options::smartTriggers() ) );
   }
 }
-/*
-InstStrategyUserPatterns::Statistics::Statistics():
-  d_instantiations("InstStrategyUserPatterns::Instantiations", 0)
-{
-  StatisticsRegistry::registerStat(&d_instantiations);
-}
-
-InstStrategyUserPatterns::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_instantiations);
-}
-*/
 
 void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){
   //reset triggers
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 99dc29bf8..e5705882a 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -209,7 +209,7 @@ void InstantiationEngine::check( Theory::Effort e ){
     for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       Node n = d_quantEngine->getModel()->getAssertedQuantifier( i );
       //it is not active if we have found the skolemized negation is unsat
-      if( n.hasAttribute(QRewriteRuleAttribute()) ){
+      if( TermDb::isRewriteRule( n ) ){
         d_quant_active[n] = false;
       }else if( options::cbqi() && hasAddedCbqiLemma( n ) ){
         Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( n );
@@ -292,19 +292,23 @@ void InstantiationEngine::check( Theory::Effort e ){
 }
 
 void InstantiationEngine::registerQuantifier( Node f ){
-  //Notice() << "do cbqi " << f << " ? " << std::endl;
-  Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
-  if( !doCbqi( f ) ){
-    d_quantEngine->addTermToDatabase( ceBody, true );
-  }
+  if( !TermDb::isRewriteRule( f ) ){
+    //Notice() << "do cbqi " << f << " ? " << std::endl;
+    if( options::cbqi() ){
+      Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
+      if( !doCbqi( f ) ){
+        d_quantEngine->addTermToDatabase( ceBody, true );
+      }
+    }
 
-  //take into account user patterns
-  if( f.getNumChildren()==3 ){
-    Node subsPat = d_quantEngine->getTermDatabase()->getInstConstantNode( f[2], f );
-    //add patterns
-    for( int i=0; i<(int)subsPat.getNumChildren(); i++ ){
-      //Notice() << "Add pattern " << subsPat[i] << " for " << f << std::endl;
-      addUserPattern( f, subsPat[i] );
+    //take into account user patterns
+    if( f.getNumChildren()==3 ){
+      Node subsPat = d_quantEngine->getTermDatabase()->getInstConstantNode( f[2], f );
+      //add patterns
+      for( int i=0; i<(int)subsPat.getNumChildren(); i++ ){
+        //Notice() << "Add pattern " << subsPat[i] << " for " << f << std::endl;
+        addUserPattern( f, subsPat[i] );
+      }
     }
   }
 }
diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds
index ab0e9d934..795bc1ab4 100644
--- a/src/theory/quantifiers/kinds
+++ b/src/theory/quantifiers/kinds
@@ -48,4 +48,25 @@ typerule BOUND_VAR_LIST ::CVC4::theory::quantifiers::QuantifierBoundVarListTypeR
 typerule INST_PATTERN ::CVC4::theory::quantifiers::QuantifierInstPatternTypeRule 
 typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule 
 
+# for rewrite rules
+# types...
+sort RRHB_TYPE \
+    Cardinality::INTEGERS \
+    not-well-founded \
+    "head and body of the rule type"
+
+# operators...
+
+# variables, guards, RR_REWRITE/REDUCTION_RULE/DEDUCTION_RULE
+operator REWRITE_RULE 3 "general rewrite rule"
+#HEAD/BODY/TRIGGER
+operator RR_REWRITE 2:3 "actual rewrite rule"
+operator RR_REDUCTION 2:3 "actual reduction rule"
+operator RR_DEDUCTION 2:3 "actual deduction rule"
+
+typerule REWRITE_RULE ::CVC4::theory::quantifiers::RewriteRuleTypeRule
+typerule RR_REWRITE   ::CVC4::theory::quantifiers::RRRewriteTypeRule
+typerule RR_REDUCTION ::CVC4::theory::quantifiers::RRRedDedTypeRule
+typerule RR_DEDUCTION ::CVC4::theory::quantifiers::RRRedDedTypeRule
+
 endtheory
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 502a34176..50a0084fc 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -24,6 +24,7 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/inst_gen.h"
 #include "theory/quantifiers/trigger.h"
+#include "theory/quantifiers/options.h"
 
 using namespace std;
 using namespace CVC4;
@@ -39,7 +40,7 @@ TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_curr_model( c, NULL ), d_qe
 }
 
 bool QModelBuilder::isQuantifierActive( Node f ) {
-  return !f.hasAttribute(QRewriteRuleAttribute());
+  return !TermDb::isRewriteRule( f );
 }
 
 
@@ -381,7 +382,7 @@ QModelBuilderIG::Statistics::~Statistics(){
 }
 
 bool QModelBuilderIG::isQuantifierActive( Node f ){
-  return !f.hasAttribute(QRewriteRuleAttribute()) &&
+  return !TermDb::isRewriteRule( f ) &&
          ( d_considerAxioms || !f.getAttribute(AxiomAttribute()) ) && d_quant_sat.find( f )==d_quant_sat.end();
 }
 
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 2967c77c8..7ee416c4e 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -125,5 +125,9 @@ option qcfMode --quant-cf-mode=MODE CVC4::theory::quantifiers::QcfMode :default
 option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :default CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfWhenMode :handler-include "theory/quantifiers/options_handlers.h"
  when to invoke conflict find mechanism for quantifiers
 
+option quantRewriteRules --rewrite-rules bool :default false
+ use rewrite rules module
+option rrOneInstPerRound --rr-one-inst-per-round bool :default false
+ add one instance of rewrite rule per round
 
 endmodule
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 9892009a3..e9c754d4a 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -131,6 +131,9 @@ conflict \n\
 partial \n\
 + Apply QCF algorithm to instantiate heuristically as well. \n\
 \n\
+partial \n\
++ Apply QCF to instantiate heuristically as well. \n\
+\n\
 mc \n\
 + Apply QCF algorithm in a complete way, so that a model is ensured when it fails. \n\
 \n\
diff --git a/src/theory/quantifiers/qinterval_builder.cpp b/src/theory/quantifiers/qinterval_builder.cpp
index ece519d1c..285834e96 100755
--- a/src/theory/quantifiers/qinterval_builder.cpp
+++ b/src/theory/quantifiers/qinterval_builder.cpp
@@ -14,6 +14,8 @@
 

 

 #include "theory/quantifiers/qinterval_builder.h"

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

+

 

 using namespace std;

 using namespace CVC4;

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index ae5a35a00..79948a063 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -18,6 +18,8 @@
 #include "theory/quantifiers/quant_conflict_find.h"

 #include "theory/quantifiers/quant_util.h"

 #include "theory/theory_engine.h"

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

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

 

 using namespace CVC4;

 using namespace CVC4::kind;

@@ -107,27 +109,16 @@ void QuantInfo::initialize( Node q, Node qn ) {
       std::vector< int > bvars;

       d_mg->determineVariableOrder( this, bvars );

     }

-

-    //must also contain all variables?

-    if( d_isPartial ){

-      for( unsigned i=0; i<q[0].getNumChildren(); i++ ){

-        if( d_has_var.find( q[0][i] )==d_has_var.end() ){

-          d_isPartial = false;

-          d_mg->setInvalid();

-          break;

-        }

-      }

-    }

   }

-  Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? ( isPartial() ? "PARTIAL " : "VALID " ) : "INVALID" ) << " : " << q << std::endl;

+  Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl;

 }

 

 void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) {

   Trace("qcf-qregister-debug2") << "Register : " << n << std::endl;

   if( n.getKind()==FORALL ){

     registerNode( n[1], hasPol, pol, true );

-  }else{

-    if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=NOT ){

+  }else{
+    if( !MatchGen::isHandledBoolConnective( n ) ){

       if( n.hasBoundVar() ){

         //literals

         if( n.getKind()==EQUAL ){

@@ -136,11 +127,9 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant )
           }

         }else if( MatchGen::isHandledUfTerm( n ) ){

           flatten( n, beneathQuant );

-        }else if( n.getKind()==ITE ){

-          if( !n[1].getType().isBoolean() ){

-            for( unsigned i=1; i<=2; i++ ){

-              flatten( n[i], beneathQuant );

-            }

+        }else if( n.getKind()==ITE ){
+          for( unsigned i=1; i<=2; i++ ){

+            flatten( n[i], beneathQuant );

           }

         }

       }

@@ -220,6 +209,8 @@ void QuantInfo::reset_round( QuantConflictFind * p ) {
   for( std::map< int, MatchGen * >::iterator it = d_var_mg.begin(); it != d_var_mg.end(); ++it ){

     it->second->reset_round( p );

   }

+  //now, reset for matching

+  d_mg->reset( p, false, this );

 }

 

 int QuantInfo::getCurrentRepVar( int v ) {

@@ -249,6 +240,24 @@ TNode QuantInfo::getCurrentValue( TNode n ) {
   }

 }

 

+TNode QuantInfo::getCurrentExpValue( TNode n ) {

+  int v = getVarNum( n );

+  if( v==-1 ){

+    return n;

+  }else{

+    if( d_match[v].isNull() ){

+      return n;

+    }else{

+      Assert( getVarNum( d_match[v] )!=v );

+      if( d_match_term[v].isNull() ){

+        return getCurrentValue( d_match[v] );

+      }else{

+        return d_match_term[v];

+      }

+    }

+  }

+}

+

 bool QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq ) {

   //check disequalities

   std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( v );

@@ -453,109 +462,113 @@ bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) {
   return false;

 }

 

-bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assigned ) {

+bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue ) {

   //assign values for variables that were unassigned (usually not necessary, but handles corner cases)

-  Trace("qcf-check") << std::endl;

-  std::vector< int > unassigned[2];

-  std::vector< TypeNode > unassigned_tn[2];

-  for( int i=0; i<getNumVars(); i++ ){

-    if( d_match[i].isNull() ){

-      //Assert( i<(int)q[0].getNumChildren() );

-      int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;

-      unassigned[rindex].push_back( i );

-      unassigned_tn[rindex].push_back( getVar( i ).getType() );

-      assigned.push_back( i );

+  bool doFail = false;

+  bool success = true;

+  if( doContinue ){

+    doFail = true;

+    success = false;

+  }else{

+    d_unassigned.clear();

+    d_unassigned_tn.clear();

+    std::vector< int > unassigned[2];

+    std::vector< TypeNode > unassigned_tn[2];

+    for( int i=0; i<getNumVars(); i++ ){

+      if( d_match[i].isNull() ){

+        int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;

+        unassigned[rindex].push_back( i );

+        unassigned_tn[rindex].push_back( getVar( i ).getType() );

+        assigned.push_back( i );

+      }

+    }

+    d_unassigned_nvar = unassigned[0].size();

+    for( unsigned i=0; i<2; i++ ){

+      d_unassigned.insert( d_unassigned.end(), unassigned[i].begin(), unassigned[i].end() );

+      d_unassigned_tn.insert( d_unassigned_tn.end(), unassigned_tn[i].begin(), unassigned_tn[i].end() );

     }

+    d_una_eqc_count.clear();

+    d_una_index = 0;

   }

-  bool success = true;

-  for( unsigned r=0; r<2; r++ ){

-    if( success && !unassigned[r].empty() ){

-      Trace("qcf-check") << "Assign to unassigned, rep = " << r << "..." << std::endl;

-      int index = 0;

-      std::vector< int > eqc_count;

-      bool doFail = false;

-      do {

-        if( doFail ){

-          Trace("qcf-check-unassign") << "Failure, try again..." << std::endl;

-        }

-        bool invalidMatch = false;

-        while( ( index>=0 && (int)index<(int)unassigned[r].size() ) || invalidMatch || doFail ){

-          invalidMatch = false;

-          if( !doFail && index==(int)eqc_count.size() ){

-            //check if it has now been assigned

-            if( r==0 ){

-              if( !isConstrainedVar( unassigned[r][index] ) ){

-                eqc_count.push_back( -1 );

-              }else{

-                d_var_mg[ unassigned[r][index] ]->reset( p, true, this );

-                eqc_count.push_back( 0 );

-              }

+  if( !d_unassigned.empty() ){

+    Trace("qcf-check") << "Assign to unassigned..." << std::endl;

+    do {

+      if( doFail ){

+        Trace("qcf-check-unassign") << "Failure, try again..." << std::endl;

+      }

+      bool invalidMatch = false;

+      while( ( d_una_index>=0 && (int)d_una_index<(int)d_unassigned.size() ) || invalidMatch || doFail ){

+        invalidMatch = false;

+        if( !doFail && d_una_index==(int)d_una_eqc_count.size() ){

+          //check if it has now been assigned

+          if( d_una_index<d_unassigned_nvar ){

+            if( !isConstrainedVar( d_unassigned[d_una_index] ) ){

+              d_una_eqc_count.push_back( -1 );

             }else{

-              eqc_count.push_back( 0 );

+              d_var_mg[ d_unassigned[d_una_index] ]->reset( p, true, this );

+              d_una_eqc_count.push_back( 0 );

             }

           }else{

-            if( r==0 ){

-              if( !doFail && !isConstrainedVar( unassigned[r][index] ) ){

-                Trace("qcf-check-unassign") << "Succeeded, variable unconstrained at " << index << std::endl;

-                index++;

-              }else if( !doFail && d_var_mg[unassigned[r][index]]->getNextMatch( p, this ) ){

-                Trace("qcf-check-unassign") << "Succeeded match with mg at " << index << std::endl;

-                index++;

+            d_una_eqc_count.push_back( 0 );

+          }

+        }else{

+          bool failed = false;

+          if( !doFail ){

+            if( d_una_index<d_unassigned_nvar ){

+              if( !isConstrainedVar( d_unassigned[d_una_index] ) ){

+                Trace("qcf-check-unassign") << "Succeeded, variable unconstrained at " << d_una_index << std::endl;

+                d_una_index++;

+              }else if( d_var_mg[d_unassigned[d_una_index]]->getNextMatch( p, this ) ){

+                Trace("qcf-check-unassign") << "Succeeded match with mg at " << d_una_index << std::endl;

+                d_una_index++;

               }else{

-                Trace("qcf-check-unassign") << "Failed match with mg at " << index << std::endl;

-                do{

-                  if( !doFail ){

-                    eqc_count.pop_back();

-                  }else{

-                    doFail = false;

-                  }

-                  index--;

-                }while( index>=0 && eqc_count[index]==-1 );

+                failed = true;

+                Trace("qcf-check-unassign") << "Failed match with mg at " << d_una_index << std::endl;

               }

             }else{

-              Assert( doFail || index==(int)eqc_count.size()-1 );

-              if( !doFail && eqc_count[index]<(int)p->d_eqcs[unassigned_tn[r][index]].size() ){

-                int currIndex = eqc_count[index];

-                eqc_count[index]++;

-                Trace("qcf-check-unassign") << unassigned[r][index] << "->" << p->d_eqcs[unassigned_tn[r][index]][currIndex] << std::endl;

-                if( setMatch( p, unassigned[r][index], p->d_eqcs[unassigned_tn[r][index]][currIndex] ) ){

-                  //if( currIndex==0 ){

-                  //  Assert( p->areEqual( p->d_model_basis[unassigned_tn[r][index]], p->d_eqcs[unassigned_tn[r][index]][currIndex] ) );

-                  //  d_match_term[unassigned[r][index]] = p->d_model_basis[unassigned_tn[r][index]];

-                  //}else{

-                  d_match_term[unassigned[r][index]] = TNode::null();

-                  //}

-                  Trace("qcf-check-unassign") << "Succeeded match " << index << std::endl;

-                  index++;

+              Assert( doFail || d_una_index==(int)d_una_eqc_count.size()-1 );

+              if( d_una_eqc_count[d_una_index]<(int)p->d_eqcs[d_unassigned_tn[d_una_index]].size() ){

+                int currIndex = d_una_eqc_count[d_una_index];

+                d_una_eqc_count[d_una_index]++;

+                Trace("qcf-check-unassign") << d_unassigned[d_una_index] << "->" << p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] << std::endl;

+                if( setMatch( p, d_unassigned[d_una_index], p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] ) ){

+                  d_match_term[d_unassigned[d_una_index]] = TNode::null();

+                  Trace("qcf-check-unassign") << "Succeeded match " << d_una_index << std::endl;

+                  d_una_index++;

                 }else{

-                  Trace("qcf-check-unassign") << "Failed match " << index << std::endl;

+                  Trace("qcf-check-unassign") << "Failed match " << d_una_index << std::endl;

                   invalidMatch = true;

                 }

               }else{

-                Trace("qcf-check-unassign") << "No more matches " << index << std::endl;

-                if( !doFail ){

-                  eqc_count.pop_back();

-                }else{

-                  doFail = false;

-                }

-                index--;

+                failed = true;

+                Trace("qcf-check-unassign") << "No more matches " << d_una_index << std::endl;

               }

             }

           }

+          if( doFail || failed ){

+            do{

+              if( !doFail ){

+                d_una_eqc_count.pop_back();

+              }else{

+                doFail = false;

+              }

+              d_una_index--;

+            }while( d_una_index>=0 && d_una_eqc_count[d_una_index]==-1 );

+          }

         }

-        success = index>=0;

-        if( success ){

-          doFail = true;

-          Trace("qcf-check-unassign") << "  Try: " << std::endl;

-          for( unsigned i=0; i<unassigned[r].size(); i++ ){

-            int ui = unassigned[r][i];

-            if( !d_match[ui].isNull() ){

-              Trace("qcf-check-unassign") << "  Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;

-            }

+      }

+      success = d_una_index>=0;

+      if( success ){

+        doFail = true;

+        Trace("qcf-check-unassign") << "  Try: " << std::endl;

+        for( unsigned i=0; i<d_unassigned.size(); i++ ){

+          int ui = d_unassigned[i];

+          if( !d_match[ui].isNull() ){

+            Trace("qcf-check-unassign") << "  Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;

           }

         }

-      }while( success && isMatchSpurious( p ) );

-    }

+      }

+    }while( success && isMatchSpurious( p ) );

   }

   if( success ){

     return true;

@@ -568,6 +581,28 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
   }

 }

 

+void QuantInfo::getMatch( std::vector< Node >& terms ){

+  for( unsigned i=0; i<d_q[0].getNumChildren(); i++ ){

+    //Node cv = qi->getCurrentValue( qi->d_match[i] );

+    int repVar = getCurrentRepVar( i );

+    Node cv;

+    //std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar );

+    if( !d_match_term[repVar].isNull() ){

+      cv = d_match_term[repVar];

+    }else{

+      cv = d_match[repVar];

+    }

+    Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << d_match[i] << std::endl;

+    terms.push_back( cv );

+  }

+}

+

+void QuantInfo::revertMatch( std::vector< int >& assigned ) {

+  for( unsigned i=0; i<assigned.size(); i++ ){

+    d_match[ assigned[i] ] = TNode::null();

+  }

+}

+

 void QuantInfo::debugPrintMatch( const char * c ) {

   for( int i=0; i<getNumVars(); i++ ){

     Trace(c) << "  " << d_vars[i] << " -> ";

@@ -583,7 +618,10 @@ void QuantInfo::debugPrintMatch( const char * c ) {
       }

       Trace(c) << "}";

     }

-    Trace(c) << std::endl;

+    if( !d_match_term[i].isNull() && d_match_term[i]!=d_match[i] ){

+      Trace(c) << ", EXP : " << d_match_term[i];

+    }

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

   }

 }

 

@@ -614,9 +652,6 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){
           Trace("qcf-qregister-debug") << " is var #" << v << std::endl;

           d_qni_var_num[d_qni_size] = v;

           //qi->addFuncParent( v, f, j );

-          if( nn.getKind()==BOUND_VARIABLE && !beneathQuant ){

-            qi->d_has_var[nn] = true;

-          }

         }else{

           Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;

           d_qni_gterm[d_qni_size] = nn;

@@ -655,7 +690,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){
         d_type_not = !d_type_not;

       }

 

-      if( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF || d_n.getKind()==ITE || d_n.getKind()==FORALL ){

+      if( isHandledBoolConnective( d_n ) ){

         //non-literals

         d_type = typ_formula;

         bool nBeneathQuant = beneathQuant || d_n.getKind()==FORALL;

@@ -696,8 +731,6 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){
             if( d_n[i].hasBoundVar() ){

               if( !qi->isVar( d_n[i] ) ){

                 Trace("qcf-qregister-debug")  << "ERROR : not var " << d_n[i] << std::endl;

-              }else if( d_n[i].getKind()==BOUND_VARIABLE && !beneathQuant ){

-                qi->d_has_var[d_n[i]] = true;

               }

               Assert( qi->isVar( d_n[i] ) );

             }else{

@@ -708,6 +741,8 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){
         }else if( isHandledUfTerm( d_n ) ){

           Assert( qi->isVar( d_n ) );

           d_type = typ_pred;

+        }else if( d_n.getKind()==BOUND_VARIABLE ){

+          d_type = typ_bool_var;

         }else{

           Trace("qcf-invalid") << "Unhandled : " << d_n << std::endl;

         }

@@ -737,9 +772,6 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){
   Trace("qcf-qregister-debug") << std::endl;

   //Assert( d_children.size()==d_children_order.size() );

 

-  if( !isValid() && options::qcfMode()>=QCF_PARTIAL ){

-    qi->d_isPartial = true;

-  }

 }

 

 void MatchGen::collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars ) {

@@ -829,6 +861,7 @@ void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars
 

 

 void MatchGen::reset_round( QuantConflictFind * p ) {

+  d_wasSet = false;

   for( unsigned i=0; i<d_children.size(); i++ ){

     d_children[i].reset_round( p );

   }

@@ -849,6 +882,9 @@ void MatchGen::reset_round( QuantConflictFind * p ) {
       }

     }

   }

+  d_qni_bound_cons.clear();

+  d_qni_bound_cons_var.clear();

+  d_qni_bound.clear();

 }

 

 void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {

@@ -860,6 +896,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
   d_qni.clear();

   d_qni_bound.clear();

   d_child_counter = -1;

+  d_tgt_orig = d_tgt;

 

   //set up processing matches

   if( d_type==typ_invalid ){

@@ -870,6 +907,25 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
     if( d_ground_eval[0]==( d_tgt ? p->d_true : p->d_false ) ){

       d_child_counter = 0;

     }

+  }else if( d_type==typ_bool_var ){

+    //get current value of the variable

+    TNode n = qi->getCurrentValue( d_n );

+    int vn = qi->getCurrentRepVar( qi->getVarNum( n ) );

+    if( vn==-1 ){

+      //evaluate the value, see if it is compatible

+      int e = p->evaluate( n );

+      if( ( e==1 && d_tgt ) || ( e==0 && !d_tgt ) ){

+        d_child_counter = 0;

+      }

+    }else{

+      //unassigned, set match to true/false

+      d_qni_bound[0] = vn;

+      qi->setMatch( p, vn, d_tgt ? p->d_true : p->d_false );

+      d_child_counter = 0;

+    }

+    if( d_child_counter==0 ){

+      d_qn.push_back( NULL );

+    }

   }else if( d_type==typ_var ){

     Assert( isHandledUfTerm( d_n ) );

     Node f = getOperator( p, d_n );

@@ -904,6 +960,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
     }

     bool success;

     if( vn[0]==-1 && vn[1]==-1 ){

+      //Trace("qcf-explain") << "    reset : " << d_n << " check ground values " << nn[0] << " " << nn[1] << " (tgt=" << d_tgt << ")" << std::endl;

       Debug("qcf-match-debug") << "       reset: check ground values " << nn[0] << " " << nn[1] << " (" << d_tgt << ")" << std::endl;

       //just compare values

       if( d_tgt ){

@@ -931,6 +988,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
       success = addc!=-1;

       //if successful and non-redundant, store that we need to cleanup this

       if( addc==1 ){

+        //Trace("qcf-explain") << "       reset: " << d_n << " add constraint " << vn[0] << " -> " << nn[1] << " (vn=" << vn[1] << ")" << ", d_tgt = " << d_tgt << std::endl;

         for( unsigned i=0; i<2; i++ ){

           if( vn[i]!=-1 && std::find( d_qni_bound_except.begin(), d_qni_bound_except.end(), i )==d_qni_bound_except.end() ){

             d_qni_bound[vn[i]] = vn[i];

@@ -962,6 +1020,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
     }

   }

   d_binding = false;

+  d_wasSet = true;

   Debug("qcf-match") << "     reset: Finished reset for " << d_n << ", success = " << ( !d_qn.empty() || d_child_counter!=-1 ) << std::endl;

 }

 

@@ -974,9 +1033,10 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
       d_child_counter = -1;

       return true;

     }else{

+      d_wasSet = false;

       return false;

     }

-  }else if( d_type==typ_var || d_type==typ_eq || d_type==typ_pred ){

+  }else if( d_type==typ_var || d_type==typ_eq || d_type==typ_pred || d_type==typ_bool_var ){

     bool success = false;

     bool terminate = false;

     do {

@@ -1020,8 +1080,8 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
                   Debug("qcf-match-debug") << "       failed." << std::endl;

                   success = false;

                 }else{

-                  Debug("qcf-match-debug") << "       decrement..." << std::endl;

                   --d_binding_it;

+                  Debug("qcf-match-debug") << "       decrement..." << std::endl;

                 }

               }while( success && ( d_binding_it->first==0 || qi->d_var_mg.find( d_binding_it->second )==qi->d_var_mg.end() ) );

               doReset = false;

@@ -1056,6 +1116,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
             Debug("qcf-match") << "       Clean up bound var " << it->first << (d_tgt ? "!" : "") << " = " << it->second << std::endl;

             std::map< int, int >::iterator itb = d_qni_bound_cons_var.find( it->first );

             int vn = itb!=d_qni_bound_cons_var.end() ? itb->second : -1;

+            //Trace("qcf-explain") << "       cleanup: " << d_n << " remove constraint " << it->first << " -> " << it->second << " (vn=" << vn << ")" << ", d_tgt = " << d_tgt << std::endl;

             qi->addConstraint( p, it->first, it->second, vn, d_tgt, true );

           }

         }

@@ -1085,6 +1146,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
       */

     }

     Debug("qcf-match") << "    ...finished matching for " << d_n << ", success = " << success << std::endl;

+    d_wasSet = success;

     return success;

   }else if( d_type==typ_formula || d_type==typ_ite_var ){

     bool success = false;

@@ -1096,7 +1158,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
     }else{

       while( !success && d_child_counter>=0 ){

         //transition system based on d_child_counter

-        if( d_type==typ_top || d_n.getKind()==OR || d_n.getKind()==AND ){

+        if( d_n.getKind()==OR || d_n.getKind()==AND ){

           if( (d_n.getKind()==AND)==d_tgt ){

             //all children must match simultaneously

             if( getChild( d_child_counter )->getNextMatch( p, qi ) ){

@@ -1181,6 +1243,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
           }

         }

       }

+        d_wasSet = success;

       Debug("qcf-match") << "    ...finished construct match for " << d_n << ", success = " << success << std::endl;

       return success;

     }

@@ -1189,6 +1252,84 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
   return false;

 }

 

+bool MatchGen::getExplanation( QuantConflictFind * p, QuantInfo * qi, std::vector< Node >& exp ) {

+  if( d_type==typ_eq ){

+    Node n[2];

+    for( unsigned i=0; i<2; i++ ){

+      Trace("qcf-explain") << "Explain term " << d_n[i] << "..." << std::endl;

+      n[i] = getExplanationTerm( p, qi, d_n[i], exp );

+    }

+    Node eq = n[0].eqNode( n[1] );

+    if( !d_tgt_orig ){

+      eq = eq.negate();

+    }

+    exp.push_back( eq );

+    Trace("qcf-explain") << "Explanation for " << d_n << " (tgt=" << d_tgt_orig << ") is " << eq << ", set = " << d_wasSet << std::endl;

+    return true;

+  }else if( d_type==typ_pred ){

+    Trace("qcf-explain") << "Explain term " << d_n << "..." << std::endl;

+    Node n = getExplanationTerm( p, qi, d_n, exp );

+    if( !d_tgt_orig ){

+      n = n.negate();

+    }

+    exp.push_back( n );

+    Trace("qcf-explain") << "Explanation for " << d_n << " (tgt=" << d_tgt_orig << ") is " << n << ", set = " << d_wasSet << std::endl;

+    return true;

+  }else if( d_type==typ_formula ){

+    Trace("qcf-explain") << "Explanation get for " << d_n << ", counter = " << d_child_counter << ", tgt = " << d_tgt_orig << ", set = " << d_wasSet << std::endl;

+    if( d_n.getKind()==OR || d_n.getKind()==AND ){

+      if( (d_n.getKind()==AND)==d_tgt ){

+        for( unsigned i=0; i<getNumChildren(); i++ ){

+          if( !getChild( i )->getExplanation( p, qi, exp ) ){

+            return false;

+          }

+        }

+      }else{

+        return getChild( d_child_counter )->getExplanation( p, qi, exp );

+      }

+    }else if( d_n.getKind()==IFF ){

+      for( unsigned i=0; i<2; i++ ){

+        if( !getChild( i )->getExplanation( p, qi, exp ) ){

+          return false;

+        }

+      }

+    }else if( d_n.getKind()==ITE ){

+      for( unsigned i=0; i<3; i++ ){

+        bool isActive = ( ( i==0 && d_child_counter!=5 ) ||

+                          ( i==1 && d_child_counter!=( d_tgt ? 3 : 1 ) ) ||

+                          ( i==2 && d_child_counter!=( d_tgt ? 1 : 3 ) ) );

+        if( isActive ){

+          if( !getChild( i )->getExplanation( p, qi, exp ) ){

+            return false;

+          }

+        }

+      }

+    }else{

+      return false;

+    }

+    return true;

+  }else{

+    return false;

+  }

+}

+

+Node MatchGen::getExplanationTerm( QuantConflictFind * p, QuantInfo * qi, Node t, std::vector< Node >& exp ) {

+  Node v = qi->getCurrentExpValue( t );

+  if( isHandledUfTerm( t ) ){

+    for( unsigned i=0; i<t.getNumChildren(); i++ ){

+      Node vi = getExplanationTerm( p, qi, t[i], exp );

+      if( vi!=v[i] ){

+        Node eq = vi.eqNode( v[i] );

+        if( std::find( exp.begin(), exp.end(), eq )==exp.end() ){

+          Trace("qcf-explain") << "  add : " << eq << "." << std::endl;

+          exp.push_back( eq );

+        }

+      }

+    }

+  }

+  return v;

+}

+

 bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {

   if( !d_qn.empty() ){

     if( d_qn[0]==NULL ){

@@ -1297,14 +1438,17 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
         Assert( !d_qni[d_qni.size()-1]->second.d_children.empty() );

         TNode t = d_qni[d_qni.size()-1]->second.d_children.begin()->first;

         Debug("qcf-match-debug") << "       " << d_n << " matched " << t << std::endl;

+        qi->d_match_term[d_qni_var_num[0]] = t;

         //set the match terms

         for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){

           Debug("qcf-match-debug") << "       position " << it->first << " bounded " << it->second << " / " << qi->d_q[0].getNumChildren() << std::endl;

-          if( it->second<(int)qi->d_q[0].getNumChildren() && it->first>0 ){   //if it is an actual variable, we are interested in knowing the actual term

+          //if( it->second<(int)qi->d_q[0].getNumChildren() ){   //if it is an actual variable, we are interested in knowing the actual term

+          if( it->first>0 ){

             Assert( !qi->d_match[ it->second ].isNull() );

             Assert( p->areEqual( t[it->first-1], qi->d_match[ it->second ] ) );

             qi->d_match_term[it->second] = t[it->first-1];

           }

+          //}

         }

       }

     }

@@ -1322,7 +1466,7 @@ void MatchGen::debugPrintType( const char * c, short typ, bool isTrace ) {
     case typ_formula: Trace(c) << "formula";break;

     case typ_var: Trace(c) << "var";break;

     case typ_ite_var: Trace(c) << "ite_var";break;

-    case typ_top: Trace(c) << "top";break;

+    case typ_bool_var: Trace(c) << "bool_var";break;

     }

   }else{

     switch( typ ){

@@ -1333,7 +1477,7 @@ void MatchGen::debugPrintType( const char * c, short typ, bool isTrace ) {
     case typ_formula: Debug(c) << "formula";break;

     case typ_var: Debug(c) << "var";break;

     case typ_ite_var: Debug(c) << "ite_var";break;

-    case typ_top: Debug(c) << "top";break;

+    case typ_bool_var: Debug(c) << "bool_var";break;

     }

   }

 }

@@ -1343,18 +1487,37 @@ void MatchGen::setInvalid() {
   d_children.clear();

 }

 

+bool MatchGen::isHandledBoolConnective( TNode n ) {

+  return n.getType().isBoolean() && ( n.getKind()==OR || n.getKind()==AND || n.getKind()==IFF || n.getKind()==ITE || n.getKind()==FORALL || n.getKind()==NOT );

+}

+

 bool MatchGen::isHandledUfTerm( TNode n ) {

-  return n.getKind()==APPLY_UF;// || n.getKind()==GEQ;

+  return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT ||

+         n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER;// || n.getKind()==GEQ;

 }

 

 Node MatchGen::getOperator( QuantConflictFind * p, Node n ) {

   if( isHandledUfTerm( n ) ){

-    return n.getOperator();

+    return p->getQuantifiersEngine()->getTermDatabase()->getOperator( n );

   }else{

     return Node::null();

   }

 }

 

+bool MatchGen::isHandled( TNode n ) {

+  if( n.getKind()!=BOUND_VARIABLE && n.hasBoundVar() ){

+    if( !isHandledBoolConnective( n ) && !isHandledUfTerm( n ) && n.getKind()!=EQUAL && n.getKind()!=ITE ){

+      return false;

+    }

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

+      if( !isHandled( n[i] ) ){

+        return false;

+      }

+    }

+  }

+  return true;

+}

+

 

 QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) :

 QuantifiersModule( qe ),

@@ -1377,30 +1540,32 @@ Node QuantConflictFind::mkEqNode( Node a, Node b ) {
 //-------------------------------------------------- registration

 

 void QuantConflictFind::registerQuantifier( Node q ) {

-  d_quants.push_back( q );

-  d_quant_id[q] = d_quants.size();

-  Trace("qcf-qregister") << "Register ";

-  debugPrintQuant( "qcf-qregister", q );

-  Trace("qcf-qregister") << " : " << q << std::endl;

-  //make QcfNode structure

-  Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;

-  d_qinfo[q].initialize( q, q[1] );

-

-  //debug print

-  Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;

-  Trace("qcf-qregister") << "    ";

-  debugPrintQuantBody( "qcf-qregister", q, q[1] );

-  Trace("qcf-qregister") << std::endl;

-  if( d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){

-    Trace("qcf-qregister") << "  with additional constraints : " << std::endl;

-    for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){

-      Trace("qcf-qregister") << "    ?x" << j << " = ";

-      debugPrintQuantBody( "qcf-qregister", q, d_qinfo[q].d_vars[j], false );

-      Trace("qcf-qregister") << std::endl;

+  if( !TermDb::isRewriteRule( q ) ){

+    d_quants.push_back( q );

+    d_quant_id[q] = d_quants.size();

+    Trace("qcf-qregister") << "Register ";

+    debugPrintQuant( "qcf-qregister", q );

+    Trace("qcf-qregister") << " : " << q << std::endl;

+    //make QcfNode structure

+    Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;

+    d_qinfo[q].initialize( q, q[1] );

+

+    //debug print

+    Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;

+    Trace("qcf-qregister") << "    ";

+    debugPrintQuantBody( "qcf-qregister", q, q[1] );

+    Trace("qcf-qregister") << std::endl;

+    if( d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){

+      Trace("qcf-qregister") << "  with additional constraints : " << std::endl;

+      for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){

+        Trace("qcf-qregister") << "    ?x" << j << " = ";

+        debugPrintQuantBody( "qcf-qregister", q, d_qinfo[q].d_vars[j], false );

+        Trace("qcf-qregister") << std::endl;

+      }

     }

-  }

 

-  Trace("qcf-qregister") << "Done registering quantifier." << std::endl;

+    Trace("qcf-qregister") << "Done registering quantifier." << std::endl;

+  }

 }

 

 int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) {

@@ -1481,6 +1646,20 @@ int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) {
   return ret;

 }

 

+short QuantConflictFind::getMaxQcfEffort() {

+  if( options::qcfMode()==QCF_CONFLICT_ONLY ){

+    return effort_conflict;

+  }else if( options::qcfMode()==QCF_PROP_EQ ){

+    return effort_prop_eq;

+  }else if( options::qcfMode()==QCF_PARTIAL ){

+    return effort_partial;

+  }else if( options::qcfMode()==QCF_MC ){

+    return effort_mc;

+  }else{

+    return 0;

+  }

+}

+

 bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) {

   //if( d_effort==QuantConflictFind::effort_mc ){

   //  return n1==n2 || !areDisequal( n1, n2 );

@@ -1500,14 +1679,16 @@ bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) {
 //-------------------------------------------------- handling assertions / eqc

 

 void QuantConflictFind::assertNode( Node q ) {

-  Trace("qcf-proc") << "QCF : assertQuantifier : ";

-  debugPrintQuant("qcf-proc", q);

-  Trace("qcf-proc") << std::endl;

-  d_qassert.push_back( q );

-  //set the eqRegistries that this depends on to true

-  //for( std::map< EqRegistry *, bool >::iterator it = d_qinfo[q].d_rel_eqr.begin(); it != d_qinfo[q].d_rel_eqr.end(); ++it ){

-  //  it->first->d_active.set( true );

-  //}

+  if( !TermDb::isRewriteRule( q ) ){

+    Trace("qcf-proc") << "QCF : assertQuantifier : ";

+    debugPrintQuant("qcf-proc", q);

+    Trace("qcf-proc") << std::endl;

+    d_qassert.push_back( q );

+    //set the eqRegistries that this depends on to true

+    //for( std::map< EqRegistry *, bool >::iterator it = d_qinfo[q].d_rel_eqr.begin(); it != d_qinfo[q].d_rel_eqr.end(); ++it ){

+    //  it->first->d_active.set( true );

+    //}

+  }

 }

 

 eq::EqualityEngine * QuantConflictFind::getEqualityEngine() {

@@ -1518,7 +1699,7 @@ bool QuantConflictFind::areEqual( Node n1, Node n2 ) {
   return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areEqual( n1,n2 );

 }

 bool QuantConflictFind::areDisequal( Node n1, Node n2 ) {

-  return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false );

+  return n1!=n2 && getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false );

 }

 Node QuantConflictFind::getRepresentative( Node n ) {

   if( getEqualityEngine()->hasTerm( n ) ){

@@ -1677,6 +1858,10 @@ void QuantConflictFind::assertDisequal( Node a, Node b ) {
 

 //-------------------------------------------------- check function

 

+void QuantConflictFind::reset_round( Theory::Effort level ) {

+  d_needs_computeRelEqr = true;

+}

+

 /** check */

 void QuantConflictFind::check( Theory::Effort level ) {

   Trace("qcf-check") << "QCF : check : " << level << std::endl;

@@ -1695,7 +1880,6 @@ void QuantConflictFind::check( Theory::Effort level ) {
         clSet = double(clock())/double(CLOCKS_PER_SEC);

         Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level << "---" << std::endl;

       }

-      Trace("qcf-check") << "Compute relevant equalities..." << std::endl;

       computeRelevantEqr();

 

       //determine order for quantified formulas

@@ -1728,17 +1912,8 @@ void QuantConflictFind::check( Theory::Effort level ) {
         Trace("qcf-debug") << std::endl;

         debugPrint("qcf-debug");

         Trace("qcf-debug") << std::endl;

-      }

-      short end_e;

-      if( options::qcfMode()==QCF_CONFLICT_ONLY ){

-        end_e = effort_conflict;

-      }else if( options::qcfMode()==QCF_PROP_EQ ){

-        end_e = effort_prop_eq;

-      }else if( options::qcfMode()==QCF_PARTIAL ){

-        end_e = effort_partial;

-      }else{

-        end_e = effort_mc;

-      }

+      }
+      short end_e = getMaxQcfEffort();

       for( short e = effort_conflict; e<=end_e; e++ ){

         d_effort = e;

         Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl;

@@ -1748,79 +1923,106 @@ void QuantConflictFind::check( Theory::Effort level ) {
 

           Assert( d_qinfo.find( q )!=d_qinfo.end() );

           if( qi->d_mg->isValid() ){

-            if( qi->isPartial()==(e==effort_partial) ){

-              Trace("qcf-check") << "Check quantified formula ";

-              debugPrintQuant("qcf-check", q);

-              Trace("qcf-check") << " : " << q << "..." << std::endl;

-

-              Trace("qcf-check-debug") << "Reset round..." << std::endl;

-              qi->reset_round( this );

-              //try to make a matches making the body false

-              Trace("qcf-check-debug") << "Reset..." << std::endl;

-              qi->d_mg->reset( this, false, qi );

-              Trace("qcf-check-debug") << "Get next match..." << std::endl;

-              while( qi->d_mg->getNextMatch( this, qi ) ){

-

-                Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl;

-                qi->debugPrintMatch("qcf-check");

-                Trace("qcf-check") << std::endl;

-

-                if( !qi->isMatchSpurious( this ) ){

-                  std::vector< int > assigned;

-                  if( qi->completeMatch( this, assigned ) ){

-                    std::vector< Node > terms;

-                    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){

-                      //Node cv = qi->getCurrentValue( qi->d_match[i] );

-                      int repVar = qi->getCurrentRepVar( i );

-                      Node cv;

-                      //std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar );

-                      if( !qi->d_match_term[repVar].isNull() ){

-                        cv = qi->d_match_term[repVar];

-                      }else{

-                        cv = qi->d_match[repVar];

+            Trace("qcf-check") << "Check quantified formula ";

+            debugPrintQuant("qcf-check", q);

+            Trace("qcf-check") << " : " << q << "..." << std::endl;

+

+            Trace("qcf-check-debug") << "Reset round..." << std::endl;

+            qi->reset_round( this );

+            //try to make a matches making the body false

+            Trace("qcf-check-debug") << "Get next match..." << std::endl;

+            while( qi->d_mg->getNextMatch( this, qi ) ){

+              Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl;

+              qi->debugPrintMatch("qcf-check");

+              Trace("qcf-check") << std::endl;

+              std::vector< int > assigned;

+              if( !qi->isMatchSpurious( this ) ){

+                if( qi->completeMatch( this, assigned ) ){

+                  /*

+                  if( options::qcfExp() && d_effort==effort_conflict ){

+                    std::vector< Node > exp;

+                    if( qi->d_mg->getExplanation( this, qi, exp ) ){

+                      Trace("qcf-check-exp") << "Base explanation is : " << std::endl;

+                      for( unsigned c=0; c<exp.size(); c++ ){

+                        Trace("qcf-check-exp") << "  " << exp[c] << std::endl;

                       }

-                      Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << qi->d_match[i] << std::endl;

-                      terms.push_back( cv );

-                    }

-                    if( Debug.isOn("qcf-check-inst") ){

-                      //if( e==effort_conflict ){

-                      Node inst = d_quantEngine->getInstantiation( q, terms );

-                      Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;

-                      Assert( evaluate( inst )!=1 );

-                      Assert( evaluate( inst )==-1 || e>effort_conflict );

-                      //}

-                    }

-                    if( d_quantEngine->addInstantiation( q, terms ) ){

-                      Trace("qcf-check") << "   ... Added instantiation" << std::endl;

-                      ++addedLemmas;

-                      if( e==effort_conflict ){

-                        d_quant_order.insert( d_quant_order.begin(), q );

-                        d_conflict.set( true );

-                        ++(d_statistics.d_conflict_inst);

-                        break;

-                      }else if( e==effort_prop_eq ){

-                        ++(d_statistics.d_prop_inst);

-                      }else if( e==effort_partial ){

-                        ++(d_statistics.d_partial_inst);

+                      std::vector< TNode > c_exp;

+                      eq::EqualityEngine* ee = ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getEqualityEngine() ;

+                      for( unsigned c=0; c<exp.size(); c++ ){

+                        bool pol = exp[c].getKind()!=NOT;

+                        TNode lit = pol ? exp[c] : exp[c][0];

+                        Trace("qcf-check-exp") << "Explain " << lit << ", polarity " << pol << std::endl;

+                        if( lit.getKind()==EQUAL ){

+                          if( !pol && !ee->areDisequal( lit[0], lit[1], true ) ){

+                            exit( 98 );

+                          }else if( pol && !ee->areEqual( lit[0], lit[1] ) ){

+                            exit( 99 );

+                          }

+                          ee->explainEquality( lit[0], lit[1], pol, c_exp );

+                        }else{

+                          if( !ee->areEqual( lit, pol ? d_true : d_false ) ){

+                            exit( pol ? 96 : 97 );

+                          }

+                          ee->explainPredicate( lit, pol, c_exp );

+                        }

+                      }

+                      std::vector< Node > c_lem;

+                      Trace("qcf-check-exp") << "Actual explanation is : " << std::endl;

+                      for( unsigned c=0; c<c_exp.size(); c++ ){

+                        Trace("qcf-check-exp") << "  " << c_exp[c] << std::endl;

+                        Node ccc = c_exp[c].negate();

+                        if( std::find( c_lem.begin(), c_lem.end(), ccc )==c_lem.end() ){

+                          c_lem.push_back( ccc );

+                        }

                       }

-                    }else{

-                      Trace("qcf-check") << "   ... Failed to add instantiation" << std::endl;

-                      //Assert( false );

+

+                      c_lem.push_back( q.negate() );

+                      Node conf = NodeManager::currentNM()->mkNode( OR, c_lem );

+                      Trace("qcf-conflict") << "QCF conflict : " << conf << std::endl;

+                      d_quantEngine->addLemma( conf, false );

+                      d_conflict.set( true );

+                      ++(d_statistics.d_conflict_inst);

+                      ++addedLemmas;

+                      break;

                     }

-                    //clean up assigned

-                    for( unsigned i=0; i<assigned.size(); i++ ){

-                      qi->d_match[ assigned[i] ] = TNode::null();

+                  }

+                  */

+                  std::vector< Node > terms;

+                  qi->getMatch( terms );

+                  if( Debug.isOn("qcf-check-inst") ){

+                    //if( e==effort_conflict ){

+                    Node inst = d_quantEngine->getInstantiation( q, terms );

+                    Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;

+                    Assert( evaluate( inst )!=1 );

+                    Assert( evaluate( inst )==-1 || e>effort_conflict );

+                    //}

+                  }

+                  if( d_quantEngine->addInstantiation( q, terms ) ){

+                    Trace("qcf-check") << "   ... Added instantiation" << std::endl;

+                    ++addedLemmas;

+                    if( e==effort_conflict ){

+                      d_quant_order.insert( d_quant_order.begin(), q );

+                      d_conflict.set( true );

+                      ++(d_statistics.d_conflict_inst);

+                      break;

+                    }else if( e==effort_prop_eq ){

+                      ++(d_statistics.d_prop_inst);

                     }

                   }else{

-                    Trace("qcf-check") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;

+                    Trace("qcf-check") << "   ... Failed to add instantiation" << std::endl;

+                    //Assert( false );

                   }

+                  //clean up assigned

+                  qi->revertMatch( assigned );

                 }else{

-                  Trace("qcf-check") << "   ... Spurious instantiation (does not meet variable constraints)" << std::endl;

+                  Trace("qcf-check") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;

                 }

-              }

-              if( d_conflict ){

-                break;

-              }

+              }else{

+                Trace("qcf-check") << "   ... Spurious instantiation (match is inconsistent)" << std::endl;

+              }
+            }

+            if( d_conflict ){

+              break;

             }

           }

         }

@@ -1845,7 +2047,7 @@ void QuantConflictFind::check( Theory::Effort level ) {
 

 bool QuantConflictFind::needsCheck( Theory::Effort level ) {

   d_performCheck = false;

-  if( !d_conflict ){

+  if( options::quantConflictFind() && !d_conflict ){

     if( level==Theory::EFFORT_LAST_CALL ){

       d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL;

     }else if( level==Theory::EFFORT_FULL ){

@@ -1858,131 +2060,133 @@ bool QuantConflictFind::needsCheck( Theory::Effort level ) {
 }

 

 void QuantConflictFind::computeRelevantEqr() {

-  d_uf_terms.clear();

-  d_eqc_uf_terms.clear();

-  d_eqcs.clear();

-  d_model_basis.clear();

-  d_arg_reps.clear();

-  //double clSet = 0;

-  //if( Trace.isOn("qcf-opt") ){

-  //  clSet = double(clock())/double(CLOCKS_PER_SEC);

-  //}

-

-  //long nTermst = 0;

-  //long nTerms = 0;

-  //long nEqc = 0;

+  if( d_needs_computeRelEqr ){

+    d_needs_computeRelEqr = false;

+    Trace("qcf-check") << "Compute relevant equalities..." << std::endl;

+    d_uf_terms.clear();

+    d_eqc_uf_terms.clear();

+    d_eqcs.clear();

+    d_model_basis.clear();

+    d_arg_reps.clear();

+    //double clSet = 0;

+    //if( Trace.isOn("qcf-opt") ){

+    //  clSet = double(clock())/double(CLOCKS_PER_SEC);

+    //}

 

-  //which nodes are irrelevant for disequality matches

-  std::map< TNode, bool > irrelevant_dnode;

-  //now, store matches

-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );

-  while( !eqcs_i.isFinished() ){

-    //nEqc++;

-    Node r = (*eqcs_i);

-    TypeNode rtn = r.getType();

-    if( options::qcfMode()==QCF_MC ){

-      std::map< TypeNode, std::vector< TNode > >::iterator itt = d_eqcs.find( rtn );

-      if( itt==d_eqcs.end() ){

-        Node mb = getQuantifiersEngine()->getTermDatabase()->getModelBasisTerm( rtn );

-        if( !getEqualityEngine()->hasTerm( mb ) ){

-          Trace("qcf-warn") << "WARNING: Model basis term does not exist!" << std::endl;

-          Assert( false );

-        }

-        Node mbr = getRepresentative( mb );

-        if( mbr!=r ){

-          d_eqcs[rtn].push_back( mbr );

+    //long nTermst = 0;

+    //long nTerms = 0;

+    //long nEqc = 0;

+

+    //which nodes are irrelevant for disequality matches

+    std::map< TNode, bool > irrelevant_dnode;

+    //now, store matches

+    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );

+    while( !eqcs_i.isFinished() ){

+      //nEqc++;

+      Node r = (*eqcs_i);

+      TypeNode rtn = r.getType();

+      if( options::qcfMode()==QCF_MC ){

+        std::map< TypeNode, std::vector< TNode > >::iterator itt = d_eqcs.find( rtn );

+        if( itt==d_eqcs.end() ){

+          Node mb = getQuantifiersEngine()->getTermDatabase()->getModelBasisTerm( rtn );

+          if( !getEqualityEngine()->hasTerm( mb ) ){

+            Trace("qcf-warn") << "WARNING: Model basis term does not exist!" << std::endl;

+            Assert( false );

+          }

+          Node mbr = getRepresentative( mb );

+          if( mbr!=r ){

+            d_eqcs[rtn].push_back( mbr );

+          }

+          d_eqcs[rtn].push_back( r );

+          d_model_basis[rtn] = mb;

+        }else{

+          itt->second.push_back( r );

         }

-        d_eqcs[rtn].push_back( r );

-        d_model_basis[rtn] = mb;

       }else{

-        itt->second.push_back( r );

-      }

-    }else{

-      d_eqcs[rtn].push_back( r );

-    }

-    /*

-    eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );

-    while( !eqc_i.isFinished() ){

-      TNode n = (*eqc_i);

-      if( n.hasBoundVar() ){

-        std::cout << "BAD TERM IN DB : " << n << std::endl;

-        exit( 199 );

-      }

-      ++eqc_i;

-    }

-    */

+        d_eqcs[rtn].push_back( r );

+      }
+      eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );

+      while( !eqc_i.isFinished() ){

+        TNode n = (*eqc_i);

+        if( n.hasBoundVar() ){

+          std::cout << "BAD TERM IN DB : " << n << std::endl;

+          exit( 199 );

+        }

+        ++eqc_i;

+      }
 

-    //if( r.getType().isInteger() ){

-    //  Trace("qcf-mv") << "Model value for eqc(" << r << ") : " << d_quantEngine->getValuation().getModelValue( r ) << std::endl;

-    //}

-    //EqcInfo * eqcir = getEqcInfo( r, false );

-    //get relevant nodes that we are disequal from

-    /*

-    std::vector< Node > deqc;

-    if( eqcir ){

-      for( NodeBoolMap::iterator it = eqcir->d_diseq.begin(); it != eqcir->d_diseq.end(); ++it ){

-        if( (*it).second ){

-          //Node rd = (*it).first;

-          //if( rd!=getRepresentative( rd ) ){

-          //  std::cout << "Bad rep!" << std::endl;

-          //  exit( 0 );

-          //}

-          deqc.push_back( (*it).first );

+      //if( r.getType().isInteger() ){

+      //  Trace("qcf-mv") << "Model value for eqc(" << r << ") : " << d_quantEngine->getValuation().getModelValue( r ) << std::endl;

+      //}

+      //EqcInfo * eqcir = getEqcInfo( r, false );

+      //get relevant nodes that we are disequal from

+      /*

+      std::vector< Node > deqc;

+      if( eqcir ){

+        for( NodeBoolMap::iterator it = eqcir->d_diseq.begin(); it != eqcir->d_diseq.end(); ++it ){

+          if( (*it).second ){

+            //Node rd = (*it).first;

+            //if( rd!=getRepresentative( rd ) ){

+            //  std::cout << "Bad rep!" << std::endl;

+            //  exit( 0 );

+            //}

+            deqc.push_back( (*it).first );

+          }

         }

       }

-    }

-    */

-    //process disequalities

-    /*

-    eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );

-    while( !eqc_i.isFinished() ){

-      TNode n = (*eqc_i);

-      if( n.getKind()!=EQUAL ){

-        nTermst++;

-        //node_to_rep[n] = r;

-        //if( n.getNumChildren()>0 ){

-        //  if( n.getKind()!=APPLY_UF ){

-        //    std::cout << n.getKind() << " " << n.getOperator() << " " << n << std::endl;

-        //  }

-        //}

-        if( !n.hasBoundVar() ){    //temporary

-

-          bool isRedundant;

-          std::map< TNode, std::vector< TNode > >::iterator it_na;

-          TNode fn;

-          if( MatchGen::isHandledUfTerm( n ) ){

-            Node f = MatchGen::getOperator( this, n );

-            computeArgReps( n );

-            it_na = d_arg_reps.find( n );

-            Assert( it_na!=d_arg_reps.end() );

-            Node nadd = d_eqc_uf_terms[f].d_children[r].addTerm( n, d_arg_reps[n] );

-            isRedundant = (nadd!=n);

-            d_uf_terms[f].addTerm( n, d_arg_reps[n] );

+      */

+      //process disequalities

+      /*

+      eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );

+      while( !eqc_i.isFinished() ){

+        TNode n = (*eqc_i);

+        if( n.getKind()!=EQUAL ){

+          nTermst++;

+          //node_to_rep[n] = r;

+          //if( n.getNumChildren()>0 ){

+          //  if( n.getKind()!=APPLY_UF ){

+          //    std::cout << n.getKind() << " " << n.getOperator() << " " << n << std::endl;

+          //  }

+          //}

+          if( !quantifiers::TermDb::hasBoundVarAttr( n ) ){    //temporary

+

+            bool isRedundant;

+            std::map< TNode, std::vector< TNode > >::iterator it_na;

+            TNode fn;

+            if( MatchGen::isHandledUfTerm( n ) ){

+              Node f = MatchGen::getOperator( this, n );

+              computeArgReps( n );

+              it_na = d_arg_reps.find( n );

+              Assert( it_na!=d_arg_reps.end() );

+              Node nadd = d_eqc_uf_terms[f].d_children[r].addTerm( n, d_arg_reps[n] );

+              isRedundant = (nadd!=n);

+              d_uf_terms[f].addTerm( n, d_arg_reps[n] );

+            }else{

+              isRedundant = false;

+            }

+            nTerms += isRedundant ? 0 : 1;

           }else{

-            isRedundant = false;

-          }

-          nTerms += isRedundant ? 0 : 1;

-        }else{

-          if( Debug.isOn("qcf-nground") ){

-            Debug("qcf-nground") << "Non-ground term in eqc : " << n << std::endl;

-            Assert( false );

+            if( Debug.isOn("qcf-nground") ){

+              Debug("qcf-nground") << "Non-ground term in eqc : " << n << std::endl;

+              Assert( false );

+            }

           }

         }

+        ++eqc_i;

       }

-      ++eqc_i;

+      */

+      ++eqcs_i;

+    }

+    /*

+    if( Trace.isOn("qcf-opt") ){

+      double clSet2 = double(clock())/double(CLOCKS_PER_SEC);

+      Trace("qcf-opt") << "Compute rel eqc : " << std::endl;

+      Trace("qcf-opt") << "   " << nEqc << " equivalence classes. " << std::endl;

+      Trace("qcf-opt") << "   " << nTerms << " / " << nTermst << " terms." << std::endl;

+      Trace("qcf-opt") << "   Time : " << (clSet2-clSet) << std::endl;

     }

     */

-    ++eqcs_i;

   }

-  /*

-  if( Trace.isOn("qcf-opt") ){

-    double clSet2 = double(clock())/double(CLOCKS_PER_SEC);

-    Trace("qcf-opt") << "Compute rel eqc : " << std::endl;

-    Trace("qcf-opt") << "   " << nEqc << " equivalence classes. " << std::endl;

-    Trace("qcf-opt") << "   " << nTerms << " / " << nTermst << " terms." << std::endl;

-    Trace("qcf-opt") << "   Time : " << (clSet2-clSet) << std::endl;

-  }

-  */

 }

 

 void QuantConflictFind::computeArgReps( TNode n ) {

@@ -2079,20 +2283,17 @@ void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, boo
 QuantConflictFind::Statistics::Statistics():

   d_inst_rounds("QuantConflictFind::Inst_Rounds", 0),

   d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 ),

-  d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ),

-  d_partial_inst("QuantConflictFind::Instantiations_Partial", 0 )

+  d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 )

 {

   StatisticsRegistry::registerStat(&d_inst_rounds);

   StatisticsRegistry::registerStat(&d_conflict_inst);

   StatisticsRegistry::registerStat(&d_prop_inst);

-  StatisticsRegistry::registerStat(&d_partial_inst);

 }

 

 QuantConflictFind::Statistics::~Statistics(){

   StatisticsRegistry::unregisterStat(&d_inst_rounds);

   StatisticsRegistry::unregisterStat(&d_conflict_inst);

   StatisticsRegistry::unregisterStat(&d_prop_inst);

-  StatisticsRegistry::unregisterStat(&d_partial_inst);

 }

 

 }

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 944cfa584..090af8143 100755
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -83,13 +83,15 @@ public:
     typ_formula,

     typ_var,

     typ_ite_var,

-    typ_top,

+    typ_bool_var,

   };

   void debugPrintType( const char * c, short typ, bool isTrace = false );

 public:

   MatchGen() : d_type( typ_invalid ){}

   MatchGen( QuantInfo * qi, Node n, bool isVar = false, bool beneathQuant = false );

   bool d_tgt;

+  bool d_tgt_orig;

+  bool d_wasSet;

   Node d_n;

   std::vector< MatchGen > d_children;

   short d_type;

@@ -97,21 +99,32 @@ public:
   void reset_round( QuantConflictFind * p );

   void reset( QuantConflictFind * p, bool tgt, QuantInfo * qi );

   bool getNextMatch( QuantConflictFind * p, QuantInfo * qi );

+  bool getExplanation( QuantConflictFind * p, QuantInfo * qi, std::vector< Node >& exp );

+  Node getExplanationTerm( QuantConflictFind * p, QuantInfo * qi, Node t, std::vector< Node >& exp );

   bool isValid() { return d_type!=typ_invalid; }

   void setInvalid();

 

   // is this term treated as UF application?

+  static bool isHandledBoolConnective( TNode n );

   static bool isHandledUfTerm( TNode n );

   static Node getOperator( QuantConflictFind * p, Node n );

+  //can this node be handled by the algorithm

+  static bool isHandled( TNode n );

 };

 

 //info for quantifiers

 class QuantInfo {

 private:

   void registerNode( Node n, bool hasPol, bool pol, bool beneathQuant = false );

-  void flatten( Node n, bool beneathQuant );

+  void flatten( Node n, bool beneathQuant );
+private: //for completing match

+  std::vector< int > d_unassigned;

+  std::vector< TypeNode > d_unassigned_tn;

+  int d_unassigned_nvar;

+  int d_una_index;

+  std::vector< int > d_una_eqc_count;

 public:

-  QuantInfo() : d_mg( NULL ), d_isPartial( false ) {}

+  QuantInfo() : d_mg( NULL ) {}

   std::vector< TNode > d_vars;

   std::map< TNode, int > d_var_num;

   std::map< TNode, bool > d_nbeneathQuant;

@@ -120,6 +133,7 @@ public:
   bool isVar( TNode v ) { return d_var_num.find( v )!=d_var_num.end(); }

   int getNumVars() { return (int)d_vars.size(); }

   TNode getVar( int i ) { return d_vars[i]; }

+

   MatchGen * d_mg;

   Node d_q;

   std::map< int, MatchGen * > d_var_mg;

@@ -133,20 +147,18 @@ public:
   std::map< int, std::map< TNode, int > > d_curr_var_deq;

   int getCurrentRepVar( int v );

   TNode getCurrentValue( TNode n );

+  TNode getCurrentExpValue( TNode n );

   bool getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq = false );

   int addConstraint( QuantConflictFind * p, int v, TNode n, bool polarity );

   int addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove );

   bool setMatch( QuantConflictFind * p, int v, TNode n );

   bool isMatchSpurious( QuantConflictFind * p );

-  bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned );

+  bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue = false );

+  void revertMatch( std::vector< int >& assigned );

   void debugPrintMatch( const char * c );

-  bool isConstrainedVar( int v );

-public:

-  // is partial

-  bool d_isPartial;

-  //the variables that this quantified formula has not beneath nested quantifiers

-  std::map< TNode, bool > d_has_var;

-  bool isPartial() { return d_isPartial; }

+  bool isConstrainedVar( int v );
+public:
+  void getMatch( std::vector< Node >& terms );

 };

 

 class QuantConflictFind : public QuantifiersModule

@@ -218,6 +230,8 @@ public:
     effort_mc,

   };

   short d_effort;

+  void setEffort( int e ) { d_effort = e; }

+  static short getMaxQcfEffort();

   bool areMatchEqual( TNode n1, TNode n2 );

   bool areMatchDisequal( TNode n1, TNode n2 );

 public:

@@ -233,11 +247,15 @@ public:
   void merge( Node a, Node b );

   /** assert disequal */

   void assertDisequal( Node a, Node b );

+  /** reset round */

+  void reset_round( Theory::Effort level );

   /** check */

   void check( Theory::Effort level );

   /** needs check */

   bool needsCheck( Theory::Effort level );

 private:

+  bool d_needs_computeRelEqr;

+public:

   void computeRelevantEqr();

 private:

   void debugPrint( const char * c );

@@ -253,7 +271,6 @@ public:
     IntStat d_inst_rounds;

     IntStat d_conflict_inst;

     IntStat d_prop_inst;

-    IntStat d_partial_inst;

     Statistics();

     ~Statistics();

   };

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index ac847678d..db61b046f 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/options.h"
+#include "theory/quantifiers/term_database.h"
 
 using namespace std;
 using namespace CVC4;
@@ -90,19 +91,29 @@ void QuantifiersRewriter::addNodeToOrBuilder( Node n, NodeBuilder<>& t ){
   }
 }
 
-void QuantifiersRewriter::computeArgs( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ){
+void QuantifiersRewriter::computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n ){
   if( n.getKind()==BOUND_VARIABLE ){
-    if( std::find( args.begin(), args.end(), n )!=args.end() &&
-        std::find( activeArgs.begin(), activeArgs.end(), n )==activeArgs.end() ){
-      activeArgs.push_back( n );
+    if( std::find( args.begin(), args.end(), n )!=args.end() ){
+      activeMap[ n ] = true;
     }
   }else{
     for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      computeArgs( args, activeArgs, n[i] );
+      computeArgs( args, activeMap, n[i] );
     }
   }
 }
 
+void QuantifiersRewriter::computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ) {
+  std::map< Node, bool > activeMap;
+  computeArgs( args, activeMap, n );
+  for( unsigned i=0; i<args.size(); i++ ){
+    if( activeMap[args[i]] ){
+      activeArgs.push_back( args[i] );
+    }
+  }
+}
+
+
 bool QuantifiersRewriter::hasArg( std::vector< Node >& args, Node n ){
   if( std::find( args.begin(), args.end(), n )!=args.end() ){
     return true;
@@ -135,7 +146,6 @@ void QuantifiersRewriter::setNestedQuantifiers2( Node n, Node q, std::vector< No
   }
 }
 
-
 RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
   Trace("quantifiers-rewrite-debug") << "pre-rewriting " << in << " " << in.hasAttribute(NestedQuantAttribute()) << std::endl;
   if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){
@@ -164,9 +174,7 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
       }
       Node n = NodeManager::currentNM()->mkNode( in.getKind(), children );
       if( in!=n ){
-        if( in.hasAttribute(NestedQuantAttribute()) ){
-          setNestedQuantifiers( n, in.getAttribute(NestedQuantAttribute()) );
-        }
+        setAttributes( in, n );
         Trace("quantifiers-pre-rewrite") << "*** pre-rewrite " << in << std::endl;
         Trace("quantifiers-pre-rewrite") << " to " << std::endl;
         Trace("quantifiers-pre-rewrite") << n << std::endl;
@@ -178,8 +186,9 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
 }
 
 RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
-  Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << " " << in.hasAttribute(NestedQuantAttribute()) << std::endl;
-  if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){
+  Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << std::endl;
+  Trace("quantifiers-rewrite-debug") << "Attributes : " << in.hasAttribute(NestedQuantAttribute())  << std::endl;
+  if( !options::quantRewriteRules() || !TermDb::isRewriteRule( in ) ){
     RewriteStatus status = REWRITE_DONE;
     Node ret = in;
     //get the arguments
@@ -217,12 +226,13 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
     }
     //print if changed
     if( in!=ret ){
-      if( in.hasAttribute(NestedQuantAttribute()) ){
-        setNestedQuantifiers( ret, in.getAttribute(NestedQuantAttribute()) );
-      }
+      setAttributes( in, ret );
       Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl;
       Trace("quantifiers-rewrite") << " to " << std::endl;
       Trace("quantifiers-rewrite") << ret << std::endl;
+      Trace("quantifiers-rewrite-debug") << "Attributes : " << ret.hasAttribute(NestedQuantAttribute()) << std::endl;
+
+
     }
     return RewriteResponse( status, ret );
   }
@@ -409,6 +419,15 @@ Node QuantifiersRewriter::computeClause( Node n ){
   }
 }
 
+void QuantifiersRewriter::setAttributes( Node in, Node n ) {
+  if( in.hasAttribute(NestedQuantAttribute()) ){
+    setNestedQuantifiers( n, in.getAttribute(NestedQuantAttribute()) );
+  }
+  //if( in.hasAttribute(QRewriteRuleAttribute()) ){
+  //  n.setAttribute(QRewriteRuleAttribute(), in.getAttribute(QRewriteRuleAttribute()));
+  //}
+}
+
 Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ){
   if( isLiteral( n ) ){
     return n;
@@ -432,7 +451,7 @@ Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBui
       //compute the free variables
       Node nt = t;
       std::vector< Node > activeArgs;
-      computeArgs( args, activeArgs, nt );
+      computeArgVec( args, activeArgs, nt );
       std::vector< TypeNode > argTypes;
       for( int i=0; i<(int)activeArgs.size(); i++ ){
         argTypes.push_back( activeArgs[i].getType() );
@@ -581,7 +600,7 @@ Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >&
       //get variables contained in the literal
       Node n = body[i];
       std::vector<Node> lit_vars;
-      computeArgs( vars, lit_vars, n);
+      computeArgVec( vars, lit_vars, n);
       //collectVars( n, vars, lit_vars );
       if (lit_vars.empty()) {
         lits.push_back(n);
@@ -689,7 +708,7 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption ){
       n = computeElimSymbols( n );
     }else if( computeOption==COMPUTE_MINISCOPING ){
       //return directly
-      return computeMiniscoping( args, n, ipl, f.hasAttribute(NestedQuantAttribute()) );
+      return computeMiniscoping( f, args, n, ipl, f.hasAttribute(NestedQuantAttribute()) );
     }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
       return computeAggressiveMiniscoping( args, n, f.hasAttribute(NestedQuantAttribute()) );
     }else if( computeOption==COMPUTE_NNF ){
@@ -735,7 +754,7 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption ){
 
 Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node ipl ){
   std::vector< Node > activeArgs;
-  computeArgs( args, activeArgs, body );
+  computeArgVec( args, activeArgs, body );
   if( activeArgs.empty() ){
     return body;
   }else{
@@ -749,7 +768,7 @@ Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node i
   }
 }
 
-Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node body, Node ipl, bool isNested ){
+Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl, bool isNested ){
   //Notice() << "rewrite quant " << body << std::endl;
   if( body.getKind()==FORALL ){
     //combine arguments
@@ -763,21 +782,21 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo
     if( body.getKind()==NOT ){
       //push not downwards
       if( body[0].getKind()==NOT ){
-        return computeMiniscoping( args, body[0][0], ipl );
+        return computeMiniscoping( f, args, body[0][0], ipl );
       }else if( body[0].getKind()==AND ){
         if( doMiniscopingNoFreeVar() ){
           NodeBuilder<> t(kind::OR);
           for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
             t <<  ( body[0][i].getKind()==NOT ? body[0][i][0] : body[0][i].notNode() );
           }
-          return computeMiniscoping( args, t.constructNode(), ipl );
+          return computeMiniscoping( f, args, t.constructNode(), ipl );
         }
       }else if( body[0].getKind()==OR ){
         if( doMiniscopingAnd() ){
           NodeBuilder<> t(kind::AND);
           for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
             Node trm = body[0][i].negate();
-            t << computeMiniscoping( args, trm, ipl );
+            t << computeMiniscoping( f, args, trm, ipl );
           }
           return t.constructNode();
         }
@@ -787,7 +806,7 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo
         //break apart
         NodeBuilder<> t(kind::AND);
         for( int i=0; i<(int)body.getNumChildren(); i++ ){
-          t << computeMiniscoping( args, body[i], ipl );
+          t << computeMiniscoping( f, args, body[i], ipl );
         }
         Node retVal = t;
         return retVal;
@@ -815,7 +834,11 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo
       }
     }
   }
-  return mkForAll( args, body, ipl );
+  if( body==f[1] ){
+    return f;
+  }else{
+    return mkForAll( args, body, ipl );
+  }
 }
 
 Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& args, Node body, bool isNested ){
@@ -826,7 +849,7 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg
       Trace("ag-miniscope") << "compute aggressive miniscoping on " << body << std::endl;
       for( size_t i=0; i<body.getNumChildren(); i++ ){
         std::vector< Node > activeArgs;
-        computeArgs( args, activeArgs, body[i] );
+        computeArgVec( args, activeArgs, body[i] );
         for (unsigned j=0; j<activeArgs.size(); j++ ){
           varLits[activeArgs[j]].push_back( body[i] );
         }
@@ -964,3 +987,220 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption
     return false;
   }
 }
+
+
+
+
+Node QuantifiersRewriter::rewriteRewriteRule( Node r ) {
+  Kind rrkind = r[2].getKind();
+
+  //guards, pattern, body
+
+  //   Replace variables by Inst_* variable and tag the terms that contain them
+  std::vector<Node> vars;
+  vars.reserve(r[0].getNumChildren());
+  for( Node::const_iterator v = r[0].begin(); v != r[0].end(); ++v ){
+    vars.push_back(*v);
+  };
+
+  // Body/Remove_term/Guards/Triggers
+  Node body = r[2][1];
+  TNode new_terms = r[2][1];
+  std::vector<Node> guards;
+  std::vector<Node> pattern;
+  Node true_node = NodeManager::currentNM()->mkConst(true);
+  // shortcut
+  TNode head = r[2][0];
+  switch(rrkind){
+  case kind::RR_REWRITE:
+    // Equality
+    pattern.push_back( head );
+    if( head.getType().isBoolean() ){
+      body = head.iffNode(body);
+    }else{
+      body = head.eqNode(body);
+    }
+    break;
+  case kind::RR_REDUCTION:
+  case kind::RR_DEDUCTION:
+    // Add head to guards and pattern
+    switch(head.getKind()){
+    case kind::AND:
+      for( unsigned i = 0; i<head.getNumChildren(); i++ ){
+        guards.push_back(head[i]);
+        pattern.push_back(head[i]);
+      }
+      break;
+    default:
+      if( head!=true_node ){
+        guards.push_back(head);
+        pattern.push_back( head );
+      }
+      break;
+    }
+    break;
+  default:
+    Unreachable("RewriteRules can be of only three kinds");
+    break;
+  }
+  // Add the other guards
+  TNode g = r[1];
+  switch(g.getKind()){
+  case kind::AND:
+    for( unsigned i = 0; i<g.getNumChildren(); i++ ){
+      guards.push_back(g[i]);
+    }
+    break;
+  default:
+    if( g != true_node ){
+      guards.push_back( g );
+    }
+    break;
+  }
+  // Add the other triggers
+  if( r[2].getNumChildren() >= 3 ){
+    for( unsigned i=0; i<r[2][2][0].getNumChildren(); i++ ) {
+      pattern.push_back( r[2][2][0][i] );
+    }
+  }
+
+  Trace("rr-rewrite") << "Rule is " << r << std::endl;
+  Trace("rr-rewrite") << "Head is " << head << std::endl;
+  Trace("rr-rewrite") << "Patterns are ";
+  for( unsigned i=0; i<pattern.size(); i++ ){
+    Trace("rr-rewrite") << pattern[i] << " ";
+  }
+  Trace("rr-rewrite") << std::endl;
+
+  NodeBuilder<> forallB(kind::FORALL);
+  forallB << r[0];
+  Node gg = guards.size()==0 ? true_node : ( guards.size()==1 ? guards[0] : NodeManager::currentNM()->mkNode( AND, guards ) );
+  gg = NodeManager::currentNM()->mkNode( OR, gg.negate(), body );
+  gg = Rewriter::rewrite( gg );
+  forallB << gg;
+  NodeBuilder<> patternB(kind::INST_PATTERN);
+  patternB.append(pattern);
+  NodeBuilder<> patternListB(kind::INST_PATTERN_LIST);
+  //the entire rewrite rule is the first pattern
+  if( options::quantRewriteRules() ){
+    patternListB << NodeManager::currentNM()->mkNode( INST_PATTERN, r );
+  }
+  patternListB << static_cast<Node>(patternB);
+  forallB << static_cast<Node>(patternListB);
+  Node rn = (Node) forallB;
+
+  return rn;
+}
+
+struct ContainsQuantAttributeId {};
+typedef expr::Attribute<ContainsQuantAttributeId, uint64_t> ContainsQuantAttribute;
+
+// check if the given node contains a universal quantifier
+bool QuantifiersRewriter::containsQuantifiers(Node n) {
+  if( n.hasAttribute(ContainsQuantAttribute()) ){
+    return n.getAttribute(ContainsQuantAttribute())==1;
+  } else if(n.getKind() == kind::FORALL) {
+    return true;
+  } else {
+    bool cq = false;
+    for( unsigned i = 0; i < n.getNumChildren(); ++i ){
+      if( containsQuantifiers(n[i]) ){
+        cq = true;
+        break;
+      }
+    }
+    ContainsQuantAttribute cqa;
+    n.setAttribute(cqa, cq ? 1 : 0);
+    return cq;
+  }
+}
+
+Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< Node >& fvs ){
+  Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << endl;
+  if( n.getKind()==kind::NOT ){
+    Node nn = preSkolemizeQuantifiers( n[0], !polarity, fvs );
+    return nn.negate();
+  }else if( n.getKind()==kind::FORALL ){
+    if( polarity ){
+      vector< Node > children;
+      children.push_back( n[0] );
+      //add children to current scope
+      vector< Node > fvss;
+      fvss.insert( fvss.begin(), fvs.begin(), fvs.end() );
+      for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
+        fvss.push_back( n[0][i] );
+      }
+      //process body
+      children.push_back( preSkolemizeQuantifiers( n[1], polarity, fvss ) );
+      if( n.getNumChildren()==3 ){
+        children.push_back( n[2] );
+      }
+      //return processed quantifier
+      return NodeManager::currentNM()->mkNode( kind::FORALL, children );
+    }else{
+      //process body
+      Node nn = preSkolemizeQuantifiers( n[1], polarity, fvs );
+      //now, substitute skolems for the variables
+      vector< TypeNode > argTypes;
+      for( int i=0; i<(int)fvs.size(); i++ ){
+        argTypes.push_back( fvs[i].getType() );
+      }
+      //calculate the variables and substitution
+      vector< Node > vars;
+      vector< Node > subs;
+      for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
+        vars.push_back( n[0][i] );
+      }
+      for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
+        //make the new function symbol
+        if( argTypes.empty() ){
+          Node s = NodeManager::currentNM()->mkSkolem( "sk_$$", n[0][i].getType(), "created during pre-skolemization" );
+          subs.push_back( s );
+        }else{
+          TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, n[0][i].getType() );
+          Node op = NodeManager::currentNM()->mkSkolem( "skop_$$", typ, "op created during pre-skolemization" );
+          //DOTHIS: set attribute on op, marking that it should not be selected as trigger
+          vector< Node > funcArgs;
+          funcArgs.push_back( op );
+          funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() );
+          subs.push_back( NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs ) );
+        }
+      }
+      //apply substitution
+      nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+      return nn;
+    }
+  }else{
+    //check if it contains a quantifier as a subterm
+    //if so, we will write this node
+    if( containsQuantifiers( n ) ){
+      if( n.getType().isBoolean() ){
+        if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){
+          Node nn;
+          //must remove structure
+          if( n.getKind()==kind::ITE ){
+            nn = NodeManager::currentNM()->mkNode( kind::AND,
+                   NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ),
+                   NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) );
+          }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){
+            nn = NodeManager::currentNM()->mkNode( kind::AND,
+                   NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ),
+                   NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) );
+          }else if( n.getKind()==kind::IMPLIES ){
+            nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] );
+          }
+          return preSkolemizeQuantifiers( nn, polarity, fvs );
+        }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){
+          vector< Node > children;
+          for( int i=0; i<(int)n.getNumChildren(); i++ ){
+            children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvs ) );
+          }
+          return NodeManager::currentNM()->mkNode( n.getKind(), children );
+        }else{
+          //must pull ite's
+        }
+      }
+    }
+    return n;
+  }
+}
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index e97d84701..4cbdb0cd1 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -38,14 +38,16 @@ public:
 private:
   static void addNodeToOrBuilder( Node n, NodeBuilder<>& t );
   static Node mkForAll( std::vector< Node >& args, Node body, Node ipl );
-  static void computeArgs( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n );
+  static void computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n );
+  static void computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n );
   static bool hasArg( std::vector< Node >& args, Node n );
   static void setNestedQuantifiers( Node n, Node q );
   static void setNestedQuantifiers2( Node n, Node q, std::vector< Node >& processed );
   static Node computeClause( Node n );
+  static void setAttributes( Node in, Node n );
 private:
   static Node computeElimSymbols( Node body );
-  static Node computeMiniscoping( std::vector< Node >& args, Node body, Node ipl, bool isNested = false );
+  static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl, bool isNested = false );
   static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body, bool isNested = false );
   static Node computeNNF( Node body );
   static Node computeSimpleIteLift( Node body );
@@ -79,6 +81,10 @@ private:
   static bool doMiniscopingAnd();
   static bool doOperation( Node f, bool isNested, int computeOption );
 public:
+  static Node rewriteRewriteRule( Node r );
+  static bool containsQuantifiers(Node n);
+  static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector<Node>& fvs);
+public:
   //static Node rewriteQuants( Node n, bool isNested = false );
   //static Node rewriteQuant( Node n, bool isNested = false );
 };/* class QuantifiersRewriter */
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 952f3409a..20ab4e55f 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -118,6 +118,7 @@ void RelevantDomain::compute(){
           for( unsigned j=0; j<n.getNumChildren(); j++ ){
             RDomain * rf = getRDomain( op, j );
             rf->addTerm( n[j] );
+            Trace("rel-dom-debug") << "...add ground term " << n[j] << " to rel dom " << op << "[" << j << "]" << std::endl;
           }
         }
       }
@@ -188,6 +189,7 @@ void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) {
     }else if( varCount==1 ){
       int oCh = varCh==0 ? 1 : 0;
       bool ng = d_qe->getTermDatabase()->hasInstConstAttr( n[oCh] );
+      Trace("rel-dom-debug") << "...add term " << n[oCh] << ", is ground = " << (!ng) << std::endl;
       //the negative occurrence adds the term to the domain
       if( !hasPol || !pol ){
         rds[varCh]->addTerm( n[oCh], ng );
@@ -219,6 +221,7 @@ void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) {
       rq->merge( rf );
     }
   }else if( !d_qe->getTermDatabase()->hasInstConstAttr( n ) ){
+    Trace("rel-dom-debug") << "...add ground term to rel dom " << n << std::endl;
     //term to add
     rf->addTerm( n );
   }
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 81de1e11d..59ba40ca7 100644
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -21,6 +21,7 @@
 #include "theory/quantifiers/options.h"
 #include "theory/quantifiers/inst_match_generator.h"
 #include "theory/theory_engine.h"
+#include "theory/quantifiers/term_database.h"
 
 using namespace CVC4;
 using namespace std;
@@ -37,14 +38,15 @@ struct PrioritySort {
 
 
 RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule(qe) {
-
+  d_true = NodeManager::currentNM()->mkConst( true );
 }
 
 double RewriteEngine::getPriority( Node f ) {
-  Node rr = f.getAttribute(QRewriteRuleAttribute());
+  Node rr = TermDb::getRewriteRule( f );
   Node rrr = rr[2];
   Trace("rr-priority") << "Get priority : " << rrr << " " << rrr.getKind() << std::endl;
   bool deterministic = rrr[1].getKind()!=OR;
+
   if( rrr.getKind()==RR_REWRITE ){
     return deterministic ? 0.0 : 3.0;
   }else if( rrr.getKind()==RR_DEDUCTION ){
@@ -54,26 +56,31 @@ double RewriteEngine::getPriority( Node f ) {
   }else{
     return 6.0;
   }
+
+  //return deterministic ? 0.0 : 1.0;
 }
 
 void RewriteEngine::check( Theory::Effort e ) {
-  if( e==Theory::EFFORT_LAST_CALL ){
-    if( !d_quantEngine->getModel()->isModelSet() ){
-      d_quantEngine->getTheoryEngine()->getModelBuilder()->buildModel( d_quantEngine->getModel(), true );
-    }
-    if( d_true.isNull() ){
-      d_true = NodeManager::currentNM()->mkConst( true );
-    }
-    std::vector< Node > priority_order;
-    PrioritySort ps;
-    std::vector< int > indicies;
-    for( int i=0; i<(int)d_rr_quant.size(); i++ ){
-      ps.d_priority.push_back( getPriority( d_rr_quant[i] ) );
-      indicies.push_back( i );
-    }
-    std::sort( indicies.begin(), indicies.end(), ps );
-    for( unsigned i=0; i<indicies.size(); i++ ){
-      priority_order.push_back( d_rr_quant[indicies[i]] );
+  if( e==Theory::EFFORT_FULL ){
+    Trace("rewrite-engine") << "---Rewrite Engine Round, effort = " << e << "---" << std::endl;
+    //if( e==Theory::EFFORT_LAST_CALL ){
+    //  if( !d_quantEngine->getModel()->isModelSet() ){
+    //    d_quantEngine->getTheoryEngine()->getModelBuilder()->buildModel( d_quantEngine->getModel(), true );
+    //  }
+    //}
+    if( d_needsSort ){
+      d_priority_order.clear();
+      PrioritySort ps;
+      std::vector< int > indicies;
+      for( int i=0; i<(int)d_rr_quant.size(); i++ ){
+        ps.d_priority.push_back( getPriority( d_rr_quant[i] ) );
+        indicies.push_back( i );
+      }
+      std::sort( indicies.begin(), indicies.end(), ps );
+      for( unsigned i=0; i<indicies.size(); i++ ){
+        d_priority_order.push_back( d_rr_quant[indicies[i]] );
+      }
+      d_needsSort = false;
     }
 
     //apply rewrite rules
@@ -81,16 +88,17 @@ void RewriteEngine::check( Theory::Effort e ) {
     //per priority level
     int index = 0;
     bool success = true;
-    while( success && index<(int)priority_order.size() ) {
-      addedLemmas += checkRewriteRule( priority_order[index] );
+    while( success && index<(int)d_priority_order.size() ) {
+      addedLemmas += checkRewriteRule( d_priority_order[index], e );
       index++;
-      if( index<(int)priority_order.size() ){
-        success = addedLemmas==0 || getPriority( priority_order[index] )==getPriority( priority_order[index-1] );
+      if( index<(int)d_priority_order.size() ){
+        success = addedLemmas==0 || getPriority( d_priority_order[index] )==getPriority( d_priority_order[index-1] );
       }
     }
 
-    Trace("inst-engine") << "Rewrite engine added " << addedLemmas << " lemmas." << std::endl;
+    Trace("rewrite-engine") << "Finished rewrite engine, added " << addedLemmas << " lemmas." << std::endl;
     if (addedLemmas==0) {
+
     }else{
       //otherwise, the search will continue
       d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
@@ -98,85 +106,185 @@ void RewriteEngine::check( Theory::Effort e ) {
   }
 }
 
-int RewriteEngine::checkRewriteRule( Node f ) {
-  Trace("rewrite-engine-inst") << "Check " << f << ", priority = " << getPriority( f ) << "..." << std::endl;
+int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) {
   int addedLemmas = 0;
-  //reset triggers
-  Node rr = f.getAttribute(QRewriteRuleAttribute());
-  if( d_rr_triggers.find(f)==d_rr_triggers.end() ){
-    std::vector< inst::Trigger * > triggers;
-    if( f.getNumChildren()==3 ){
-      for(unsigned i=0; i<f[2].getNumChildren(); i++ ){
-        Node pat = f[2][i];
-        std::vector< Node > nodes;
-        Trace("rewrite-engine-trigger") << "Trigger is : ";
-        for( int j=0; j<(int)pat.getNumChildren(); j++ ){
-          Node p = d_quantEngine->getTermDatabase()->getInstConstantNode( pat[j], f );
-          nodes.push_back( p );
-          Trace("rewrite-engine-trigger") << p << " " << p.getKind() << " ";
-        }
-        Trace("rewrite-engine-trigger") << std::endl;
-        Assert( inst::Trigger::isUsableTrigger( nodes, f ) );
-        inst::Trigger * tr = inst::Trigger::mkTrigger( d_quantEngine, f, nodes, 0, true, inst::Trigger::TR_MAKE_NEW, false );
-        tr->getGenerator()->setActiveAdd(false);
-        triggers.push_back( tr );
-      }
-    }
-    d_rr_triggers[f].insert( d_rr_triggers[f].end(), triggers.begin(), triggers.end() );
-  }
-  for( unsigned i=0; i<d_rr_triggers[f].size(); i++ ){
-    Trace("rewrite-engine-inst") << "Try trigger " << *d_rr_triggers[f][i] << std::endl;
-    d_rr_triggers[f][i]->resetInstantiationRound();
-    d_rr_triggers[f][i]->reset( Node::null() );
-    bool success;
-    do
-    {
-      InstMatch m( f );
-      success = d_rr_triggers[f][i]->getNextMatch( f, m );
-      if( success ){
-        //see if instantiation is true in the model
-        Node rr = f.getAttribute(QRewriteRuleAttribute());
-        Node rrg = rr[1];
-        std::vector< Node > vars;
-        std::vector< Node > terms;
-        d_quantEngine->computeTermVector( f, m, vars, terms );
-        Trace("rewrite-engine-inst-debug") << "Instantiation : " << m << std::endl;
-        Node inst = d_rr_guard[f];
-        inst = inst.substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
-        Trace("rewrite-engine-inst-debug") << "Try instantiation, guard : " << inst << std::endl;
-        FirstOrderModel * fm = d_quantEngine->getModel();
-        Node v = fm->getValue( inst );
-        Trace("rewrite-engine-inst-debug") << "Evaluated to " << v << std::endl;
-        if( v==d_true ){
-          Trace("rewrite-engine-inst-debug") << "Add instantiation : " << m << std::endl;
-          if( d_quantEngine->addInstantiation( f, m ) ){
-            addedLemmas++;
-            Trace("rewrite-engine-inst-debug") << "success" << std::endl;
-            //set the no-match attribute (the term is rewritten and can be ignored)
-            //Trace("rewrite-engine-inst-debug") << "We matched on : " << m.d_matched << std::endl;
-            //if( !m.d_matched.isNull() ){
-            //  NoMatchAttribute nma;
-            //  m.d_matched.setAttribute(nma,true);
+  Trace("rewrite-engine-inst") << "Check " << d_qinfo_n[f] << ", priority = " << getPriority( f ) << ", effort = " << e << "..." << std::endl;
+  QuantConflictFind * qcf = d_quantEngine->getConflictFind();
+  if( qcf ){
+    //reset QCF module
+    qcf->computeRelevantEqr();
+    qcf->setEffort( QuantConflictFind::effort_conflict );
+    //get the proper quantifiers info
+    std::map< Node, QuantInfo >::iterator it = d_qinfo.find( f );
+    if( it!=d_qinfo.end() ){
+      QuantInfo * qi = &it->second;
+      if( qi->d_mg->isValid() ){
+        Node rr = TermDb::getRewriteRule( f );
+        Trace("rewrite-engine-inst-debug") << "   Reset round..." << std::endl;
+        qi->reset_round( qcf );
+        Trace("rewrite-engine-inst-debug") << "   Get matches..." << std::endl;
+        while( qi->d_mg->getNextMatch( qcf, qi ) && ( addedLemmas==0 || !options::rrOneInstPerRound() ) ){
+          Trace("rewrite-engine-inst-debug") << "   Got match to complete..." << std::endl;
+          qi->debugPrintMatch( "rewrite-engine-inst-debug" );
+          std::vector< int > assigned;
+          if( !qi->isMatchSpurious( qcf ) ){
+            bool doContinue = false;
+            bool success = true;
+            int tempAddedLemmas = 0;
+            while( tempAddedLemmas==0 && success && ( addedLemmas==0 || !options::rrOneInstPerRound() ) ){
+              success = qi->completeMatch( qcf, assigned, doContinue );
+              doContinue = true;
+              if( success ){
+                Trace("rewrite-engine-inst-debug") << "   Construct match..." << std::endl;
+                std::vector< Node > inst;
+                qi->getMatch( inst );
+                Trace("rewrite-engine-inst-debug") << "   Add instantiation..." << std::endl;
+                for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+                  Trace("rewrite-engine-inst-debug") << "  " << f[0][i] << " -> ";
+                  if( i<inst.size() ){
+                    Trace("rewrite-engine-inst-debug") << inst[i] << std::endl;
+                  }else{
+                    Trace("rewrite-engine-inst-debug") << "OUT_OF_RANGE" << std::endl;
+                    Assert( false );
+                  }
+                }
+                //resize to remove auxiliary variables
+                if( inst.size()>f[0].getNumChildren() ){
+                  inst.resize( f[0].getNumChildren() );
+                }
+                if( d_quantEngine->addInstantiation( f, inst ) ){
+                  addedLemmas++;
+                  tempAddedLemmas++;
+                  /*
+                  //remove rewritten terms from consideration
+                  std::vector< Node > to_remove;
+                  switch( rr[2].getKind() ){
+                  case kind::RR_REWRITE:
+                    to_remove.push_back( rr[2][0] );
+                    break;
+                  case kind::RR_REDUCTION:
+                    for( unsigned i=0; i<rr[2][0].getNumChildren(); i++ ){
+                      to_remove.push_back( rr[2][0][i] );
+                    }
+                    break;
+                  default:
+                    break;
+                  }
+                  for( unsigned j=0; j<to_remove.size(); j++ ){
+                    Node ns = d_quantEngine->getSubstitute( to_remove[j], inst );
+                    Trace("rewrite-engine-inst-debug") << "Will remove : " << ns << std::endl;
+                    ns.setAttribute(NoMatchAttribute(),true);
+                  }
+                  */
+                }else{
+                  Trace("rewrite-engine-inst-debug") << "   - failed." << std::endl;
+                }
+                Trace("rewrite-engine-inst-debug") << "   Get next completion..." << std::endl;
+              }
+            }
+            //Trace("rewrite-engine-inst-debug") << "   Reverted assigned variables : ";
+            //for( unsigned a=0; a<assigned.size(); a++ ) {
+            //  Trace("rewrite-engine-inst-debug") << assigned[a] << " ";
             //}
+            //Trace("rewrite-engine-inst-debug") << std::endl;
+            //qi->revertMatch( assigned );
+            //Assert( assigned.empty() );
+            Trace("rewrite-engine-inst-debug") << "   - failed to complete." << std::endl;
           }else{
-            Trace("rewrite-engine-inst-debug") << "failure." << std::endl;
+            Trace("rewrite-engine-inst-debug") << "   - match is spurious." << std::endl;
           }
+          Trace("rewrite-engine-inst-debug") << "   Get next match..." << std::endl;
         }
+      }else{
+        Trace("rewrite-engine-inst-debug") << "...Invalid qinfo." << std::endl;
       }
-    }while(success);
+    }else{
+      Trace("rewrite-engine-inst-debug") << "...No qinfo." << std::endl;
+    }
   }
-  Trace("rewrite-engine-inst") << "Rule " << f << " generated " << addedLemmas << " lemmas." << std::endl;
+  Trace("rewrite-engine-inst") << "-> Generated " << addedLemmas << " lemmas." << std::endl;
   return addedLemmas;
 }
 
 void RewriteEngine::registerQuantifier( Node f ) {
-  if( f.hasAttribute(QRewriteRuleAttribute()) ){
-    Trace("rewrite-engine") << "Register quantifier " << f << std::endl;
-    Node rr = f.getAttribute(QRewriteRuleAttribute());
-    Trace("rewrite-engine") << "  rewrite rule is : " << rr << std::endl;
+  Node rr = TermDb::getRewriteRule( f );
+  if( !rr.isNull() ){
+    Trace("rr-register") << "Register quantifier " << f << std::endl;
+    Trace("rr-register") << "  rewrite rule is : " << rr << std::endl;
     d_rr_quant.push_back( f );
-    d_rr_guard[f] = rr[1];
-    Trace("rewrite-engine") << "  guard is : " << d_rr_guard[f] << std::endl;
+    d_rr[f] = rr;
+    d_needsSort = true;
+    Trace("rr-register") << "  guard is : " << d_rr[f][1] << std::endl;
+
+    QuantConflictFind * qcf = d_quantEngine->getConflictFind();
+    if( qcf ){
+      std::vector< Node > qcfn_c;
+
+      std::vector< Node > bvl;
+      for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+        bvl.push_back( f[0][i] );
+      }
+
+      std::vector< Node > cc;
+      //Node head = rr[2][0];
+      //if( head!=d_true ){
+        //Node head_eq = head.getType().isBoolean() ? head.iffNode( head ) : head.eqNode( head );
+        //head_eq = head_eq.negate();
+        //cc.push_back( head_eq );
+        //Trace("rr-register-debug") << "  head eq is " << head_eq << std::endl;
+      //}
+      //add patterns
+      for( unsigned i=1; i<f[2].getNumChildren(); i++ ){
+        std::vector< Node > nc;
+        for( unsigned j=0; j<f[2][i].getNumChildren(); j++ ){
+          Node nn;
+          Node nbv = NodeManager::currentNM()->mkBoundVar( f[2][i][j].getType() );
+          if( f[2][i][j].getType().isBoolean() ){
+            if( f[2][i][j].getKind()!=APPLY_UF ){
+              nn = f[2][i][j].negate();
+            }else{
+              nn = f[2][i][j].iffNode( nbv ).negate();
+              bvl.push_back( nbv );
+            }
+            //nn = f[2][i][j].negate();
+          }else{
+            nn = f[2][i][j].eqNode( nbv ).negate();
+            bvl.push_back( nbv );
+          }
+          nc.push_back( nn );
+        }
+        if( !nc.empty() ){
+          Node n = nc.size()==1 ? nc[0] : NodeManager::currentNM()->mkNode( AND, nc );
+          Trace("rr-register-debug") << "  pattern is " << n << std::endl;
+          if( std::find( cc.begin(), cc.end(), n )==cc.end() ){
+            cc.push_back( n );
+          }
+        }
+      }
+      qcfn_c.push_back( NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvl ) );
+
+      std::vector< Node > body_c;
+      //add the guards
+      if( d_rr[f][1].getKind()==AND ){
+        for( unsigned j=0; j<d_rr[f][1].getNumChildren(); j++ ){
+          if( MatchGen::isHandled( d_rr[f][1][j] ) ){
+            body_c.push_back( d_rr[f][1][j].negate() );
+          }
+        }
+      }else if( d_rr[f][1]!=d_true ){
+        if( MatchGen::isHandled( d_rr[f][1] ) ){
+          body_c.push_back( d_rr[f][1].negate() );
+        }
+      }
+      //add the patterns to the body
+      body_c.push_back( cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( AND, cc ) );
+      //make the body
+      qcfn_c.push_back( body_c.size()==1 ? body_c[0] : NodeManager::currentNM()->mkNode( OR, body_c ) );
+      //make the quantified formula
+      d_qinfo_n[f] = NodeManager::currentNM()->mkNode( FORALL, qcfn_c );
+      Trace("rr-register") << "  qcf formula is : " << d_qinfo_n[f] << std::endl;
+      d_qinfo[f].initialize( d_qinfo_n[f], d_qinfo_n[f][1] );
+    }
   }
 }
 
@@ -184,3 +292,13 @@ void RewriteEngine::assertNode( Node n ) {
 
 }
 
+Node RewriteEngine::getInstConstNode( Node n, Node q ) {
+  std::map< Node, Node >::iterator it = d_inst_const_node[q].find( n );
+  if( it==d_inst_const_node[q].end() ){
+    Node nn = d_quantEngine->getTermDatabase()->getInstConstantNode( n, q );
+    d_inst_const_node[q][n] = nn;
+    return nn;
+  }else{
+    return it->second;
+  }
+}
\ No newline at end of file
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index a9a2f9b46..f85803617 100644
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -29,19 +29,28 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class QuantInfo;
+
 class RewriteEngine : public QuantifiersModule
 {
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
   std::vector< Node > d_rr_quant;
-  std::map< Node, Node > d_rr_guard;
+  std::vector< Node > d_priority_order;
+  std::map< Node, Node > d_rr;
   Node d_true;
   /** explicitly provided patterns */
   std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers;
+  /** get the quantifer info object */
+  std::map< Node, Node > d_qinfo_n;
+  std::map< Node, QuantInfo > d_qinfo;
   double getPriority( Node f );
+  bool d_needsSort;
+  std::map< Node, std::map< Node, Node > > d_inst_const_node;
+  Node getInstConstNode( Node n, Node q );
 private:
-  int checkRewriteRule( Node f );
+  int checkRewriteRule( Node f, Theory::Effort e );
 public:
   RewriteEngine( context::Context* c, QuantifiersEngine* qe );
 
diff --git a/src/theory/quantifiers/symmetry_breaking.cpp b/src/theory/quantifiers/symmetry_breaking.cpp
index 0023b05bc..900db62d0 100644
--- a/src/theory/quantifiers/symmetry_breaking.cpp
+++ b/src/theory/quantifiers/symmetry_breaking.cpp
@@ -21,6 +21,7 @@
 #include "theory/theory_engine.h"
 #include "util/sort_inference.h"
 #include "theory/uf/theory_uf_strong_solver.h"
+#include "theory/uf/theory_uf.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 9a912130f..a9e77d3d2 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -47,19 +47,6 @@ bool TermArgTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){
   }
 }
 
-void TermDb::addTermEfficient( Node n, std::set< Node >& added){
-  static AvailableInTermDb aitdi;
-  if (inst::Trigger::isAtomicTrigger( n ) && !n.getAttribute(aitdi)){
-    //Already processed but new in this branch
-    n.setAttribute(aitdi,true);
-    added.insert( n );
-    for( size_t i=0; i< n.getNumChildren(); i++ ){
-      addTermEfficient(n[i],added);
-    }
-  }
-
-}
-
 
 Node TermDb::getOperator( Node n ) {
   //return n.getOperator();
@@ -94,10 +81,8 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
     return;
   }
   if( d_processed.find( n )==d_processed.end() ){
-    ++(d_quantEngine->d_statistics.d_term_in_termdb);
     d_processed.insert(n);
     d_type_map[ n.getType() ].push_back( n );
-    n.setAttribute(AvailableInTermDb(),true);
     //if this is an atomic trigger, consider adding it
     //Call the children?
     if( inst::Trigger::isAtomicTrigger( n ) ){
@@ -110,22 +95,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
 
         for( size_t i=0; i<n.getNumChildren(); i++ ){
           addTerm( n[i], added, withinQuant );
-          if( options::efficientEMatching() ){
-            EfficientEMatcher* eem = d_quantEngine->getEfficientEMatcher();
-            if( d_parents[n[i]][op].empty() ){
-              //must add parent to equivalence class info
-              Node nir = d_quantEngine->getEqualityQuery()->getRepresentative( n[i] );
-              EqClassInfo* eci_nir = eem->getEquivalenceClassInfo( nir );
-              if( eci_nir ){
-                eci_nir->d_pfuns[ op ] = true;
-              }
-            }
-            //add to parent structure
-            if( std::find( d_parents[n[i]][op][i].begin(), d_parents[n[i]][op][i].end(), n )==d_parents[n[i]][op][i].end() ){
-              d_parents[n[i]][op][i].push_back( n );
-              Assert(!getParents(n[i],op,i).empty());
-            }
-          }
           if( options::eagerInstQuant() ){
             if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
               int addedLemmas = 0;
@@ -143,13 +112,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
         addTerm( n[i], added, withinQuant );
       }
     }
-  }else{
-    if( options::efficientEMatching() && !TermDb::hasInstConstAttr(n)){
-      //Efficient e-matching must be notified
-      //The term in triggers are not important here
-      Debug("term-db") << "New in this branch term " << n << std::endl;
-      addTermEfficient(n,added);
-    }
   }
 }
 
@@ -647,3 +609,15 @@ void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){
     d_op_triggers[op].push_back( tr );
   }
 }
+
+bool TermDb::isRewriteRule( Node q ) {
+  return !getRewriteRule( q ).isNull();
+}
+
+Node TermDb::getRewriteRule( Node q ) {
+  if( q.getKind()==FORALL && q.getNumChildren()==3 && q[2].getNumChildren()>0 && q[2][0][0].getKind()==REWRITE_RULE ){
+    return q[2][0][0];
+  }else{
+    return Node::null();
+  }
+}
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 66b45be2f..b3db6d266 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -44,15 +44,6 @@ typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
 struct InstVarNumAttributeId {};
 typedef expr::Attribute<InstVarNumAttributeId, uint64_t> InstVarNumAttribute;
 
-// Attribute that tell if a node have been asserted in this branch
-struct AvailableInTermDbId {};
-/** use the special for boolean flag */
-typedef expr::Attribute<AvailableInTermDbId,
-                        bool,
-                        expr::attr::NullCleanupStrategy,
-                        true  // context dependent
-                        > AvailableInTermDb;
-
 struct ModelBasisAttributeId {};
 typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
 //for APPLY_UF terms, 1 : term has direct child with model basis attribute,
@@ -60,10 +51,6 @@ typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
 struct ModelBasisArgAttributeId {};
 typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute;
 
-//for rewrite rules
-struct QRewriteRuleAttributeId {};
-typedef expr::Attribute<QRewriteRuleAttributeId, Node> QRewriteRuleAttribute;
-
 //for bounded integers
 struct BoundIntLitAttributeId {};
 typedef expr::Attribute<BoundIntLitAttributeId, uint64_t> BoundIntLitAttribute;
@@ -128,9 +115,6 @@ public:
   void reset( Theory::Effort effort );
   /** get operation */
   Node getOperator( Node n );
-private:
-  /** for efficient e-matching */
-  void addTermEfficient( Node n, std::set< Node >& added);
 public:
   /** parent structure (for efficient E-matching):
       n -> op -> index -> L
@@ -252,6 +236,11 @@ public:
   int isInstanceOf( Node n1, Node n2 );
   /** filter all nodes that have instances */
   void filterInstances( std::vector< Node >& nodes );
+public:
+  /** is quantifier treated as a rewrite rule? */
+  static bool isRewriteRule( Node q );
+  /** get the rewrite rule associated with the quanfied formula */
+  static Node getRewriteRule( Node q );
 };/* class TermDb */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h
index b13d8601e..93bd2c012 100644
--- a/src/theory/quantifiers/theory_quantifiers_type_rules.h
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h
@@ -104,6 +104,92 @@ struct QuantifierInstPatternListTypeRule {
   }
 };/* struct QuantifierInstPatternListTypeRule */
 
+
+class RewriteRuleTypeRule {
+public:
+
+  /**
+   * Compute the type for (and optionally typecheck) a term belonging
+   * to the theory of rewriterules.
+   *
+   * @param nodeManager the NodeManager in use
+   * @param n the node to compute the type of
+   * @param check if true, the node's type should be checked as well
+   * as computed.
+   */
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
+                                     bool check)
+    throw(TypeCheckingExceptionPrivate) {
+    Debug("typecheck-r") << "type check for rr " << n << std::endl;
+    Assert(n.getKind() == kind::REWRITE_RULE && n.getNumChildren()==3 );
+    if( check ){
+      if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){
+        throw TypeCheckingExceptionPrivate(n[0],
+                     "first argument of rewrite rule is not bound var list");
+      }
+      if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){
+        throw TypeCheckingExceptionPrivate(n[1],
+                     "guard of rewrite rule is not an actual guard");
+      }
+      if( n[2].getType(check) !=
+          TypeNode(nodeManager->mkTypeConst<TypeConstant>(RRHB_TYPE))){
+        throw TypeCheckingExceptionPrivate(n[2],
+                     "not a correct rewrite rule");
+      }
+    }
+    return nodeManager->booleanType();
+  }
+};/* class RewriteRuleTypeRule */
+
+
+class RRRewriteTypeRule {
+public:
+
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw(TypeCheckingExceptionPrivate) {
+    Assert(n.getKind() == kind::RR_REWRITE );
+    if( check ){
+      if( n[0].getType(check)!=n[1].getType(check) ){
+        throw TypeCheckingExceptionPrivate(n,
+                     "terms of rewrite rule are not equal");
+      }
+      if( n.getNumChildren() == 3 && n[2].getType(check)!=nodeManager->instPatternListType() ){
+        throw TypeCheckingExceptionPrivate(n, "third argument of rewrite rule is not instantiation pattern list");
+      }
+      if( n[0].getKind()!=kind::APPLY_UF ){
+        throw TypeCheckingExceptionPrivate(n[0], "head of rewrite rules must start with an uninterpreted symbols. If you want to write a propagation rule, add the guard [true] for disambiguation");
+      }
+    }
+    return TypeNode(nodeManager->mkTypeConst<TypeConstant>(RRHB_TYPE));
+  }
+};/* struct QuantifierReductionRuleRule */
+
+class RRRedDedTypeRule {
+public:
+
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw(TypeCheckingExceptionPrivate) {
+    Assert(n.getKind() == kind::RR_REDUCTION ||
+           n.getKind() == kind::RR_DEDUCTION );
+    if( check ){
+      if( n[ 0 ].getType(check)!=nodeManager->booleanType() ){
+        throw TypeCheckingExceptionPrivate(n, "head of reduction rule is not boolean");
+      }
+      if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){
+        throw TypeCheckingExceptionPrivate(n, "body of reduction rule is not boolean");
+      }
+      if( n.getNumChildren() == 3 && n[2].getType(check)!=nodeManager->instPatternListType() ){
+        throw TypeCheckingExceptionPrivate(n, "third argument of rewrite rule is not instantiation pattern list");
+      }
+      if( n.getNumChildren() < 3 && n[ 0 ] == nodeManager->mkConst<bool>(true) ){
+        throw TypeCheckingExceptionPrivate(n, "A rewrite rule must have one head or one trigger at least");
+      }
+    }
+    return TypeNode(nodeManager->mkTypeConst<TypeConstant>(RRHB_TYPE));
+  }
+};/* struct QuantifierReductionRuleRule */
+
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 41f53740a..02423e54d 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -25,13 +25,14 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/trigger.h"
-#include "theory/rewriterules/efficient_e_matching.h"
-#include "theory/rewriterules/rr_trigger.h"
+//#include "theory/rewriterules/efficient_e_matching.h"
+//#include "theory/rewriterules/rr_trigger.h"
 #include "theory/quantifiers/bounded_integers.h"
 #include "theory/quantifiers/rewrite_engine.h"
 #include "theory/quantifiers/quant_conflict_find.h"
 #include "theory/quantifiers/relevant_domain.h"
 #include "theory/uf/options.h"
+#include "theory/uf/theory_uf.h"
 
 using namespace std;
 using namespace CVC4;
@@ -46,8 +47,8 @@ d_lemmas_produced_c(u){
   d_eq_query = new EqualityQueryQuantifiersEngine( this );
   d_term_db = new quantifiers::TermDb( this );
   d_tr_trie = new inst::TriggerTrie;
-  d_rr_tr_trie = new rrinst::TriggerTrie;
-  d_eem = new EfficientEMatcher( this );
+  //d_rr_tr_trie = new rrinst::TriggerTrie;
+  //d_eem = new EfficientEMatcher( this );
   d_hasAddedLemma = false;
 
   Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
@@ -74,7 +75,7 @@ d_lemmas_produced_c(u){
   }
 
   //add quantifiers modules
-  if( options::quantConflictFind() ){
+  if( options::quantConflictFind() || options::quantRewriteRules() ){
     d_qcf = new quantifiers::QuantConflictFind( this, c);
     d_modules.push_back( d_qcf );
   }else{
@@ -100,7 +101,7 @@ d_lemmas_produced_c(u){
     d_model_engine = NULL;
     d_bint = NULL;
   }
-  if( options::rewriteRulesAsAxioms() ){
+  if( options::quantRewriteRules() ){
     d_rr_engine = new quantifiers::RewriteEngine( c, this );
     d_modules.push_back(d_rr_engine);
   }else{
@@ -129,10 +130,6 @@ EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() {
   return d_eq_query;
 }
 
-//Instantiator* QuantifiersEngine::getInstantiator( theory::TheoryId id ){
-//  return d_te->theoryOf( id )->getInstantiator();
-//}
-
 context::Context* QuantifiersEngine::getSatContext(){
   return d_te->theoryOf( THEORY_QUANTIFIERS )->getSatContext();
 }
@@ -176,6 +173,9 @@ void QuantifiersEngine::check( Theory::Effort e ){
     if( d_rel_dom ){
       d_rel_dom->reset();
     }
+    for( int i=0; i<(int)d_modules.size(); i++ ){
+      d_modules[i]->reset_round( e );
+    }
     if( e==Theory::EFFORT_LAST_CALL ){
       //if effort is last call, try to minimize model first
       if( options::finiteModelFind() ){
@@ -216,7 +216,11 @@ void QuantifiersEngine::check( Theory::Effort e ){
 
 void QuantifiersEngine::registerQuantifier( Node f ){
   if( std::find( d_quants.begin(), d_quants.end(), f )==d_quants.end() ){
-    Trace("quant") << "Register quantifier : " << f << std::endl;
+    Trace("quant") << "QuantifiersEngine : Register quantifier ";
+    if( d_term_db->isRewriteRule( f ) ){
+      Trace("quant") << " (rewrite rule)";
+    }
+    Trace("quant") << " : " << f << std::endl;
     d_quants.push_back( f );
 
     ++(d_statistics.d_num_quant);
@@ -277,9 +281,6 @@ Node QuantifiersEngine::getNextDecisionRequest(){
 void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){
   std::set< Node > added;
   getTermDatabase()->addTerm( n, added, withinQuant );
-  if( options::efficientEMatching() ){
-    d_eem->newTerms( added );
-  }
   //added contains also the Node that just have been asserted in this branch
   if( d_quant_rel ){
     for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){
@@ -361,7 +362,7 @@ void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){
   }
 }
 
-Node QuantifiersEngine::doSubstitute( Node n, std::vector< Node >& terms ){
+Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms ){
   if( n.getKind()==INST_CONSTANT ){
     Debug("check-inst") << "Substitute inst constant : " << n << std::endl;
     return terms[n.getAttribute(InstVarNumAttribute())];
@@ -377,7 +378,7 @@ Node QuantifiersEngine::doSubstitute( Node n, std::vector< Node >& terms ){
     }
     bool changed = false;
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      Node c = doSubstitute( n[i], terms );
+      Node c = getSubstitute( n[i], terms );
       cc.push_back( c );
       changed = changed || c!=n[i];
     }
@@ -410,7 +411,7 @@ Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std
   }else{
     //do optimized version
     Node icb = d_term_db->getInstConstantBody( f );
-    body = doSubstitute( icb, terms );
+    body = getSubstitute( icb, terms );
     if( Debug.isOn("check-inst") ){
       Node body2 = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
       if( body!=body2 ){
@@ -612,15 +613,7 @@ QuantifiersEngine::Statistics::Statistics():
   d_triggers("QuantifiersEngine::Triggers", 0),
   d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
   d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
-  d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0),
-  d_term_in_termdb("QuantifiersEngine::Term_in_TermDb", 0),
-  d_num_mono_candidates("QuantifiersEngine::NumMonoCandidates", 0),
-  d_num_mono_candidates_new_term("QuantifiersEngine::NumMonoCandidatesNewTerm", 0),
-  d_num_multi_candidates("QuantifiersEngine::NumMultiCandidates", 0),
-  d_mono_candidates_cache_hit("QuantifiersEngine::MonoCandidatesCacheHit", 0),
-  d_mono_candidates_cache_miss("QuantifiersEngine::MonoCandidatesCacheMiss", 0),
-  d_multi_candidates_cache_hit("QuantifiersEngine::MultiCandidatesCacheHit", 0),
-  d_multi_candidates_cache_miss("QuantifiersEngine::MultiCandidatesCacheMiss", 0)
+  d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0)
 {
   StatisticsRegistry::registerStat(&d_num_quant);
   StatisticsRegistry::registerStat(&d_instantiation_rounds);
@@ -634,14 +627,6 @@ QuantifiersEngine::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_simple_triggers);
   StatisticsRegistry::registerStat(&d_multi_triggers);
   StatisticsRegistry::registerStat(&d_multi_trigger_instantiations);
-  StatisticsRegistry::registerStat(&d_term_in_termdb);
-  StatisticsRegistry::registerStat(&d_num_mono_candidates);
-  StatisticsRegistry::registerStat(&d_num_mono_candidates_new_term);
-  StatisticsRegistry::registerStat(&d_num_multi_candidates);
-  StatisticsRegistry::registerStat(&d_mono_candidates_cache_hit);
-  StatisticsRegistry::registerStat(&d_mono_candidates_cache_miss);
-  StatisticsRegistry::registerStat(&d_multi_candidates_cache_hit);
-  StatisticsRegistry::registerStat(&d_multi_candidates_cache_miss);
 }
 
 QuantifiersEngine::Statistics::~Statistics(){
@@ -657,14 +642,6 @@ QuantifiersEngine::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_simple_triggers);
   StatisticsRegistry::unregisterStat(&d_multi_triggers);
   StatisticsRegistry::unregisterStat(&d_multi_trigger_instantiations);
-  StatisticsRegistry::unregisterStat(&d_term_in_termdb);
-  StatisticsRegistry::unregisterStat(&d_num_mono_candidates);
-  StatisticsRegistry::unregisterStat(&d_num_mono_candidates_new_term);
-  StatisticsRegistry::unregisterStat(&d_num_multi_candidates);
-  StatisticsRegistry::unregisterStat(&d_mono_candidates_cache_hit);
-  StatisticsRegistry::unregisterStat(&d_mono_candidates_cache_miss);
-  StatisticsRegistry::unregisterStat(&d_multi_candidates_cache_hit);
-  StatisticsRegistry::unregisterStat(&d_multi_candidates_cache_miss);
 }
 
 eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index fbc501aec..858093543 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -20,8 +20,8 @@
 #include "theory/theory.h"
 #include "util/hash.h"
 #include "theory/quantifiers/inst_match.h"
-#include "theory/rewriterules/rr_inst_match.h"
 #include "theory/quantifiers/quant_util.h"
+#include "expr/attribute.h"
 
 #include "util/statistics_registry.h"
 
@@ -49,6 +49,8 @@ public:
   virtual void finishInit() {}
   /* whether this module needs to check this round */
   virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; }
+  /* reset at a round */
+  virtual void reset_round( Theory::Effort e ){}
   /* Call during quantifier engine's check */
   virtual void check( Theory::Effort e ) = 0;
   /* Called for new quantifiers */
@@ -75,11 +77,7 @@ namespace inst {
   class TriggerTrie;
 }/* CVC4::theory::inst */
 
-namespace rrinst {
-  class TriggerTrie;
-}/* CVC4::theory::inst */
-
-class EfficientEMatcher;
+//class EfficientEMatcher;
 class EqualityQueryQuantifiersEngine;
 
 class QuantifiersEngine {
@@ -102,8 +100,6 @@ private:
   quantifiers::RelevantDomain* d_rel_dom;
   /** phase requirements for each quantifier for each instantiation literal */
   std::map< Node, QuantPhaseReq* > d_phase_reqs;
-  /** efficient e-matcher */
-  EfficientEMatcher* d_eem;
   /** instantiation engine */
   quantifiers::InstantiationEngine* d_inst_engine;
   /** model engine */
@@ -131,8 +127,6 @@ private:
   quantifiers::TermDb* d_term_db;
   /** all triggers will be stored in this trie */
   inst::TriggerTrie* d_tr_trie;
-  /** all triggers for rewrite rules will be stored in this trie */
-  rrinst::TriggerTrie* d_rr_tr_trie;
   /** extended model object */
   quantifiers::FirstOrderModel* d_model;
   /** statistics for debugging */
@@ -144,8 +138,6 @@ private:
 public:
   QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te);
   ~QuantifiersEngine();
-  /** get instantiator for id */
-  //Instantiator* getInstantiator( theory::TheoryId id );
   /** get theory engine */
   TheoryEngine* getTheoryEngine() { return d_te; }
   /** get equality query object for the given type. The default is the
@@ -171,8 +163,6 @@ public:
   QuantPhaseReq* getPhaseRequirements( Node f ) { return d_phase_reqs.find( f )==d_phase_reqs.end() ? NULL : d_phase_reqs[f]; }
   /** get phase requirement terms */
   void getPhaseReqTerms( Node f, std::vector< Node >& nodes );
-  /** get efficient e-matching utility */
-  EfficientEMatcher* getEfficientEMatcher() { return d_eem; }
   /** get bounded integers utility */
   quantifiers::BoundedIntegers * getBoundedIntegers() { return d_bint; }
   /** Conflict find mechanism for quantifiers */
@@ -199,8 +189,6 @@ private:
   bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
   /** set instantiation level attr */
   void setInstantiationLevelAttr( Node n, uint64_t level );
-  /** do substitution */
-  Node doSubstitute( Node n, std::vector< Node >& terms );
 public:
   /** get instantiation */
   Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
@@ -208,6 +196,8 @@ public:
   Node getInstantiation( Node f, InstMatch& m );
   /** get instantiation */
   Node getInstantiation( Node f, std::vector< Node >& terms );
+  /** do substitution */
+  Node getSubstitute( Node n, std::vector< Node >& terms );
   /** exist instantiation ? */
   bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false );
   /** add lemma lem */
@@ -238,8 +228,6 @@ public:
   quantifiers::TermDb* getTermDatabase() { return d_term_db; }
   /** get trigger database */
   inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
-  /** get rewrite trigger database */
-  rrinst::TriggerTrie* getRRTriggerDatabase() { return d_rr_tr_trie; }
   /** add term to database */
   void addTermToDatabase( Node n, bool withinQuant = false );
   /** get the master equality engine */
@@ -260,14 +248,6 @@ public:
     IntStat d_simple_triggers;
     IntStat d_multi_triggers;
     IntStat d_multi_trigger_instantiations;
-    IntStat d_term_in_termdb;
-    IntStat d_num_mono_candidates;
-    IntStat d_num_mono_candidates_new_term;
-    IntStat d_num_multi_candidates;
-    IntStat d_mono_candidates_cache_hit;
-    IntStat d_mono_candidates_cache_miss;
-    IntStat d_multi_candidates_cache_hit;
-    IntStat d_multi_candidates_cache_miss;
     Statistics();
     ~Statistics();
   };/* class QuantifiersEngine::Statistics */
diff --git a/src/theory/rewriterules/kinds b/src/theory/rewriterules/kinds
index 490c8f100..4ea0ecd43 100644
--- a/src/theory/rewriterules/kinds
+++ b/src/theory/rewriterules/kinds
@@ -14,24 +14,4 @@ properties check
 
 # constants...
 
-# types...
-sort RRHB_TYPE \
-    Cardinality::INTEGERS \
-    not-well-founded \
-    "head and body of the rule type"
-
-# operators...
-
-# variables, guards, RR_REWRITE/REDUCTION_RULE/DEDUCTION_RULE
-operator REWRITE_RULE 3 "general rewrite rule"
-#HEAD/BODY/TRIGGER
-operator RR_REWRITE 2:3 "actual rewrite rule"
-operator RR_REDUCTION 2:3 "actual reduction rule"
-operator RR_DEDUCTION 2:3 "actual deduction rule"
-
-typerule REWRITE_RULE ::CVC4::theory::rewriterules::RewriteRuleTypeRule
-typerule RR_REWRITE   ::CVC4::theory::rewriterules::RRRewriteTypeRule
-typerule RR_REDUCTION ::CVC4::theory::rewriterules::RRRedDedTypeRule
-typerule RR_DEDUCTION ::CVC4::theory::rewriterules::RRRedDedTypeRule
-
 endtheory
diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp
index 7fe625da1..37187e684 100644
--- a/src/theory/rewriterules/theory_rewriterules.cpp
+++ b/src/theory/rewriterules/theory_rewriterules.cpp
@@ -16,12 +16,7 @@
  **/
 
 #include "theory/rewriterules/theory_rewriterules.h"
-#include "theory/rewriterules/theory_rewriterules_rules.h"
-#include "theory/rewriterules/theory_rewriterules_params.h"
-
-#include "theory/rewriterules/theory_rewriterules_preprocess.h"
 #include "theory/rewriter.h"
-#include "theory/rewriterules/options.h"
 
 
 using namespace std;
@@ -38,159 +33,26 @@ namespace theory {
 namespace rewriterules {
 
 
-inline std::ostream& operator <<(std::ostream& stream, const RuleInst& ri) {
-  ri.toStream(stream);
-  return stream;
-}
-
-static const RuleInst* RULEINST_TRUE = (RuleInst*) 1;
-static const RuleInst* RULEINST_FALSE = (RuleInst*) 2;
-
-  /** Rule an instantiation with the given match */
-RuleInst::RuleInst(TheoryRewriteRules & re, const RewriteRule * r,
-                   std::vector<Node> & inst_subst,
-                   Node matched):
-  rule(r), d_matched(matched)
-{
-  Assert(r != NULL);
-  Assert(!r->directrr || !d_matched.isNull());
-  subst.swap(inst_subst);
-};
-
-Node RuleInst::substNode(const TheoryRewriteRules & re, TNode r,
-                         TCache cache ) const {
-  Assert(this != RULEINST_TRUE && this != RULEINST_FALSE);
-  return r.substitute (rule->free_vars.begin(),rule->free_vars.end(),
-                       subst.begin(),subst.end(),cache);
-};
-size_t RuleInst::findGuard(TheoryRewriteRules & re, size_t start)const{
-  TCache cache;
-  Assert(this != RULEINST_TRUE && this != RULEINST_FALSE);
-  while (start < (rule->guards).size()){
-    Node g = substNode(re,rule->guards[start],cache);
-    switch(re.addWatchIfDontKnow(g,this,start)){
-    case ATRUE:
-      Debug("rewriterules::guards") << g << "is true" << std::endl;
-      ++start;
-      continue;
-    case AFALSE:
-      Debug("rewriterules::guards") << g << "is false" << std::endl;
-      return -1;
-    case ADONTKNOW:
-      Debug("rewriterules::guards") << g << "is unknown" << std::endl;
-      return start;
-    }
-  }
-  /** All the guards are verified */
-  re.propagateRule(this,cache);
-  return start;
-};
-
-bool RuleInst::alreadyRewritten(TheoryRewriteRules & re) const{
-  Assert(this != RULEINST_TRUE && this != RULEINST_FALSE);
-  static NoMatchAttribute rewrittenNodeAttribute;
-  TCache cache;
-  for(std::vector<Node>::const_iterator
-        iter = rule->to_remove.begin();
-      iter != rule->to_remove.end(); ++iter){
-    if (substNode(re,*iter,cache).getAttribute(rewrittenNodeAttribute))
-      return true;
-  };
-  return false;
-}
-
-void RuleInst::toStream(std::ostream& out) const{
-  if(this == RULEINST_TRUE){ out << "TRUE"; return;};
-  if(this == RULEINST_FALSE){ out << "FALSE"; return;};
-  out << "(" << *rule << ") ";
-  for(std::vector<Node>::const_iterator
-        iter = subst.begin(); iter != subst.end(); ++iter){
-    out << *iter << " ";
-  };
-}
-
-
-void Guarded::nextGuard(TheoryRewriteRules & re)const{
-  Assert(inst != RULEINST_TRUE && inst != RULEINST_FALSE);
-  if(simulateRewritting && inst->alreadyRewritten(re)) return;
-  inst->findGuard(re,d_guard+1);
-};
-
-/** start indicate the first guard which is not true */
-Guarded::Guarded(const RuleInst* ri, const size_t start) :
-  d_guard(start),inst(ri) {};
-Guarded::Guarded(const Guarded & g) :
-  d_guard(g.d_guard),inst(g.inst) {};
-Guarded::Guarded() :
-  //dumb value
-  d_guard(-1),inst(RULEINST_TRUE) {};
-
 TheoryRewriteRules::TheoryRewriteRules(context::Context* c,
                                        context::UserContext* u,
                                        OutputChannel& out,
                                        Valuation valuation,
                                        const LogicInfo& logicInfo) :
-  Theory(THEORY_REWRITERULES, c, u, out, valuation, logicInfo),
-  d_rules(c), d_ruleinsts(c), d_guardeds(c), d_checkLevel(c,0),
-  d_explanations(c), d_ruleinsts_to_add(), d_ppAssert_on(false)
+  Theory(THEORY_REWRITERULES, c, u, out, valuation, logicInfo)
 {
-  d_true = NodeManager::currentNM()->mkConst<bool>(true);
-  d_false = NodeManager::currentNM()->mkConst<bool>(false);
-}
-
-void TheoryRewriteRules::addMatchRuleTrigger(const RewriteRule * r,
-                                             rrinst::InstMatch & im,
-                                             bool delay){
-  ++r->nb_matched;
-  ++d_statistics.d_match_found;
-  if(rewrite_instantiation) im.applyRewrite();
-  if(representative_instantiation)
-    im.makeRepresentative( getQuantifiersEngine() );
 
-  if(!cache_match || !r->inCache(*this,im)){
-    ++r->nb_applied;
-    ++d_statistics.d_cache_miss;
-    std::vector<Node> subst;
-    //AJR: replaced computeTermVec with this
-    for( size_t i=0; i<r->inst_vars.size(); i++ ){
-      Node n = im.getValue( r->inst_vars[i] );
-      Assert( !n.isNull() );
-      subst.push_back( n );
-    }
-    RuleInst * ri = new RuleInst(*this,r,subst,
-                                 r->directrr ? im.d_matched : Node::null());
-    Debug("rewriterules::matching") << "One matching found"
-                                    << (delay? "(delayed)":"")
-                                    << ":" << *ri << std::endl;
-    // Find the first non verified guard, don't save the rule if the
-    // rule can already be fired In fact I save it otherwise strange
-    // things append.
-    Assert(ri->rule != NULL);
-    if(delay) d_ruleinsts_to_add.push_back(ri);
-    else{
-      if(simulateRewritting && ri->alreadyRewritten(*this)) return;
-      if(ri->findGuard(*this, 0) != (r->guards).size())
-        d_ruleinsts.push_back(ri);
-      else delete(ri);
-    };
-  }else{
-    ++d_statistics.d_cache_hit;
-  };
 }
 
 void TheoryRewriteRules::check(Effort level) {
   CodeTimer codeTimer(d_theoryTime);
 
-  Assert(d_ruleinsts_to_add.empty());
-
   while(!done()) {
     // Get all the assertions
     // TODO: Test that it have already been ppAsserted
 
     //if we are here and ppAssert has not been done
     // that means that ppAssert is off so we need to assert now
-    if(!d_ppAssert_on) addRewriteRule(get());
-    else get();
+    Assertion assertion = get();
     // Assertion assertion = get();
     // TNode fact = assertion.assertion;
 
@@ -199,442 +61,18 @@ void TheoryRewriteRules::check(Effort level) {
     //     Unhandled(getValuation().getDecisionLevel());
     //   addRewriteRule(fact);
 
-    };
-
-  Debug("rewriterules::check") << "RewriteRules::Check start " << d_checkLevel << (level==EFFORT_FULL? " EFFORT_FULL":"") << std::endl;
-
-  /** Test each rewrite rule */
-  for(size_t rid = 0, end = d_rules.size(); rid < end; ++rid) {
-    RewriteRule * r = d_rules[rid];
-    if (level!=EFFORT_FULL && r->d_split) continue;
-    Debug("rewriterules::check") << "RewriteRules::Check  rule: " << *r << std::endl;
-    Trigger & tr = r->trigger;
-    //reset instantiation round for trigger (set up match production)
-    tr.resetInstantiationRound();
-
-    /** Test the possible matching one by one */
-    while(tr.getNextMatch()){
-      rrinst::InstMatch im = tr.getInstMatch();
-      addMatchRuleTrigger(r, im, true);
-    }
-  }
-
-  const bool do_notification = d_checkLevel == 0 || level==EFFORT_FULL;
-  bool polldone = false;
-
-  if(level==EFFORT_FULL) ++d_statistics.d_full_check;
-  else ++d_statistics.d_check;
-
-  GuardedMap::const_iterator p = d_guardeds.begin();
-  do{
-
-
-    //dequeue instantiated rules
-    for(; !d_ruleinsts_to_add.empty();){
-      RuleInst * ri = d_ruleinsts_to_add.back(); d_ruleinsts_to_add.pop_back();
-      if(simulateRewritting && ri->alreadyRewritten(*this)) continue;
-      if(ri->findGuard(*this, 0) != ri->rule->guards.size())
-        d_ruleinsts.push_back(ri);
-      else delete(ri);
-    };
-
-    if(do_notification)
-    /** Temporary way. Poll value */
-    for (; p != d_guardeds.end(); ++p){
-      TNode g = (*p).first;
-      const GList * const l = (*p).second;
-      const Guarded & glast = l->back();
-      // Notice() << "Polled?:" << g << std::endl;
-      if(glast.inst == RULEINST_TRUE||glast.inst == RULEINST_FALSE) continue;
-      // Notice() << "Polled!:" << g << "->" << (glast.inst == RULEINST_TRUE||glast.inst == RULEINST_FALSE) << std::endl;
-      bool value;
-      if(getValuation().hasSatValue(g,value)){
-        if(value) polldone = true; //One guard is true so pass n check
-        Debug("rewriterules::guards") << "Poll value:" << g
-                             << " is " << (value ? "true" : "false") << std::endl;
-        notification(g,value);
-        //const Guarded & glast2 = (*l)[l->size()-1];
-        // Notice() << "Polled!!:" << g << "->" << (glast2.inst == RULEINST_TRUE||glast2.inst == RULEINST_FALSE) << std::endl;
-      };
-    };
-
-  }while(!d_ruleinsts_to_add.empty() ||
-         (p != d_guardeds.end() && do_notification));
-
-  if(polldone) d_checkLevel = checkSlowdown;
-  else d_checkLevel = d_checkLevel > 0 ? (d_checkLevel - 1) : 0;
-
-  /** Narrowing by splitting on the guards */
-  /** Perhaps only when no notification? */
-  if(narrowing_full_effort && level==EFFORT_FULL){
-    for (GuardedMap::const_iterator p = d_guardeds.begin();
-         p != d_guardeds.end(); ++p){
-      TNode g = (*p).first;
-      const GList * const l = (*p).second;
-      const Guarded & glast = (*l)[l->size()-1];
-      if(glast.inst == RULEINST_TRUE||glast.inst == RULEINST_FALSE)
-        continue;
-      // If it has a value it should already has been notified
-      bool value CVC4_UNUSED;
-      Assert(!getValuation().hasSatValue(g,value));
-      Debug("rewriterules::check") << "RewriteRules::Check Narrowing on:" << g << std::endl;
-      /** Can split on already rewritten instrule... but... */
-      getOutputChannel().split(g);
     }
-  }
-
-  Assert(d_ruleinsts_to_add.empty());
-  Debug("rewriterules::check") << "RewriteRules::Check done " << d_checkLevel << std::endl;
-
-};
-
-void TheoryRewriteRules::registerQuantifier( Node n ){};
-
-Trigger TheoryRewriteRules::createTrigger( TNode n, std::vector<Node> & pattern ) {
-  //  Debug("rewriterules") << "createTrigger:";
-  getQuantifiersEngine()->registerPattern(pattern);
-  return *Trigger::mkTrigger(getQuantifiersEngine(),n,pattern,
-                             options::efficientEMatching()?
-                             Trigger::MATCH_GEN_EFFICIENT_E_MATCH :
-                             Trigger::MATCH_GEN_DEFAULT,
-                             true,
-                             Trigger::TR_MAKE_NEW,
-                             false);
-  //                             options::smartMultiTriggers());
-};
-
-bool TheoryRewriteRules::notifyIfKnown(const GList * const ltested,
-                                        GList * const lpropa) {
-    Assert(ltested->size() > 0);
-    const Guarded & glast = (*ltested)[ltested->size()-1];
-    if(glast.inst == RULEINST_TRUE || glast.inst == RULEINST_FALSE){
-      notification(lpropa,glast.inst == RULEINST_TRUE);
-      return true;
-    };
-    return false;
-};
-
-void TheoryRewriteRules::notification(GList * const lpropa, bool b){
-  if (b){
-    for(size_t ig = 0;
-        ig != lpropa->size(); ++ig) {
-      (*lpropa)[ig].nextGuard(*this);
-    };
-    lpropa->push_back(Guarded(RULEINST_TRUE,0));
-  }else{
-    lpropa->push_back(Guarded(RULEINST_FALSE,0));
-  };
-  Assert(lpropa->back().inst == RULEINST_TRUE ||
-         lpropa->back().inst == RULEINST_FALSE);
 };
 
-
-
-Answer TheoryRewriteRules::addWatchIfDontKnow(Node g0, const RuleInst* ri,
-                                              const size_t gid){
-  /** Currently create a node with a literal */
-  Node g = getValuation().ensureLiteral(g0);
-  GuardedMap::iterator l_i = d_guardeds.find(g);
-  GList* l;
-  if( l_i == d_guardeds.end() ) {
-    /** Normally Not watched so IDONTNOW but since we poll, we can poll now */
-    bool value;
-    if(getValuation().hasSatValue(g,value)){
-      if(value) return ATRUE;
-      else      return AFALSE;
-    };
-    //Not watched so IDONTNOW
-    l = new(getSatContext()->getCMM())
-      GList(true, getSatContext());//,
-            //ContextMemoryAllocator<Guarded>(getContext()->getCMM()));
-    d_guardeds.insert(g ,l);//.insertDataFromContextMemory(g, l);
-    /* TODO Add register propagation */
-  } else {
-    l = (*l_i).second;
-    Assert(l->size() > 0);
-    const Guarded & glast = (*l)[l->size()-1];
-    if(glast.inst == RULEINST_TRUE) return ATRUE;
-    if(glast.inst == RULEINST_FALSE) return AFALSE;
-
-  };
-  /** I DONT KNOW because not watched or because not true nor false */
-  l->push_back(Guarded(ri,gid));
-  return ADONTKNOW;
-};
-
-void TheoryRewriteRules::notification(Node g, bool b){
-  GuardedMap::const_iterator l = d_guardeds.find(g);
-  /** Should be a propagated node already known */
-  Assert(l != d_guardeds.end());
-  notification((*l).second,b);
-}
-
-
-void TheoryRewriteRules::notifyEq(TNode lhs, TNode rhs) {
-  GuardedMap::const_iterator ilhs = d_guardeds.find(lhs);
-  GuardedMap::const_iterator irhs = d_guardeds.find(rhs);
-  /** Should be a propagated node already known */
-  Assert(ilhs != d_guardeds.end());
-  if( irhs == d_guardeds.end() ) {
-    /** Not watched so points to the list directly */
-    d_guardeds.insertDataFromContextMemory(rhs, (*ilhs).second);
-  } else {
-    GList * const llhs = (*ilhs).second;
-    GList * const lrhs = (*irhs).second;
-    if(!(notifyIfKnown(llhs,lrhs) || notifyIfKnown(lrhs,llhs))){
-      /** If none of the two is known */
-      for(GList::const_iterator g = llhs->begin(); g != llhs->end(); ++g){
-        lrhs->push_back(*g);
-      };
-    };
-  };
-};
-
-
-Node TheoryRewriteRules::normalizeConjunction(NodeBuilder<> & conjunction){
-  Assert(conjunction.getKind() == kind::AND);
-  switch(conjunction.getNumChildren()){
-  case 0:
-    return d_true;
-  case 1:
-    return conjunction[0];
-  default:
-    return conjunction;
-  }
-
-}
-
-void explainInstantiation(const RuleInst *inst, TNode substHead, NodeBuilder<> & conjunction ){
-  TypeNode booleanType = NodeManager::currentNM()->booleanType();
-  // if the rule is directly applied by the rewriter,
-  // we should take care to use the representative that can't be directly rewritable:
-  // If "car(a)" is somewhere and we know that "a = cons(x,l)" we shouldn't
-  // add the constraint car(cons(x,l) = x because it is rewritten to x = x.
-  // But we should say cons(a) = x
-  Assert(!inst->d_matched.isNull());
-  Assert( inst->d_matched.getKind() == kind::APPLY_UF);
-  Assert( substHead.getKind() == kind::APPLY_UF );
-  Assert( inst->d_matched.getOperator() == substHead.getOperator() );
-  Assert(conjunction.getKind() == kind::AND);
-  // replace the left hand side by the term really matched
-  NodeBuilder<2> nb;
-  for(size_t i = 0,
-        iend = inst->d_matched.getNumChildren(); i < iend; ++i){
-    nb.clear( inst->d_matched[i].getType(false) == booleanType ?
-              kind::IFF : kind::EQUAL );
-    nb << inst->d_matched[i] << substHead[i];
-    conjunction << static_cast<Node>(nb);
-  }
-}
-
-Node skolemizeBody( Node f ){
-  /*TODO skolemize the subformula of s with constant or skolemize
-    directly in the body of the rewrite rule with an uninterpreted
-    function.
-   */
-  if ( f.getKind()!=EXISTS ) return f;
-  std::vector< Node > vars;
-  std::vector< Node > csts;
-  for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
-    csts.push_back( NodeManager::currentNM()->mkSkolem( "skolem_$$", f[0][i].getType(), "is from skolemizing the body of a rewrite rule" ) );
-    vars.push_back( f[0][i] );
-  }
-  return f[ 1 ].substitute( vars.begin(), vars.end(),
-                            csts.begin(), csts.end() );
-}
-
-
-void TheoryRewriteRules::propagateRule(const RuleInst * inst, TCache cache){
-  //   Debug("rewriterules") << "A rewrite rules is verified. Add lemma:";
-  Debug("rewriterules::propagate") << "propagateRule" << *inst << std::endl;
-  const RewriteRule * rule = inst->rule;
-  ++rule->nb_applied;
-  // Can be more something else than an equality in fact (eg. propagation rule)
-  Node equality = skolemizeBody(inst->substNode(*this,rule->body,cache));
-  if(propagate_as_lemma){
-    Node lemma = equality;
-    if(rule->directrr){
-      NodeBuilder<> conjunction(kind::AND);
-      explainInstantiation(inst,
-                           rule->guards.size() > 0?
-                           inst->substNode(*this,rule->guards[0],cache) : equality[0],
-                           conjunction);
-      Debug("rewriterules-directrr") << "lemma:" << lemma << " :: " << inst->d_matched;
-      //rewrite rule
-      TypeNode booleanType = NodeManager::currentNM()->booleanType();
-      if(equality[1].getType(false) == booleanType)
-        equality = inst->d_matched.iffNode(equality[1]);
-      else equality = inst->d_matched.eqNode(equality[1]);
-      lemma = normalizeConjunction(conjunction).impNode(equality);
-      Debug("rewriterules-directrr") << " -> " << lemma << std::endl;
-    }
-    else if(rule->guards.size() > 0){
-      // We can use implication for reduction rules since the head is known
-      // to be true
-      NodeBuilder<> conjunction(kind::AND);
-      substGuards(inst,cache,conjunction);
-      lemma = normalizeConjunction(conjunction).impNode(equality);
-    }
-    Debug("rewriterules::propagate") << "propagated " << lemma << std::endl;
-    getOutputChannel().lemma(lemma);
-  }else{
-    Node lemma_lit = equality;
-    if(rule->directrr && rule->guards.size() == 0)
-      lemma_lit = inst->d_matched.eqNode(equality[1]); // rewrite rules
-    lemma_lit = getValuation().ensureLiteral(lemma_lit);
-    ExplanationMap::const_iterator p = d_explanations.find(lemma_lit);
-    if(p!=d_explanations.end()) return; //Already propagated
-    bool value;
-    if(getValuation().hasSatValue(lemma_lit,value)){
-      /* Already assigned */
-      if (!value){
-        NodeBuilder<> conflict(kind::AND);
-
-        if(rule->directrr){
-          explainInstantiation(inst,
-                               rule->guards.size() > 0?
-                               inst->substNode(*this,rule->guards[0],cache) : equality[0],
-                               conflict);
-          if(rule->guards.size() > 0){
-            //reduction rule
-            Assert(rule->guards.size() == 1);
-            conflict << inst->d_matched; //this one will be two times
-          }
-        }
-        substGuards(inst,cache,conflict);
-        conflict << lemma_lit;
-        getOutputChannel().conflict(normalizeConjunction(conflict));
-      };
-    }else{
-      getOutputChannel().propagate(lemma_lit);
-      d_explanations.insert(lemma_lit, *inst);
-   };
-  };
-
-  if(simulateRewritting){
-    static NoMatchAttribute rewrittenNodeAttribute;
-    // Tag the rewritted terms
-    // for(std::vector<Node>::iterator i = rule->to_remove.begin();
-    //     i == rule->to_remove.end(); ++i){
-    //   (*i).setAttribute(rewrittenNodeAttribute,true);
-    // };
-    for(size_t i = 0; i < rule->to_remove.size(); ++i){
-      Node rewritten = inst->substNode(*this,rule->to_remove[i],cache);
-      Debug("rewriterules::simulateRewriting") << "tag " << rewritten << " as rewritten" << std::endl;
-      rewritten.setAttribute(rewrittenNodeAttribute,true);
-    };
-
-  };
-
-  if ( compute_opt && !rule->body_match.empty() ){
-
-    uf::TheoryUF* uf = static_cast<uf::TheoryUF *>(getQuantifiersEngine()->getTheoryEngine()->theoryOf( theory::THEORY_UF ));
-    eq::EqualityEngine* ee =
-      static_cast<eq::EqualityEngine*>(uf->getEqualityEngine());
-
-    //Verify that this instantiation can't immediately fire another rule
-    for(RewriteRule::BodyMatch::const_iterator p = rule->body_match.begin();
-        p != rule->body_match.end(); ++p){
-      RewriteRule * r = (*p).second;
-      // Use trigger2 since we can be in check
-      ApplyMatcher * tr = r->trigger_for_body_match;
-      Assert(tr != NULL);
-      tr->resetInstantiationRound(getQuantifiersEngine());
-      rrinst::InstMatch im;
-      TNode m = inst->substNode(*this,(*p).first, cache);
-      Assert( m.getKind() == kind::APPLY_UF );
-      ee->addTerm(m);
-      if( tr->reset(m,im,getQuantifiersEngine()) ){
-        im.d_matched = m;
-        Debug("rewriterules::matching") << "SimulatedRewrite: " << std::endl;
-        addMatchRuleTrigger(r, im);
-      }
-    }
-
-  }
-};
-
-void TheoryRewriteRules::substGuards(const RuleInst *inst,
-                                     TCache cache,
-                                     NodeBuilder<> & conjunction){
-  const RewriteRule * r = inst->rule;
-  /** Guards */ /* TODO remove the duplicate with a set like in uf? */
-  for(std::vector<Node>::const_iterator p = r->guards.begin();
-      p != r->guards.end(); ++p) {
-    Assert(!p->isNull());
-    conjunction << inst->substNode(*this,*p,cache);
-  };
-}
-
 Node TheoryRewriteRules::explain(TNode n){
-  ExplanationMap::const_iterator p = d_explanations.find(n);
-  Assert(p!=d_explanations.end(),"I forget the explanation...");
-  RuleInst inst = (*p).second;
-  const RewriteRule * rule = inst.rule;
-  TCache cache;
-  NodeBuilder<> explanation(kind::AND);
-  if(rule->directrr){
-    explainInstantiation(&inst,
-                         rule->guards.size() > 0?
-                         inst.substNode(*this,rule->guards[0],cache):
-                         inst.substNode(*this,rule->body[0]  ,cache),
-                         explanation);
-    if(rule->guards.size() > 0){
-      //reduction rule
-      Assert(rule->guards.size() == 1);
-      explanation << inst.d_matched; //this one will be two times
-    }
-  };
-  substGuards(&inst, cache ,explanation);
-  return normalizeConjunction(explanation);
-}
-
-void TheoryRewriteRules::collectModelInfo( TheoryModel* m, bool fullModel ){
 
+  return Node::null();
 }
 
-Theory::PPAssertStatus TheoryRewriteRules::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
-  //TODO: here add only to the rewriterules database for ppRewrite,
-  //and not for the general one. Otherwise rewriting that occur latter
-  //on this rewriterules will be lost. But if the rewriting of the
-  //body is not done in "in", will it be done latter after
-  //substitution? Perhaps we should add the rewriterules to the
-  //database for ppRewrite also after the subtitution at the levvel of check
-
-  // addRewriteRule(in);
-  // d_ppAssert_on = true;
-  return PP_ASSERT_STATUS_UNSOLVED;
-}
-
-TheoryRewriteRules::Statistics::Statistics():
-  d_num_rewriterules("TheoryRewriteRules::Num_RewriteRules", 0),
-  d_check("TheoryRewriteRules::Check", 0),
-  d_full_check("TheoryRewriteRules::FullCheck", 0),
-  d_poll("TheoryRewriteRules::Poll", 0),
-  d_match_found("TheoryRewriteRules::MatchFound", 0),
-  d_cache_hit("TheoryRewriteRules::CacheHit", 0),
-  d_cache_miss("TheoryRewriteRules::CacheMiss", 0)
-{
-  StatisticsRegistry::registerStat(&d_num_rewriterules);
-  StatisticsRegistry::registerStat(&d_check);
-  StatisticsRegistry::registerStat(&d_full_check);
-  StatisticsRegistry::registerStat(&d_poll);
-  StatisticsRegistry::registerStat(&d_match_found);
-  StatisticsRegistry::registerStat(&d_cache_hit);
-  StatisticsRegistry::registerStat(&d_cache_miss);
-}
+void TheoryRewriteRules::collectModelInfo( TheoryModel* m, bool fullModel ){
 
-TheoryRewriteRules::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_num_rewriterules);
-  StatisticsRegistry::unregisterStat(&d_check);
-  StatisticsRegistry::unregisterStat(&d_full_check);
-  StatisticsRegistry::unregisterStat(&d_poll);
-  StatisticsRegistry::unregisterStat(&d_match_found);
-  StatisticsRegistry::unregisterStat(&d_cache_hit);
-  StatisticsRegistry::unregisterStat(&d_cache_miss);
 }
 
-
 }/* CVC4::theory::rewriterules namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h
index 2cefe7f07..85cd9a85c 100644
--- a/src/theory/rewriterules/theory_rewriterules.h
+++ b/src/theory/rewriterules/theory_rewriterules.h
@@ -25,173 +25,17 @@
 #include "theory/theory_engine.h"
 #include "theory/quantifiers_engine.h"
 #include "context/context_mm.h"
-#include "theory/rewriterules/rr_inst_match_impl.h"
-#include "theory/rewriterules/rr_trigger.h"
-#include "theory/rewriterules/rr_inst_match.h"
 #include "util/statistics_registry.h"
-#include "theory/rewriterules/theory_rewriterules_preprocess.h"
 
 namespace CVC4 {
 namespace theory {
 namespace rewriterules {
-using namespace CVC4::theory::rrinst;
-typedef CVC4::theory::rrinst::Trigger Trigger;
-
-typedef std::hash_map<TNode, TNode, TNodeHashFunction> TCache;
-
-  enum Answer {ATRUE, AFALSE, ADONTKNOW};
-
-  class TheoryRewriteRules; /** forward */
-
-  class RewriteRule{
-  public:
-    // constant
-    const size_t id; //for debugging
-    const bool d_split;
-    mutable Trigger trigger;
-    std::vector<Node> guards;
-    mutable std::vector<Node> to_remove; /** terms to remove */
-    const Node body;
-    const TNode new_terms; /** new terms included in the body */
-    std::vector<Node> free_vars; /* free variable in the rule */
-    std::vector<Node> inst_vars; /* corresponding vars in the triggers */
-    /* After instantiating the body new match can appear (TNode
-       because is a subterm of a body on the assicaited rewrite
-       rule) */
-    typedef context::CDList< std::pair<TNode,RewriteRule* > > BodyMatch;
-    mutable BodyMatch body_match;
-    mutable ApplyMatcher * trigger_for_body_match; // used because we can be matching
-                                    // trigger when we need new match.
-                                    // So currently we use another
-                                    // trigger for that.
-
-    //context dependent
-    typedef InstMatchTrie2<true> CacheNode;
-    mutable CacheNode d_cache;
-
-    const bool directrr;
-
-    RewriteRule(TheoryRewriteRules & re,
-                Trigger & tr, ApplyMatcher * tr2,
-                std::vector<Node> & g, Node b, TNode nt,
-                std::vector<Node> & fv,std::vector<Node> & iv,
-                std::vector<Node> & to_r, bool drr);
-    RewriteRule(const RewriteRule & r) CVC4_UNUSED;
-    RewriteRule& operator=(const RewriteRule &) CVC4_UNUSED;
-    ~RewriteRule();
-
-    bool noGuard()const throw () { return guards.size() == 0; };
-    bool inCache(TheoryRewriteRules & re, rrinst::InstMatch & im)const;
-
-    void toStream(std::ostream& out) const;
-
-    /* statistics */
-    mutable size_t nb_matched;
-    mutable size_t nb_applied;
-    mutable size_t nb_propagated;
-
-  };
-
-  class RuleInst{
-  public:
-    /** The rule has at least one guard */
-    const RewriteRule* rule;
-
-    /** the substitution */
-    std::vector<Node> subst;
-
-    /** the term matched (not null if mono-pattern and direct-rr) */
-    Node d_matched;
-
-    /** Rule an instantiation with the given match */
-    RuleInst(TheoryRewriteRules & re, const RewriteRule* r,
-             std::vector<Node> & inst_subst,
-             Node matched);
-    RuleInst():rule(NULL){} // Dumb
-
-    Node substNode(const TheoryRewriteRules & re, TNode r, TCache cache) const;
-    size_t findGuard(TheoryRewriteRules & re, size_t start)const;
-
-    void toStream(std::ostream& out) const;
-
-    bool alreadyRewritten(TheoryRewriteRules & re) const;
-  };
-
-/** A pair? */
-  class Guarded {
-  public:
-    /** The backtracking is done somewhere else */
-    const size_t d_guard; /* the id of the guard */
-
-    /** The shared instantiation data */
-    const RuleInst* inst;
-
-    void nextGuard(TheoryRewriteRules & re)const;
-
-    /** start indicate the first guard which is not true */
-    Guarded(const RuleInst* ri, const size_t start);
-    Guarded(const Guarded & g);
-    /** Should be ssigned by a good garded after */
-    Guarded();
-
-    ~Guarded(){};
-    void destroy(){};
-  };
-
-template<class T>
-class CleanUpPointer{
-public:
-  inline void operator()(T** e){
-    delete(*e);
-  };
-};
 
 class TheoryRewriteRules : public Theory {
 private:
 
   KEEP_STATISTIC(TimerStat, d_theoryTime, "theory::rewriterules::theoryTime");
-
-  /** list of all rewrite rules */
-  /* std::vector< Node > d_rules; */
-  // typedef std::vector< std::pair<Node, Trigger > > Rules;
-  typedef context::CDList< RewriteRule *,
-                           CleanUpPointer<RewriteRule >,
-                           std::allocator< RewriteRule * > > Rules;
-  Rules d_rules;
-  typedef context::CDList< RuleInst *,
-                           CleanUpPointer<RuleInst>,
-                           std::allocator< RuleInst * > > RuleInsts;
-  RuleInsts d_ruleinsts;
-
-  /** The GList* will lead too memory leaks since that doesn't use
-      CDChunckList */
-  typedef context::CDList< Guarded > GList;
-  typedef context::CDHashMap<Node, GList *, NodeHashFunction> GuardedMap;
-  GuardedMap d_guardeds;
-
-  /* In order to not monopolize, the system slow down himself: If a
-     guard stored in d_guardeds become true or false, it waits
-     checkSlowdown(=10) checks before checking again if some guard take a
-     value. At FULL_EFFORT regardless of d_checkLevel it check the
-     guards
-   */
-  context::CDO<size_t> d_checkLevel;
-
-  /** explanation */
-  typedef context::CDHashMap<Node, RuleInst , NodeHashFunction> ExplanationMap;
-  ExplanationMap d_explanations;
-
-  /** new instantiation must be cleared at each conflict used only
-      inside check */
-  typedef std::vector< RuleInst* > QRuleInsts;
-  QRuleInsts d_ruleinsts_to_add;
-  bool d_ppAssert_on; //Indicate if a ppAssert have been done
-
  public:
-  /** true and false for predicate */
-  Node d_true;
-  Node d_false;
-
   /** Constructs a new instance of TheoryRewriteRules
       w.r.t. the provided context.*/
   TheoryRewriteRules(context::Context* c,
@@ -209,76 +53,6 @@ private:
     return "THEORY_REWRITERULES";
   }
 
-  Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
-
-  bool ppDontRewriteSubterm(TNode atom) { return true; }
-
-
- private:
-  void registerQuantifier( Node n );
-
- public:
-  /* TODO modify when notification will be available */
-  void notification( Node n, bool b);
-
-  Trigger createTrigger( TNode n, std::vector<Node> & pattern );
-
-  /** return if the guard (already substituted) is known true or false
-      or unknown. In the last case it add the Guarded(rid,gid) to the watch
-      list of this guard */
-  Answer addWatchIfDontKnow(Node g, const RuleInst* r, const size_t gid);
-
-  /** An instantiation of a rule is fired (all guards true) we
-      propagate the body. That can be done by theory propagation if
-      possible or by lemmas.
-   */
-  void propagateRule(const RuleInst * r, TCache cache);
-
-  /** Auxiliary functions */
-private:
-  /** A guard is verify, notify the Guarded */
-  void notification(GList * const lpropa, bool b);
-  /* If two guards becomes equals we should notify if one of them is
-     already true */
-  bool notifyIfKnown(const GList * const ltested, GList * const lpropa);
-
-  void substGuards(const RuleInst * inst,
-                   TCache cache,
-                   NodeBuilder<> & conjunction);
-
-  void addRewriteRule(const Node r);
-  void computeMatchBody ( const RewriteRule * r, size_t start = 0);
-  void addMatchRuleTrigger(const RewriteRule* r,
-                           rrinst::InstMatch & im, bool delay = true);
-
-  Node normalizeConjunction(NodeBuilder<> & conjunction);
-
-  /* rewrite pattern */
-  typedef std::hash_map< Node, rewriter::RRPpRewrite*, NodeHashFunction > RegisterRRPpRewrite;
-  RegisterRRPpRewrite d_registeredRRPpRewrite;
-
-  bool addRewritePattern(TNode pattern, TNode body,
-                         rewriter::Subst & pvars,
-                         rewriter::Subst & vars);
-
-  //create inst variable
-  std::vector<Node> createInstVariable( Node r, std::vector<Node> & vars );
-
-    /** statistics class */
-  class Statistics {
-  public:
-    IntStat d_num_rewriterules;
-    IntStat d_check;
-    IntStat d_full_check;
-    IntStat d_poll;
-    IntStat d_match_found;
-    IntStat d_cache_hit;
-    IntStat d_cache_miss;
-    Statistics();
-    ~Statistics();
-  };
-  Statistics d_statistics;
-
 };/* class TheoryRewriteRules */
 
 }/* CVC4::theory::rewriterules namespace */
diff --git a/src/theory/rewriterules/theory_rewriterules_type_rules.h b/src/theory/rewriterules/theory_rewriterules_type_rules.h
index fa6bb2227..28b10f91f 100644
--- a/src/theory/rewriterules/theory_rewriterules_type_rules.h
+++ b/src/theory/rewriterules/theory_rewriterules_type_rules.h
@@ -26,89 +26,7 @@ namespace CVC4 {
 namespace theory {
 namespace rewriterules {
 
-class RewriteRuleTypeRule {
-public:
 
-  /**
-   * Compute the type for (and optionally typecheck) a term belonging
-   * to the theory of rewriterules.
-   *
-   * @param nodeManager the NodeManager in use
-   * @param n the node to compute the type of
-   * @param check if true, the node's type should be checked as well
-   * as computed.
-   */
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check)
-    throw(TypeCheckingExceptionPrivate) {
-    Debug("typecheck-r") << "type check for rr " << n << std::endl;
-    Assert(n.getKind() == kind::REWRITE_RULE && n.getNumChildren()==3 );
-    if( check ){
-      if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){
-        throw TypeCheckingExceptionPrivate(n[0],
-                     "first argument of rewrite rule is not bound var list");
-      }
-      if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){
-        throw TypeCheckingExceptionPrivate(n[1],
-                     "guard of rewrite rule is not an actual guard");
-      }
-      if( n[2].getType(check) !=
-          TypeNode(nodeManager->mkTypeConst<TypeConstant>(RRHB_TYPE))){
-        throw TypeCheckingExceptionPrivate(n[2],
-                     "not a correct rewrite rule");
-      }
-    }
-    return nodeManager->booleanType();
-  }
-};/* class RewriteRuleTypeRule */
-
-
-class RRRewriteTypeRule {
-public:
-
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw(TypeCheckingExceptionPrivate) {
-    Assert(n.getKind() == kind::RR_REWRITE );
-    if( check ){
-      if( n[0].getType(check)!=n[1].getType(check) ){
-        throw TypeCheckingExceptionPrivate(n,
-                     "terms of rewrite rule are not equal");
-      }
-      if( n.getNumChildren() == 3 && n[2].getType(check)!=nodeManager->instPatternListType() ){
-        throw TypeCheckingExceptionPrivate(n, "third argument of rewrite rule is not instantiation pattern list");
-      }
-      if( n[0].getKind()!=kind::APPLY_UF ){
-        throw TypeCheckingExceptionPrivate(n[0], "head of rewrite rules must start with an uninterpreted symbols. If you want to write a propagation rule, add the guard [true] for disambiguation");
-      }
-    }
-    return TypeNode(nodeManager->mkTypeConst<TypeConstant>(RRHB_TYPE));
-  }
-};/* struct QuantifierReductionRuleRule */
-
-class RRRedDedTypeRule {
-public:
-
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw(TypeCheckingExceptionPrivate) {
-    Assert(n.getKind() == kind::RR_REDUCTION ||
-           n.getKind() == kind::RR_DEDUCTION );
-    if( check ){
-      if( n[ 0 ].getType(check)!=nodeManager->booleanType() ){
-        throw TypeCheckingExceptionPrivate(n, "head of reduction rule is not boolean");
-      }
-      if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){
-        throw TypeCheckingExceptionPrivate(n, "body of reduction rule is not boolean");
-      }
-      if( n.getNumChildren() == 3 && n[2].getType(check)!=nodeManager->instPatternListType() ){
-        throw TypeCheckingExceptionPrivate(n, "third argument of rewrite rule is not instantiation pattern list");
-      }
-      if( n.getNumChildren() < 3 && n[ 0 ] == nodeManager->mkConst<bool>(true) ){
-        throw TypeCheckingExceptionPrivate(n, "A rewrite rule must have one head or one trigger at least");
-      }
-    }
-    return TypeNode(nodeManager->mkTypeConst<TypeConstant>(RRHB_TYPE));
-  }
-};/* struct QuantifierReductionRuleRule */
 
 }/* CVC4::theory::rewriterules namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 80d1152da..45c9402ab 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -52,7 +52,7 @@
 
 #include "theory/uf/equality_engine.h"
 
-#include "theory/rewriterules/efficient_e_matching.h"
+//#include "theory/rewriterules/efficient_e_matching.h"
 
 #include "proof/proof_manager.h"
 
@@ -95,7 +95,7 @@ void TheoryEngine::eqNotifyNewClass(TNode t){
 void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){
   //TODO: add notification to efficient E-matching
   if( d_logicInfo.isQuantified() ){
-    d_quantEngine->getEfficientEMatcher()->merge( t1, t2 );
+    //d_quantEngine->getEfficientEMatcher()->merge( t1, t2 );
     if( options::quantConflictFind() ){
       d_quantEngine->getConflictFind()->merge( t1, t2 );
     }
diff --git a/test/regress/regress0/push-pop/bug326.smt2 b/test/regress/regress0/push-pop/bug326.smt2
index 8fe88e9f5..51d60e920 100644
--- a/test/regress/regress0/push-pop/bug326.smt2
+++ b/test/regress/regress0/push-pop/bug326.smt2
@@ -31,7 +31,7 @@
 (check-sat)
 (pop)
 
-; EXPECT: sat
+; EXPECT: unknown
 (push);;sat
 (assert (and (not (R e1 e3)) (R e4 e1)))
 (check-sat)
diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am
index b7eac2535..5aba7dcec 100644
--- a/test/regress/regress0/rewriterules/Makefile.am
+++ b/test/regress/regress0/rewriterules/Makefile.am
@@ -1,4 +1,4 @@
-CVC4_REGRESSION_ARGS ?= --efficient-e-matching
+CVC4_REGRESSION_ARGS ?= --rewrite-rules
 export CVC4_REGRESSION_ARGS
 
 # don't override a BINARY imported from a personal.mk
@@ -23,10 +23,11 @@ MAKEFLAGS = -k
 # put it below in "TESTS +="
 TESTS =	\
 	length_trick.smt2 length_trick2.smt2 length_gen_020.smt2 \
-	datatypes.smt2 datatypes_sat.smt2 set_A_new_fast_tableau-base.smt2 \
-	set_A_new_fast_tableau-base_sat.smt2 relation.smt2 simulate_rewriting.smt2 \
-	reachability_back_to_the_future.smt2 native_arrays.smt2
-# reachability_bbttf_eT_arrays.smt2
+	datatypes.smt2 datatypes_sat.smt2 reachability_back_to_the_future.smt2 \
+        relation.smt2 simulate_rewriting.smt2 \
+        native_arrays.smt2
+
+# reachability_bbttf_eT_arrays.smt2 set_A_new_fast_tableau-base.smt2 set_A_new_fast_tableau-base_sat.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/rewriterules/simulate_rewriting.smt2 b/test/regress/regress0/rewriterules/simulate_rewriting.smt2
index d1d88a549..838c0cd16 100644
--- a/test/regress/regress0/rewriterules/simulate_rewriting.smt2
+++ b/test/regress/regress0/rewriterules/simulate_rewriting.smt2
@@ -1,6 +1,6 @@
 ;; A new fast tableau-base ... Domenico Cantone et Calogero G.Zarba
 (set-logic AUFLIA)
-(set-info :status sat)
+(set-info :status unsat)
 
 (declare-sort elt1 0)
 (declare-sort elt2 0)