From: vijay_ganesh Date: Tue, 13 Oct 2009 19:12:36 +0000 (+0000) Subject: push/pop now working through the c_interface. Clearalltabes has been implemented... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=f0b55c1462958d59c689095b726e9163efee0310;p=francis%2Fstp.git push/pop now working through the c_interface. Clearalltabes has been implemented correctly and tested git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@300 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h index 97b7775..8ae199d 100644 --- a/src/AST/ArrayTransformer.h +++ b/src/AST/ArrayTransformer.h @@ -124,6 +124,7 @@ namespace BEEV { Arrayread_IteMap = new ASTNodeMap(INITIAL_TABLE_SIZE); Arrayname_ReadindicesMap = new ASTNodeToVecMap(INITIAL_TABLE_SIZE); + runTimes = bm->GetRunTimes(); ASTTrue = bm->CreateNode(TRUE); ASTFalse = bm->CreateNode(FALSE); @@ -176,11 +177,19 @@ namespace BEEV void ClearAllTables(void) { + + for (ASTNodeToVecMap::iterator + iset = Arrayname_ReadindicesMap->begin(), + iset_end = Arrayname_ReadindicesMap->end(); + iset != iset_end; iset++) + { + iset->second.clear(); + } + Arrayname_ReadindicesMap->clear(); Arrayread_SymbolMap.clear(); Arrayread_IteMap->clear(); Introduced_SymbolsSet.clear(); - TransformMap->clear(); } }; //end of class Transformer diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 77c6f4b..abc58a4 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -91,9 +91,8 @@ namespace BEEV { } } while (inputToSAT != simplified_solved_InputToSAT); - bm->ASTNodeStats("After SimplifyWrites_Inplace: ", simplified_solved_InputToSAT); - delete bvsolver; - bvsolver = NULL; + bm->ASTNodeStats("After SimplifyWrites_Inplace: ", + simplified_solved_InputToSAT); bm->start_abstracting = (arraywrite_refinement_flag) ? true : false; bm->SimplifyWrites_InPlace_Flag = false; @@ -179,92 +178,92 @@ namespace BEEV { return SOLVER_ERROR; } //End of TopLevelSTPAux - void STP::ClearAllTables(void) - { -// //Clear STPManager caches - -// //Clear ArrayTransformer caches - -// //Clear Simplifier caches - -// //Clear BVSolver caches - -// //Clear AbsRefine_CounterExample caches - -// //clear all tables before calling toplevelsat -// //_ASTNode_to_SATVar.clear(); -// //_SATVar_to_AST.clear(); - -// // for (ASTtoBitvectorMap::iterator it = _ASTNode_to_Bitvector.begin(), -// // itend = _ASTNode_to_Bitvector.end(); it != itend; it++) -// // { -// // (it->second)->clear(); -// // delete (it->second); -// // } -// // _ASTNode_to_Bitvector.clear(); - -// NodeLetVarMap.clear(); -// NodeLetVarMap1.clear(); -// PLPrintNodeSet.clear(); -// AlreadyPrintedSet.clear(); -// //ReferenceCount->clear(); -// //_arrayread_ite.clear(); -// //_introduced_symbols.clear(); -// //CounterExampleMap.clear(); -// //ComputeFormulaMap.clear(); -// StatInfoSet.clear(); - -// _asserts.clear(); - -// // for (ASTNodeToVecMap::iterator iset = -// // _arrayname_readindices.begin(), iset_end = -// // _arrayname_readindices.end(); iset != iset_end; iset++) { -// // iset->second.clear(); } -// // _arrayname_readindices.clear(); - -// _interior_unique_table.clear(); -// _symbol_unique_table->clear(); -// _bvconst_unique_table.clear(); - } - - void STP::ClearAllCaches(void) - { -// //clear all tables before calling toplevelsat -// //_ASTNode_to_SATVar.clear(); -// //_SATVar_to_AST.clear(); - -// // for (ASTtoBitvectorMap::iterator it = _ASTNode_to_Bitvector.begin(), -// // itend = _ASTNode_to_Bitvector.end(); it != itend; it++) -// // { -// // (it->second)->clear(); -// // delete (it->second); -// // } -// // _ASTNode_to_Bitvector.clear(); +// void STP::ClearAllTables(void) +// { +// // //Clear STPManager caches + +// // //Clear ArrayTransformer caches + +// // //Clear Simplifier caches + +// // //Clear BVSolver caches + +// // //Clear AbsRefine_CounterExample caches + +// // //clear all tables before calling toplevelsat +// // //_ASTNode_to_SATVar.clear(); +// // //_SATVar_to_AST.clear(); + +// // // for (ASTtoBitvectorMap::iterator it = _ASTNode_to_Bitvector.begin(), +// // // itend = _ASTNode_to_Bitvector.end(); it != itend; it++) +// // // { +// // // (it->second)->clear(); +// // // delete (it->second); +// // // } +// // // _ASTNode_to_Bitvector.clear(); + +// // NodeLetVarMap.clear(); +// // NodeLetVarMap1.clear(); +// // PLPrintNodeSet.clear(); +// // AlreadyPrintedSet.clear(); +// // //ReferenceCount->clear(); +// // //_arrayread_ite.clear(); +// // //_introduced_symbols.clear(); +// // //CounterExampleMap.clear(); +// // //ComputeFormulaMap.clear(); +// // StatInfoSet.clear(); + +// // _asserts.clear(); + +// // // for (ASTNodeToVecMap::iterator iset = +// // // _arrayname_readindices.begin(), iset_end = +// // // _arrayname_readindices.end(); iset != iset_end; iset++) { +// // // iset->second.clear(); } +// // // _arrayname_readindices.clear(); + +// // _interior_unique_table.clear(); +// // _symbol_unique_table->clear(); +// // _bvconst_unique_table.clear(); +// } + +// void STP::ClearAllCaches(void) +// { +// // //clear all tables before calling toplevelsat +// // //_ASTNode_to_SATVar.clear(); +// // //_SATVar_to_AST.clear(); + +// // // for (ASTtoBitvectorMap::iterator it = _ASTNode_to_Bitvector.begin(), +// // // itend = _ASTNode_to_Bitvector.end(); it != itend; it++) +// // // { +// // // (it->second)->clear(); +// // // delete (it->second); +// // // } +// // // _ASTNode_to_Bitvector.clear(); -// NodeLetVarMap.clear(); -// NodeLetVarMap1.clear(); -// PLPrintNodeSet.clear(); -// AlreadyPrintedSet.clear(); -// // SimplifyMap->clear(); -// // SimplifyNegMap->clear(); -// // ReferenceCount->clear(); -// // SolverMap.clear(); -// //AlwaysTrueFormMap.clear(); -// //_arrayread_ite.clear(); -// //_arrayread_symbol.clear(); -// //_introduced_symbols.clear(); -// //CounterExampleMap.clear(); -// //ComputeFormulaMap.clear(); -// StatInfoSet.clear(); - -// // for (ASTNodeToVecMap::iterator iset = _arrayname_readindices.begin(), iset_end = _arrayname_readindices.end(); iset != iset_end; iset++) -// // { -// // iset->second.clear(); -// // } +// // NodeLetVarMap.clear(); +// // NodeLetVarMap1.clear(); +// // PLPrintNodeSet.clear(); +// // AlreadyPrintedSet.clear(); +// // // SimplifyMap->clear(); +// // // SimplifyNegMap->clear(); +// // // ReferenceCount->clear(); +// // // SolverMap.clear(); +// // //AlwaysTrueFormMap.clear(); +// // //_arrayread_ite.clear(); +// // //_arrayread_symbol.clear(); +// // //_introduced_symbols.clear(); +// // //CounterExampleMap.clear(); +// // //ComputeFormulaMap.clear(); +// // StatInfoSet.clear(); + +// // // for (ASTNodeToVecMap::iterator iset = _arrayname_readindices.begin(), iset_end = _arrayname_readindices.end(); iset != iset_end; iset++) +// // // { +// // // iset->second.clear(); +// // // } -// // _arrayname_readindices.clear(); -// //_interior_unique_table.clear(); -// //_symbol_unique_table.clear(); -// //_bvconst_unique_table.clear(); - } +// // // _arrayname_readindices.clear(); +// // //_interior_unique_table.clear(); +// // //_symbol_unique_table.clear(); +// // //_bvconst_unique_table.clear(); +// } }; //end of namespace diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h index e751b30..5929778 100644 --- a/src/STPManager/STP.h +++ b/src/STPManager/STP.h @@ -85,9 +85,17 @@ namespace BEEV // request. SOLVER_RETURN_TYPE TopLevelSTPAux(const ASTNode& inputasserts_and_query); - void ClearAllCaches(void); + //void ClearAllCaches(void); - void ClearAllTables(void); + void ClearAllTables(void) + { + bm->ClearAllTables(); + simp->ClearAllTables(); + bvsolver->ClearAllTables(); + arrayTransformer->ClearAllTables(); + tosat->ClearAllTables(); + Ctr_Example->ClearAllTables(); + } }; //End of Class STP };//end of namespace #endif diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h index af20429..337b707 100644 --- a/src/STPManager/STPManager.h +++ b/src/STPManager/STPManager.h @@ -79,7 +79,11 @@ namespace BEEV // created by PUSH/POP std::vector _asserts; - //bool Begin_RemoveWrites; + // Memo table that tracks terms already seen + ASTNodeMap TermsAlreadySeenMap; + + //Map for computing ASTNode stats + ASTNodeSet StatInfoSet; // The query for the current logical context. ASTNode _current_query; @@ -90,12 +94,6 @@ namespace BEEV // Ptr to class that reports on the running time of various parts // of the code RunTimes * runTimes; - - // Memo table that tracks terms already seen - ASTNodeMap TermsAlreadySeenMap; - - //Map for computing ASTNode stats - ASTNodeSet StatInfoSet; /**************************************************************** * Private Member Functions * @@ -373,10 +371,16 @@ namespace BEEV void ClearAllTables(void) { - _interior_unique_table.clear(); - _bvconst_unique_table.clear(); - _symbol_unique_table.clear(); - } + // _interior_unique_table.clear(); + // _bvconst_unique_table.clear(); + // _symbol_unique_table.clear(); + NodeLetVarMap.clear(); + NodeLetVarMap1.clear(); + PLPrintNodeSet.clear(); + AlreadyPrintedSet.clear(); + StatInfoSet.clear(); + //_asserts.clear(); + } //End of ClearAllTables() };//End of Class STPMgr };//end of namespace diff --git a/src/absrefine_counterexample/AbsRefine_CounterExample.h b/src/absrefine_counterexample/AbsRefine_CounterExample.h index d2629db..10f4c91 100644 --- a/src/absrefine_counterexample/AbsRefine_CounterExample.h +++ b/src/absrefine_counterexample/AbsRefine_CounterExample.h @@ -173,6 +173,15 @@ namespace BEEV void ClearAllTables(void) { + CounterExampleMap.clear(); + for (ASTtoBitvectorMap::iterator + it = _ASTNode_to_BitvectorMap.begin(), + itend = _ASTNode_to_BitvectorMap.end(); + it != itend; it++) + { + (it->second)->clear(); + delete (it->second); + } _ASTNode_to_BitvectorMap.clear(); ComputeFormulaMap.clear(); } //End of ClearAllTables() diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index 1a7ca01..6c93812 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -485,7 +485,7 @@ int vc_query(VC vc, Expr e) { void vc_push(VC vc) { bmstar b = (bmstar)(((stpstar)vc)->bm); - ((stpstar)vc)->ClearAllCaches(); + ((stpstar)vc)->ClearAllTables(); b->Push(); } diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h index 6c531c6..91048b5 100644 --- a/src/simplifier/bvsolver.h +++ b/src/simplifier/bvsolver.h @@ -149,6 +149,14 @@ namespace BEEV //Top Level Solver: Goes over the input DAG, identifies the //equation to be solved, solves them, ASTNode TopLevelBVSolve(const ASTNode& a); + + void ClearAllTables(void) + { + DoNotSolve_TheseVars.clear(); + FormulasAlreadySolvedMap.clear(); + TermsAlreadySeenMap_ForArrays.clear(); + } //End of ClearAllTables() + }; //end of class bvsolver };//end of namespace BEEV #endif diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h index 5f113cc..9e602db 100644 --- a/src/simplifier/simplifier.h +++ b/src/simplifier/simplifier.h @@ -251,6 +251,7 @@ namespace BEEV NewName_ReadOverWrite_Map.clear(); AlwaysTrueFormMap.clear(); MultInverseMap.clear(); + ReferenceCount->clear(); } };//end of class Simplifier }; //end of namespace diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile index 6fa9f78..01e651e 100644 --- a/tests/c-api-tests/Makefile +++ b/tests/c-api-tests/Makefile @@ -18,8 +18,8 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 g++ $(CXXFLAGS) getbvunsignedlonglong-check.c -lstp -o a3.out ./a3.out 4: -# g++ $(CXXFLAGS) multiple-queries.c -lstp -o a4.out -# ./a4.out + g++ $(CXXFLAGS) multiple-queries.c -lstp -o a4.out + ./a4.out 5: g++ $(CXXFLAGS) parsefile-using-cinterface.c -lstp -o a5.out ./a5.out @@ -27,8 +27,8 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 g++ $(CXXFLAGS) print.c -lstp -o a6.out ./a6.out 7: -# g++ $(CXXFLAGS) push-pop-1.c -lstp -o a7.out -# ./a7.out + g++ $(CXXFLAGS) push-pop-1.c -lstp -o a7.out + ./a7.out 8: g++ $(CXXFLAGS) sbvmod.c -lstp -o a8.out ./a8.out @@ -42,11 +42,11 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 g++ $(CXXFLAGS) squares-leak.c -lstp -o a11.out ./a11.out 12: -# g++ $(CXXFLAGS) stp-counterex.c -lstp -o a12.out -# ./a12.out + g++ $(CXXFLAGS) stp-counterex.c -lstp -o a12.out + ./a12.out 13: -# g++ $(CXXFLAGS) stp-div-001.c -lstp -o a13.out -# ./a13.out + g++ $(CXXFLAGS) stp-div-001.c -lstp -o a13.out + ./a13.out 14: g++ $(CXXFLAGS) stpcheck.c -o a14.out -lstp ./a14.out @@ -57,8 +57,8 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 g++ $(CXXFLAGS) y.c -lstp -o a16.out ./a16.out 17: -# g++ $(CXXFLAGS) push-pop.c -lstp -o a17.out -# ./a17.out + g++ $(CXXFLAGS) push-pop.c -lstp -o a17.out + ./a17.out 18: g++ $(CXXFLAGS) cvc-to-c.cpp -lstp -o a18.out #./a18.out ./t.cvc