Cleanup. This removes some of the code for the user controlled abstraction-refinement...

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

diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp
index db071c2fc6fc8d0555e7202228777dfc3861fa25..4592366f5829495f1543f910891f233aaa012272 100644 (file)
--- a/src/STPManager/STPManager.cpp
+++ b/src/STPManager/STPManager.cpp
@@ -434,7 +434,7 @@ namespace BEEV
   }
 
   //add an assertion to the current logical context
-  void STPMgr::AddAssert(const ASTNode& assert, int assertion_bucket_key)
+  void STPMgr::AddAssert(const ASTNode& assert)
   {
     if (!(is_Form_kind(assert.GetKind()) 
          && BOOLEAN_TYPE == assert.GetType()))
@@ -442,83 +442,28 @@ namespace BEEV
         FatalError("AddAssert:Trying to assert a non-formula:", assert);
       }
 
-    IntToASTVecMap * AssertsMap;
-    //if the stack of assertion contexts is not empty, then take the
-    //top ASTVec and add the input assert to it
-    if(!_asserts.empty())
-      {
-       AssertsMap = _asserts.back();
-      }
-    else
-      {
-       AssertsMap = new IntToASTVecMap();
-       _asserts.push_back(AssertsMap);
-      }
+    if(_asserts.empty())
+       _asserts.push_back(new ASTVec());
 
-    ASTVec * v;
-    if(AssertsMap->find(assertion_bucket_key) != AssertsMap->end())
-      {
-       v = (*AssertsMap)[assertion_bucket_key];
-       v->push_back(assert);
-      }
-    else
-      {
-       v = new ASTVec();
-       v->push_back(assert);
-       (*AssertsMap)[assertion_bucket_key] = v;
-      }
-
-    //     //if the stack of ASTVec is not empty, then take the top ASTVec
-    //     //and add the input assert to it
-    //     if (!_asserts.empty())
-    //       {
-    //         v = _asserts.back();
-    //         //v->push_back(TransformFormula(assert));
-    //         v->push_back(assert);
-    //       }
-    //     else
-    //       {
-    //         //else create a logical context, and add it to the top of the
-    //         //stack
-    //         v = new ASTVec();
-    //         //v->push_back(TransformFormula(assert));
-    //         v->push_back(assert);
-    //         _asserts.push_back(v);
-    //       }
+    ASTVec& v = *_asserts.back();
+    v.push_back(assert);
   }
 
   void STPMgr::Push(void)
   {
-    //     ASTVec * v;
-    //     v = new ASTVec();
-    IntToASTVecMap * v;
-    v = new IntToASTVecMap();
-    _asserts.push_back(v);
+    _asserts.push_back(new ASTVec());
   }
 
-  void STPMgr::Pop(void)
+  void
+  STPMgr::Pop(void)
   {
-    if (!_asserts.empty())
-      {
-       IntToASTVecMap * c = _asserts.back();
-       IntToASTVecMap::iterator it = c->begin(), itend = c->end();
-       for(;it!=itend;it++)
-         {
-           ASTVec * cc = (*it).second;
-           cc->clear();
-           delete cc;
-         }
-       delete c;
-       _asserts.pop_back();
-       
-        // ASTVec * c = _asserts.back();
-       //         //by calling the clear function we ensure that the
-       //         ref count is //decremented for the ASTNodes stored
-       //         in c
-       //         c->clear();
-       //         delete c;
-       //         _asserts.pop_back();
-      }
+    if (_asserts.empty())
+      FatalError("POP on empty.");
+
+    ASTVec * c = _asserts.back();
+    c->clear();
+    delete c;
+    _asserts.pop_back();
   }
 
   void STPMgr::AddQuery(const ASTNode& q)
@@ -540,74 +485,21 @@ namespace BEEV
     return _current_query;
   }
 
-  const ASTVec STPMgr::GetAsserts(void)
+  const ASTVec
+  STPMgr::GetAsserts(void)
   {
-    vector<IntToASTVecMap *>::iterator it = _asserts.begin();
-    vector<IntToASTVecMap *>::iterator itend = _asserts.end();
+    vector<ASTVec *>::iterator it = _asserts.begin();
+    vector<ASTVec *>::iterator itend = _asserts.end();
 
     ASTVec v;
-    for(; it != itend; it++)
+    for (; it != itend; it++)
       {
-       IntToASTVecMap::iterator jt = (*it)->begin();
-       IntToASTVecMap::iterator jtend = (*it)->end();
-       
-       for(; jt != jtend; jt++)
-         {
-           ASTVec * cc = (*jt).second; 
-           if(NULL != cc && !cc->empty())
-             {
-               v.insert(v.end(), cc->begin(), cc->end());
-             }
-         }
+        if (!(*it)->empty())
+          v.insert(v.end(), (*it)->begin(), (*it)->end());
       }
-
     return v;
-    // vector<ASTVec *>::iterator it = _asserts.begin();
-    //     vector<ASTVec *>::iterator itend = _asserts.end();
-    
-    //     ASTVec v;
-    //     for (; it != itend; it++)
-    //       {
-    //         if (!(*it)->empty())
-    //           v.insert(v.end(), (*it)->begin(), (*it)->end());
-    //       }
-    //     return v;
   }
 
