Wrapping TheorySetsPrivate in a unique_ptr. (#2356)

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 162ebb75797340674afd50b33c2d57823195c61a..188523a10c4ba1a6cb18ba22aeb3612744c0905f 100644 (file)
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -28,10 +28,16 @@ TheorySets::TheorySets(context::Context* c,
                        const LogicInfo& logicInfo)
     : Theory(THEORY_SETS, c, u, out, valuation, logicInfo),
       d_internal(new TheorySetsPrivate(*this, c, u))
-{}
+{
+  // Do not move me to the header.
+  // The constructor + destructor are not in the header as d_internal is a
+  // unique_ptr<TheorySetsPrivate> and TheorySetsPrivate is an opaque type in
+  // the header (Pimpl). See https://herbsutter.com/gotw/_100/ .
+}
 
-TheorySets::~TheorySets() {
-  delete d_internal;
+TheorySets::~TheorySets()
+{
+  // Do not move me to the header. See explanation in the constructor.
 }
 
 void TheorySets::addSharedTerm(TNode n) {

diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 7ccda3dad580c90ea6a9a29b0f16d87183b017c9..e679d33c37a716a9b730bfd7c7d46765abe5cb55 100644 (file)
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -19,6 +19,8 @@
 #ifndef __CVC4__THEORY__SETS__THEORY_SETS_H
 #define __CVC4__THEORY__SETS__THEORY_SETS_H
 
+#include <memory>
+
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
 
@@ -29,56 +31,41 @@ namespace sets {
 class TheorySetsPrivate;
 class TheorySetsScrutinize;
 
-class TheorySets : public Theory {
-private:
-  friend class TheorySetsPrivate;
-  friend class TheorySetsScrutinize;
-  friend class TheorySetsRels;
-  TheorySetsPrivate* d_internal;
-public:
-
-  /**
-   * Constructs a new instance of TheorySets w.r.t. the provided
-   * contexts.
-   */
-  TheorySets(context::Context* c, context::UserContext* u, OutputChannel& out,
-             Valuation valuation, const LogicInfo& logicInfo);
-
-  ~TheorySets();
+class TheorySets : public Theory
+{
+ public:
+  /** Constructs a new instance of TheorySets w.r.t. the provided contexts. */
+  TheorySets(context::Context* c,
+             context::UserContext* u,
+             OutputChannel& out,
+             Valuation valuation,
+             const LogicInfo& logicInfo);
+  ~TheorySets() override;
 
   void addSharedTerm(TNode) override;
-
   void check(Effort) override;
-
   bool needsCheckLastEffort() override;
-
   bool collectModelInfo(TheoryModel* m) override;
-
   void computeCareGraph() override;
-
   Node explain(TNode) override;
-
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
-
   Node getModelValue(TNode) override;
-
   std::string identify() const override { return "THEORY_SETS"; }
-
   void preRegisterTerm(TNode node) override;
-
   Node expandDefinition(LogicRequest& logicRequest, Node n) override;
-
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
-
   void presolve() override;
-
   void propagate(Effort) override;
-
   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
+  bool isEntailed(Node n, bool pol);
 
-  bool isEntailed( Node n, bool pol );
+ private:
+  friend class TheorySetsPrivate;
+  friend class TheorySetsScrutinize;
+  friend class TheorySetsRels;
 
-};/* class TheorySets */
+  std::unique_ptr<TheorySetsPrivate> d_internal;
+}; /* class TheorySets */
 
 }/* CVC4::theory::sets namespace */
 }/* CVC4::theory namespace */