Fix memory leak in quantifiers engine (#1219)

Commit 96a0bc3b022b67b5ab79bf2ab087573c65a8d248 introduced a memory leak
where d_quant_attr was not deleted when the QuantifiersEngine was
destroyed. This commit fixes the issue by turning d_quant_attr into an
std::unique_ptr.

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 0e10dfe54c51a00c9a58292c2457cd5d77a39665..b0f5486252e50097f8fb8383d5e5ba52c9ef8f1c 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -61,22 +61,24 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::inst;
 
-QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te):
-    d_te( te ),
-    d_conflict_c(c, false),
-    //d_quants(u),
-    d_quants_red(u),
-    d_lemmas_produced_c(u),
-    d_skolemized(u),
-    d_ierCounter_c(c),
-    //d_ierCounter(c),
-    //d_ierCounter_lc(c),
-    //d_ierCounterLastLc(c),
-    d_presolve(u, true),
-    d_presolve_in(u),
-    d_presolve_cache(u),
-    d_presolve_cache_wq(u),
-    d_presolve_cache_wic(u){
+QuantifiersEngine::QuantifiersEngine(context::Context* c,
+                                     context::UserContext* u, TheoryEngine* te)
+    : d_te(te),
+      d_conflict_c(c, false),
+      // d_quants(u),
+      d_quants_red(u),
+      d_lemmas_produced_c(u),
+      d_skolemized(u),
+      d_quant_attr(new quantifiers::QuantAttributes(this)),
+      d_ierCounter_c(c),
+      // d_ierCounter(c),
+      // d_ierCounter_lc(c),
+      // d_ierCounterLastLc(c),
+      d_presolve(u, true),
+      d_presolve_in(u),
+      d_presolve_cache(u),
+      d_presolve_cache_wq(u),
+      d_presolve_cache_wic(u) {
   //utilities
   d_eq_query = new quantifiers::EqualityQueryQuantifiersEngine( c, this );
   d_util.push_back( d_eq_query );
@@ -91,8 +93,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
   }else{
     d_sygus_tdb = NULL;
   }
-  
-  d_quant_attr = new quantifiers::QuantAttributes( this );
 
   if( options::instPropagate() ){
     // notice that this option is incompatible with options::qcfAllConflict()

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index c72038659b655bee9943aacdc51b25bec984a502..b1608e4971d83b43124dd86ae146e0a6def674e9 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -19,6 +19,7 @@
 
 #include <iostream>
 #include <map>
+#include <memory>
 #include <unordered_map>
 
 #include "context/cdchunk_list.h"
@@ -200,7 +201,7 @@ private:
   /** term utilities */
   quantifiers::TermUtil* d_term_util;
   /** quantifiers attributes */
-  quantifiers::QuantAttributes* d_quant_attr;
+  std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr;
   /** all triggers will be stored in this trie */
   inst::TriggerTrie* d_tr_trie;
   /** extended model object */
@@ -379,7 +380,9 @@ public:
   /** get term utilities */
   quantifiers::TermUtil* getTermUtil() { return d_term_util; }
   /** get quantifiers attributes */
-  quantifiers::QuantAttributes* getQuantAttributes() { return d_quant_attr; }
+  quantifiers::QuantAttributes* getQuantAttributes() {
+    return d_quant_attr.get();
+  }
   /** get trigger database */
   inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
   /** add term to database */