Using unique_ptr's for members of CegConjecture. (#1324)

diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp
index 5af8eafc810bf6ce415b9549fa3ac9d05d8cfafe..7110f103725aff0b4555c1f2bdf8789fab0c26b2 100644 (file)
--- a/src/theory/quantifiers/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/ce_guided_conjecture.cpp
@@ -45,20 +45,15 @@ void collectDisjuncts( Node n, std::vector< Node >& d ) {
 }
 
 CegConjecture::CegConjecture(QuantifiersEngine* qe)
-    : d_qe(qe), d_syntax_guided(false) {
-  d_refine_count = 0;
-  d_ceg_si = new CegConjectureSingleInv(qe, this);
-  d_ceg_pbe = new CegConjecturePbe(qe, this);
-  d_ceg_proc = new CegConjectureProcess(qe);
-  d_ceg_gc = new CegGrammarConstructor(qe, this);
-}
-
-CegConjecture::~CegConjecture() {
-  delete d_ceg_si;
-  delete d_ceg_pbe;
-  delete d_ceg_proc;
-  delete d_ceg_gc;
-}
+    : d_qe(qe),
+      d_ceg_si(new CegConjectureSingleInv(qe, this)),
+      d_ceg_pbe(new CegConjecturePbe(qe, this)),
+      d_ceg_proc(new CegConjectureProcess(qe)),
+      d_ceg_gc(new CegGrammarConstructor(qe, this)),
+      d_refine_count(0),
+      d_syntax_guided(false) {}
+
+CegConjecture::~CegConjecture() {}
 
 void CegConjecture::assign( Node q ) {
   Assert( d_embed_quant.isNull() );

diff --git a/src/theory/quantifiers/ce_guided_conjecture.h b/src/theory/quantifiers/ce_guided_conjecture.h
index b725449b492a7622024078a9eaa40ba7579c6581..90627699f9fd488b046709ac66dd59dd1d9ab2b1 100644 (file)
--- a/src/theory/quantifiers/ce_guided_conjecture.h
+++ b/src/theory/quantifiers/ce_guided_conjecture.h
@@ -18,6 +18,8 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_CONJECTURE_H
 #define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_CONJECTURE_H
 
+#include <memory>
+
 #include "theory/quantifiers/ce_guided_pbe.h"
 #include "theory/quantifiers/ce_guided_single_inv.h"
 #include "theory/quantifiers/sygus_grammar_cons.h"
@@ -111,7 +113,7 @@ public:
   //-----------------------------------end refinement lemmas
 
   /** get program by examples utility */
-  CegConjecturePbe* getPbe() { return d_ceg_pbe; }
+  CegConjecturePbe* getPbe() { return d_ceg_pbe.get(); }
   /** get the symmetry breaking predicate for type */
   Node getSymmetryBreakingPredicate(
       Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth);
@@ -121,13 +123,13 @@ private:
   /** reference to quantifier engine */
   QuantifiersEngine * d_qe;
   /** single invocation utility */
-  CegConjectureSingleInv * d_ceg_si;
+  std::unique_ptr<CegConjectureSingleInv> d_ceg_si;
   /** program by examples utility */
-  CegConjecturePbe * d_ceg_pbe;
+  std::unique_ptr<CegConjecturePbe> d_ceg_pbe;
   /** utility for static preprocessing and analysis of conjectures */
-  CegConjectureProcess* d_ceg_proc;
+  std::unique_ptr<CegConjectureProcess> d_ceg_proc;
   /** grammar utility */
-  CegGrammarConstructor * d_ceg_gc;
+  std::unique_ptr<CegGrammarConstructor> d_ceg_gc;
   /** list of constants for quantified formula
   * The Skolems for the negation of d_embed_quant.
   */