Patch from Khoo Yit Phang.

Fix the weird type of STPMgr::CreateBVConst (to have only one reference level).

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

diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp
index 197bacaec8f78d7af666ffeadf479f6438e5ed7e..8eab3db649b68a581b30a46ba14fdf676758f4d6 100644 (file)
--- a/src/STPManager/STPManager.cpp
+++ b/src/STPManager/STPManager.cpp
@@ -204,7 +204,7 @@ namespace BEEV
 
   }
 
-  ASTNode STPMgr::CreateBVConst(string*& strval, int base, int bit_width)
+  ASTNode STPMgr::CreateBVConst(string& strval, int base, int bit_width)
   {
 
     if (bit_width <= 0)
@@ -223,17 +223,17 @@ namespace BEEV
     if (2 == base)
       {
         e = CONSTANTBV::BitVector_from_Bin(bv,
-                                          (unsigned char*) strval->c_str());
+                                          (unsigned char*) strval.c_str());
       }
     else if (10 == base)
       {
         e = CONSTANTBV::BitVector_from_Dec(bv,
-                                          (unsigned char*) strval->c_str());
+                                          (unsigned char*) strval.c_str());
       }
     else if (16 == base)
       {
         e = CONSTANTBV::BitVector_from_Hex(bv, 
-                                          (unsigned char*) strval->c_str());
+                                          (unsigned char*) strval.c_str());
       }
     else
       {

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index bf68c34791f4b0a8b35efc24bedc432cc56db191..6650852bfb959fe3aa655b02478f4b3625304471 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -275,7 +275,7 @@ namespace BEEV
     ASTNode CreateZeroConst(unsigned int width);
     ASTNode CreateBVConst(CBV bv, unsigned width);
     ASTNode CreateBVConst(const char *strval, int base);
-    ASTNode CreateBVConst(string*& strval, int base, int bit_width);    
+    ASTNode CreateBVConst(string& strval, int base, int bit_width);    
     ASTNode CreateBVConst(unsigned int width, unsigned long long int bvconst);
     
     /****************************************************************

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index d9139b95c899e4f035d9b8b2a48c0041a5c918bb..5738611fe24ee1c7ca14246ac4f5df3ac73f6a64 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -981,18 +981,14 @@ Type vc_bv32Type(VC vc) {
 }
 
 Expr vc_bvConstExprFromDecStr(VC vc, 
-                              const size_t width, 
+                              int width, 
                               const char* decimalInput ) 
 {
   bmstar b = (bmstar)(((stpstar)vc)->bm);
-
-  string *param = new string(decimalInput);
-  // funny type to get it to compile. fix later when I
-  // understand what this does.
-  node n = b->CreateBVConst((string*&)param, (int)10,(int)width);
+  string str(decimalInput);
+  node n = b->CreateBVConst(str, 10, width);
   BVTypeCheck(n);
   nodestar output = new node(n);
-  delete param;
   return output;
 }
 

diff --git a/src/c_interface/c_interface.h b/src/c_interface/c_interface.h
index a4679e7d0c09393da0099fd1dbb813734d27098e..275bd92039884b9f6a1274bb8b763593b537059b 100644 (file)
--- a/src/c_interface/c_interface.h
+++ b/src/c_interface/c_interface.h
@@ -233,7 +233,7 @@ extern "C" {
   Type vc_bvType(VC vc, int no_bits);
   Type vc_bv32Type(VC vc);
 
-  Expr vc_bvConstExprFromDecStr(VC vc, const size_t width, const char* decimalInput );
+  Expr vc_bvConstExprFromDecStr(VC vc, int width, const char* decimalInput );
   Expr vc_bvConstExprFromStr(VC vc, const char* binary_repr);
   Expr vc_bvConstExprFromInt(VC vc, int n_bits, unsigned int value);
   Expr vc_bvConstExprFromLL(VC vc, int n_bits, unsigned long long value);

diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index fe057bab97eb0360899162340b1fa4d51752a5dc..0d4221dd314d37e67c591de59b399759314736cc 100644 (file)
--- a/src/parser/CVC.y
+++ b/src/parser/CVC.y
@@ -729,21 +729,21 @@ Expr            :      TERMID_TOK { $$ = new ASTNode(parserInterface->letMgr.Res
 }
 | NUMERAL_TOK BIN_BASED_NUMBER 
 { 
-  std::string* vals = new std::string($2);
+  std::string vals($2);
   $$ = new ASTNode(parserInterface->CreateBVConst(vals, 2, $1));
-  free($2); delete vals;
+  free($2);
 }
 | NUMERAL_TOK DEC_BASED_NUMBER
 { 
-  std::string* vals = new std::string($2);
+  std::string vals($2);
   $$ = new ASTNode(parserInterface->CreateBVConst(vals, 10, $1));
-  free($2); delete vals;
+  free($2);
 }
 | NUMERAL_TOK HEX_BASED_NUMBER 
 { 
-  std::string* vals = new std::string($2);
+  std::string vals($2);
   $$ = new ASTNode(parserInterface->CreateBVConst(vals, 16, $1));
-  free($2); delete vals;
+  free($2);
 }
 |      Expr '[' Expr ']' 
 {                        

diff --git a/src/parser/ParserInterface.h b/src/parser/ParserInterface.h
index 0b8cb7f0e1daee67f769ab319059a6959e1c55dc..6a7488829ec6e41c740c1ae06e866857f309ce36 100644 (file)
--- a/src/parser/ParserInterface.h
+++ b/src/parser/ParserInterface.h
@@ -72,7 +72,7 @@ public:
         return bm.CreateOneConst(width);
     }
 
-    ASTNode CreateBVConst(string*& strval, int base, int bit_width)
+    ASTNode CreateBVConst(string& strval, int base, int bit_width)
     {
        return bm.CreateBVConst(strval, base, bit_width);
     }

diff --git a/src/parser/smtlib.y b/src/parser/smtlib.y
index 53f7f705ae7a6532d46f16eea8bfbc98c24875d9..9dd83918b5d8b8bc620985c7558fb81e34981ea7 100644 (file)
--- a/src/parser/smtlib.y
+++ b/src/parser/smtlib.y
@@ -683,12 +683,12 @@ an_terms an_term
 an_term:
 BVCONST_TOK
 {
-  $$ = new ASTNode(parserInterface->CreateBVConst($1, 10, 32));
+  $$ = new ASTNode(parserInterface->CreateBVConst(*$1, 10, 32));
   delete $1;
 }
 | BVCONST_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
 {
-  $$ = new ASTNode(parserInterface->CreateBVConst($1,10,$3));
+  $$ = new ASTNode(parserInterface->CreateBVConst(*$1,10,$3));
   delete $1;
 }
 | an_nonbvconst_term

diff --git a/src/parser/smtlib2.y b/src/parser/smtlib2.y
index 463260b5e707dc0d79a6167febbb8c18cda779ac..927dec165e75f88acd04a233d03bd8fe84d6365f 100644 (file)
--- a/src/parser/smtlib2.y
+++ b/src/parser/smtlib2.y
@@ -930,21 +930,21 @@ TERMID_TOK
 }
 | UNDERSCORE_TOK BVCONST_DECIMAL_TOK NUMERAL_TOK
 {
-       $$ = new ASTNode(parserInterface->CreateBVConst($2, 10, $3));
+       $$ = new ASTNode(parserInterface->CreateBVConst(*$2, 10, $3));
     $$->SetValueWidth($3);
     delete $2;
 }
 | BVCONST_HEXIDECIMAL_TOK
 {
        unsigned width = $1->length()*4;
-       $$ = new ASTNode(parserInterface->CreateBVConst($1, 16, width));
+       $$ = new ASTNode(parserInterface->CreateBVConst(*$1, 16, width));
     $$->SetValueWidth(width);
     delete $1;
 }
 | BVCONST_BINARY_TOK
 {
        unsigned width = $1->length();
-       $$ = new ASTNode(parserInterface->CreateBVConst($1, 2, width));
+       $$ = new ASTNode(parserInterface->CreateBVConst(*$1, 2, width));
     $$->SetValueWidth(width);
     delete $1;
 }