Initial refactor of rewrite rules, make theory_rewriterules empty theory. Push kinds to quantifiers/kinds, rewrite rewrite rules in rewriter.

Fix rewrite rule attribute, refactor QCF, instantiation engine does not register rewrite rules, minor clean up.

QCF is now functional backend to rewrite rules. Support boolean variables in QCF.  Change check-model to ignore rewrite rules.  Incorporate some fixes from master.

Move rewrite of rewrite rules from rewriter to preprocessor, attribute becomes pattern.

Minor fixes to QCF/rewrite engine, removes RE on last call approach.  Add option for one inst per round in RE.

Merging rewrite rules into master, check-model current fails on 3 FMF regressions.

Fix check-model issue, a line of code was omitted during merge.

4 files changed, 4 insertions, 894 deletions

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 */