Simple memory fixes, minor cleanup in quantifiers.

6 files changed, 54 insertions, 53 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8f282b413..6f4135af2 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -552,10 +552,10 @@ class SmtEnginePrivate : public NodeManagerListener {
    */
   unsigned d_simplifyAssertionsDepth;
 
-  /** whether certain preprocess steps are necessary */
-  bool d_needsExpandDefs;
-  bool d_needsRewriteBoolTerms;
-  bool d_needsConstrainSubTypes;
+  /** TODO: whether certain preprocess steps are necessary */
+  //bool d_needsExpandDefs;
+  //bool d_needsRewriteBoolTerms;
+  //bool d_needsConstrainSubTypes;
 
 public:
   /**
@@ -684,9 +684,9 @@ public:
     d_abstractValueMap(&d_fakeContext),
     d_abstractValues(),
     d_simplifyAssertionsDepth(0),
-    d_needsExpandDefs(true),
-    d_needsRewriteBoolTerms(true),
-    d_needsConstrainSubTypes(true), //TODO
+    //d_needsExpandDefs(true),
+    //d_needsRewriteBoolTerms(true),
+    //d_needsConstrainSubTypes(true), //TODO
     d_iteSkolemMap(),
     d_iteRemover(smt.d_userContext),
     d_pbsProcessor(smt.d_userContext),
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 95d704a0e..7994351ee 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -82,6 +82,8 @@ TheoryDatatypes::~TheoryDatatypes() {
     Assert(current != NULL);
     delete current;
   }
+  delete d_sygus_split;
+  delete d_sygus_sym_break;
 }
 
 void TheoryDatatypes::setMasterEqualityEngine(eq::EqualityEngine* eq) {
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index bd5100a2e..2d3bf76f6 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -32,6 +32,7 @@ namespace theory {
 namespace inst {
 
 InstMatchGenerator::InstMatchGenerator( Node pat ){
+  d_cg = NULL;
   d_needsReset = true;
   d_active_add = false;
   Assert( quantifiers::TermDb::hasInstConstAttr(pat) );
@@ -43,12 +44,20 @@ InstMatchGenerator::InstMatchGenerator( Node pat ){
 }
 
 InstMatchGenerator::InstMatchGenerator() {
+  d_cg = NULL;
   d_needsReset = true;
   d_active_add = false;
   d_next = NULL;
   d_matchPolicy = MATCH_GEN_DEFAULT;
 }
 
+InstMatchGenerator::~InstMatchGenerator() throw() {
+  for( unsigned i=0; i<d_children.size(); i++ ){
+    delete d_children[i];
+  }
+  delete d_cg;
+}
+
 void InstMatchGenerator::setActiveAdd(bool val){
   d_active_add = val;
   if( d_next!=NULL ){
@@ -249,7 +258,7 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi
       Trace("matching-debug2") << "Reset children..." << std::endl;
       //now, fit children into match
       //we will be requesting candidates for matching terms for each child
-      for( int i=0; i<(int)d_children.size(); i++ ){
+      for( unsigned i=0; i<d_children.size(); i++ ){
         d_children[i]->reset( t[ d_children_index[i] ], qe );
       }
       Trace("matching-debug2") << "Continue next " << d_next << std::endl;
@@ -484,7 +493,7 @@ d_f( q ){
     }
     Debug("smart-multi-trigger") << std::endl;
   }
-  for( int i=0; i<(int)pats.size(); i++ ){
+  for( unsigned i=0; i<pats.size(); i++ ){
     Node n = pats[i];
     //make the match generator
     d_children.push_back( InstMatchGenerator::mkInstMatchGenerator(q, n, qe ) );
@@ -492,7 +501,7 @@ d_f( q ){
     std::vector< int > unique_vars;
     std::map< int, bool > shared_vars;
     int numSharedVars = 0;
-    for( int j=0; j<(int)d_var_contains[n].size(); j++ ){
+    for( unsigned j=0; j<d_var_contains[n].size(); j++ ){
       if( d_var_to_node[ d_var_contains[n][j] ].size()==1 ){
         Debug("smart-multi-trigger") << "Var " << d_var_contains[n][j] << " is unique to " << pats[i] << std::endl;
         unique_vars.push_back( d_var_contains[n][j] );
@@ -503,7 +512,7 @@ d_f( q ){
     }
     //we use the latest shared variables, then unique variables
     std::vector< int > vars;
-    int index = i==0 ? (int)(pats.size()-1) : (i-1);
+    unsigned index = i==0 ? pats.size()-1 : (i-1);
     while( numSharedVars>0 && index!=i ){
       for( std::map< int, bool >::iterator it = shared_vars.begin(); it != shared_vars.end(); ++it ){
         if( it->second ){
@@ -519,16 +528,24 @@ d_f( q ){
     }
     vars.insert( vars.end(), unique_vars.begin(), unique_vars.end() );
     Debug("smart-multi-trigger") << "   Index[" << i << "]: ";
-    for( int i=0; i<(int)vars.size(); i++ ){
-      Debug("smart-multi-trigger") << vars[i] << " ";
+    for( unsigned j=0; j<vars.size(); j++ ){
+      Debug("smart-multi-trigger") << vars[j] << " ";
     }
     Debug("smart-multi-trigger") << std::endl;
     //make ordered inst match trie
-    InstMatchTrie::ImtIndexOrder* imtio = new InstMatchTrie::ImtIndexOrder;
-    imtio->d_order.insert( imtio->d_order.begin(), vars.begin(), vars.end() );
-    d_children_trie.push_back( InstMatchTrieOrdered( imtio ) );
+    d_imtio[i] = new InstMatchTrie::ImtIndexOrder;
+    d_imtio[i]->d_order.insert( d_imtio[i]->d_order.begin(), vars.begin(), vars.end() );
+    d_children_trie.push_back( InstMatchTrieOrdered( d_imtio[i] ) );
   }
+}
 
+InstMatchGeneratorMulti::~InstMatchGeneratorMulti() throw() {
+  for( unsigned i=0; i<d_children.size(); i++ ){
+    delete d_children[i];
+  }
+  for( std::map< unsigned, InstMatchTrie::ImtIndexOrder* >::iterator it = d_imtio.begin(); it != d_imtio.end(); ++it ){
+    delete it->second;
+  }
 }
 
 /** reset instantiation round (call this whenever equivalence classes have changed) */
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index 49e3c1ec5..096774c51 100644
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -91,7 +91,7 @@ public:
   InstMatchGenerator( Node pat );
   InstMatchGenerator();
   /** destructor */
-  ~InstMatchGenerator() throw() {}
+  virtual ~InstMatchGenerator() throw();
   /** The pattern we are producing matches for.
       If null, this is a multi trigger that is merging matches from d_children.
   */
@@ -125,7 +125,7 @@ public:
 class VarMatchGeneratorBooleanTerm : public InstMatchGenerator {
 public:
   VarMatchGeneratorBooleanTerm( Node var, Node comp );
-  ~VarMatchGeneratorBooleanTerm() throw() {}
+  virtual ~VarMatchGeneratorBooleanTerm() throw() {}
   Node d_comp;
   bool d_rm_prev;
   /** reset instantiation round (call this at beginning of instantiation round) */
@@ -142,7 +142,7 @@ public:
 class VarMatchGeneratorTermSubs : public InstMatchGenerator {
 public:
   VarMatchGeneratorTermSubs( Node var, Node subs );
-  ~VarMatchGeneratorTermSubs() throw() {}
+  virtual ~VarMatchGeneratorTermSubs() throw() {}
   TNode d_var;
   TypeNode d_var_type;
   Node d_subs;
@@ -183,6 +183,8 @@ private:
   int d_matchPolicy;
   /** children generators */
   std::vector< InstMatchGenerator* > d_children;
+  /** order */
+  std::map< unsigned, InstMatchTrie::ImtIndexOrder* > d_imtio;
   /** inst match tries for each child */
   std::vector< InstMatchTrieOrdered > d_children_trie;
   /** calculate matches */
@@ -191,7 +193,7 @@ public:
   /** constructors */
   InstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe );
   /** destructor */
-  ~InstMatchGeneratorMulti() throw() {}
+  virtual ~InstMatchGeneratorMulti() throw();
   /** reset instantiation round (call this whenever equivalence classes have changed) */
   void resetInstantiationRound( QuantifiersEngine* qe );
   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 5645c3401..c34d86497 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -238,10 +238,15 @@ void TermDb::computeUfTerms( TNode f ) {
     if( it!=d_op_map.end() ){
       eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
       Trace("term-db-debug") << "Adding terms for operator " << f << std::endl;
+      unsigned congruentCount = 0;
+      unsigned nonCongruentCount = 0;
+      unsigned alreadyCongruentCount = 0;
+      unsigned relevantCount = 0;
       for( unsigned i=0; i<it->second.size(); i++ ){
         Node n = it->second[i];
         //to be added to term index, term must be relevant, and exist in EE
         if( hasTermCurrent( n ) && ee->hasTerm( n ) ){
+          relevantCount++;
           if( isTermActive( n ) ){
             computeArgReps( n );
 
@@ -260,7 +265,7 @@ void TermDb::computeUfTerms( TNode f ) {
             if( at!=n && ee->areEqual( at, n ) ){
               setTermInactive( n );
               Trace("term-db-debug") << n << " is redundant." << std::endl;
-              //congruentCount++;
+              congruentCount++;
             }else{
               if( at!=n && ee->areDisequal( at, n, false ) ){
                 std::vector< Node > lits;
@@ -282,29 +287,22 @@ void TermDb::computeUfTerms( TNode f ) {
                 d_consistent_ee = false;
                 return;
               }
-              //nonCongruentCount++;
+              nonCongruentCount++;
               d_op_nonred_count[ f ]++;
             }
           }else{
             Trace("term-db-debug") << n << " is already redundant." << std::endl;
-            //congruentCount++;
-            //alreadyCongruentCount++;
+            alreadyCongruentCount++;
           }
         }else{
           Trace("term-db-debug") << n << " is not relevant." << std::endl;
-          //nonRelevantCount++;
         }
       }
-      
-      /*
-      if( Trace.isOn("term-db-index") ){
-        Trace("term-db-index") << "Term index for " << f << " : " << std::endl;
-        Trace("term-db-index") << "- " << it->first << std::endl;
-        d_func_map_trie[ f ].debugPrint("term-db-index", it->second[0]);
-        Trace("term-db-index") << "Non-Congruent/Congruent/Non-Relevant = ";
-        Trace("term-db-index") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl; 
+      if( Trace.isOn("tdb") ){
+        Trace("tdb") << "Term db size [" << f << "] : " << nonCongruentCount << " / ";
+        Trace("tdb") << ( nonCongruentCount + congruentCount ) << " / " << ( nonCongruentCount + congruentCount + alreadyCongruentCount ) << " / ";
+        Trace("tdb") << relevantCount << " / " << it->second.size() << std::endl;
       }
-      */
     }
   }
 }
@@ -676,10 +674,6 @@ void TermDb::presolve() {
 }
 
 bool TermDb::reset( Theory::Effort effort ){
-  //int nonCongruentCount = 0;
-  //int congruentCount = 0;
-  //int alreadyCongruentCount = 0;
-  //int nonRelevantCount = 0;
   d_op_nonred_count.clear();
   d_arg_reps.clear();
   d_func_map_trie.clear();
@@ -743,20 +737,6 @@ bool TermDb::reset( Theory::Effort effort ){
     }
   }
 */  
-  /*
-  Trace("term-db-stats") << "TermDb: Reset" << std::endl;
-  Trace("term-db-stats") << "Non-Congruent/Congruent/Non-Relevant = ";
-  Trace("term-db-stats") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl;
-  if( Trace.isOn("term-db-index") ){
-    Trace("term-db-index") << "functions : " << std::endl;
-    for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
-      if( it->second.size()>0 ){
-        Trace("term-db-index") << "- " << it->first << std::endl;
-        d_func_map_trie[ it->first ].debugPrint("term-db-index", it->second[0]);
-      }
-    }
-  }
-  */
   return true;
 }
 
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 214a4d055..802acc089 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -86,7 +86,7 @@ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes )
 }
 
 Trigger::~Trigger() {
-  if(d_mg != NULL) { delete d_mg; }
+  delete d_mg;
 }
 
 void Trigger::resetInstantiationRound(){