renamed BeevMgr to STPMgr

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

diff --git a/src/AST/AST.h b/src/AST/AST.h
index a8070dc9dc0cfdf072b5a9390dc2eac6b104a221..f68f31408c81ed6bfbf53d201834d0958908f712 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -9,7 +9,7 @@
 
 #ifndef AST_H
 #define AST_H
-#include "TopLevel.h"
+#include "UsefulDefs.h"
 #include "ASTNode.h"
 #include "ASTInternal.h"
 #include "ASTInterior.h"

diff --git a/src/AST/ASTBVConst.h b/src/AST/ASTBVConst.h
index f93c5652fae5d0b7e6c52fdcbc36201901381735..093c1ce9fb93e62d3bfe3b8b1935d371b553a50c 100644 (file)
--- a/src/AST/ASTBVConst.h
+++ b/src/AST/ASTBVConst.h
@@ -11,7 +11,7 @@
 #define ASTBVCONST_H
 namespace BEEV
 {
-  class BeevMgr;
+  class STPMgr;
   void FatalError(const char * str);
 
   /******************************************************************
@@ -21,7 +21,7 @@ namespace BEEV
    ******************************************************************/
   class ASTBVConst: public ASTInternal
   {
-    friend class BeevMgr;
+    friend class STPMgr;
     friend class ASTNode;
     friend class ASTNodeHasher;
     friend class ASTNodeEqual;

diff --git a/src/AST/ASTInterior.h b/src/AST/ASTInterior.h
index eeb73e4cd5ff97686ddfee1c2437c19fc98a8121..4db901ae6adbed42844ac4b965e5aec1ebd8d354 100644 (file)
--- a/src/AST/ASTInterior.h
+++ b/src/AST/ASTInterior.h
@@ -10,11 +10,11 @@
 #ifndef ASTINTERIOR_H
 #define ASTINTERIOR_H
 
-#include "TopLevel.h"
+#include "UsefulDefs.h"
 namespace BEEV
 {
   class ASTNode;
-  class BeevMgr;
+  class STPMgr;
   typedef vector<ASTNode> ASTVec;
   
   /******************************************************************
@@ -26,7 +26,7 @@ namespace BEEV
   class ASTInterior: public ASTInternal
   {
 
-    friend class BeevMgr;
+    friend class STPMgr;
     friend class ASTNodeHasher;
     friend class ASTNodeEqual;
 

diff --git a/src/AST/ASTNode.cpp b/src/AST/ASTNode.cpp
index 3f47d50040c88b293b5e427025be352037cfaf97..a87ca49481e673f297bd2ef42e39c4e7a850c405 100644 (file)
--- a/src/AST/ASTNode.cpp
+++ b/src/AST/ASTNode.cpp
@@ -114,15 +114,15 @@ namespace BEEV
       }
   } //End of Destructor()
 
-   BeevMgr* ASTNode::GetBeevMgr() const
+   STPMgr* ASTNode::GetSTPMgr() const
   {
     return GlobalSTP->bm;
-  } //End of GetBeevMgr()
+  } //End of GetSTPMgr()
 
   // Checks if the node has alreadybeen printed or not
   bool ASTNode::IsAlreadyPrinted() const
   {
-    BeevMgr * bm = GetBeevMgr();
+    STPMgr * bm = GetSTPMgr();
     return (bm->AlreadyPrintedSet.find(*this) != 
            bm->AlreadyPrintedSet.end());
   } //End of IsAlreadyPrinted()
@@ -130,7 +130,7 @@ namespace BEEV
   // Mark the node as printed if it has been already printed
   void ASTNode::MarkAlreadyPrinted() const
   {
-    BeevMgr * bm = GetBeevMgr();
+    STPMgr * bm = GetSTPMgr();
     bm->AlreadyPrintedSet.insert(*this);
   } //End of MarkAlreadyPrinted()
 
@@ -202,7 +202,7 @@ namespace BEEV
       return;
 
     //FIXME: this is ugly.
-    BeevMgr * bm = GetBeevMgr();
+    STPMgr * bm = GetSTPMgr();
     const ASTVec &c = this->GetChildren();
     for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++)
       {

diff --git a/src/AST/ASTNode.h b/src/AST/ASTNode.h
index e41f0f4cccc2b3aecc2501dd8e86a664b9d5cbc5..0355c07d89da1a0c789f3e3116665a29e3968d27 100644 (file)
--- a/src/AST/ASTNode.h
+++ b/src/AST/ASTNode.h
@@ -23,7 +23,7 @@ namespace BEEV
    ******************************************************************/
   class ASTNode
   {
-    friend class BeevMgr;
+    friend class STPMgr;
     friend class CNFMgr;
     friend class ASTInterior;
     friend class vector<ASTNode>;
@@ -151,9 +151,9 @@ namespace BEEV
     // Assignment (for ref counting)
     ASTNode& operator=(const ASTNode& n);
 
-    //Get the BeevMgr pointer. FIXME: Currently uses a global
+    //Get the STPMgr pointer. FIXME: Currently uses a global
     //ptr. BAD!!
-    BeevMgr* GetBeevMgr() const;
+    STPMgr* GetSTPMgr() const;
 
     // Access node number
     int GetNodeNum() const;

diff --git a/src/AST/ASTSymbol.h b/src/AST/ASTSymbol.h
index 6bc8a5dcc8efd83d660192fc79302d33f6c4372f..e1667995137bdc54128a9004c8c99b6dcfe35b50 100644 (file)
--- a/src/AST/ASTSymbol.h
+++ b/src/AST/ASTSymbol.h
@@ -21,7 +21,7 @@ namespace BEEV
    ******************************************************************/
   class ASTSymbol : public ASTInternal
   {
-    friend class BeevMgr;
+    friend class STPMgr;
     friend class ASTNode;
     friend class ASTNodeHasher;
     friend class ASTNodeEqual;

diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp
index e96ab26a3714b18840ffc7deb74a89353354352f..6616d37214496844631a1ded027f0406b6de5519 100644 (file)
--- a/src/AST/ArrayTransformer.cpp
+++ b/src/AST/ArrayTransformer.cpp
@@ -176,7 +176,7 @@ namespace BEEV
    ********************************************************/
   ASTNode ArrayTransformer::TransformFormula(const ASTNode& form)
   {
-    BeevMgr* bm = form.GetBeevMgr();
+    STPMgr* bm = form.GetSTPMgr();
 
     assert(TransformMap != NULL);
 
@@ -300,11 +300,8 @@ namespace BEEV
   {
     assert(TransformMap != NULL);
 
-    BeevMgr* bm = inputterm.GetBeevMgr();
-
     ASTNode result;
     ASTNode term = inputterm;
-
     Kind k = term.GetKind();
     if (!is_Term_kind(k))
       FatalError("TransformTerm: Illegal kind: You have input a nonterm:", inputterm, k);

diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h
index fdfb1366b7ed761d7e45c1b6ddde5629c055bf0c..ca6f111b561071590482d38e07741781f7e96bb9 100644 (file)
--- a/src/AST/ArrayTransformer.h
+++ b/src/AST/ArrayTransformer.h
@@ -84,7 +84,7 @@ namespace BEEV
     Simplifier * simp;
 
     // Ptr to STPManager
-    BeevMgr * bm;
+    STPMgr * bm;
     
     // Ptr to class that records the runtimes for various parts of the
     // code
@@ -115,7 +115,7 @@ namespace BEEV
      ****************************************************************/      
     
     // Constructor
-    ArrayTransformer(BeevMgr * bm, Simplifier* s) : 
+    ArrayTransformer(STPMgr * bm, Simplifier* s) : 
       Arrayread_SymbolMap(INITIAL_TABLE_SIZE),
       Introduced_SymbolsSet(INITIAL_TABLE_SIZE),
       bm(bm), 

diff --git a/src/AST/TopLevel.h b/src/AST/UsefulDefs.h
similarity index 97%
rename from src/AST/TopLevel.h
rename to src/AST/UsefulDefs.h
index 11e482ddb6645f5008434ae2213d803c2a3ab69b..4d936ba802d9b917cfea4470414de64271e5c126 100644 (file)
--- a/src/AST/TopLevel.h
+++ b/src/AST/UsefulDefs.h
@@ -21,7 +21,7 @@
 #include <algorithm>
 #include <assert.h>
 
-#define  INITIAL_TABLE_SIZE 100
+#define  INITIAL_TABLE_SIZE 1000
 
 #ifdef EXT_HASH_MAP
  #include <ext/hash_set>
@@ -58,7 +58,7 @@ namespace BEEV {
    * Important classes declared as part of AST datastructures       *
    *                                                                *
    ******************************************************************/
-  class BeevMgr;
+  class STPMgr;
   class ASTNode;
   class ASTInternal;
   class ASTInterior;

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 893bf9f4ca94f1cb39d977ac87cb63fdb54ef735..77c6f4bcb2c8b564ba4728a160aa252c345c455c 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -14,7 +14,7 @@ namespace BEEV {
   //Acceps a query, calls the SAT solver and generates Valid/InValid.
   //if returned 0 then input is INVALID if returned 1 then input is
   //VALID if returned 2 then UNDECIDED
-  SOLVER_RETURN_TYPE STP::TopLevelSATAux(const ASTNode& inputasserts_and_query)
+  SOLVER_RETURN_TYPE STP::TopLevelSTPAux(const ASTNode& inputasserts_and_query)
   {
     ASTNode inputToSAT = inputasserts_and_query;
     ASTNode orig_input = inputToSAT;
@@ -173,9 +173,98 @@ namespace BEEV {
         return res;
       }
 
-    FatalError("TopLevelSATAux: reached the end without proper conclusion:"
+    FatalError("TopLevelSTPAux: reached the end without proper conclusion:"
                "either a divide by zero in the input or a bug in STP");
     //bogus return to make the compiler shut up
     return SOLVER_ERROR;
-  } //End of TopLevelSATAux
+  } //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();
+    
+//     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();
+  }
 }; //end of namespace

diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h
index 03a356e4eb04743c6a78e26b097d61302e633211..58275bf423fb552bc7d139dc50e9d68c58b130a9 100644 (file)
--- a/src/STPManager/STP.h
+++ b/src/STPManager/STP.h
@@ -24,7 +24,7 @@ namespace BEEV
 {
   class STP {
   public:
-    BeevMgr * bm;
+    STPMgr * bm;
     Simplifier * simp;
     BVSolver * bvsolver;
     ArrayTransformer * arrayTransformer;
@@ -32,7 +32,7 @@ namespace BEEV
     AbsRefine_CounterExample * Ctr_Example;
 
     //Constructor
-    STP(BeevMgr* b,
+    STP(STPMgr* b,
        Simplifier* s,
        BVSolver* bsolv,
        ArrayTransformer * a,
@@ -47,20 +47,31 @@ namespace BEEV
       Ctr_Example = ce;
     }// End of constructor
 
-    SOLVER_RETURN_TYPE TopLevelSAT(const ASTNode& inputasserts, 
+    ~STP()
+    {
+      ClearAllTables();          
+    }
+
+    // The absolute TopLevel function that invokes STP on the input
+    // formula
+    SOLVER_RETURN_TYPE TopLevelSTP(const ASTNode& inputasserts, 
                                   const ASTNode& query)
     {      
       ASTNode q = bm->CreateNode(AND, 
                                 inputasserts, 
                                 bm->CreateNode(NOT, query));
-      return TopLevelSATAux(q);
-    } //End of TopLevelSAT()    
+      return TopLevelSTPAux(q);
+    } //End of TopLevelSTP()    
 
     // Accepts query and returns the answer. if query is valid,
     // returns VALID, else returns INVALID. Automatically constructs
     // counterexample for invalid queries, and prints them upon
     // request.    
-    SOLVER_RETURN_TYPE TopLevelSATAux(const ASTNode& inputasserts_and_query);
+    SOLVER_RETURN_TYPE TopLevelSTPAux(const ASTNode& inputasserts_and_query);
+
+    void ClearAllCaches(void);
+    
+    void ClearAllTables(void);    
   }; //End of Class STP
 };//end of namespace
 #endif

diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp
index e04f907dec26326cac4932441b50d4b6efaf5e65..bade332271f19a7f2c64b275b898c8785fdf65b8 100644 (file)
--- a/src/STPManager/STPManager.cpp
+++ b/src/STPManager/STPManager.cpp
@@ -16,7 +16,7 @@
 
 namespace BEEV
 {
-  ASTInterior *BeevMgr::LookupOrCreateInterior(ASTInterior *n_ptr)
+  ASTInterior *STPMgr::LookupOrCreateInterior(ASTInterior *n_ptr)
   {
     ASTInteriorSet::iterator it = _interior_unique_table.find(n_ptr);
     if (it == _interior_unique_table.end())
@@ -44,9 +44,9 @@ namespace BEEV
   
  
   ////////////////////////////////////////////////////////////////
-  //  BeevMgr members
+  //  STPMgr members
   ////////////////////////////////////////////////////////////////
-  ASTNode BeevMgr::CreateNode(Kind kind, const ASTVec & back_children)
+  ASTNode STPMgr::CreateNode(Kind kind, const ASTVec & back_children)
   {
     // create a new node.  Children will be modified.
     ASTInterior *n_ptr = new ASTInterior(kind);
@@ -56,7 +56,7 @@ namespace BEEV
     return n;
   }
 
-  ASTNode BeevMgr::CreateNode(Kind kind, 
+  ASTNode STPMgr::CreateNode(Kind kind, 
                              const ASTNode& child0, 
                              const ASTVec & back_children)
   {
@@ -68,7 +68,7 @@ namespace BEEV
     return n;
   }
 
-  ASTNode BeevMgr::CreateNode(Kind kind, 
+  ASTNode STPMgr::CreateNode(Kind kind, 
                              const ASTNode& child0, 
                              const ASTNode& child1, 
                              const ASTVec & back_children)
@@ -81,7 +81,7 @@ namespace BEEV
     return n;
   }
 
-  ASTNode BeevMgr::CreateNode(Kind kind, 
+  ASTNode STPMgr::CreateNode(Kind kind, 
                              const ASTNode& child0, 
                              const ASTNode& child1, 
                              const ASTNode& child2, 
@@ -96,7 +96,7 @@ namespace BEEV
     return n;
   }
 
-  ASTInterior *BeevMgr::CreateInteriorNode(Kind kind,
+  ASTInterior *STPMgr::CreateInteriorNode(Kind kind,
                                            // children array of this node will be modified.
                                            ASTInterior *n_ptr,
                                            const ASTVec & back_children)
@@ -136,9 +136,9 @@ namespace BEEV
   }
 
   ////////////////////////////////////////////////////////////////
-  // BeevMgr member functions to create ASTSymbol and ASTBVConst
+  // STPMgr member functions to create ASTSymbol and ASTBVConst
   ////////////////////////////////////////////////////////////////
-  ASTNode BeevMgr::CreateSymbol(const char * const name)
+  ASTNode STPMgr::CreateSymbol(const char * const name)
   {
     ASTSymbol temp_sym(name);    
     ASTNode n(LookupOrCreateSymbol(temp_sym));
@@ -155,7 +155,7 @@ namespace BEEV
   // inserted.  FIXME: Is there a way to do this with insert?  Need a
   // function to make a new object in the middle of insert.  Read STL
   // documentation.
-  ASTSymbol *BeevMgr::LookupOrCreateSymbol(ASTSymbol& s)
+  ASTSymbol *STPMgr::LookupOrCreateSymbol(ASTSymbol& s)
   {
     ASTSymbol *s_ptr = &s; // it's a temporary key.
 
@@ -184,7 +184,7 @@ namespace BEEV
       }
   } // End of LookupOrCreateSymbol
 
-  bool BeevMgr::LookupSymbol(ASTSymbol& s)
+  bool STPMgr::LookupSymbol(ASTSymbol& s)
   {
     ASTSymbol* s_ptr = &s; // it's a temporary key.
 
@@ -196,7 +196,7 @@ namespace BEEV
   }
 
   //Create a ASTBVConst node
-  ASTNode BeevMgr::CreateBVConst(unsigned int width, unsigned long long int bvconst)
+  ASTNode STPMgr::CreateBVConst(unsigned int width, unsigned long long int bvconst)
   {
     if (width > (sizeof(unsigned long long int) << 3) || width <= 0)
       FatalError("CreateBVConst: "\
@@ -228,7 +228,7 @@ namespace BEEV
     return CreateBVConst(bv, width);
   }
 
-  ASTNode BeevMgr::CreateBVConst(string*& strval, int base, int bit_width)
+  ASTNode STPMgr::CreateBVConst(string*& strval, int base, int bit_width)
   {
 
        if (bit_width <= 0)
@@ -270,7 +270,7 @@ namespace BEEV
   }
 
   //Create a ASTBVConst node from std::string
-  ASTNode BeevMgr::CreateBVConst(const char* const strval, int base)
+  ASTNode STPMgr::CreateBVConst(const char* const strval, int base)
   {
     size_t width = strlen((const char *) strval);
     if (!(2 == base || 10 == base || 16 == base))
@@ -315,7 +315,7 @@ namespace BEEV
   }
 
   //FIXME Code currently assumes that it will destroy the bitvector passed to it
-  ASTNode BeevMgr::CreateBVConst(CBV bv, unsigned width)
+  ASTNode STPMgr::CreateBVConst(CBV bv, unsigned width)
   {
     ASTBVConst temp_bvconst(bv, width);
     ASTNode n(LookupOrCreateBVConst(temp_bvconst));
@@ -325,13 +325,13 @@ namespace BEEV
     return n;
   }
 
-  ASTNode BeevMgr::CreateZeroConst(unsigned width)
+  ASTNode STPMgr::CreateZeroConst(unsigned width)
   {
     CBV z = CONSTANTBV::BitVector_Create(width, true);
     return CreateBVConst(z, width);
   }
 
-  ASTNode BeevMgr::CreateOneConst(unsigned width)
+  ASTNode STPMgr::CreateOneConst(unsigned width)
   {
     CBV o = CONSTANTBV::BitVector_Create(width, true);
     CONSTANTBV::BitVector_increment(o);
@@ -339,7 +339,7 @@ namespace BEEV
     return CreateBVConst(o, width);
   }
 
-  ASTNode BeevMgr::CreateTwoConst(unsigned width)
+  ASTNode STPMgr::CreateTwoConst(unsigned width)
   {
     CBV two = CONSTANTBV::BitVector_Create(width, true);
     CONSTANTBV::BitVector_increment(two);
@@ -348,7 +348,7 @@ namespace BEEV
     return CreateBVConst(two, width);
   }
 
-  ASTNode BeevMgr::CreateMaxConst(unsigned width)
+  ASTNode STPMgr::CreateMaxConst(unsigned width)
   {
     CBV max = CONSTANTBV::BitVector_Create(width, false);
     CONSTANTBV::BitVector_Fill(max);
@@ -358,7 +358,7 @@ namespace BEEV
 
   //To ensure unique BVConst nodes, lookup the node in unique-table
   //before creating a new one.
-  ASTBVConst *BeevMgr::LookupOrCreateBVConst(ASTBVConst &s)
+  ASTBVConst *STPMgr::LookupOrCreateBVConst(ASTBVConst &s)
   {
     ASTBVConst *s_ptr = &s; // it's a temporary key.
 
@@ -384,7 +384,7 @@ namespace BEEV
   }
 
   // Create and return an ASTNode for a term
-  ASTNode BeevMgr::CreateTerm(Kind kind, 
+  ASTNode STPMgr::CreateTerm(Kind kind, 
                              unsigned int width, 
                              const ASTVec &children)
   {
@@ -400,7 +400,7 @@ namespace BEEV
     return n;
   }
 
-  ASTNode BeevMgr::CreateTerm(Kind kind, 
+  ASTNode STPMgr::CreateTerm(Kind kind, 
                              unsigned int width, 
                              const ASTNode& child0, 
                              const ASTVec &children)
@@ -413,7 +413,7 @@ namespace BEEV
       return n;
   }
 
-  ASTNode BeevMgr::CreateTerm(Kind kind, 
+  ASTNode STPMgr::CreateTerm(Kind kind, 
                              unsigned int width, 
                              const ASTNode& child0,
                              const ASTNode& child1, 
@@ -426,7 +426,7 @@ namespace BEEV
     return n;
   }
   
-  ASTNode BeevMgr::CreateTerm(Kind kind,
+  ASTNode STPMgr::CreateTerm(Kind kind,
                              unsigned int width,
                              const ASTNode& child0,
                              const ASTNode& child1,
@@ -476,7 +476,7 @@ namespace BEEV
   }
 
   //add an assertion to the current logical context
-  void BeevMgr::AddAssert(const ASTNode& assert)
+  void STPMgr::AddAssert(const ASTNode& assert)
   {
     if (!(is_Form_kind(assert.GetKind()) && BOOLEAN_TYPE == assert.GetType()))
       {
@@ -503,14 +503,14 @@ namespace BEEV
       }
   }
 
-  void BeevMgr::Push(void)
+  void STPMgr::Push(void)
   {
     ASTVec * v;
     v = new ASTVec();
     _asserts.push_back(v);
   }
 
-  void BeevMgr::Pop(void)
+  void STPMgr::Pop(void)
   {
     if (!_asserts.empty())
       {
@@ -523,26 +523,26 @@ namespace BEEV
       }
   }
 
-  void BeevMgr::AddQuery(const ASTNode& q)
+  void STPMgr::AddQuery(const ASTNode& q)
   {
     //_current_query = TransformFormula(q);
     //cerr << "\nThe current query is: " << q << endl;
     _current_query = q;
   }
 
-  const ASTNode BeevMgr::PopQuery()
+  const ASTNode STPMgr::PopQuery()
   {
     ASTNode q = _current_query;
     _current_query = ASTTrue;
     return q;
   }
 
-  const ASTNode BeevMgr::GetQuery()
+  const ASTNode STPMgr::GetQuery()
   {
     return _current_query;
   }
 
-  const ASTVec BeevMgr::GetAsserts(void)
+  const ASTVec STPMgr::GetAsserts(void)
   {
     vector<ASTVec *>::iterator it = _asserts.begin();
     vector<ASTVec *>::iterator itend = _asserts.end();
@@ -557,7 +557,7 @@ namespace BEEV
   }
 
   // //Create a new variable of ValueWidth 'n'
-//   ASTNode BeevMgr::NewArrayVar(unsigned int index, unsigned int value)
+//   ASTNode STPMgr::NewArrayVar(unsigned int index, unsigned int value)
 //   {
 //     std::string c("v");
 //     char d[32];
@@ -572,7 +572,7 @@ namespace BEEV
 //   } //end of NewArrayVar()
 
   //prints statistics for the ASTNode
-  void BeevMgr::ASTNodeStats(const char * c, const ASTNode& a)
+  void STPMgr::ASTNodeStats(const char * c, const ASTNode& a)
   {
     if (!stats_flag)
       return;
@@ -590,7 +590,7 @@ namespace BEEV
     cout << NodeSize(a) << endl;
   }
 
-  unsigned int BeevMgr::NodeSize(const ASTNode& a, bool clearStatInfo)
+  unsigned int STPMgr::NodeSize(const ASTNode& a, bool clearStatInfo)
   {
     if (clearStatInfo)
       StatInfoSet.clear();
@@ -616,93 +616,13 @@ namespace BEEV
     return newn;
   }
 
-  void BeevMgr::ClearAllTables(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();
-//     //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 BeevMgr::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();
-    //       }
-    
-    //     _arrayname_readindices.clear();
-    //_interior_unique_table.clear();
-    //_symbol_unique_table.clear();
-    //_bvconst_unique_table.clear();
-  }
-
-  BeevMgr::~BeevMgr()
+  STPMgr::~STPMgr()
   {
-    ClearAllTables();    
   }
 
 
   // GLOBAL FUNCTION: Prints statistics from the MINISAT Solver
-  void BeevMgr::PrintStats(MINISAT::Solver& s)
+  void STPMgr::PrintStats(MINISAT::Solver& s)
   {
     if (!stats_flag)
       return;
@@ -721,7 +641,7 @@ namespace BEEV
 
 
   //Create a new variable of ValueWidth 'n'
-  ASTNode BeevMgr::NewVar(unsigned int n)
+  ASTNode STPMgr::NewVar(unsigned int n)
   {
     std::string c("v");
     char d[32];
@@ -735,7 +655,7 @@ namespace BEEV
     return CurrentSymbol;
   } //end of NewVar()
 
-  bool BeevMgr::VarSeenInTerm(const ASTNode& var, const ASTNode& term)
+  bool STPMgr::VarSeenInTerm(const ASTNode& var, const ASTNode& term)
   {
     if (READ == term.GetKind() 
        && WRITE == term[0].GetKind() 
@@ -782,7 +702,7 @@ namespace BEEV
   }//End of VarSeenInTerm
 
   
-  ASTNode BeevMgr::NewParameterized_BooleanVar(const ASTNode& var,
+  ASTNode STPMgr::NewParameterized_BooleanVar(const ASTNode& var,
                                               const ASTNode& constant)
   {
     ostringstream outVar;

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index 1cf2f0094e2a0dc504a04367663098f39b209945..56cf1ed5eef2800b902d6f633572166722bfd171 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -16,10 +16,10 @@
 namespace BEEV
 {
   /*****************************************************************
-   * Class BeevMgr.  This holds all "global" variables for the system,
+   * Class STPMgr.  This holds all "global" variables for the system,
    * such as unique tables for the various kinds of nodes.
    *****************************************************************/
-  class BeevMgr
+  class STPMgr
   {
     friend class ASTNode;
     friend class ASTInterior;
@@ -159,7 +159,7 @@ namespace BEEV
      ****************************************************************/
 
     // Constructor
-    BeevMgr() : 
+    STPMgr() : 
       _symbol_unique_table(INITIAL_TABLE_SIZE),
       _bvconst_unique_table(INITIAL_TABLE_SIZE),
       _interior_unique_table(INITIAL_TABLE_SIZE),
@@ -183,7 +183,7 @@ namespace BEEV
     }    
 
     //destructor
-    ~BeevMgr();
+    ~STPMgr();
 
     //Return ptr to let-variables manager (see parser/let-funcs.h)
     LETMgr * GetLetMgr(void)
@@ -322,9 +322,6 @@ namespace BEEV
     //add an assertion to the current logical context
     void AddAssert(const ASTNode& assert);
     
-    void ClearAllTables(void);
-    void ClearAllCaches(void);
-
     /****************************************************************
      * Toplevel printing and stats functions                        *
      ****************************************************************/
@@ -374,6 +371,6 @@ namespace BEEV
       TermsAlreadySeenMap.clear();
     }
 
-  };//End of Class BeevMgr
+  };//End of Class STPMgr
 };//end of namespace
 #endif

diff --git a/src/absrefine_counterexample/AbsRefine_CounterExample.h b/src/absrefine_counterexample/AbsRefine_CounterExample.h
index bb4a655ad5710056b5edd76828ccab185bd41876..d85b5ac183ccd4f69c5047af38dcc3d4e46b7f06 100644 (file)
--- a/src/absrefine_counterexample/AbsRefine_CounterExample.h
+++ b/src/absrefine_counterexample/AbsRefine_CounterExample.h
@@ -43,7 +43,7 @@ namespace BEEV
       ASTNodeMap ComputeFormulaMap;
       
       // Ptr to STPManager
-      BeevMgr * bm;
+      STPMgr * bm;
       
       // Ptr to Simplifier
       Simplifier * simp;
@@ -76,7 +76,7 @@ namespace BEEV
     public:
 
       // Constructor
-      AbsRefine_CounterExample(BeevMgr * b, 
+      AbsRefine_CounterExample(STPMgr * b, 
                               Simplifier * s, 
                               ArrayTransformer * at,
                               ToSAT * t) : 
@@ -176,9 +176,9 @@ namespace BEEV
   class CompleteCounterExample
     {
       ASTNodeMap counterexample;
-      BeevMgr * bv;
+      STPMgr * bv;
     public:
-      CompleteCounterExample(ASTNodeMap a, BeevMgr* beev) :
+      CompleteCounterExample(ASTNodeMap a, STPMgr* beev) :
        counterexample(a), bv(beev)
        {
        }

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 54fdbd7e4b2dcccaf7511f65a05a264420c7860e..2d6b54d99d243169f8087521282c0f7afe98a911 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -17,7 +17,7 @@
 //many overloaded meanings of the word type)
 typedef BEEV::ASTNode                    node;
 typedef BEEV::ASTNode*                   nodestar;
-typedef BEEV::BeevMgr*                   bmstar;
+typedef BEEV::STPMgr*                   bmstar;
 typedef BEEV::STP*                       stpstar;
 typedef BEEV::Simplifier*                simpstar;
 typedef BEEV::BVSolver*                  bvsolverstar;
@@ -119,7 +119,7 @@ void vc_setFlags(char c) {
   }
 }
 
-//Create a validity Checker. This is the global BeevMgr
+//Create a validity Checker. This is the global STPMgr
 VC vc_createValidityChecker(void) {
   vc_setFlags('d');
   CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot();
@@ -128,18 +128,20 @@ VC vc_createValidityChecker(void) {
     return 0;
   }
 
-  BEEV::BeevMgr * bm       = new BEEV::BeevMgr();
+  BEEV::STPMgr * bm       = new BEEV::STPMgr();
   BEEV::Simplifier * simp  = new BEEV::Simplifier(bm);
   BEEV::BVSolver* bvsolver = new BEEV::BVSolver(bm, simp);
   BEEV::ToSAT * tosat      = new BEEV::ToSAT(bm, simp);
-  BEEV::ArrayTransformer * arrayTransformer = new BEEV::ArrayTransformer(bm, simp);
+  BEEV::ArrayTransformer * arrayTransformer = 
+    new BEEV::ArrayTransformer(bm, simp);
   BEEV::AbsRefine_CounterExample * Ctr_Example = 
-    new BEEV::AbsRefine_CounterExample(bm, simp, arrayTransformer, tosat);      
-  
-  BEEV::ParserBM          = bm;
-  stpstar stp             = new BEEV::STP(bm, simp, 
-                                         bvsolver, arrayTransformer, 
-                                         tosat, Ctr_Example);
+    new BEEV::AbsRefine_CounterExample(bm, simp, arrayTransformer, tosat);
+
+  BEEV::ParserBM = bm;
+  stpstar stp =
+    new BEEV::STP(bm, simp, 
+                 bvsolver, arrayTransformer, 
+                 tosat, Ctr_Example);
   
   BEEV::GlobalSTP = stp;
   decls = new BEEV::ASTVec();
@@ -445,14 +447,14 @@ int vc_query(VC vc, Expr e) {
   int output;
   if(!v.empty()) {
     if(v.size()==1) {
-      output = stp->TopLevelSAT(v[0],*a);
+      output = stp->TopLevelSTP(v[0],*a);
     }
     else {
-      output = stp->TopLevelSAT(b->CreateNode(BEEV::AND,v),*a);
+      output = stp->TopLevelSTP(b->CreateNode(BEEV::AND,v),*a);
     }
   }
   else {
-    output = stp->TopLevelSAT(b->CreateNode(BEEV::TRUE),*a);
+    output = stp->TopLevelSTP(b->CreateNode(BEEV::TRUE),*a);
   }
   return output;
 } //end of vc_query
@@ -473,17 +475,17 @@ int vc_query(VC vc, Expr e) {
 //   node o;
 //   if(!v.empty()) {
 //     if(v.size()==1)
-//       return b->TopLevelSAT(v[0],*a);
+//       return b->TopLevelSTP(v[0],*a);
 //     else
-//       return b->TopLevelSAT(b->CreateNode(BEEV::AND,v),*a);
+//       return b->TopLevelSTP(b->CreateNode(BEEV::AND,v),*a);
 //   }
 //   else
-//     return b->TopLevelSAT(b->CreateNode(BEEV::TRUE),*a);
+//     return b->TopLevelSTP(b->CreateNode(BEEV::TRUE),*a);
 // }
 
 void vc_push(VC vc) {
   bmstar b = (bmstar)(((stpstar)vc)->bm);
-  b->ClearAllCaches();
+  ((stpstar)vc)->ClearAllCaches();
   b->Push();
 }
 
@@ -1627,7 +1629,7 @@ Expr vc_parseExpr(VC vc, const char* infile) {
   cvcparse((void*)AssertsQuery);
   BEEV::ASTNode asserts = (*(BEEV::ASTVec*)AssertsQuery)[0];
   BEEV::ASTNode query   = (*(BEEV::ASTVec*)AssertsQuery)[1];
-  //b->TopLevelSAT(asserts, query);
+  //b->TopLevelSTP(asserts, query);
 
   node oo = b->CreateNode(BEEV::NOT,query);
   node o = b->CreateNode(BEEV::AND,asserts,oo);

diff --git a/src/main/Globals.cpp b/src/main/Globals.cpp
index f195a37fbe498609dac484509ae3c3330d829797..8f7b9983ff4ac026f6be69b09361ed9df56bfe50 100644 (file)
--- a/src/main/Globals.cpp
+++ b/src/main/Globals.cpp
@@ -86,7 +86,7 @@ namespace BEEV
 
   //global BEEVMGR for the parser. Use exclusively for parsing
   STP     * GlobalSTP;
-  BeevMgr * ParserBM;
+  STPMgr  * ParserBM;
 
   void (*vc_error_hdlr)(const char* err_msg) = NULL;
   /** This is reusable empty vector, for representing empty children

diff --git a/src/main/Globals.h b/src/main/Globals.h
index 8df7b81617e747bfa191ede653e9048473192b85..eaae76d95127f3cac6177d0c5e4adc57c715f586 100644 (file)
--- a/src/main/Globals.h
+++ b/src/main/Globals.h
@@ -28,7 +28,7 @@ namespace MINISAT
 
 namespace BEEV
 {  
-  class BeevMgr;
+  class STPMgr;
   class ASTNode;
   class ASTInternal;
   class ASTInterior;
@@ -134,9 +134,9 @@ namespace BEEV
 
   //Useful global variables. Use for parsing only
   extern  STP * GlobalSTP;
-  extern  BeevMgr * ParserBM;
+  extern  STPMgr * ParserBM;
 
-  //Empty vector
+  //Empty vector. Useful commonly used ASTNodes
   extern std::vector<ASTNode> _empty_ASTVec;  
   extern ASTNode ASTFalse, ASTTrue, ASTUndefined;
 

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 59576c2675da55cde08f1144fd493838b37d87fa..518d1bff09fd6aa1884bf3431e1f14cba89dfd93 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -45,7 +45,7 @@ int main(int argc, char ** argv) {
     }
 
 
-  BeevMgr * bm       = new BeevMgr();
+  STPMgr * bm       = new STPMgr();
   Simplifier * simp  = new Simplifier(bm);
   BVSolver* bvsolver = new BVSolver(bm, simp);
   ArrayTransformer * arrayTransformer = new ArrayTransformer(bm, simp);
@@ -226,7 +226,7 @@ int main(int argc, char ** argv) {
       return 0;
     } //end of PrintBack if
 
-  SOLVER_RETURN_TYPE ret = GlobalSTP->TopLevelSAT(asserts, query);
+  SOLVER_RETURN_TYPE ret = GlobalSTP->TopLevelSTP(asserts, query);
   if (quick_statistics_flag) 
     {
       bm->GetRunTimes()->print();

diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index 777e08ce522574c73f17b76bc59d42976c3e3c70..8ca1e7404c59550fa92747170e5a980065a72829 100644 (file)
--- a/src/parser/CVC.y
+++ b/src/parser/CVC.y
@@ -23,8 +23,6 @@
 #define YY_EXIT_FAILURE -1
 #define YYPARSE_PARAM AssertsQuery
   
-  //BeevMgr * ParserBM = GlobalSTP->bm;
-  
   extern int cvclex(void);
   extern char* yytext;
   extern int cvclineno;

diff --git a/src/printer/AssortedPrinters.cpp b/src/printer/AssortedPrinters.cpp
index 2f960b57b688a4cd1a0977655979cb7302a65b96..1c50b88235a174e0b7588c16957dff54ca810155 100644 (file)
--- a/src/printer/AssortedPrinters.cpp
+++ b/src/printer/AssortedPrinters.cpp
@@ -65,12 +65,12 @@ namespace BEEV
 
   void lpvec(const ASTVec &vec)
   {
-    (vec[0].GetBeevMgr())->AlreadyPrintedSet.clear();
+    (vec[0].GetSTPMgr())->AlreadyPrintedSet.clear();
     LispPrintVec(cout, vec, 0);
     cout << endl;
   }
 
-  //   void BeevMgr::PrintClauseList(ostream& os, BeevMgr::ClauseList& cll)
+  //   void STPMgr::PrintClauseList(ostream& os, STPMgr::ClauseList& cll)
   //   {
   //     int num_clauses = cll.size();
   //     os << "Clauses: " << endl << "=========================================" << endl;
@@ -88,7 +88,7 @@ namespace BEEV
   //   void Convert_MINISATVar_To_ASTNode_Print(int minisat_var, 
   //                                      int decision_level, int polarity)
   //   {
-  //     BEEV::ASTNode vv = BEEV::GlobalBeevMgr->_SATVar_to_AST[minisat_var];
+  //     BEEV::ASTNode vv = BEEV::GlobalSTPMgr->_SATVar_to_AST[minisat_var];
   //     cout << spaces(decision_level);
   //     if (polarity)
   //       {
@@ -98,7 +98,7 @@ namespace BEEV
   //     cout << endl;
   //   } //end of Convert_MINISATVar_To_ASTNode_Print()
 
-  void BeevMgr::printVarDeclsToStream(ostream &os) {
+  void STPMgr::printVarDeclsToStream(ostream &os) {
     for(ASTVec::iterator i = ListOfDeclaredVars.begin(),iend=ListOfDeclaredVars.end();i!=iend;i++) {
       BEEV::ASTNode a = *i;
       switch(a.GetType()) {
@@ -124,7 +124,7 @@ namespace BEEV
 
 
 
-  void BeevMgr::printAssertsToStream(ostream &os, int simplify_print) {
+  void STPMgr::printAssertsToStream(ostream &os, int simplify_print) {
   ASTVec v = GetAsserts();
   for(ASTVec::iterator i=v.begin(),iend=v.end();i!=iend;i++) {
     //Begin_RemoveWrites = true;

diff --git a/src/printer/CPrinter.cpp b/src/printer/CPrinter.cpp
index 3243441ce6d1747efc58f2b5e935f574a6d2fc30..84988aa5d3c0cb92eb7788e5575912b5b4ab929c 100644 (file)
--- a/src/printer/CPrinter.cpp
+++ b/src/printer/CPrinter.cpp
@@ -37,7 +37,7 @@ namespace printer
       }
 
     //if this node is present in the letvar Map, then print the letvar
-    BeevMgr *bm = n.GetBeevMgr();
+    STPMgr *bm = n.GetSTPMgr();
 
     //this is to print letvars for shared subterms inside the printing
     //of "(LET v0 = term1, v1=term1@term2,...
@@ -433,7 +433,7 @@ namespace printer
   ostream& C_Print(ostream &os, const ASTNode n, int indentation)
   {
     // Clear the PrintMap
-    BeevMgr* bm = n.GetBeevMgr();
+    STPMgr* bm = n.GetSTPMgr();
     bm->PLPrintNodeSet.clear();
     bm->NodeLetVarMap.clear();
     bm->NodeLetVarVec.clear();

diff --git a/src/printer/LispPrinter.cpp b/src/printer/LispPrinter.cpp
index 8caf9f0880dbe239020bd1ff7291b0c333d2505a..f7fe05f0c09f3a7390a25bfc9cc657353197019b 100644 (file)
--- a/src/printer/LispPrinter.cpp
+++ b/src/printer/LispPrinter.cpp
@@ -91,7 +91,7 @@ namespace printer
   ostream &Lisp_Print(ostream &os, const ASTNode& n,  int indentation)
   {
     // Clear the PrintMap
-    BeevMgr* bm = n.GetBeevMgr();
+    STPMgr* bm = n.GetSTPMgr();
     bm->AlreadyPrintedSet.clear();
     Lisp_Print_indent(os, n, indentation);
     printf("\n");

diff --git a/src/printer/PLPrinter.cpp b/src/printer/PLPrinter.cpp
index 50aadc80e9c30a235419d869dc16d72e23707716..dcc83184a19542781959db86486fa7d5c7261a4d 100644 (file)
--- a/src/printer/PLPrinter.cpp
+++ b/src/printer/PLPrinter.cpp
@@ -26,7 +26,7 @@ namespace printer
       }
 
     //if this node is present in the letvar Map, then print the letvar
-    BeevMgr *bm = n.GetBeevMgr();
+    STPMgr *bm = n.GetSTPMgr();
 
     //this is to print letvars for shared subterms inside the printing
     //of "(LET v0 = term1, v1=term1@term2,...
@@ -327,7 +327,7 @@ namespace printer
   ostream& PL_Print(ostream &os,  const ASTNode& n, int indentation)
   {
     // Clear the PrintMap
-    BeevMgr* bm = n.GetBeevMgr();
+    STPMgr* bm = n.GetSTPMgr();
     bm->PLPrintNodeSet.clear();
     bm->NodeLetVarMap.clear();
     bm->NodeLetVarVec.clear();

diff --git a/src/printer/SMTLIBPrinter.cpp b/src/printer/SMTLIBPrinter.cpp
index cd544d4f3799c000f4432eea0d9f318e41aa020d..215f37d4e8a0f1cd8906c9cc453efb01e9cb12bd 100644 (file)
--- a/src/printer/SMTLIBPrinter.cpp
+++ b/src/printer/SMTLIBPrinter.cpp
@@ -23,19 +23,19 @@ namespace printer
 
   string functionToSMTLIBName(const BEEV::Kind k);
   void SMTLIB_Print1(ostream& os, const BEEV::ASTNode n, int indentation, bool letize);
-  void printVarDeclsToStream( const BeevMgr* mgr, ostream &os);
+  void printVarDeclsToStream( const STPMgr* mgr, ostream &os);
 
   // Initial version intended to print the whole thing back.
   void SMTLIB_PrintBack(ostream &os, const ASTNode& n) {
          // need to add fake headers into here.
          os << "(" << endl;
          os << "benchmark blah" << endl;
-         printVarDeclsToStream(n.GetBeevMgr(),os);
+         printVarDeclsToStream(n.GetSTPMgr(),os);
          SMTLIB_Print(os, n, 0);
          os << ")" << endl;
   }
 
-  void printVarDeclsToStream( const BeevMgr* mgr, ostream &os) {
+  void printVarDeclsToStream( const STPMgr* mgr, ostream &os) {
       for(ASTVec::const_iterator i = mgr->ListOfDeclaredVars.begin(),
            iend=mgr->ListOfDeclaredVars.end();i!=iend;i++) {
         const BEEV::ASTNode& a = *i;
@@ -91,7 +91,7 @@ namespace printer
     // Prepend with zero to convert to unsigned.
 
     os << "bv";
-    CBV unsign = CONSTANTBV::BitVector_Concat((n.GetBeevMgr())->CreateZeroConst(1).GetBVConst(), op.GetBVConst());
+    CBV unsign = CONSTANTBV::BitVector_Concat((n.GetSTPMgr())->CreateZeroConst(1).GetBVConst(), op.GetBVConst());
     unsigned char * str = CONSTANTBV::BitVector_to_Dec(unsign);
     CONSTANTBV::BitVector_Destroy(unsign);
     os << str << "[" << op.GetValueWidth() << "]";
@@ -109,7 +109,7 @@ namespace printer
       }
 
     //if this node is present in the letvar Map, then print the letvar
-    BeevMgr * bm = n.GetBeevMgr();
+    STPMgr * bm = n.GetSTPMgr();
 
     //this is to print letvars for shared subterms inside the printing
     //of "(LET v0 = term1, v1=term1@term2,...
@@ -191,7 +191,7 @@ namespace printer
   ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation)
   {
     // Clear the PrintMap
-    BeevMgr* bm = n.GetBeevMgr();
+    STPMgr* bm = n.GetSTPMgr();
     bm->PLPrintNodeSet.clear();
     bm->NodeLetVarMap.clear();
     bm->NodeLetVarVec.clear();

diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h
index 00753f701b89174c4780d67aaff1db73cae4d5e9..6c531c61c3a5d1f9ed532a07cd4669fce25ecf93 100644 (file)
--- a/src/simplifier/bvsolver.h
+++ b/src/simplifier/bvsolver.h
@@ -44,7 +44,7 @@ namespace BEEV
       // Ptr to toplevel manager that manages bit-vector expressions
       // (i.e. construct various kinds of expressions), and also has
       // member functions that simplify bit-vector expressions
-      BeevMgr * _bm;
+      STPMgr * _bm;
       
       // Ptr to Simplifier
       Simplifier * _simp;
@@ -129,7 +129,7 @@ namespace BEEV
 
     public:
       //constructor
-      BVSolver(BeevMgr * bm, Simplifier * simp) : _bm(bm), _simp(simp) 
+      BVSolver(STPMgr * bm, Simplifier * simp) : _bm(bm), _simp(simp)  
         {
           ASTTrue = _bm->CreateNode(TRUE);
           ASTFalse = _bm->CreateNode(FALSE);

diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h
index 64d514758b26faaad87f982cdcfb37089610ec7b..929f68b517dbfdd63176bcc6c7fc3420781e2305 100644 (file)
--- a/src/simplifier/simplifier.h
+++ b/src/simplifier/simplifier.h
@@ -56,14 +56,14 @@ namespace BEEV
       ASTNodeCountMap *ReferenceCount;
       
       //Ptr to STP Manager
-      BeevMgr * _bm;
+      STPMgr * _bm;
 
     public:
       
       /****************************************************************
        * Public Member Functions                                      *
        ****************************************************************/      
-      Simplifier(BeevMgr * bm) : _bm(bm) 
+      Simplifier(STPMgr * bm) : _bm(bm) 
       {
        SimplifyMap    = new ASTNodeMap(INITIAL_TABLE_SIZE);
        SimplifyNegMap = new ASTNodeMap(INITIAL_TABLE_SIZE);

diff --git a/src/to-sat/BitBlast.h b/src/to-sat/BitBlast.h
index a0aedd334d636635549e058595be74e2ad25e76c..21fea95a8b1b8fb93b30f6311a031d3163067932 100644 (file)
--- a/src/to-sat/BitBlast.h
+++ b/src/to-sat/BitBlast.h
@@ -22,7 +22,7 @@ namespace BEEV
     /****************************************************************
      * Private Data                                                 *
      ****************************************************************/
-    BeevMgr * _bm;
+    STPMgr * _bm;
     ASTNode ASTTrue, ASTFalse, ASTUndefined;
     
     // Memo table for bit blasted terms.  If a node has already been
@@ -99,7 +99,7 @@ namespace BEEV
      * Public Member Functions                                      *
      ****************************************************************/
     
-    BitBlaster(BeevMgr * bm) : _bm(bm) 
+    BitBlaster(STPMgr * bm) : _bm(bm) 
     {
       ASTTrue = _bm->CreateNode(TRUE);
       ASTFalse = _bm->CreateNode(FALSE);

diff --git a/src/to-sat/SimpBool.cpp b/src/to-sat/SimpBool.cpp
index 2ba5544cf3d7c99c0bf2e34f455ef2763016827c..b33ab866f4ec61d85c4a34b6178776d525efd11b 100644 (file)
--- a/src/to-sat/SimpBool.cpp
+++ b/src/to-sat/SimpBool.cpp
@@ -27,7 +27,7 @@ static bool _disable_simpbool = 0;
 namespace BEEV
 {
 
-  ASTNode BeevMgr::CreateSimpForm(Kind kind, ASTVec &children = _empty_ASTVec)
+  ASTNode STPMgr::CreateSimpForm(Kind kind, ASTVec &children = _empty_ASTVec)
   {
     if (_disable_simpbool)
       {
@@ -80,7 +80,7 @@ namespace BEEV
 
   // specialized versions
 
-  ASTNode BeevMgr::CreateSimpForm(Kind kind, const ASTNode& child0)
+  ASTNode STPMgr::CreateSimpForm(Kind kind, const ASTNode& child0)
   {
     ASTVec children;
     //child_stack.clear();      // could just reset top pointer.
@@ -90,7 +90,7 @@ namespace BEEV
     //return CreateSimpForm(kind, child_stack);
   }
 
-  ASTNode BeevMgr::CreateSimpForm(Kind kind, const ASTNode& child0, const ASTNode& child1)
+  ASTNode STPMgr::CreateSimpForm(Kind kind, const ASTNode& child0, const ASTNode& child1)
   {
     ASTVec children;
     //child_stack.clear();      // could just reset top pointer.
@@ -102,7 +102,7 @@ namespace BEEV
     //return CreateSimpForm(kind, child_stack);
   }
 
-  ASTNode BeevMgr::CreateSimpForm(Kind kind, const ASTNode& child0, const ASTNode& child1, const ASTNode& child2)
+  ASTNode STPMgr::CreateSimpForm(Kind kind, const ASTNode& child0, const ASTNode& child1, const ASTNode& child2)
   {
     ASTVec children;
     //child_stack.clear();      // could just reset top pointer.
@@ -116,7 +116,7 @@ namespace BEEV
     //return CreateSimpForm(kind, child_stack);
   }
 
-  ASTNode BeevMgr::CreateSimpNot(const ASTNode& form)
+  ASTNode STPMgr::CreateSimpNot(const ASTNode& form)
   {
     Kind k = form.GetKind();
     switch (k)
@@ -154,7 +154,7 @@ namespace BEEV
   // CreateSimpAndOr instead of CreateSimpXor until 1/9/07 with no
   // ill effects.  Calls seem to go to the version that takes a vector
   // of children.
-  ASTNode BeevMgr::CreateSimpXor(const ASTNode& form1, const ASTNode& form2)
+  ASTNode STPMgr::CreateSimpXor(const ASTNode& form1, const ASTNode& form2)
   {
     ASTVec children;
     children.push_back(form1);
@@ -206,7 +206,7 @@ namespace BEEV
     return flat_children;
   }
 
-  ASTNode BeevMgr::CreateSimpAndOr(bool IsAnd, const ASTNode& form1, const ASTNode& form2)
+  ASTNode STPMgr::CreateSimpAndOr(bool IsAnd, const ASTNode& form1, const ASTNode& form2)
   {
     ASTVec children;
     children.push_back(form1);
@@ -215,7 +215,7 @@ namespace BEEV
   }
 
   // FIXME: Could also handle (AND ... (NOT (OR ...) ...)
-  ASTNode BeevMgr::CreateSimpAndOr(bool IsAnd, ASTVec &children)
+  ASTNode STPMgr::CreateSimpAndOr(bool IsAnd, ASTVec &children)
   {
 
     Kind k = IsAnd ? AND : OR;
@@ -318,7 +318,7 @@ namespace BEEV
   }
 
   // Constant children are accumulated in "accumconst".
-  ASTNode BeevMgr::CreateSimpXor(ASTVec &children)
+  ASTNode STPMgr::CreateSimpXor(ASTVec &children)
   {
 
     if (_trace_simpbool)
@@ -440,7 +440,7 @@ namespace BEEV
   }
 
   // FIXME:  How do I know whether ITE is a formula or not?
-  ASTNode BeevMgr::CreateSimpFormITE(const ASTNode& child0, const ASTNode& child1, const ASTNode& child2)
+  ASTNode STPMgr::CreateSimpFormITE(const ASTNode& child0, const ASTNode& child1, const ASTNode& child2)
   {
 
     ASTNode retval;

diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index bfcb9a82a4e808ae18d15ecf67ba133879b42f23..8e984bb6217bff17e4dd949ac11118ca77d1dc9e 100644 (file)
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -1654,7 +1654,7 @@ namespace BEEV
     //########################################
     // constructor
 
-    CNFMgr::CNFMgr(BeevMgr *bmgr)
+    CNFMgr::CNFMgr(STPMgr *bmgr)
     {
       bm = bmgr;
     }
@@ -1678,7 +1678,7 @@ namespace BEEV
 
     ClauseList* CNFMgr::convertToCNF(const ASTNode& varphi)
     {
-      varphi.GetBeevMgr()->GetRunTimes()->start(RunTimes::CNFConversion);
+      bm->GetRunTimes()->start(RunTimes::CNFConversion);
       scanFormula(varphi, true);
       ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*");
       ClauseList* defs = SINGLETON(dummy_true_var);
@@ -1687,7 +1687,7 @@ namespace BEEV
       defs->insert(defs->begin() + 1, top->begin(), top->end());
 
       cleanup(varphi);
-      varphi.GetBeevMgr()->GetRunTimes()->stop(RunTimes::CNFConversion);
+      bm->GetRunTimes()->stop(RunTimes::CNFConversion);
       return defs;
     }//End of convertToCNF()
 

diff --git a/src/to-sat/ToCNF.h b/src/to-sat/ToCNF.h
index 630dc74d29d20c187c3b10e89bd3f3fb435e4383..f2e6fd2e1615ddd589c0433486fc39235cbb4946 100644 (file)
--- a/src/to-sat/ToCNF.h
+++ b/src/to-sat/ToCNF.h
@@ -52,7 +52,7 @@ namespace BEEV
     //########################################
     // this is the data
 
-    BeevMgr *bm;
+    STPMgr *bm;
     ASTNodeToCNFInfoMap info;
     ASTNodeToASTNodePtrMap store;
 
@@ -255,7 +255,7 @@ namespace BEEV
     //########################################
     //########################################
     // constructor
-    CNFMgr(BeevMgr *bmgr);
+    CNFMgr(STPMgr *bmgr);
    
     //########################################
     //########################################

diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h
index 203eb7cb715515977f3738171fb2a758aa09d37c..f267e6a93446af195c89c742e0798a916c33abae 100644 (file)
--- a/src/to-sat/ToSAT.h
+++ b/src/to-sat/ToSAT.h
@@ -50,7 +50,7 @@ namespace BEEV
     vector<ASTNode> _SATVar_to_AST;
 
     // Ptr to STPManager
-    BeevMgr * bm;
+    STPMgr * bm;
 
     // Ptr to Simplifier
     Simplifier * simp;
@@ -88,7 +88,7 @@ namespace BEEV
      ****************************************************************/
     
     // Constructor
-    ToSAT(BeevMgr * bm, Simplifier * s) :
+    ToSAT(STPMgr * bm, Simplifier * s) :
       bm(bm), simp(s)
     {
       ASTTrue      = bm->CreateNode(TRUE);