5 files changed, 6 insertions, 78 deletions
diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index e00bc957f..9070ed51d 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -293,39 +293,6 @@ void CandidateRewriteDatabase::setExtendedRewriter(ExtendedRewriter* er)
   d_ext_rewrite = er;
 }
 
-CandidateRewriteDatabaseGen::CandidateRewriteDatabaseGen(
-    std::vector<Node>& vars, unsigned nsamples)
-    : d_qe(nullptr), d_vars(vars.begin(), vars.end()), d_nsamples(nsamples)
-{
-}
-
-bool CandidateRewriteDatabaseGen::addTerm(Node n, std::ostream& out)
-{
-  ExtendedRewriter* er = &d_ext_rewrite;
-  Node nr;
-  if (er == nullptr)
-  {
-    nr = Rewriter::rewrite(n);
-  }
-  else
-  {
-    nr = er->extendedRewrite(n);
-  }
-  TypeNode tn = nr.getType();
-  std::map<TypeNode, CandidateRewriteDatabase>::iterator itc = d_cdbs.find(tn);
-  if (itc == d_cdbs.end())
-  {
-    Trace("synth-rr-dbg") << "Initialize database for " << tn << std::endl;
-    // initialize with the extended rewriter owned by this class
-    d_cdbs[tn].initialize(d_vars, &d_sampler[tn]);
-    d_cdbs[tn].setExtendedRewriter(er);
-    itc = d_cdbs.find(tn);
-    Trace("synth-rr-dbg") << "...finish." << std::endl;
-  }
-  Trace("synth-rr-dbg") << "Add term " << nr << " for " << tn << std::endl;
-  return itc->second.addTerm(nr, false, out);
-}
-
 } /* CVC4::theory::quantifiers namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h
index b68b20998..a9ca659e1 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.h
+++ b/src/theory/quantifiers/candidate_rewrite_database.h
@@ -103,44 +103,6 @@ class CandidateRewriteDatabase : public ExprMiner
   bool d_silent;
 };
 
-/**
- * This class generates and stores candidate rewrite databases for multiple
- * types as needed.
- */
-class CandidateRewriteDatabaseGen
-{
- public:
-  /** constructor
-   *
-   * vars : the variables we are testing substitutions for, for all types,
-   * nsamples : number of sample points this class will test for all types.
-   */
-  CandidateRewriteDatabaseGen(std::vector<Node>& vars, unsigned nsamples);
-  /** add term
-   *
-   * This registers term n with this class. We generate the candidate rewrite
-   * database of the appropriate type (if not allocated already), and register
-   * n with this database. This may result in "candidate-rewrite" being
-   * printed on the output stream out. We return true if the term sol is
-   * distinct (up to equivalence) with all previous terms added to this class.
-   */
-  bool addTerm(Node n, std::ostream& out);
-
- private:
-  /** reference to quantifier engine */
-  QuantifiersEngine* d_qe;
-  /** the variables */
-  std::vector<Node> d_vars;
-  /** sygus sampler object for each type */
-  std::map<TypeNode, SygusSampler> d_sampler;
-  /** the number of samples */
-  unsigned d_nsamples;
-  /** candidate rewrite databases for each type */
-  std::map<TypeNode, CandidateRewriteDatabase> d_cdbs;
-  /** an extended rewriter object */
-  ExtendedRewriter d_ext_rewrite;
-};
-
 } /* CVC4::theory::quantifiers namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index 7920ecbeb..b0a474c56 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -1692,7 +1692,7 @@ Node ExtendedRewriter::extendedRewriteStrings(Node ret)
 
   if (ret.getKind() == EQUAL)
   {
-    new_ret = strings::SequencesRewriter::rewriteEqualityExt(ret);
+    new_ret = strings::SequencesRewriter(nullptr).rewriteEqualityExt(ret);
   }
 
   return new_ret;
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index e3e3c3824..5253638a7 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -54,11 +54,6 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output
 TheoryQuantifiers::~TheoryQuantifiers() {
 }
 
-std::unique_ptr<TheoryRewriter> TheoryQuantifiers::mkTheoryRewriter()
-{
-  return std::unique_ptr<TheoryRewriter>(new QuantifiersRewriter());
-}
-
 void TheoryQuantifiers::finishInit()
 {
   // quantifiers are not evaluated in getModelValue
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 7efe7419c..991a47ad0 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -23,6 +23,7 @@
 #include "context/context.h"
 #include "expr/node.h"
 #include "theory/output_channel.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
 #include "theory/valuation.h"
@@ -39,7 +40,7 @@ class TheoryQuantifiers : public Theory {
                     const LogicInfo& logicInfo);
   ~TheoryQuantifiers();
 
-  std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+  TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
 
   /** finish initialization */
   void finishInit() override;
@@ -58,6 +59,9 @@ class TheoryQuantifiers : public Theory {
                         std::vector<Node> node_values,
                         std::string str_value) override;
 
+ private:
+  /** The theory rewriter for this theory. */
+  QuantifiersRewriter d_rewriter;
 };/* class TheoryQuantifiers */
 
 }/* CVC4::theory::quantifiers namespace */