* Make GetUnsignedConst a member function of ASTNode.

* In GetUnsignedConst check the position of the maximum bit only if the size is > , not >=

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

diff --git a/src/AST/ASTNode.cpp b/src/AST/ASTNode.cpp
index fe1dc4102e0f287f268dcecd25c7d16aeb7a4808..09d43f17d78376fccd45f1e5cf8d34f116c08745 100644 (file)
--- a/src/AST/ASTNode.cpp
+++ b/src/AST/ASTNode.cpp
@@ -159,6 +159,31 @@ namespace BEEV
     return ((ASTBVConst *) _int_node_ptr)->GetBVConst();
   } //End of GetBVConst()
 
+  unsigned int ASTNode::GetUnsignedConst() const
+  {
+       const ASTNode& n = *this;
+    assert(BVCONST == n.GetKind());
+
+    if (sizeof(unsigned int) * 8 < n.GetValueWidth())
+      {
+        // It may only contain a small value in a bit type,
+        // which fits nicely into an unsigned int.  This is
+        // common for functions like: bvshl(bv1[128],
+        // bv1[128]) where both operands have the same type.
+        signed long maxBit = CONSTANTBV::Set_Max(n.GetBVConst());
+        if (maxBit >= ((signed long) sizeof(unsigned int)) * 8)
+          {
+            n.LispPrint(cerr); //print the node so they can find it.
+            FatalError("GetUnsignedConst: cannot convert bvconst "\
+                       "of length greater than 32 to unsigned int");
+          }
+      }
+    return (unsigned int) *((unsigned int *) n.GetBVConst());
+  } //end of GetUnsignedConst
+
+
+
+
   void ASTNode::NFASTPrint(int l, int max, int prefix) const
   {
     //****************************************

diff --git a/src/AST/ASTNode.h b/src/AST/ASTNode.h
index 3f4c6b0d447dd4ba2036dcf35944237ac780d9e5..013247dc95c38bfa743cc940ab7510b84f056adf 100644 (file)
--- a/src/AST/ASTNode.h
+++ b/src/AST/ASTNode.h
@@ -335,6 +335,9 @@ namespace BEEV
     //Get the BVCONST value.
     CBV GetBVConst() const;
 
+    unsigned int GetUnsignedConst() const;
+
+
     /*******************************************************************
      * ASTNode is of type BV      <==> ((indexwidth=0)&&(valuewidth>0))*
      * ASTNode is of type ARRAY   <==> ((indexwidth>0)&&(valuewidth>0))*

diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp
index b700eb5f79436e8e956999ec4ca4df4594fdeb25..23b3bc8577070a646b1eae2f0bf5058e9556be81 100644 (file)
--- a/src/AST/ASTmisc.cpp
+++ b/src/AST/ASTmisc.cpp
@@ -262,9 +262,9 @@ namespace BEEV
               FatalError("BVTypeCheck: should have exactly 3 args\n", n);
             if (!(BVCONST == n[1].GetKind() && BVCONST == n[2].GetKind()))
               FatalError("BVTypeCheck: indices should be BVCONST\n", n);
-            if (n.GetValueWidth() != GetUnsignedConst(n[1]) - GetUnsignedConst(n[2]) + 1)
+            if (n.GetValueWidth() != n[1].GetUnsignedConst() - n[2].GetUnsignedConst() + 1)
               FatalError("BVTypeCheck: length mismatch\n", n);
-            if (GetUnsignedConst(n[1]) >= n[0].GetValueWidth())
+            if (n[1].GetUnsignedConst() >= n[0].GetValueWidth())
               FatalError("BVTypeCheck: Top index of select is greater or equal to the bitwidth.\n", n);
             break;
           case BVLEFTSHIFT:
@@ -351,30 +351,6 @@ namespace BEEV
     return true;
   } //End of TypeCheck function
 
-  //Return the unsigned constant value of the input 'n'
-  unsigned int GetUnsignedConst(const ASTNode n)
-  {
-    if(BVCONST != n.GetKind()){
-      FatalError("GetUnsignedConst: cannot extract an "\
-                 "unsigned value from a non-bvconst");
-    }
-
-    if (sizeof(unsigned int) * 8 <= n.GetValueWidth())
-      {
-        // It may only contain a small value in a bit type,
-        // which fits nicely into an unsigned int.  This is
-        // common for functions like: bvshl(bv1[128],
-        // bv1[128]) where both operands have the same type.
-        signed long maxBit = CONSTANTBV::Set_Max(n.GetBVConst());
-        if (maxBit >= ((signed long) sizeof(unsigned int)) * 8)
-          {
-            n.LispPrint(cerr); //print the node so they can find it.
-            FatalError("GetUnsignedConst: cannot convert bvconst "\
-                       "of length greater than 32 to unsigned int");
-          }
-      }
-    return (unsigned int) *((unsigned int *) n.GetBVConst());
-  } //end of GetUnsignedConst
 
   //if a is READ(Arr,const) or SYMBOL, and b is BVCONST then return 1
   //if b is READ(Arr,const) or SYMBOL, and a is BVCONST then return -1

diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp
index e4ab1d037d95a5baf2dbc5976165ab1adabf0543..be693a00bc5d202e2cb9a21b26ccd4bac431db54 100644 (file)
--- a/src/absrefine_counterexample/CounterExample.cpp
+++ b/src/absrefine_counterexample/CounterExample.cpp
@@ -69,7 +69,7 @@ namespace BEEV
                 v = _ASTNode_to_BitvectorMap[symbol];
 
                 //kk is the index of BVGETBIT
-                const unsigned int kk = GetUnsignedConst(s[1]);
+                const unsigned int kk = s[1].GetUnsignedConst();
 
                 //Collect the bits of 'symbol' and store in v. Store
                 //in reverse order.
@@ -868,7 +868,7 @@ namespace BEEV
                   GetCounterExample(t, readexpr);
                 //cout << "ASSERT( ";
                 //cout << " = ";
-                out_int.push_back(GetUnsignedConst(val));
+                out_int.push_back(val.GetUnsignedConst());
                 //cout << "\n";
               }
           }

diff --git a/src/printer/CPrinter.cpp b/src/printer/CPrinter.cpp
index 99af73cd9d388173b1bc357366b53f39cc36841a..dce9d364a8f72e773297b65895d8b46915a7499a 100644 (file)
--- a/src/printer/CPrinter.cpp
+++ b/src/printer/CPrinter.cpp
@@ -149,8 +149,8 @@ namespace printer
         // we only accept indices that are byte-aligned
         // (e.g., [15:8], [23:16])
         // and round down to byte indices rather than bit indices
-        upper = GetUnsignedConst(c[1]);
-        lower = GetUnsignedConst(c[2]);
+        upper = c[1].GetUnsignedConst();
+        lower = c[2].GetUnsignedConst();
         assert(upper > lower);
         assert(lower % 8 == 0);
         assert((upper + 1) % 8 == 0);
@@ -178,7 +178,7 @@ namespace printer
         os << "(";
         C_Print1(os, c[0], indentation, letize);
         os << " << ";
-        os << GetUnsignedConst(c[1]);
+        os << c[1].GetUnsignedConst();
         os << ")";
         break;
       case BVRIGHTSHIFT:
@@ -187,7 +187,7 @@ namespace printer
         os << "(";
         C_Print1(os, c[0], indentation, letize);
         os << " >> ";
-        os << GetUnsignedConst(c[1]);
+        os << c[1].GetUnsignedConst();
         os << ")";
         break;
       case BVMULT:
@@ -308,14 +308,14 @@ namespace printer
         // comparison
         if (LHSkind == BVEXTRACT)
           {
-            upper = GetUnsignedConst(c[0].GetChildren()[1]);
-            lower = GetUnsignedConst(c[0].GetChildren()[2]);
+            upper = c[0].GetChildren()[1].GetUnsignedConst();
+            lower = c[0].GetChildren()[2].GetUnsignedConst();
             num_bytes = (upper - lower + 1) / 8;
           }
         else if (RHSkind == BVEXTRACT)
           {
-            upper = GetUnsignedConst(c[1].GetChildren()[1]);
-            lower = GetUnsignedConst(c[1].GetChildren()[2]);
+            upper = c[1].GetChildren()[1].GetUnsignedConst();
+            lower = c[1].GetChildren()[2].GetUnsignedConst();
             num_bytes = (upper - lower + 1) / 8;
           }
 
@@ -478,8 +478,8 @@ namespace printer
             // see if it's a BVEXTRACT, and if so, whether it's multi-byte
             if (it->second.GetKind() == BVEXTRACT)
               {
-                upper = GetUnsignedConst(it->second.GetChildren()[1]);
-                lower = GetUnsignedConst(it->second.GetChildren()[2]);
+                upper = it->second.GetChildren()[1].GetUnsignedConst();
+                lower = it->second.GetChildren()[2].GetUnsignedConst();
                 num_bytes = (upper - lower + 1) / 8;
                 assert(num_bytes > 0);
               }

diff --git a/src/printer/PLPrinter.cpp b/src/printer/PLPrinter.cpp
index d6c791e65059c3f1f108dcbff019f0d399b0e9d8..499ac62507c73b54ced04e7e721efbaae739fe0e 100644 (file)
--- a/src/printer/PLPrinter.cpp
+++ b/src/printer/PLPrinter.cpp
@@ -162,9 +162,9 @@ string functionToCVCName(const Kind k) {
       case BVEXTRACT:
         PL_Print1(os, c[0], indentation, letize);
         os << "[";
-        os << GetUnsignedConst(c[1]);
+        os << c[1].GetUnsignedConst();
         os << ":";
-        os << GetUnsignedConst(c[2]);
+        os << c[2].GetUnsignedConst();
         os << "]";
         break;
       case BVLEFTSHIFT:
@@ -175,7 +175,7 @@ string functionToCVCName(const Kind k) {
         {
                FatalError("PL_Print1: The shift argument to a left shift must be a constant. Found:",c[1]);
         }
-        os << GetUnsignedConst(c[1]);
+        os << c[1].GetUnsignedConst();
         os << ")";
         os << "[";
         os << (c[0].GetValueWidth()-1);

diff --git a/src/printer/SMTLIB1Printer.cpp b/src/printer/SMTLIB1Printer.cpp
index d56f3b7cab9617c4e5bbf902c3ce4cef1c581f34..0d318e8c45109c9886f13c0b74d69b5791c48600 100644 (file)
--- a/src/printer/SMTLIB1Printer.cpp
+++ b/src/printer/SMTLIB1Printer.cpp
@@ -181,7 +181,7 @@ void printSMTLIB1VarDeclsToStream(ASTNodeSet& symbols, ostream& os)
       case BVSX:
       case BVZX:
         {
-          unsigned int amount = GetUnsignedConst(c[1]);
+          unsigned int amount = c[1].GetUnsignedConst();
           if (BVZX == kind)
             os << "(zero_extend[";
           else
@@ -194,8 +194,8 @@ void printSMTLIB1VarDeclsToStream(ASTNodeSet& symbols, ostream& os)
         break;
       case BVEXTRACT:
         {
-          unsigned int upper = GetUnsignedConst(c[1]);
-          unsigned int lower = GetUnsignedConst(c[2]);
+          unsigned int upper = c[1].GetUnsignedConst();
+          unsigned int lower = c[2].GetUnsignedConst();
           assert(upper >= lower);
           os << "(extract[" << upper << ":" << lower << "] ";
           SMTLIB1_Print1(os, c[0], indentation, letize);

diff --git a/src/printer/SMTLIB2Printer.cpp b/src/printer/SMTLIB2Printer.cpp
index 9f437c15bda7785caf1fecc87ad501dc8bd2875d..8d3b3fd36c4ae4b63090e499205a741381d51351 100644 (file)
--- a/src/printer/SMTLIB2Printer.cpp
+++ b/src/printer/SMTLIB2Printer.cpp
@@ -177,7 +177,7 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os)
       case BVSX:
       case BVZX:
         {
-          unsigned int amount = GetUnsignedConst(c[1]);
+          unsigned int amount = c[1].GetUnsignedConst();
           if (BVZX == kind)
             os << "((_ zero_extend ";
           else
@@ -190,8 +190,8 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os)
         break;
       case BVEXTRACT:
         {
-          unsigned int upper = GetUnsignedConst(c[1]);
-          unsigned int lower = GetUnsignedConst(c[2]);
+          unsigned int upper = c[1].GetUnsignedConst();
+          unsigned int lower = c[2].GetUnsignedConst();
           assert(upper >= lower);
           os << "((_ extract " << upper << " " << lower << ") ";
           SMTLIB2_Print1(os, c[0], indentation, letize);

diff --git a/src/simplifier/consteval.cpp b/src/simplifier/consteval.cpp
index d81f238352aa200fc721699ad3dc00161678c162..8fbab6057289a07e0d112a8c6029ee1e3eb99cb8 100644 (file)
--- a/src/simplifier/consteval.cpp
+++ b/src/simplifier/consteval.cpp
@@ -135,7 +135,7 @@ namespace BEEV
               // the shift is destructive, get a copy.
               CONSTANTBV::BitVector_Interval_Copy(output, tmp0, 0, 0, inputwidth);
 
-              unsigned int shift = GetUnsignedConst(shiftNode);
+              unsigned int shift = shiftNode.GetUnsignedConst();
 
               if (k == BVLEFTSHIFT)
                 CONSTANTBV::BitVector_Move_Left(output, shift);
@@ -201,8 +201,8 @@ namespace BEEV
         {
           output = CONSTANTBV::BitVector_Create(inputwidth, true);
           tmp0 = children[0].GetBVConst();
-          unsigned int hi = GetUnsignedConst(children[1]);
-          unsigned int low = GetUnsignedConst(children[2]);
+          unsigned int hi = children[1].GetUnsignedConst();
+          unsigned int low = children[2].GetUnsignedConst();
           unsigned int len = hi - low + 1;
 
           CONSTANTBV::BitVector_Destroy(output);

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index d2a268047940e2eac98b4ee55bf3fd73dbecaf0f..4a5b5047476887a7f9810fcf446491237be0757e 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -2005,8 +2005,8 @@ namespace BEEV
           ASTNode zero = _bm->CreateBVConst(32, 0);
           //recall that the indices of BVEXTRACT are always 32 bits
           //long. therefore doing a GetBVUnsigned is ok.
-          unsigned int i_val = GetUnsignedConst(i);
-          unsigned int j_val = GetUnsignedConst(j);
+          unsigned int i_val = i.GetUnsignedConst();
+          unsigned int j_val = j.GetUnsignedConst();
 
           // a0[i:0] and len(a0)=i+1, then return a0
           if (0 == j_val && a_len == a0.GetValueWidth())
@@ -2502,7 +2502,7 @@ namespace BEEV
                 }
               else
                 {
-                  const unsigned int shift = GetUnsignedConst(b);
+                  const unsigned int shift = b.GetUnsignedConst();
                   if (shift >= width)
                     {
                       output = _bm->CreateZeroConst(width);

diff --git a/src/to-sat/BitBlastNew.cpp b/src/to-sat/BitBlastNew.cpp
index 82420d49f89fa2cfba12c540f8e49eda3ad71ddc..c5b3650fe8bcb8dfadbc733a2c666269a23604e1 100644 (file)
--- a/src/to-sat/BitBlastNew.cpp
+++ b/src/to-sat/BitBlastNew.cpp
@@ -223,8 +223,8 @@ const BBNodeVec BitBlasterNew::BBTerm(const ASTNode& term, BBNodeSet& support) {
                // with memo-ization.
 
                const BBNodeVec& bbkids = BBTerm(term[0], support);
-               const unsigned int high = GetUnsignedConst(term[1]);
-               const unsigned int low = GetUnsignedConst(term[2]);
+               const unsigned int high = term[1].GetUnsignedConst();
+               const unsigned int low = term[2].GetUnsignedConst();
 
                BBNodeVec::const_iterator bbkfit = bbkids.begin();
                // I should have used pointers to BBNodeVec, to avoid this crock