Remove quantifiers rewrite rules infrastructure (#3754)

10 files changed, 19 insertions, 693 deletions

diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds
index dc11ed562..1534d2d4d 100644
--- a/src/theory/quantifiers/kinds
+++ b/src/theory/quantifiers/kinds
@@ -55,25 +55,4 @@ typerule INST_ATTRIBUTE ::CVC4::theory::quantifiers::QuantifierInstAttributeType
 typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule 
 typerule INST_CLOSURE ::CVC4::theory::quantifiers::QuantifierInstClosureTypeRule 
 
-# for rewrite rules
-# types...
-sort RRHB_TYPE \
-    Cardinality::INTEGERS \
-    not-well-founded \
-    "head and body of the rule type (for rewrite-rules theory)"
-
-# operators...
-
-# variables, guards, RR_REWRITE/REDUCTION_RULE/DEDUCTION_RULE
-operator REWRITE_RULE 3 "general rewrite rule (for rewrite-rules theory)"
-#HEAD/BODY/TRIGGER
-operator RR_REWRITE 2:3 "actual rewrite rule (for rewrite-rules theory)"
-operator RR_REDUCTION 2:3 "actual reduction rule (for rewrite-rules theory)"
-operator RR_DEDUCTION 2:3 "actual deduction rule (for rewrite-rules theory)"
-
-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/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 0e6eb1581..af4011bd9 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -16,7 +16,6 @@
 
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
-#include "theory/quantifiers/rewrite_engine.h"
 #include "theory/quantifiers/sygus/synth_engine.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
@@ -80,12 +79,6 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve
     Trace("quant-attr-debug") << "Set instantiation level " << n << " to " << lvl << std::endl;
     QuantInstLevelAttribute qila;
     n.setAttribute( qila, lvl );
-  }else if( attr=="rr-priority" ){
-    Assert(node_values.size() == 1);
-    uint64_t lvl = node_values[0].getConst<Rational>().getNumerator().getLong();
-    Trace("quant-attr-debug") << "Set rewrite rule priority " << n << " to " << lvl << std::endl;
-    RrPriorityAttribute rrpa;
-    n.setAttribute( rrpa, lvl );
   }else if( attr=="quant-elim" ){
     Trace("quant-attr-debug") << "Set quantifier elimination " << n << std::endl;
     QuantElimAttribute qea;
@@ -97,21 +90,6 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve
   }
 }
 
-bool QuantAttributes::checkRewriteRule( Node q ) {
-  return !getRewriteRule( q ).isNull();
-}
-
-Node QuantAttributes::getRewriteRule( Node q ) {
-  if (q.getKind() == FORALL && q.getNumChildren() == 3
-      && q[2][0].getNumChildren() > 0
-      && q[2][0][0].getKind() == REWRITE_RULE)
-  {
-    return q[2][0][0];
-  }else{
-    return Node::null();
-  }
-}
-
 bool QuantAttributes::checkFunDef( Node q ) {
   return !getFunDefHead( q ).isNull();
 }
@@ -275,10 +253,6 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
           qa.d_qinstLevel = avar.getAttribute(QuantInstLevelAttribute());
           Trace("quant-attr") << "Attribute : quant inst level " << qa.d_qinstLevel << " : " << q << std::endl;
         }
-        if( avar.hasAttribute(RrPriorityAttribute()) ){
-          qa.d_rr_priority = avar.getAttribute(RrPriorityAttribute());
-          Trace("quant-attr") << "Attribute : rr priority " << qa.d_rr_priority << " : " << q << std::endl;
-        }
         if( avar.getAttribute(QuantElimAttribute()) ){
           Trace("quant-attr") << "Attribute : quantifier elimination : " << q << std::endl;
           qa.d_quant_elim = true;
@@ -294,11 +268,6 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
           qa.d_qid_num = avar;
           Trace("quant-attr") << "Attribute : id number " << qa.d_qid_num.getAttribute(QuantIdNumAttribute()) << " : " << q << std::endl;
         }
