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 18345b3b27450a832bac70f68a615ad1c618b3a5..e681b831bbec091b119b4eff31d8ffdc67e80ec1 100644 (file)
--- 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 f88b302123880530c8d9b1bf98190bbe70fc911d..b2a0cfc0c6239cbe12630630b234db0d2486cda7 100644 (file)
--- 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 4514453dbe372da31d58a77c579387a87a7eaf58..0ecc6e547dc0f5f4deb2e578bf8de821cfaba815 100644 (file)
--- 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 0add578f03d30a270588af64a5c2ff20179a4514..155b15e52c1441ae6b0e6de4313fa7e94e7f1aba 100644 (file)
--- 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 b4b51fd842b9b88c81fbea92c47a42d1cd5aa750..8166925c6f38947332568960d2ddb30600174e6b 100644 (file)
--- 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 aae8f6c5b3dcbeaf969c676aa60c4d9fba9baaef..1d6a2af19c90679b7a822268042a5ac84e4a817f 100644 (file)
--- 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 42c6d12198605a0841f341fa3b6cc4206b22f2e8..6e60a3790cf1611efff4d40436ce137f4ada22d2 100644 (file)
--- 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{