Fix a few obvious memory leaks in sygus and quantifiers. Minor fix cvc3_compat.

5 files changed, 25 insertions, 1 deletions

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 4514453db..0ecc6e547 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -765,6 +765,16 @@ SygusSymBreak::SygusSymBreak( quantifiers::TermDbSygus * tds, context::Context*
 
 }
 
+SygusSymBreak::~SygusSymBreak() {
+  for(std::map< Node, ProgSearch* >::iterator i = d_prog_search.begin(), iend = d_prog_search.end();
+      i != iend; ++i){
+    ProgSearch* current = (*i).second;
+    if(current != NULL){
+      delete current;
+    }
+  }
+}
+
 void SygusSymBreak::addTester( int tindex, Node n, Node exp ) {
   if( options::sygusNormalFormGlobal() ){
     Node a = getAnchor( n );
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index 0add578f0..155b15e52 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -69,6 +69,7 @@ private:
   bool isGenericRedundant( TypeNode tn, Node g, bool active = true );
 public:
   SygusSplit( quantifiers::TermDbSygus * tds ) : d_tds( tds ){}
+  ~SygusSplit(){}
   /** get sygus splits */
   void getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits, std::vector< Node >& lemmas );
 };
@@ -97,6 +98,7 @@ private:
       d_parent( p ), d_anchor( a ), d_testers( c ), d_watched_terms( c ), d_watched_count( c ), d_prog_depth( c, 0 ) {
       d_anchor_type = d_anchor.getType();
     }
+    ~ProgSearch(){}
     Node d_anchor;
     NodeMap d_testers;
     IntMap d_watched_terms;
@@ -129,6 +131,7 @@ private:
   Node getSeparationTemplate( TypeNode tn, Node rep_prog, Node anc_var, int& status );
 public:
   SygusSymBreak( quantifiers::TermDbSygus * tds, context::Context* c );
+  ~SygusSymBreak();
   /** add tester */
   void addTester( int tindex, Node n, Node exp );
   /** lemmas we have generated */
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index b4b51fd84..8166925c6 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -73,6 +73,16 @@ RelevantDomain::RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ) : d_
    d_is_computed = false;
 }
 
+RelevantDomain::~RelevantDomain() {
+  for( std::map< Node, std::map< int, RDomain * > >::iterator itr = d_rel_doms.begin(); itr != d_rel_doms.end(); ++itr ){
+    for( std::map< int, RDomain * >::iterator itr2 = itr->second.begin(); itr2 != itr->second.end(); ++itr2 ){
+      RDomain * current = (*itr2).second;
+      Assert( current != NULL );
+      delete current;
+    }
+  }
+}
+
 RelevantDomain::RDomain * RelevantDomain::getRDomain( Node n, int i, bool getParent ) {
   if( d_rel_doms.find( n )==d_rel_doms.end() || d_rel_doms[n].find( i )==d_rel_doms[n].end() ){
     d_rel_doms[n][i] = new RDomain;
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
index aae8f6c5b..1d6a2af19 100644
--- a/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -64,7 +64,7 @@ private:
   void computeRelevantDomainLit( Node q, bool hasPol, bool pol, Node n );
 public:
   RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m );
-  virtual ~RelevantDomain(){}
+  virtual ~RelevantDomain();
   /* reset */
   bool reset( Theory::Effort e );
   /** identify */
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 42c6d1219..6e60a3790 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -316,6 +316,7 @@ void TheorySep::check(Effort e) {
         Node b_lbl = getBaseLabel( refType );
         Node s_atom_new = NodeManager::currentNM()->mkNode( kind::SEP_LABEL, s_atom, b_lbl );
         Node lem;
+        Trace("sep-lemma-debug") << "...polarity is " << polarity << std::endl;
         if( polarity ){
           lem = NodeManager::currentNM()->mkNode( kind::OR, s_atom.negate(), s_atom_new );
         }else{