Clean up. I think this is just a refactor, but aren't sure. The c_interface set remov...

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 68f13e5111bacb642c1acf0c8a244ffd03ac9969..47d29ec3e7161828fc3bd1fb33b3dea3b3e18de4 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -268,8 +268,8 @@ namespace BEEV {
     //DAG is minimized as much as possibly, and ideally should
     //garuntee that all liketerms in BVPLUSes have been combined.
     bm->SimplifyWrites_InPlace_Flag = false;
-    bm->Begin_RemoveWrites = false;
-    bm->start_abstracting = false;
+    //bm->Begin_RemoveWrites = false;
+    //bm->start_abstracting = false;
     bm->TermsAlreadySeenMap_Clear();
     do
       {
@@ -419,9 +419,9 @@ namespace BEEV {
 
     bm->TermsAlreadySeenMap_Clear();
 
-    bm->start_abstracting = false;
+    //bm->start_abstracting = false;
     bm->SimplifyWrites_InPlace_Flag = false;
-    bm->Begin_RemoveWrites = false;
+    //bm->Begin_RemoveWrites = false;
 
     long final_difficulty_score = difficulty.score(simplified_solved_InputToSAT);
     if (bm->UserFlags.stats_flag)

diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp
index e47541a4994a7ee62b3d47796d893077d92851b1..db071c2fc6fc8d0555e7202228777dfc3861fa25 100644 (file)
--- a/src/STPManager/STPManager.cpp
+++ b/src/STPManager/STPManager.cpp
@@ -637,14 +637,14 @@ namespace BEEV
   {
     if (READ == term.GetKind() 
         && WRITE == term[0].GetKind() 
-        && !GetRemoveWritesFlag())
+        /*&& !GetRemoveWritesFlag()*/)
       {
         return false;
       }
 
     if (READ == term.GetKind() 
         && WRITE == term[0].GetKind() 
-        && GetRemoveWritesFlag())
+        /*&& GetRemoveWritesFlag()*/)
       {
         return true;
       }
@@ -680,7 +680,7 @@ namespace BEEV
     return false;
   }//End of VarSeenInTerm
 
-  
+
   ASTNode STPMgr::NewParameterized_BooleanVar(const ASTNode& var,
                                               const ASTNode& constant)
   {
@@ -697,6 +697,7 @@ namespace BEEV
     return CurrentSymbol;
   } // End of NewParameterized_BooleanVar()
 
+
   
   //If ASTNode remain with references (somewhere), this will segfault.
   STPMgr::~STPMgr() {
@@ -712,7 +713,7 @@ namespace BEEV
                ASTTrue = ASTNode(0);
                ASTUndefined = ASTNode(0);
                _current_query = ASTNode(0);
-               dummy_node = ASTNode(0);
+               //dummy_node = ASTNode(0);
 
                zeroes.clear();
                ones.clear();

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index 8542ad00380452f736ec47ca966e99daee68fc79..03576ce2f098e0a76bac5ca7168fe49623474d25 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -54,11 +54,13 @@ namespace BEEV
       ASTBVConst::ASTBVConstHasher, 
       ASTBVConst::ASTBVConstEqual> ASTBVConstSet;
 
+#if 0
     typedef HASHMAP<
       ASTNode, 
       ASTNodeSet,
       ASTNode::ASTNodeHasher, 
       ASTNode::ASTNodeEqual> ASTNodeToSetMap;
+#endif
 
     // Unique node tables that enables common subexpression sharing
     ASTInteriorSet _interior_unique_table;
@@ -72,8 +74,8 @@ namespace BEEV
     // Global for assigning new node numbers.
     int _max_node_num;
 
-    ASTNode dummy_node;
-    
+    uint8_t last_iteration;
+
   public:
     HashingNodeFactory* hashingNodeFactory;
     NodeFactory *defaultNodeFactory;
@@ -81,8 +83,6 @@ namespace BEEV
     //frequently used nodes
     ASTNode ASTFalse, ASTTrue, ASTUndefined;
 
-    uint8_t last_iteration;
-
     // No nodes should already have the iteration number that is returned from here.
     // This never returns zero.
     uint8_t getNextIteration()
@@ -118,7 +118,6 @@ namespace BEEV
     // logical context is represented by a ptr to a vector of
     // assertions in that logical context. Logical contexts are
     // created by PUSH/POP
-    //std::vector<ASTVec *> _asserts;
     std::vector<IntToASTVecMap *> _asserts;
 
     // Memo table that tracks terms already seen
@@ -194,8 +193,8 @@ namespace BEEV
     // Flags indicates that counterexample will now be checked by the
     // counterexample checker, and hence simplifyterm must switch off
     // certain optimizations. In particular, array write optimizations
-    bool start_abstracting;
-    bool Begin_RemoveWrites;
+    //bool start_abstracting;
+    //bool Begin_RemoveWrites;
     bool SimplifyWrites_InPlace_Flag;
    
     //count is used in the creation of new variables
@@ -220,12 +219,12 @@ namespace BEEV
 
     {
       _max_node_num = 0;
-      Begin_RemoveWrites = false;
+      //Begin_RemoveWrites = false;
       ValidFlag = false;
       bvdiv_exception_occured = false;
       counterexample_checking_during_refinement = false;
-      start_abstracting = false;
-      Begin_RemoveWrites = false;
+      //start_abstracting = false;
+      //Begin_RemoveWrites = false;
       SimplifyWrites_InPlace_Flag = false;      
 
       // Need to initiate the node factories before any nodes are created.
@@ -245,6 +244,7 @@ namespace BEEV
       return runTimes;
     }
 
+#if 0
     void SetRemoveWritesFlag(bool in)
     {
       Begin_RemoveWrites = in;
@@ -254,6 +254,7 @@ namespace BEEV
     {
       return Begin_RemoveWrites;
     }
+#endif
 
     int NewNodeNum()
     {

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 165c8d9d3dc23c9602e3c28134c26a76a66f9e52..0d282d8644696a12f20a0e03d813022c19973ed1 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -208,14 +208,14 @@ static void vc_printAssertsToStream(VC vc, ostream &os, int simplify_print) {
   BEEV::ASTVec v = b->GetAsserts();
   BEEV::Simplifier * simp = new BEEV::Simplifier(b);
   for(BEEV::ASTVec::iterator i=v.begin(),iend=v.end();i!=iend;i++) {
-    b->Begin_RemoveWrites = true;
+    //b->Begin_RemoveWrites = true;
     BEEV::ASTNode q = 
       (simplify_print == 1) ? 
       simp->SimplifyFormula_TopLevel(*i,false) : *i;
     q = 
       (simplify_print == 1) ? 
       simp->SimplifyFormula_TopLevel(q,false) : q;
-    b->Begin_RemoveWrites = false;
+    //b->Begin_RemoveWrites = false;
     os << "ASSERT( ";
     q.PL_Print(os);
     os << ");" << endl;
@@ -243,12 +243,12 @@ void vc_printQueryStateToBuffer(VC vc, Expr e,
   vc_printAssertsToStream(vc, os, simplify_print);
   os << "%----------------------------------------------------" << endl;
   os << "QUERY( ";
-  b->Begin_RemoveWrites = true;
+  //b->Begin_RemoveWrites = true;
   BEEV::ASTNode q = 
     (simplify_print == 1) ? 
     simp->SimplifyFormula_TopLevel(*((nodestar)e),false) : 
     *(nodestar)e;
-  b->Begin_RemoveWrites = false;
+  //b->Begin_RemoveWrites = false;
   q.PL_Print(os);
   os << " );" << endl;
 
@@ -1417,21 +1417,21 @@ Expr vc_simplify(VC vc, Expr e) {
     {
       nodestar round1 = 
         new node(simp->SimplifyFormula_TopLevel(*a,false));
-      b->Begin_RemoveWrites = true;
+      //b->Begin_RemoveWrites = true;
       nodestar output = 
         new node(simp->SimplifyFormula_TopLevel(*round1,false));
       //if(cinterface_exprdelete_on) created_exprs.push_back(output);
-      b->Begin_RemoveWrites = false;
+      //b->Begin_RemoveWrites = false;
       delete round1;
       return output;
     }
   else 
     {
       nodestar round1 = new node(simp->SimplifyTerm(*a));
-      b->Begin_RemoveWrites = true;
+      //b->Begin_RemoveWrites = true;
       nodestar output = new node(simp->SimplifyTerm(*round1));
       //if(cinterface_exprdelete_on) created_exprs.push_back(output);
-      b->Begin_RemoveWrites = false;
+      //b->Begin_RemoveWrites = false;
       delete round1;
       return output;
     }

diff --git a/src/cpp_interface/cpp_interface.h b/src/cpp_interface/cpp_interface.h
index 3b2f3af9bf9f0c5970f0b96656e12968c7e40a1f..5b7e4a970547b9fae8c053e3b39bd8a85f7bdfbe 100644 (file)
--- a/src/cpp_interface/cpp_interface.h
+++ b/src/cpp_interface/cpp_interface.h
@@ -21,6 +21,34 @@ namespace BEEV
     //boost::object_pool<ASTNode> node_pool;
     bool alreadyWarned;
     bool print_success;
+
+    // Used to cache prior queries.
+    struct Entry
+    {
+      explicit
+      Entry(SOLVER_RETURN_TYPE result_)
+      {
+        result = result_;
+      }
+
+      SOLVER_RETURN_TYPE result;
+      ASTNode node;
+
+      void
+      print()
+      {
+        if (result == SOLVER_UNSATISFIABLE)
+          cerr << "u";
+        else if (result == SOLVER_SATISFIABLE)
+          cerr << "s";
+        else if (result == SOLVER_UNDECIDED)
+          cerr << "?";
+      }
+    };
+    vector<Entry> cache;
+    vector<vector<ASTNode> > symbols;
+
+
   public:
     LETMgr letMgr;
     NodeFactory* nf;
@@ -35,6 +63,16 @@ namespace BEEV
       print_success = false;
     }
 
+    void
+    startup()
+    {
+      CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot();
+      if(0 != c) {
+        cout << CONSTANTBV::BitVector_Error(c) << endl;
+        FatalError("Bad startup");
+      }
+    }
+
     const ASTVec
     GetAsserts(void)
     {
@@ -176,31 +214,6 @@ namespace BEEV
       //node_pool.destroy(n);
     }
 
-    struct Entry
-    {
-      explicit
-      Entry(SOLVER_RETURN_TYPE result_)
-      {
-        result = result_;
-      }
-
-      SOLVER_RETURN_TYPE result;
-      ASTNode node;
-
-      void
-      print()
-      {
-        if (result == SOLVER_UNSATISFIABLE)
-          cerr << "u";
-        else if (result == SOLVER_SATISFIABLE)
-          cerr << "s";
-        else if (result == SOLVER_UNDECIDED)
-          cerr << "?";
-      }
-    };
-    vector<Entry> cache;
-    vector<vector<ASTNode> > symbols;
-
     void
     addSymbol(ASTNode &s)
     {
@@ -270,4 +283,4 @@ namespace BEEV
   };
 }
 
-#endif /* PARSERINTERFACE_H_ */
+#endif

diff --git a/src/main/main.cpp b/src/main/main.cpp
index f043fe50519fad7d77c4a606cf9c9d8ea45019ad..d40acb4feacda37941cde4a7e827d5edc5bf194b 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -410,11 +410,6 @@ int main(int argc, char ** argv) {
   //want to print the output always from the commandline.
   bm->UserFlags.print_output_flag = true;
   ASTVec * AssertsQuery = new ASTVec;
-  CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot();
-  if(0 != c) {
-    cout << CONSTANTBV::BitVector_Error(c) << endl;
-    return 0;
-  }
 
   bm->GetRunTimes()->start(RunTimes::Parsing);
        {
@@ -433,6 +428,8 @@ int main(int argc, char ** argv) {
                else
                        parserInterface = &piTypeCheckSimp;
 
+                 parserInterface->startup();
+
                if (onePrintBack)
                  {
                    if (bm->UserFlags.smtlib2_parser_flag)

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index fa3c59b80c66e042c230f08739f5b18bbaeea3e7..1afbb20ae07f0ab351c070987dd6aa5a98d22d8d 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -219,7 +219,7 @@ namespace BEEV
   ASTNode
   Simplifier::SimplifyFormula_NoRemoveWrites(const ASTNode& b, bool pushNeg, ASTNodeMap* VarConstMap)
   {
-    _bm->Begin_RemoveWrites = false;
+    //_bm->Begin_RemoveWrites = false;
     ASTNode out = SimplifyFormula(b, pushNeg, VarConstMap);
     return out;
   }