Free up more memory before SAT solving. In particular this deletes the Tseitin variab...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@836 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 8dd54f452b21f3017dfe8ee10abfcf042d533f53..346bc15cf14694861cb07623d5e444e7d9ca8b0a 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -188,6 +188,12 @@ namespace BEEV {
         bm->counterexample_checking_during_refinement = true;
       }
 
+    if(bm->UserFlags.stats_flag)
+       simp->printCacheStatus();
+
+    simp->ClearCaches();
+    bm->ClearAllTables();
+
     res = 
       Ctr_Example->CallSAT_ResultCheck(NewSolver, 
                                        simplified_solved_InputToSAT, 

diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp
index 3f9ac522b9deb55605aec7b2ba04a8a50e47d73b..1947efbbadb76960a07bbcc5ece83de03dd22dfe 100644 (file)
--- a/src/STPManager/STPManager.cpp
+++ b/src/STPManager/STPManager.cpp
@@ -53,6 +53,7 @@ namespace BEEV
 
     // insert back_children at end of front_children
     ASTVec &front_children = n_ptr->_children;
+       front_children.reserve(front_children.size()+ back_children.size());
 
     front_children.insert(front_children.end(), 
                           back_children.begin(), 
@@ -591,8 +592,8 @@ namespace BEEV
       return 1;
 
     unsigned newn = 1;
-    ASTVec c = a.GetChildren();
-    for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
+    const ASTVec& c = a.GetChildren();
+    for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++)
       newn += NodeSize(*it);
     return newn;
   }

diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp
index be693a00bc5d202e2cb9a21b26ccd4bac431db54..73acbe6f82803544539a4c2671566d15241efa01 100644 (file)
--- a/src/absrefine_counterexample/CounterExample.cpp
+++ b/src/absrefine_counterexample/CounterExample.cpp
@@ -51,7 +51,7 @@ namespace BEEV
             ASTNode s = tosat->SATVar_to_ASTMap(i);
 
             //assemble the counterexample here
-            if (s.GetKind() == BVGETBIT && s[0].GetKind() == SYMBOL)
+            if (!s.IsNull() && s.GetKind() == BVGETBIT && s[0].GetKind() == SYMBOL)
               {
                 const ASTNode& symbol = s[0];
                 const unsigned int symbolWidth = symbol.GetValueWidth();
@@ -80,7 +80,7 @@ namespace BEEV
               }
             else
               {
-                if (s.GetKind() == SYMBOL && s.GetType() == BOOLEAN_TYPE)
+                if (!s.IsNull() && s.GetKind() == SYMBOL && s.GetType() == BOOLEAN_TYPE)
                   {
                     const char * zz = s.GetName();
                     //if the variables are not cnf variables then add
@@ -895,14 +895,16 @@ namespace BEEV
     cout << "Satisfying assignment: " << endl;
     for (int i = 0; i < num_vars; i++)
       {
-        if (newS.model[i] == MINISAT::l_True)
+        ASTNode s = tosat->SATVar_to_ASTMap(i);
+        if (s.IsNull())
+               continue;
+
+       if (newS.model[i] == MINISAT::l_True)
           {
-            ASTNode s = tosat->SATVar_to_ASTMap(i);
             cout << s << endl;
           }
         else if (newS.model[i] == MINISAT::l_False)
           {
-            ASTNode s = tosat->SATVar_to_ASTMap(i);
             cout << bm->CreateNode(NOT, s) << endl;
           }
       }

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 4a5b5047476887a7f9810fcf446491237be0757e..da4e501e8c783d70d1f81788a81e9c89a049dbc8 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -3644,12 +3644,13 @@ namespace BEEV
 
   void Simplifier::printCacheStatus()
   {
-    cerr << SimplifyMap->size() << endl;
-    cerr << SimplifyNegMap->size() << endl;
-    //cerr << TermsAlreadySeenMap.size() << endl;
-  
-    cerr << SimplifyMap->bucket_count() << endl;
-    cerr << SimplifyNegMap->bucket_count() << endl;
-    //cerr << TermsAlreadySeenMap.bucket_count() << endl;
+    cerr << "SimplifyMap:" << SimplifyMap->size() << ":" << SimplifyMap->bucket_count() << endl;
+    cerr << "SimplifyNegMap:" << SimplifyNegMap->size() << ":" << SimplifyNegMap->bucket_count() << endl;
+    cerr << "AlwaysTrueFormMap" << AlwaysTrueFormMap.size() << ":" << AlwaysTrueFormMap.bucket_count() << endl;
+    cerr << "MultInverseMap" << MultInverseMap.size() << ":" << MultInverseMap.bucket_count() << endl;
+    cerr << "ReadOverWrite_NewName_Map" << ReadOverWrite_NewName_Map->size() << ":" << ReadOverWrite_NewName_Map->bucket_count() << endl;
+    cerr << "NewName_ReadOverWrite_Map" << NewName_ReadOverWrite_Map.size() << ":" << NewName_ReadOverWrite_Map.bucket_count() << endl;
+    cerr << "substn_map" << substitutionMap.Return_SolverMap()->size() << ":" << substitutionMap.Return_SolverMap()->bucket_count() << endl;
+
   } //printCacheStatus()
 };//end of namespace

diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h
index b78924dd85234e600022fc4655bb49c8c56c0cb7..f33074a1d7b1dfbd8aad622340afb8252cec7f69 100644 (file)
--- a/src/simplifier/simplifier.h
+++ b/src/simplifier/simplifier.h
@@ -252,6 +252,16 @@ namespace BEEV
       MultInverseMap.clear();
       substitutionMap.clear();
     }