-  const ASTVec STPMgr::GetAsserts_WithKey(int key)
-  {
-    vector<IntToASTVecMap *>::iterator it = _asserts.begin();
-    vector<IntToASTVecMap *>::iterator itend = _asserts.end();
-
-    ASTVec v;
-    for(; it != itend; it++)
-      {
-       IntToASTVecMap * assert_map = (*it);
-       ASTVec * cc = (*assert_map)[key];
-       if(!cc->empty())
-         {
-           v.insert(v.end(), cc->begin(), cc->end());
-         }
-      }
-
-    return v;   
-  }
-
-  // //Create a new variable of ValueWidth 'n'
-  //   ASTNode STPMgr::NewArrayVar(unsigned int index, unsigned int value)
-  //   {
-  //     std::string c("v");
-  //     char d[32];
-  //     sprintf(d, "%d", _symbol_count++);
-  //     std::string ccc(d);
-  //     c += "_writearray_" + ccc;
-
-  //     ASTNode CurrentSymbol = CreateSymbol(c.c_str());
-  //     CurrentSymbol.SetValueWidth(value);
-  //     CurrentSymbol.SetIndexWidth(index);
-  //     return CurrentSymbol;
-  //   } //end of NewArrayVar()
-
   //prints statistics for the ASTNode
   void STPMgr::ASTNodeStats(const char * c, const ASTNode& a)
   {
@@ -726,15 +618,11 @@ namespace BEEV
                _symbol_unique_table.clear();
                _bvconst_unique_table.clear();
 
-               vector<IntToASTVecMap*>::iterator it = _asserts.begin();
-               vector<IntToASTVecMap*>::iterator itend = _asserts.end();
+               vector<ASTVec*>::iterator it = _asserts.begin();
+               vector<ASTVec*>::iterator itend = _asserts.end();
 
                for (; it != itend; it++) {
-                       IntToASTVecMap * j = (*it);
-                       for (IntToASTVecMap::iterator it2 = j->begin(); it2 != j->end(); it2++) {
-                               it2->second->clear();
-                               delete (it2->second);
-                       }
+                       ASTVec * j = (*it);
                        j->clear();
                        delete j;
                }

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index a329728c3fff1eed5c2509358576b4cf2736d1f5..937e2cb3211678f7d39795c5d84812c5ec209024 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -120,7 +120,7 @@ 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<IntToASTVecMap *> _asserts;
+    std::vector<ASTVec*> _asserts;
 
     // Memo table that tracks terms already seen
     ASTNodeMap TermsAlreadySeenMap;
@@ -389,11 +389,10 @@ namespace BEEV
     const ASTNode PopQuery();
     const ASTNode GetQuery();
     const ASTVec GetAsserts(void);
-    const ASTVec GetAsserts_WithKey(int key);
 
     //add a query/assertion to the current logical context
     void AddQuery(const ASTNode& q);
-    void AddAssert(const ASTNode& assert, int userguided_absrefine=0);
+    void AddAssert(const ASTNode& assert);
     
     /****************************************************************
      * Toplevel printing and stats functions                        *

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index aaba6b222b5f4d3ecc76ed414dd47bdb2c4b8dc3..5034c39caa1e780a9eaa749d1281e3d836c0f38e 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -399,7 +399,7 @@ Expr vc_writeExpr(VC vc, Expr array, Expr index, Expr newValue) {
 /////////////////////////////////////////////////////////////////////////////
 //! Assert a new formula in the current context.
 /*! The formula must have Boolean type. */
-void vc_assertFormula(VC vc, Expr e, int absrefine_bucket_num) {
+void vc_assertFormula(VC vc, Expr e) {
   nodestar a = (nodestar)e;
   bmstar b = (bmstar)(((stpstar)vc)->bm);
 
@@ -407,7 +407,7 @@ void vc_assertFormula(VC vc, Expr e, int absrefine_bucket_num) {
     BEEV::FatalError("Trying to assert a NON formula: ",*a);
 
   assert(BVTypeCheck(*a));
-  b->AddAssert(*a, absrefine_bucket_num);
+  b->AddAssert(*a);
 }
 
 void soft_time_out(int ignored)

diff --git a/src/c_interface/c_interface.h b/src/c_interface/c_interface.h
index de0dbd5e63967d95868a00ada705d1e9d27d7577..21847278fef405cac442bdfa6be9835243ebe721 100644 (file)
--- a/src/c_interface/c_interface.h
+++ b/src/c_interface/c_interface.h
@@ -198,7 +198,7 @@ extern "C" {
 
   //! Assert a new formula in the current context.
   /*! The formula must have Boolean type. */
-  void vc_assertFormula(VC vc, Expr e, int absrefine_bucket_num _CVCL_DEFAULT_ARG(0));
+  void vc_assertFormula(VC vc, Expr e);
 
   //! Simplify e with respect to the current context
   Expr vc_simplify(VC vc, Expr e);