diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-07-02 11:59:39 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-07-02 11:59:39 -0500 |
commit | 2c289524f23a2ec481224b2ea569397acbb5e39e (patch) | |
tree | b94c4e25d0f8c37cc2511811997f634566f36010 /src/theory | |
parent | 1c5a8e7bee22e9b154a5ac65c52cc04d3d2ba3c0 (diff) |
Use unique_ptr for UF modules (#3080)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 9 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 13 |
2 files changed, 11 insertions, 11 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 393d9f640..7ea3f8370 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -50,7 +50,8 @@ TheoryUF::TheoryUF(context::Context* c, d_notify(*this), /* The strong theory solver can be notified by EqualityEngine::init(), * so make sure it's initialized first. */ - d_thss(NULL), + d_thss(nullptr), + d_ho(nullptr), d_equalityEngine(d_notify, c, instanceName + "theory::uf::ee", true), d_conflict(c, false), d_functionsTerms(c), @@ -63,7 +64,6 @@ TheoryUF::TheoryUF(context::Context* c, } TheoryUF::~TheoryUF() { - delete d_thss; } void TheoryUF::setMasterEqualityEngine(eq::EqualityEngine* eq) { @@ -81,12 +81,13 @@ void TheoryUF::finishInit() { if (getLogicInfo().isTheoryEnabled(THEORY_UF) && options::finiteModelFind() && options::ufssMode() != UF_SS_NONE) { - d_thss = new StrongSolverTheoryUF(getSatContext(), getUserContext(), *d_out, this); + d_thss.reset(new StrongSolverTheoryUF( + getSatContext(), getUserContext(), *d_out, this)); } if (options::ufHo()) { d_equalityEngine.addFunctionKind(kind::HO_APPLY); - d_ho = new HoExtension(*this, getSatContext(), getUserContext()); + d_ho.reset(new HoExtension(*this, getSatContext(), getUserContext())); } } diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index df1cc232b..248f46900 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -120,8 +120,10 @@ private: /** The notify class */ NotifyClass d_notify; - /** The associated theory strong solver (or NULL if none) */ - StrongSolverTheoryUF* d_thss; + /** The associated theory strong solver (or nullptr if it does not exist) */ + std::unique_ptr<StrongSolverTheoryUF> d_thss; + /** the higher-order solver extension (or nullptr if it does not exist) */ + std::unique_ptr<HoExtension> d_ho; /** Equaltity engine */ eq::EqualityEngine d_equalityEngine; @@ -132,8 +134,6 @@ private: /** The conflict node */ Node d_conflictNode; - /** the higher-order solver extension */ - HoExtension* d_ho; /** node for true */ Node d_true; @@ -218,9 +218,8 @@ private: eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; } - StrongSolverTheoryUF* getStrongSolver() { - return d_thss; - } + /** get a pointer to the strong solver (uf with cardinality) */ + StrongSolverTheoryUF* getStrongSolver() const { return d_thss.get(); } /** are we in conflict? */ bool inConflict() const { return d_conflict; } |