From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 2 Nov 2016 17:42:25 +0000 (-0500)
Subject: Fix a few obvious memory leaks in sygus and quantifiers. Minor fix cvc3_compat.
X-Git-Tag: cvc5-1.0.0~6009
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=81c1bee05d9d7c323f49d33554a523f8f4fbf387;p=cvc5.git

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

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 18345b3b2..e681b831b 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -1425,7 +1425,7 @@ void ValidityChecker::dataType(const std::vector<std::string>& names,
     const CVC4::Datatype& dt = (*i).getDatatype();
     // ensure it's well-founded (the check is done here because
     // that's how it is in CVC3)
-    CompatCheckArgument(!dt.isWellFounded(), "datatype is not well-founded");
+    CompatCheckArgument(dt.isWellFounded(), "datatype is not well-founded");
     for(CVC4::Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) {
       // For each constructor, register its name and its selectors names.
       CompatCheckArgument(
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index f88b30212..b2a0cfc0c 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -639,7 +639,6 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
       for( unsigned i=0; i<datatypes.size(); i++ ){
         Debug("parser-sygus") << "  " << i << " : " << datatypes[i].getName() << std::endl;
       }
-      seq = new CommandSequence();
       std::vector<DatatypeType> datatypeTypes = PARSER_STATE->mkMutualDatatypeTypes(datatypes);
       seq->addCommand(new DatatypeDeclarationCommand(datatypeTypes));
       std::map<DatatypeType, Expr> evals;
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{