From 1b7855194005d5aa0adb244ec22124144deb841e Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sat, 12 Jun 2010 14:55:37 +0000 Subject: [PATCH] Free up more memory before SAT solving. In particular this deletes the Tseitin variables before calling the SAT solver. This makes good sense for problems that aren't solved by abstraction / refinement. However, I'm not sure how it impacts difficult array problems. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@836 e59a4935-1847-0410-ae03-e826735625c1 --- src/STPManager/STP.cpp | 6 +++ src/STPManager/STPManager.cpp | 5 ++- .../CounterExample.cpp | 12 ++--- src/simplifier/simplifier.cpp | 15 ++++--- src/simplifier/simplifier.h | 10 +++++ src/to-sat/ToSAT.cpp | 44 ++++++++++++++----- src/to-sat/ToSAT.h | 7 ++- 7 files changed, 74 insertions(+), 25 deletions(-) diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 8dd54f4..346bc15 100644 --- 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 3f9ac52..1947efb 100644 --- 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 be693a0..73acbe6 100644 --- 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 4a5b504..da4e501 100644 --- 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 b78924d..f33074a 100644 --- 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 ecca806..81eac9f 100644 --- 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 9e413d5..4a44dd4 100644 --- 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); -- 2.47.3