Fix a few more minor memory leaks.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c9484dbf069f0f518617ea7590409d12db50d052..46469fb0dcc34082c75a96e772ef5c2e1f0aa39f 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -989,8 +989,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_propEngine(NULL),
   d_proofManager(NULL),
   d_definedFunctions(NULL),
-  d_fmfRecFunctionsAbs(NULL),
-  d_fmfRecFunctionsConcrete(NULL),
+  d_fmfRecFunctionsDefined(NULL),
   d_assertionList(NULL),
   d_assignments(NULL),
   d_modelGlobalCommands(),
@@ -1059,8 +1058,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
 
   d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
   if( options::fmfFunWellDefined() || options::fmfFunWellDefinedRelevant() ){
-    d_fmfRecFunctionsAbs = new(true) TypeNodeMap(d_userContext);
-    d_fmfRecFunctionsConcrete = new(true) NodeListMap(d_userContext);
+    d_fmfRecFunctionsDefined = new(true) NodeList(d_userContext);
   }
   d_modelCommands = new(true) smt::CommandList(d_userContext);
 }
@@ -1206,13 +1204,10 @@ SmtEngine::~SmtEngine() throw() {
 
     d_definedFunctions->deleteSelf();
 
-    if( d_fmfRecFunctionsAbs != NULL ){
-      d_fmfRecFunctionsAbs->deleteSelf();
+    if( d_fmfRecFunctionsDefined != NULL ){
+      d_fmfRecFunctionsDefined->deleteSelf();
     }
-    if( d_fmfRecFunctionsConcrete != NULL ){
-      d_fmfRecFunctionsConcrete->deleteSelf();
-    }
-
+    
     delete d_theoryEngine;
     d_theoryEngine = NULL;
     delete d_propEngine;
@@ -3998,27 +3993,28 @@ void SmtEnginePrivate::processAssertions() {
     if( options::fmfFunWellDefined() ){
       quantifiers::FunDefFmf fdf;
       //must carry over current definitions (for incremental)
-      for( SmtEngine::TypeNodeMap::const_iterator fit = d_smt.d_fmfRecFunctionsAbs->begin(); fit != d_smt.d_fmfRecFunctionsAbs->end(); ++fit ){
-        Node f = (*fit).first;
-        TypeNode ft = (*fit).second;
+      for( context::CDList<Node>::const_iterator fit = d_smt.d_fmfRecFunctionsDefined->begin(); 
+           fit != d_smt.d_fmfRecFunctionsDefined->end(); ++fit ) {
+        Node f = (*fit);
+        Assert( d_smt.d_fmfRecFunctionsAbs.find( f )!=d_smt.d_fmfRecFunctionsAbs.end() );
+        TypeNode ft = d_smt.d_fmfRecFunctionsAbs[f];
         fdf.d_sorts[f] = ft;
-        SmtEngine::NodeListMap::const_iterator fcit = d_smt.d_fmfRecFunctionsConcrete->find( f );
-        Assert( fcit!=d_smt.d_fmfRecFunctionsConcrete->end() );
-        SmtEngine::NodeList* cl = (*fcit).second;
-        for( SmtEngine::NodeList::const_iterator cit = cl->begin(); cit != cl->end(); ++cit ){
-          fdf.d_input_arg_inj[f].push_back( *cit );
+        std::map< Node, std::vector< Node > >::iterator fcit = d_smt.d_fmfRecFunctionsConcrete.find( f );
+        Assert( fcit!=d_smt.d_fmfRecFunctionsConcrete.end() );
+        for( unsigned j=0; j<fcit->second.size(); j++ ){
+          fdf.d_input_arg_inj[f].push_back( fcit->second[j] );
         }
       }
       fdf.simplify( d_assertions.ref() );
       //must store new definitions (for incremental)
       for( unsigned i=0; i<fdf.d_funcs.size(); i++ ){
         Node f = fdf.d_funcs[i];
-        d_smt.d_fmfRecFunctionsAbs->insert( f, fdf.d_sorts[f] );
-        SmtEngine::NodeList* cl = new(true) SmtEngine::NodeList( d_smt.d_userContext );
+        d_smt.d_fmfRecFunctionsAbs[f] = fdf.d_sorts[f];
+        d_smt.d_fmfRecFunctionsConcrete[f].clear();
         for( unsigned j=0; j<fdf.d_input_arg_inj[f].size(); j++ ){
-          cl->push_back( fdf.d_input_arg_inj[f][j] );
+          d_smt.d_fmfRecFunctionsConcrete[f].push_back( fdf.d_input_arg_inj[f][j] );
         }
-        d_smt.d_fmfRecFunctionsConcrete->insert( f, cl );
+        d_smt.d_fmfRecFunctionsDefined->push_back( f );
       }
     }
     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << endl;

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 760c7c07188aa1a68b7997f91dc86b901fe2af5a..f1ce2e0e980bc64807991de99e87973d60baf503 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -130,9 +130,7 @@ class CVC4_PUBLIC SmtEngine {
   /** The type of our internal assignment set */
   typedef context::CDHashSet<Node, NodeHashFunction> AssignmentSet;
   /** The types for the recursive function definitions */
-  typedef context::CDHashMap< Node, TypeNode, NodeHashFunction > TypeNodeMap;
   typedef context::CDList<Node> NodeList;
-  typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap;
 
   /** Expr manager context */
   context::Context* d_context;
@@ -157,8 +155,9 @@ class CVC4_PUBLIC SmtEngine {
   /** An index of our defined functions */
   DefinedFunctionMap* d_definedFunctions;
   /** recursive function definition abstractions for --fmf-fun */
-  TypeNodeMap* d_fmfRecFunctionsAbs;
-  NodeListMap* d_fmfRecFunctionsConcrete;
+  std::map< Node, TypeNode > d_fmfRecFunctionsAbs;
+  std::map< Node, std::vector< Node > > d_fmfRecFunctionsConcrete;
+  NodeList* d_fmfRecFunctionsDefined;
 
   /**
    * The assertion list (before any conversion) for supporting

diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp
index 9ccba38cd43193d7d26ab8da1197c2ed54c2fb80..908aeecfd5ac0ad81c606b41a1e747211023346d 100644 (file)
--- a/src/theory/quantifiers/anti_skolem.cpp
+++ b/src/theory/quantifiers/anti_skolem.cpp
@@ -9,7 +9,7 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Implementation of anti-skolemization
+ ** \brief Implementation of anti-skolemization, e.g.:
  **          ( forall x. P[ f( x ) ] ^ forall x. Q[ f( x ) ]  ) => forall x. exists y. ( P[ y ] ^ Q[ y ] )
  **/
 
@@ -75,6 +75,15 @@ bool QuantAntiSkolem::CDSkQuantCache::add( context::Context* c, std::vector< Nod
   }
 }
 
+QuantAntiSkolem::CDSkQuantCache::~CDSkQuantCache() {
+  for(std::map< Node, CDSkQuantCache* >::iterator i = d_data.begin(), iend = d_data.end();
+      i != iend; ++i){
+    CDSkQuantCache* current = (*i).second;
+    Assert(current != NULL);
+    delete current;
+  }
+}
+
 QuantAntiSkolem::QuantAntiSkolem(QuantifiersEngine* qe)
     : QuantifiersModule(qe) {
   d_sqc = new CDSkQuantCache(qe->getUserContext());

diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h
index 48205db9d0f4dbcd353225c7fdff115d53ce7e26..c996b171ec3543b70c1a7c693fab551e887dfc4a 100644 (file)
--- a/src/theory/quantifiers/anti_skolem.h
+++ b/src/theory/quantifiers/anti_skolem.h
@@ -9,7 +9,7 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief dynamic quantifiers splitting
+ ** \brief anti-skolemization
  **/
 
 #include "cvc4_private.h"
@@ -71,6 +71,7 @@ public:
   class CDSkQuantCache {
   public:
     CDSkQuantCache( context::Context* c ) : d_valid( c, false ){}
+    ~CDSkQuantCache();
     std::map< Node, CDSkQuantCache* > d_data;
     context::CDO< bool > d_valid;
     bool add( context::Context* c, std::vector< Node >& quants, unsigned index = 0 );

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 9de8fa0ddfdc88a9196ac6c8a32bc12bab59edea..cf7611dabb3bf3553c25e25eb5f5299ae5567c9b 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -739,7 +739,7 @@ void TheoryEngine::propagate(Theory::Effort effort) {
 
 Node TheoryEngine::getNextDecisionRequest() {
   // Definition of the statement that is to be run by every theory
-  unsigned min_priority;
+  unsigned min_priority = 0;
   Node dec;
 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 #undef CVC4_FOR_EACH_THEORY_STATEMENT