push/pop now working through the c_interface. Clearalltabes has been implemented...

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 97b7775727acae432ca04fb7943ce1db3ce3390e..8ae199d5a7c42a5cb3f2b9fc9c90a7546e82e4c4 100644 (file)
--- 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 77c6f4bcb2c8b564ba4728a160aa252c345c455c..abc58a41608b35abc5dd28cb5196492e4ec9f86a 100644 (file)
--- 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 e751b303f0432178fbce49a06285196c717ddc66..59297788522011003de5d1059e12600155676bb5 100644 (file)
--- 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 af204298b8ea1b36768686204b6393c0bbb31af9..337b70757bba99e698d825f2db2b1277b9855332 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -79,7 +79,11 @@ namespace BEEV
     // created by PUSH/POP
     std::vector<ASTVec *> _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 d2629db344722e08e0595f4f7040793f00ea519b..10f4c9103f1f3688797670f98fa81dc1024c9e60 100644 (file)
--- 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 1a7ca01a5e8151dc9622e64b44b193f271e364da..6c9381215056e23f13d6704690029d379eacbe9a 100644 (file)
--- 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 6c531c61c3a5d1f9ed532a07cd4669fce25ecf93..91048b5d888583be6a4c94700f3fd0353c7760c5 100644 (file)
--- 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 5f113ccdd9bc13f1c5a7d7456095346a700f2a72..9e602dbad932252757961db90c24315ff2c981fb 100644 (file)
--- 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 6fa9f78dce5e7a16da5ca3396dc28b00b55b4b2a..01e651ebdb28b58ad40cfa18897f43a79df3aa4b 100644 (file)
--- 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