+
+    // These can be cleared (to save memory) without changing the answer.
+    void ClearCaches()
+    {
+        AlwaysTrueFormMap.clear();
+        MultInverseMap.clear();
+        SimplifyMap->clear();
+        SimplifyNegMap->clear();
+    }
+
   };//end of class Simplifier
 }; //end of namespace
 #endif

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index ecca8060117d227c04f6077fb924642d3cbafc93..81eac9fe0bafa5b86a2c8e982a0846c294687f40 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -69,14 +69,15 @@ namespace BEEV
    * unsat. else continue.
    */
   bool ToSAT::toSATandSolve(MINISAT::Solver& newSolver,
-                            ClauseList& cll, 
-                           bool add_xor_clauses,
+                            ClauseList& cll,
+                            bool final,
+                            CNFMgr*& cm,
+                            bool add_xor_clauses,
                            bool enable_clausal_abstraction)
   {
     CountersAndStats("SAT Solver", bm);
     bm->GetRunTimes()->start(RunTimes::SendingToSAT);
 
-    
     int input_clauselist_size = cll.size();
     if (cll.size() == 0)
       {
@@ -219,6 +220,24 @@ namespace BEEV
     // Free the clause list before SAT solving.
     cll.deleteJustVectors();
 
+    // Remove references to Tseitin variables.
+    // Delete the cnf generator.
+    if (final)
+    {
+       for (int i =0; i < _SATVar_to_AST_Vector.size();i++)
+       {
+               ASTNode n = _SATVar_to_AST_Vector[i];
+               if (!n.IsNull() && isTseitinVariable(n))
+               {
+                       _ASTNode_to_SATVar_Map.erase(n);
+                       _SATVar_to_AST_Vector[i] = ASTNode();
+               }
+       }
+       delete cm;
+       cm = NULL;
+    }
+
+
     bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
     bm->GetRunTimes()->start(RunTimes::Solving);    
 
@@ -272,7 +291,7 @@ namespace BEEV
   } //End of SortClauseList_IntoBuckets()
 
   bool ToSAT::CallSAT_On_ClauseBuckets(MINISAT::Solver& SatSolver,
-                                       ClauseBuckets * cb)
+                                       ClauseBuckets * cb, CNFMgr*& cm)
   {
     ClauseBuckets::iterator it = cb->begin();
     ClauseBuckets::iterator itend = cb->end();
@@ -281,7 +300,7 @@ namespace BEEV
     for(int count=1;it!=itend;it++, count++)
       {
         ClauseList *cl = (*it).second;
-           sat = toSATandSolve(SatSolver,*cl);
+           sat = toSATandSolve(SatSolver,*cl, count==cb->size(),cm);
 
         if(!sat)
           {
@@ -322,15 +341,17 @@ namespace BEEV
                file.close();
     }
 
-    CNFMgr cm(bm);
-    ClauseList* cl = cm.convertToCNF(BBFormula);
+    // The CNFMgr is deleted inside the CallSAT_On_ClauseBuckets,
+    // just before the final call to the SAT solver.
 
-    ClauseList* xorcl = cm.ReturnXorClauses();
+    CNFMgr* cm = new CNFMgr(bm);
+    ClauseList* cl = cm->convertToCNF(BBFormula);
+    ClauseList* xorcl = cm->ReturnXorClauses();
 
     ClauseBuckets * cb = Sort_ClauseList_IntoBuckets(cl);
     cl->asList()->clear(); // clause buckets now point to the clauses.
     delete cl;
-    bool sat = CallSAT_On_ClauseBuckets(SatSolver, cb);
+    bool sat = CallSAT_On_ClauseBuckets(SatSolver, cb, cm);
 
     for (ClauseBuckets::iterator it = cb->begin(); it != cb->end(); it++)
        delete it->second;
@@ -340,6 +361,8 @@ namespace BEEV
       {
        xorcl->deleteJustVectors();
        delete xorcl;
+       if (NULL != cm)
+               delete cm;
        return sat;
       }
 
@@ -350,8 +373,9 @@ namespace BEEV
       }
 #endif
 
-
     delete xorcl;
+       if (NULL != cm)
+               delete cm;
     return sat;
   }
 

diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h
index 9e413d5b0a49ba68f1ac57c0171ad8a5d7753b4a..4a44dd4eba09e62e4411305a4ca22e907a2e78b5 100644 (file)
--- a/src/to-sat/ToSAT.h
+++ b/src/to-sat/ToSAT.h
@@ -89,11 +89,16 @@ namespace BEEV
     //Iteratively goes through the Clause Buckets, and calls
       //toSATandSolve()
     bool CallSAT_On_ClauseBuckets(MINISAT::Solver& SatSolver,
-                                    ClauseBuckets * cb);
+                                    ClauseBuckets * cb
+                                    , CNFMgr*& cm);
+
 
       // Converts the clause to SAT and calls SAT solver
       bool toSATandSolve(MINISAT::Solver& S,
                          ClauseList& cll,
+                         bool final,
+                         CNFMgr*& cm,
+
                       bool add_xor_clauses=false,
                       bool enable_clausal_abstraction=false);