From: Tim King Date: Wed, 22 Aug 2018 20:09:39 +0000 (-0700) Subject: Wrapping TheorySetsPrivate in a unique_ptr. (#2356) X-Git-Tag: cvc5-1.0.0~4740 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=923bd039728c972fef1bbf1a24f23f735e295bce;p=cvc5.git Wrapping TheorySetsPrivate in a unique_ptr. (#2356) --- diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 162ebb757..188523a10 100644 --- 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 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 7ccda3dad..e679d33c3 100644 --- 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 + #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 d_internal; +}; /* class TheorySets */ }/* CVC4::theory::sets namespace */ }/* CVC4::theory namespace */