-        if( avar.getKind()==REWRITE_RULE ){
-          Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl;
-          Assert(i == 0);
-          qa.d_rr = avar;
-        }
       }
     }
   }
@@ -349,15 +318,6 @@ int QuantAttributes::getQuantInstLevel( Node q ) {
   }
 }
 
-int QuantAttributes::getRewriteRulePriority( Node q ) {
-  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
-  if( it==d_qattr.end() ){
-    return -1;
-  }else{
-    return it->second.d_rr_priority;
-  }
-}
-
 bool QuantAttributes::isQuantElim( Node q ) {
   std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
   if( it==d_qattr.end() ){
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 827c5e7f4..fc0f85956 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -111,7 +111,6 @@ struct QAttributes
         d_conjecture(false),
         d_axiom(false),
         d_sygus(false),
-        d_rr_priority(-1),
         d_qinstLevel(-1),
         d_quant_elim(false),
         d_quant_elim_partial(false)
@@ -120,9 +119,6 @@ struct QAttributes
   ~QAttributes(){}
   /** does the quantified formula have a pattern? */
   bool d_hasPattern;
-  /** if non-null, this is the rewrite rule representation of the quantified
-   * formula */
-  Node d_rr;
   /** is this formula marked a conjecture? */
   bool d_conjecture;
   /** is this formula marked an axiom? */
@@ -134,8 +130,6 @@ struct QAttributes
   bool d_sygus;
   /** side condition for sygus conjectures */
   Node d_sygusSideCondition;
-  /** if a rewrite rule, then this is the priority value for the rewrite rule */
-  int d_rr_priority;
   /** stores the maximum instantiation level allowed for this quantified formula
    * (-1 means allow any) */
   int d_qinstLevel;
@@ -150,8 +144,6 @@ struct QAttributes
   Node d_name;
   /** the quantifier id associated with this formula */
   Node d_qid_num;
-  /** is this quantified formula a rewrite rule? */
-  bool isRewriteRule() const { return !d_rr.isNull(); }
   /** is this quantified formula a function definition? */
   bool isFunDef() const { return !d_fundef_f.isNull(); }
   /**
@@ -193,10 +185,6 @@ public:
   /** compute the attributes for q */
   void computeAttributes(Node q);
 
-  /** is quantifier treated as a rewrite rule? */
-  static bool checkRewriteRule( Node q );
-  /** get the rewrite rule associated with the quanfied formula */
-  static Node getRewriteRule( Node q );
   /** is fun def */
   static bool checkFunDef( Node q );
   /** is fun def */
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index e35595287..e2ee99ceb 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -185,15 +185,13 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
       //compute attributes
       QAttributes qa;
       QuantAttributes::computeQuantAttributes( in, qa );
-      if( !qa.isRewriteRule() ){
-        for( int op=0; op<COMPUTE_LAST; op++ ){
-          if( doOperation( in, op, qa ) ){
-            ret = computeOperation( in, op, qa );
-            if( ret!=in ){
-              rew_op = op;
-              status = REWRITE_AGAIN_FULL;
-              break;
-            }
+      for( int op=0; op<COMPUTE_LAST; op++ ){
+        if( doOperation( in, op, qa ) ){
+          ret = computeOperation( in, op, qa );
+          if( ret!=in ){
+            rew_op = op;
+            status = REWRITE_AGAIN_FULL;
+            break;
           }
         }
       }
@@ -2088,102 +2086,6 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut
   }
 }
 
-
-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 );
-    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_ATTRIBUTE, r );
-  }
-  patternListB << static_cast<Node>(patternB);
-  forallB << static_cast<Node>(patternListB);
-  Node rn = (Node) forallB;
-
-  return rn;
-}
-
 bool QuantifiersRewriter::isPrenexNormalForm( Node n ) {
   if( n.getKind()==FORALL ){
     return n[1].getKind()!=FORALL && isPrenexNormalForm( n[1] );
@@ -2272,17 +2174,14 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
 
 Node QuantifiersRewriter::preprocess( Node n, bool isInst ) {
   Node prev = n;
-  if( n.getKind() == kind::REWRITE_RULE ){
-    n = quantifiers::QuantifiersRewriter::rewriteRewriteRule( n );
-  }else{
-    if( options::preSkolemQuant() ){
-      if( !isInst || !options::preSkolemQuantNested() ){
-        Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl;
-        //apply pre-skolemization to existential quantifiers
-        std::vector< TypeNode > fvTypes;
-        std::vector< TNode > fvs;
-        n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs );
-      }
+
+  if( options::preSkolemQuant() ){
+    if( !isInst || !options::preSkolemQuantNested() ){
+      Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl;
+      //apply pre-skolemization to existential quantifiers
+      std::vector< TypeNode > fvTypes;
+      std::vector< TNode > fvs;
+      n = preSkolemizeQuantifiers( prev, true, fvTypes, fvs );
     }
   }
   //pull all quantifiers globally
@@ -2291,7 +2190,7 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) {
   {
     Trace("quantifiers-prenex") << "Prenexing : " << n << std::endl;
     std::map< unsigned, std::map< Node, Node > > visited;
-    n = quantifiers::QuantifiersRewriter::computePrenexAgg( n, true, visited );
+    n = computePrenexAgg( n, true, visited );
     n = Rewriter::rewrite( n );
     Trace("quantifiers-prenex") << "Prenexing returned : " << n << std::endl;
     //Assert( isPrenexNormalForm( n ) );
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index e8f069882..69e057c76 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -204,7 +204,6 @@ private:
 private:
   static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs);
 public:
-  static Node rewriteRewriteRule( Node r );
   static bool isPrenexNormalForm( Node n );
   /** preprocess
    *
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
deleted file mode 100644
index 9903456c9..000000000
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ /dev/null
@@ -1,309 +0,0 @@
-/*********************                                                        */
-/*! \file rewrite_engine.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Rewrite engine module
- **
- ** This class manages rewrite rules for quantifiers
- **/
-
-#include "theory/quantifiers/rewrite_engine.h"
-
-#include "options/quantifiers_options.h"
-#include "theory/quantifiers_engine.h"
-
-using namespace CVC4;
-using namespace std;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace CVC4::kind;
-
-struct PrioritySort {
-  std::vector< double > d_priority;
-  bool operator() (int i,int j) {
-    return d_priority[i] < d_priority[j];
-  }
-};
-
-RewriteEngine::RewriteEngine(context::Context* c,
-                             QuantifiersEngine* qe,
-                             QuantConflictFind* qcf)
-    : QuantifiersModule(qe), d_qcf(qcf)
-{
-  d_needsSort = false;
-}
-
-double RewriteEngine::getPriority( Node f ) {
-  Node rr = QuantAttributes::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 ){
-    return deterministic ? 1.0 : 4.0;
-  }else if( rrr.getKind()==RR_REDUCTION ){
-    return deterministic ? 2.0 : 5.0;
-  }else{
-    return 6.0;
-  }
-
-  //return deterministic ? 0.0 : 1.0;
-}
-
-bool RewriteEngine::needsCheck( Theory::Effort e ){
-  return e==Theory::EFFORT_FULL;
-  //return e>=Theory::EFFORT_LAST_CALL;
-}
-
-void RewriteEngine::check(Theory::Effort e, QEffort quant_e)
-{
-  if (quant_e == QEFFORT_STANDARD)
-  {
-    Assert(!d_quantEngine->inConflict());
-    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
-    int addedLemmas = 0;
-    //per priority level
-    int index = 0;
-    bool success = true;
-    while( !d_quantEngine->inConflict() && success && index<(int)d_priority_order.size() ) {
-      addedLemmas += checkRewriteRule( d_priority_order[index], e );
-      index++;
-      if( index<(int)d_priority_order.size() ){
-        success = addedLemmas==0 || getPriority( d_priority_order[index] )==getPriority( d_priority_order[index-1] );
-      }
-    }
-
-    Trace("rewrite-engine") << "Finished rewrite engine, added " << addedLemmas << " lemmas." << std::endl;
-  }
-}
-
-int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) {
-  Trace("rewrite-engine-inst") << "Check " << d_qinfo_n[f] << ", priority = " << getPriority( f ) << ", effort = " << e << "..." << std::endl;
-
-  // get the proper quantifiers info
-  std::map<Node, QuantInfo>::iterator it = d_qinfo.find(f);
-  if (it == d_qinfo.end())
-  {
-    Trace("rewrite-engine-inst-debug") << "...No qinfo." << std::endl;
-    return 0;
-  }
-  // reset QCF module
-  QuantInfo* qi = &it->second;
-  if (!qi->matchGeneratorIsValid())
-  {
-    Trace("rewrite-engine-inst-debug") << "...Invalid qinfo." << std::endl;
-    return 0;
-  }
-  d_qcf->setEffort(QuantConflictFind::EFFORT_CONFLICT);
-  Node rr = QuantAttributes::getRewriteRule(f);
-  Trace("rewrite-engine-inst-debug") << "   Reset round..." << std::endl;
-  qi->reset_round(d_qcf);
-  Trace("rewrite-engine-inst-debug") << "   Get matches..." << std::endl;
-  int addedLemmas = 0;
-  while (!d_quantEngine->inConflict() && qi->getNextMatch(d_qcf)
-         && (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(d_qcf))
-    {
-      bool doContinue = false;
-      bool success = true;
-      int tempAddedLemmas = 0;
-      while (!d_quantEngine->inConflict() && tempAddedLemmas == 0 && success
-             && (addedLemmas == 0 || !options::rrOneInstPerRound()))
-      {
-        success = qi->completeMatch(d_qcf, assigned, doContinue);
-        doContinue = true;
-        if (success)
-        {
-          Trace("rewrite-engine-inst-debug")
-              << "   Construct match..." << std::endl;
-          std::vector<Node> inst;
-          qi->getMatch(inst);
-          if (Trace.isOn("rewrite-engine-inst-debug"))
-          {
-            Trace("rewrite-engine-inst-debug")
-                << "   Add instantiation..." << std::endl;
-            for (unsigned i = 0, nchild = f[0].getNumChildren(); i < nchild;
-                 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->getInstantiate()->addInstantiation(f, inst))
-          {
-            addedLemmas++;
-            tempAddedLemmas++;
-          }
-          else
-          {
-            Trace("rewrite-engine-inst-debug") << "   - failed." << std::endl;
-          }
-          Trace("rewrite-engine-inst-debug")
-              << "   Get next completion..." << std::endl;
-        }
-      }
-      Trace("rewrite-engine-inst-debug")
-          << "   - failed to complete." << std::endl;
-    }
-    else
-    {
-      Trace("rewrite-engine-inst-debug")
-          << "   - match is spurious." << std::endl;
-    }
-    Trace("rewrite-engine-inst-debug") << "   Get next match..." << std::endl;
-  }
-  d_quantEngine->d_statistics.d_instantiations_rr += addedLemmas;
-  Trace("rewrite-engine-inst") << "-> Generated " << addedLemmas << " lemmas." << std::endl;
-  return addedLemmas;
-}
-
-void RewriteEngine::registerQuantifier( Node f ) {
-  Node rr = QuantAttributes::getRewriteRule( f );
-  if (rr.isNull())
-  {
-    return;
-  }
-  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[f] = rr;
-  d_needsSort = true;
-  Trace("rr-register") << "  guard is : " << d_rr[f][1] << std::endl;
-
-  std::vector<Node> qcfn_c;
-
-  std::vector<Node> bvl;
-  bvl.insert(bvl.end(), f[0].begin(), f[0].end());
-
-  NodeManager* nm = NodeManager::currentNM();
-  std::vector<Node> cc;
-  // add patterns
-  for (unsigned i = 1, nchild = f[2].getNumChildren(); i < nchild; i++)
-  {
-    std::vector<Node> nc;
-    for (const Node& pat : f[2][i])
-    {
-      Node nn;
-      Node nbv = nm->mkBoundVar(pat.getType());
-      if (pat.getType().isBoolean() && pat.getKind() != APPLY_UF)
-      {
-        nn = pat.negate();
-      }
-      else
-      {
-        nn = pat.eqNode(nbv).negate();
-        bvl.push_back(nbv);
-      }
-      nc.push_back(nn);
-    }
-    if (!nc.empty())
-    {
-      Node n = nc.size() == 1 ? nc[0] : nm->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(nm->mkNode(BOUND_VAR_LIST, bvl));
-
-  std::vector<Node> body_c;
-  // add the guards
-  if (d_rr[f][1].getKind() == AND)
-  {
-    for (const Node& g : d_rr[f][1])
-    {
-      if (MatchGen::isHandled(g))
-      {
-        body_c.push_back(g.negate());
-      }
-    }
-  }
-  else if (d_rr[f][1] != d_quantEngine->getTermUtil()->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] : nm->mkNode(AND, cc));
-  // make the body
-  qcfn_c.push_back(body_c.size() == 1 ? body_c[0] : nm->mkNode(OR, body_c));
-  // make the quantified formula
-  d_qinfo_n[f] = nm->mkNode(FORALL, qcfn_c);
-  Trace("rr-register") << "  qcf formula is : " << d_qinfo_n[f] << std::endl;
-  d_qinfo[f].initialize(d_qcf, d_qinfo_n[f], d_qinfo_n[f][1]);
-}
-
-void RewriteEngine::assertNode( Node n ) {
-
-}
-
-bool RewriteEngine::checkCompleteFor( Node q ) { 
-  // by semantics of rewrite rules, saturation -> SAT 
-  return std::find( d_rr_quant.begin(), d_rr_quant.end(), q )!=d_rr_quant.end();
-}
-
-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->getTermUtil()->substituteBoundVariablesToInstConstants(
-            n, q);
-    d_inst_const_node[q][n] = nn;
-    return nn;
-  }else{
-    return it->second;
-  }
-}
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
deleted file mode 100644
index 29aba0f1a..000000000
--- a/src/theory/quantifiers/rewrite_engine.h
+++ /dev/null
@@ -1,86 +0,0 @@
-/*********************                                                        */
-/*! \file rewrite_engine.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
-**/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__REWRITE_ENGINE_H
-#define CVC4__REWRITE_ENGINE_H
-
-#include <map>
-#include <vector>
-
-#include "expr/attribute.h"
-#include "theory/quantifiers/ematching/trigger.h"
-#include "theory/quantifiers/quant_conflict_find.h"
-#include "theory/quantifiers/quant_util.h"
-
-namespace CVC4 {
-namespace theory {
-
-/**
- * An attribute for marking a priority value for rewrite rules.
- */
-struct RrPriorityAttributeId
-{
-};
-typedef expr::Attribute<RrPriorityAttributeId, uint64_t> RrPriorityAttribute;
-
-namespace quantifiers {
-
-class RewriteEngine : public QuantifiersModule
-{
-  std::vector< Node > d_rr_quant;
-  std::vector< Node > d_priority_order;
-  std::map< Node, Node > d_rr;
-  /** 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, Theory::Effort e );
-
- public:
-  RewriteEngine(context::Context* c,
-                QuantifiersEngine* qe,
-                QuantConflictFind* qcf);
-
-  bool needsCheck(Theory::Effort e) override;
-  void check(Theory::Effort e, QEffort quant_e) override;
-  void registerQuantifier(Node f) override;
-  void assertNode(Node n) override;
-  bool checkCompleteFor(Node q) override;
-  /** Identify this module */
-  std::string identify() const override { return "RewriteEngine"; }
-
- private:
-  /**
-   * A pointer to the quantifiers conflict find module of the quantifiers
-   * engine. This is the module that computes instantiations for rewrite rule
-   * quantifiers.
-   */
-  QuantConflictFind* d_qcf;
-};
-
-}
-}
-}
-
-#endif
diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h
index a83dbf541..e2c9043a1 100644
--- a/src/theory/quantifiers/theory_quantifiers_type_rules.h
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h
@@ -141,91 +141,6 @@ struct QuantifierInstClosureTypeRule {
   }
 };/* struct QuantifierInstClosureTypeRule */
 
-
-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)
-  {
-    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)
-  {
-    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)
-  {
-    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 c7eafc3b8..80a493496 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -30,7 +30,6 @@
 #include "theory/quantifiers/quant_conflict_find.h"
 #include "theory/quantifiers/quant_split.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
-#include "theory/quantifiers/rewrite_engine.h"
 #include "theory/quantifiers/sygus/synth_engine.h"
 #include "theory/sep/theory_sep.h"
 #include "theory/theory_engine.h"
@@ -53,7 +52,6 @@ class QuantifiersEnginePrivate
         d_model_engine(nullptr),
         d_bint(nullptr),
         d_qcf(nullptr),
-        d_rr_engine(nullptr),
         d_sg_gen(nullptr),
         d_synth_e(nullptr),
         d_lte_part_inst(nullptr),
@@ -81,8 +79,6 @@ class QuantifiersEnginePrivate
   std::unique_ptr<quantifiers::BoundedIntegers> d_bint;
   /** Conflict find mechanism for quantifiers */
   std::unique_ptr<quantifiers::QuantConflictFind> d_qcf;
-  /** rewrite rules utility */
-  std::unique_ptr<quantifiers::RewriteEngine> d_rr_engine;
   /** subgoal generator */
   std::unique_ptr<quantifiers::ConjectureGenerator> d_sg_gen;
   /** ceg instantiation */
@@ -111,7 +107,7 @@ class QuantifiersEnginePrivate
                   bool& needsBuilder)
   {
     // add quantifiers modules
-    if (options::quantConflictFind() || options::quantRewriteRules())
+    if (options::quantConflictFind())
     {
       d_qcf.reset(new quantifiers::QuantConflictFind(qe, c));
       modules.push_back(d_qcf.get());
@@ -150,11 +146,6 @@ class QuantifiersEnginePrivate
       // finite model finder has special ways of building the model
       needsBuilder = true;
     }
-    if (options::quantRewriteRules())
-    {
-      d_rr_engine.reset(new quantifiers::RewriteEngine(c, qe, d_qcf.get()));
-      modules.push_back(d_rr_engine.get());
-    }
     if (options::ltePartialInst())
     {
       d_lte_part_inst.reset(new quantifiers::LtePartialInst(qe, c));
@@ -397,16 +388,6 @@ void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m, int priority )
 
 void QuantifiersEngine::setOwner(Node q, quantifiers::QAttributes& qa)
 {
-  if (!qa.d_rr.isNull())
-  {
-    if (d_private->d_rr_engine.get() == nullptr)
-    {
-      Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : "
-                          << q << std::endl;
-    }
-    // set rewrite engine as owner
-    setOwner(q, d_private->d_rr_engine.get(), 2);
-  }
   if (qa.d_sygus || (options::sygusRecFun() && !qa.d_fundef_f.isNull()))
   {
     if (d_private->d_synth_e.get() == nullptr)
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 3b11d8e54..6a404104f 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -35,7 +35,7 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
 
   Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
 
-  if ((parent.isClosure() || parent.getKind() == kind::REWRITE_RULE
+  if ((parent.isClosure()
        || parent.getKind() == kind::SEP_STAR
        || parent.getKind() == kind::SEP_WAND
        || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
@@ -178,7 +178,7 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
 
   Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
 
-  if ((parent.isClosure() || parent.getKind() == kind::REWRITE_RULE
+  if ((parent.isClosure()
        || parent.getKind() == kind::SEP_STAR
        || parent.getKind() == kind::SEP_WAND
        || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())