Fix the build. The speedup in the prior checkin needs these too.

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

diff --git a/src/AST/ASTBVConst.cpp b/src/AST/ASTBVConst.cpp
index 8fd0e647c71627d5920e9df1d79a38929aa11d3e..dae19e20952028c8481ccffdb2d8cddb1c09673c 100644 (file)
--- a/src/AST/ASTBVConst.cpp
+++ b/src/AST/ASTBVConst.cpp
@@ -21,6 +21,7 @@ namespace BEEV
   {
     _bvconst = CONSTANTBV::BitVector_Clone(bv);
     _value_width = width;
+    cbv_managed_outside =false;
   } //End of ASTBVConst constructor
 
   // Copy constructor.
@@ -29,6 +30,7 @@ namespace BEEV
   {
     _bvconst = CONSTANTBV::BitVector_Clone(sym._bvconst);
     _value_width = sym._value_width;
+    cbv_managed_outside =false;
   } //End of copy constructor()
 
   // Call this when deleting a node that has been stored in the the

diff --git a/src/AST/ASTBVConst.h b/src/AST/ASTBVConst.h
index 3f29dd78f83171782cea762c8f313db3ece1e5aa..32cba9a1275f8a6d89a0bdfe8ae60779921f2eb7 100644 (file)
--- a/src/AST/ASTBVConst.h
+++ b/src/AST/ASTBVConst.h
@@ -34,7 +34,10 @@ namespace BEEV
     //CBV is actually an unsigned*. The bitvector constant is
     //represented using an external library in extlib-bvconst.
     CBV _bvconst;
-  
+
+    // If the CBV is managed outside of this class. Then a defensive copy isn't taken.
+    bool cbv_managed_outside;
+
     /****************************************************************
      * Class ASTBVConstHasher:                                      *
      *                                                              *
@@ -46,6 +49,8 @@ namespace BEEV
       size_t operator()(const ASTBVConst * bvc) const;
     }; //End of class ASTBVConstHahser
     
+
+
     /****************************************************************
      * Class ASTBVConstEqual:                                       *
      *                                                              *
@@ -61,9 +66,20 @@ namespace BEEV
     /****************************************************************
      * Private Functions (virtual defs and friends)                 *
      ****************************************************************/
+
     //Constructor
     ASTBVConst(CBV bv, unsigned int width);
 
+    enum CBV_LIFETIME {CBV_MANAGED_OUTSIDE};
+
+    ASTBVConst(CBV bv, unsigned int width, enum CBV_LIFETIME l )
+    :  ASTInternal(BVCONST)
+    {
+      _bvconst = (bv);
+      _value_width = width;
+      cbv_managed_outside =true;
+    }
+
     // Copy constructor.
     ASTBVConst(const ASTBVConst &sym);  
   
@@ -94,7 +110,8 @@ namespace BEEV
     //Destructor. Call the external destructor
     virtual ~ASTBVConst()
     {
-      CONSTANTBV::BitVector_Destroy(_bvconst);
+      if (!cbv_managed_outside)
+        CONSTANTBV::BitVector_Destroy(_bvconst);
     } //End of destructor
 
     // Return the bvconst. It is a const-value