diff options
-rw-r--r-- | src/theory/sets/theory_sets.cpp | 12 | ||||
-rw-r--r-- | src/theory/sets/theory_sets.h | 51 |
2 files changed, 28 insertions, 35 deletions
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<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 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 <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 */ |