From: trevor_hansen Date: Sat, 12 Jun 2010 14:55:37 +0000 (+0000) Subject: Free up more memory before SAT solving. In particular this deletes the Tseitin variab... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=1b7855194005d5aa0adb244ec22124144deb841e;p=francis%2Fstp.git 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 --- 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);