Remove quantifiers rewrite rules infrastructure (#3754)

1 files changed, 1 insertions, 20 deletions

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)