* Add signed & unsigned shifts to a test generator

* Speed up the shifting circuit, by treating specially bits beyond log2 of the bitwidth.
* During simplification if the shift amount is known, then remove the shift replacing it with a concat and extract.

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

diff --git a/src/AST/AST.h b/src/AST/AST.h
index 6385f8dcf71965f9ddf77cfa80b2b599c4c54855..41190cf9b3a16429c6808638dbe10b5d7718823b 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -941,10 +941,6 @@ namespace BEEV
     // Return bit-blasted form for BVLE, BVGE, BVGT, SBLE, etc.
     ASTNode BBcompare(const ASTNode& form);
 
-    // Left and right shift one.  Writes into x.
-    void BBLShift(ASTVec& x);
-    void BBRShift(ASTVec& x);
-
     void BBRSignedShift(ASTVec& x, unsigned int shift);
     void BBLShift(ASTVec& x, unsigned int shift);
     void BBRShift(ASTVec& x, unsigned int shift);

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 8fb9aea5ecf0f87ade4a6fbbac21de9b5fc7a7d9..75139428fc70728e143cfc94e48b4b52612b51f9 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -10,6 +10,7 @@
 #include "../AST/AST.h"
 #include "../AST/ASTUtil.h"
 #include <cassert>
+#include <cmath>
 
 namespace BEEV
 {
@@ -2115,12 +2116,71 @@ ASTNode Flatten(const ASTNode& a)
             }
           break;
         }
+
+
+      case BVLEFTSHIFT:
+               case BVRIGHTSHIFT:
+
+               { // If the shift amount is known. Then replace it by an extract.
+                       ASTNode a = SimplifyTerm(inputterm[0], VarConstMap);
+                       ASTNode b = SimplifyTerm(inputterm[1], VarConstMap);
+                       const unsigned int width = a.GetValueWidth();
+                       if (BVCONST == b.GetKind()) // known shift amount.
+                       {
+                               if (CONSTANTBV::Set_Max(b.GetBVConst()) > 1 + log2(width))
+                               {
+                                       // Intended to remove shifts by very large amounts that don't fit into the unsigned.
+                                       // at thhe start of the "else" branch.
+                                       output = CreateZeroConst(width);
+                               }
+                               else
+                               {
+                                       const unsigned int shift = GetUnsignedConst(b);
+                                       if (shift > width)
+                                       {
+                                               output = CreateZeroConst(width);
+                                       }
+                                       else if (shift == 0)
+                                       {
+                                               output = a; // unchanged.
+                                       }
+                                       else
+                                       {
+                                               if (k == BVLEFTSHIFT)
+                                               {
+                                                       ASTNode zero = CreateZeroConst(shift);
+                                                       ASTNode hi = CreateBVConst(32, width - shift -1);
+                                                       ASTNode low = CreateBVConst(32, 0);
+                                                       ASTNode extract = CreateTerm(BVEXTRACT, width - shift, a, hi, low);
+                                                       BVTypeCheck(extract);
+                                                       output = CreateTerm(BVCONCAT, width, extract, zero);
+                                                       BVTypeCheck(output);
+                                               }
+                                               else if (k == BVRIGHTSHIFT)
+                                               {
+                                                       ASTNode zero = CreateZeroConst(shift);
+                                                       ASTNode hi = CreateBVConst(32, width );
+                                                       ASTNode low = CreateBVConst(32, shift+1);
+                                                       ASTNode extract = CreateTerm(BVEXTRACT, width - shift, a, hi, low);
+                                                       BVTypeCheck(extract);
+                                                       output = CreateTerm(BVCONCAT, width, zero, extract);
+                                                       BVTypeCheck(output);
+                                               }
+                                               else
+                                                       FatalError("herasdf");
+                                       }
+                               }
+                       }
+                       else
+                               output = CreateTerm(k, width, a, b);
+               }
+               break;
+
+
       case BVXOR:
       case BVXNOR:
       case BVNAND:
       case BVNOR:
-      case BVLEFTSHIFT:
-      case BVRIGHTSHIFT:
       case BVVARSHIFT:
       case BVSRSHIFT:
       case BVDIV:

diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp
index 88becd69c5af06c9542076019d6ab55303d6c2f3..fd537c1a2afd0848ab24a9d7d845c8a251974fcc 100644 (file)
--- a/src/to-sat/BitBlast.cpp
+++ b/src/to-sat/BitBlast.cpp
@@ -19,6 +19,8 @@
 // The 0th element of the vector corresponds to bit 0 -- the low-order bit.
 
 #include "../AST/AST.h"
+#include <cmath>
+
 namespace BEEV
 {
   //  extern void lpvec(ASTVec &vec);
@@ -45,17 +47,9 @@ namespace BEEV
         return it->second;
       }
 
-    //  ASTNode& result = ASTJunk;
     ASTNode result;
 
-    /*
-      bool weregood = false;
-      if(term.GetNodeNum() == 17408){
-      weregood = true;
-      }
-    */
-
-    Kind k = term.GetKind();
+    const Kind k = term.GetKind();
     if (!is_Term_kind(k))
       FatalError("BBTerm: Illegal kind to BBTerm", term);
 
@@ -73,121 +67,78 @@ namespace BEEV
           break;
         }
 
-      case BVLEFTSHIFT:
-        {
-          if (BVCONST == term[1].GetKind())
-            {
-              // Constant shifts should be removed during simplification.
-              unsigned int shift = GetUnsignedConst(term[1]);
-
-              ASTNode term0 = BBTerm(term[0]);
-              ASTVec children(term0.GetChildren()); // mutable copy of the children.
-              BBLShift(children, shift);
-
-              result = CreateNode(BOOLVEC, children);
-            }
-          else
-            {
-              // Barrel shifter
-              const ASTVec& bbarg1 = BBTerm(term[0]).GetChildren();
-              const ASTVec& bbarg2 = BBTerm(term[1]).GetChildren();
-
-              ASTVec temp_result(bbarg1);
-
-              for (unsigned int i = 0; i < bbarg2.size(); i++)
-                {
-                  if (bbarg2[i] == ASTFalse)
-                    continue; // Not shifting by anything.
-
-                  unsigned int shift_amount = 1 << i;
-
-                  bool done = false;
-
-                  for (unsigned int j = temp_result.size() - 1; !done; j--)
-                    {
-                      if (j < shift_amount)
-                        temp_result[j] = CreateSimpForm(ITE, bbarg2[i], ASTFalse, temp_result[j]);
-                      else
-                        temp_result[j] = CreateSimpForm(ITE, bbarg2[i], temp_result[j - shift_amount], temp_result[j]);
-
-                      // want the loop to finish after j=0, but when j=0, j-1 == MAX_INT. Hence this weird idiom.
-                      if (j == 0)
-                        done = true;
-                    }
-                }
-
-              result = CreateNode(BOOLVEC, temp_result);
-            }
-          break;
-        }
-
-      case BVRIGHTSHIFT:
-      case BVSRSHIFT:
-        {
-          if (BVCONST == term[1].GetKind())
-            {
-              // Constant shifts should be removed during simplification.
-
-              unsigned int shift = GetUnsignedConst(term[1]);
-
-              ASTNode term0 = BBTerm(term[0]);
-              ASTVec children(term0.GetChildren()); // mutable copy of the children.
-
-              if (BVRIGHTSHIFT == k)
-                BBRShift(children, shift);
-              else
-                BBRSignedShift(children, shift);
-
-              result = CreateNode(BOOLVEC, children);
-            }
-          else
-            {
-              // Barrel shifter
-              const ASTVec& bbarg1 = BBTerm(term[0]).GetChildren();
-              const ASTVec& bbarg2 = BBTerm(term[1]).GetChildren();
-
-
-              // Signed right shift, need to copy the sign bit.
-              ASTNode toFill;
-              if (BVRIGHTSHIFT == k)
-                toFill = ASTFalse;
-              else
-                toFill = bbarg1.back();
-
-              ASTVec temp_result(bbarg1);
-
-              for (unsigned int i = 0; i < bbarg2.size(); i++)
-                {
-                  if (bbarg2[i] == ASTFalse)
-                    continue; // Not shifting by anything.
-
-                  unsigned int shift_amount = 1 << i;
-
-                  bool done = false;
-
-                  for (unsigned int j = 0; j < temp_result.size(); j++)
-                    {
-                      if (j + shift_amount >= temp_result.size())
-                        temp_result[j] = CreateSimpForm(ITE, bbarg2[i], toFill, temp_result[j]);
-                      else
-                        temp_result[j] = CreateSimpForm(ITE, bbarg2[i], temp_result[j + shift_amount], temp_result[j]);
-
-                      if (j == 0)
-                        done = true;
-                    }
-                }
-
-              result = CreateNode(BOOLVEC, temp_result);
-
-              /*        cerr << result << endl;
-                        cerr << term[0] << endl;
-                        cerr << term[1] << endl;
-                        cerr << "right shift. Node size is:" << NodeSize(result) << endl;
-                        cerr << "input size: " << NodeSize(term[0]) << " " << NodeSize(term[1]) << endl;
-              */
-            }
-        }
-        break;
+               case BVRIGHTSHIFT:
+               case BVSRSHIFT:
+               case BVLEFTSHIFT:
+               {
+                       // Barrel shifter
+                       const ASTVec& bbarg1 = BBTerm(term[0]).GetChildren();
+                       const ASTVec& bbarg2 = BBTerm(term[1]).GetChildren();
+
+                       // Signed right shift, need to copy the sign bit.
+                       ASTNode toFill;
+                       if (BVSRSHIFT == k)
+                               toFill = bbarg1.back();
+                       else
+                               toFill = ASTFalse;
+
+                       ASTVec temp_result(bbarg1);
+                       // if any bit is set in bbarg2 higher than log2Width, then we know that the result is zero.
+                       // Add one to make allowance for rounding down. For example, given 300 bits, the log2 is about
+                       // 8.2 so round up to 9.
+
+                       const unsigned width = bbarg1.size();
+                       unsigned log2Width = log2(width) + 1;
+
+
+                       if (k == BVSRSHIFT || k == BVRIGHTSHIFT)
+                               for (unsigned int i = 0; i < log2Width; i++)
+                               {
+                                       if (bbarg2[i] == ASTFalse)
+                                               continue; // Not shifting by anything.
+
+                                       unsigned int shift_amount = 1 << i;
+
+                                       for (unsigned int j = 0; j < width; j++)
+                                       {
+                                               if (j + shift_amount >= width)
+                                                       temp_result[j] = CreateSimpForm(ITE, bbarg2[i], toFill, temp_result[j]);
+                                               else
+                                                       temp_result[j] = CreateSimpForm(ITE, bbarg2[i], temp_result[j + shift_amount], temp_result[j]);
+                                       }
+                               }
+                       else
+                               for (unsigned int i = 0; i < log2Width; i++)
+                               {
+                                       if (bbarg2[i] == ASTFalse)
+                                               continue; // Not shifting by anything.
+
+                                       int shift_amount = 1 << i;
+
+                                       for (signed int j = width - 1; j > 0; j--)
+                                       {
+                                               if (j < shift_amount)
+                                                       temp_result[j] = CreateSimpForm(ITE, bbarg2[i], toFill, temp_result[j]);
+                                               else
+                                                       temp_result[j] = CreateSimpForm(ITE, bbarg2[i], temp_result[j - shift_amount], temp_result[j]);
+                                       }
+                               }
+
+                       // If any of the remainder are true. Then the whole thing gets the fill value.
+                       ASTNode remainder = ASTFalse;
+                       for (unsigned int i = log2Width; i < width; i++)
+                       {
+                               remainder = CreateNode(OR, remainder, bbarg2[i]);
+                       }
+
+                       for (unsigned int i = 0; i < width; i++)
+                       {
+                               temp_result[i] = CreateSimpForm(ITE, remainder, toFill, temp_result[i]);
+                       }
+
+                       result = CreateNode(BOOLVEC, temp_result);
+               }
+                       break;
       case BVVARSHIFT:
         FatalError("BBTerm: These kinds have not been implemented in the BitBlaster: ", term);
         break;
@@ -552,7 +503,7 @@ namespace BEEV
           CBV bv = term.GetBVConst();
           for (unsigned int i = 0; i < num_bits; i++)
             {
-              tmp_res[i] = 
+              tmp_res[i] =
                 CONSTANTBV::BitVector_bit_test(bv, i) ? ASTTrue : ASTFalse;
             }
           result = CreateNode(BOOLVEC, tmp_res);
@@ -835,7 +786,7 @@ namespace BEEV
     for (xit++; xit < xend; xit++)
       {
         // shift first
-        BBLShift(ycopy);
+        BBLShift(ycopy,1);
 
         if (ASTFalse == *xit)
           {
@@ -867,16 +818,16 @@ namespace BEEV
       {
         ASTVec q1, r1;
         ASTVec yrshift1(y);
-        BBRShift(yrshift1);
+        BBRShift(yrshift1,1);
 
         // recursively divide y/2 by x.
         BBDivMod(yrshift1, x, q1, r1, rwidth - 1);
 
         ASTVec q1lshift1(q1);
-        BBLShift(q1lshift1);
+        BBLShift(q1lshift1,1);
 
         ASTVec r1lshift1(r1);
-        BBLShift(r1lshift1);
+        BBLShift(r1lshift1,1);
 
         ASTVec r1lshift1plusyodd = BBAddOneBit(r1lshift1, y[0]);
         ASTVec rminusx(r1lshift1plusyodd);
@@ -987,23 +938,6 @@ namespace BEEV
     return msb;
   }
 
-  // Left shift by 1 within fixed field inserting zeros at LSB.
-  // Writes result into first argument.
-  // Fixme: generalize to n bits
-  void BeevMgr::BBLShift(ASTVec& x)
-  {
-    // left shift x (destructively) within width.
-    // loop backwards so that copy to self works correctly. (DON'T use STL insert!)
-    ASTVec::iterator xbeg = x.begin();
-    for (ASTVec::iterator xit = x.end() - 1; xit > xbeg; xit--)
-      {
-        *xit = *(xit - 1);
-      }
-    *xbeg = ASTFalse; // new LSB is zero.
-    // cout << "Shifted result" << endl;
-    // lpvec(x);
-  }
-
   // Left shift  within fixed field inserting zeros at LSB.
   // Writes result into first argument.
   void BeevMgr::BBLShift(ASTVec& x, unsigned int shift)
@@ -1054,20 +988,6 @@ namespace BEEV
       }
   }
 
-  // Right shift by 1 within fixed field, inserting new zeros at MSB.
-  // Writes result into first argument.
-  // Fixme: generalize to n bits.
-  void BeevMgr::BBRShift(ASTVec& x)
-  {
-    ASTVec::iterator xend = x.end() - 1;
-    ASTVec::iterator xit = x.begin();
-    for (; xit < xend; xit++)
-      {
-        *xit = *(xit + 1);
-      }
-    *xit = ASTFalse; // new MSB is zero.
-  }
-
   // Return bit-blasted form for BVLE, BVGE, BVGT, SBLE, etc.
   ASTNode BeevMgr::BBcompare(const ASTNode& form)
   {

diff --git a/tests/generated_tests/Makefile b/tests/generated_tests/Makefile
new file mode 100644 (file)
index 0000000..a9cee77
--- /dev/null
+++ b/tests/generated_tests/Makefile
@@ -0,0 +1,2 @@
+mudivrem:
+       g++ mulDivRem.cpp -m32 -Wno-deprecated -DTR1_UNORDERED_MAP  -o muldiv -L../../lib -lstp
\ No newline at end of file

diff --git a/tests/generated_tests/mulDivRem.cpp b/tests/generated_tests/mulDivRem.cpp
index 13b204e1faa42bc88b578b79b1d2f87ebcc1d6e7..7ab8e50e0826e0e2f7f53461e4afec0e20b23479 100644 (file)
--- a/tests/generated_tests/mulDivRem.cpp
+++ b/tests/generated_tests/mulDivRem.cpp
@@ -1,10 +1,10 @@
-#include <cstdint>
+//#include <cstdint>
 #include <iostream>
 #include <cstdlib>
 #include <cassert>
 #include <cmath>
-#include "../constantbv/constantbv.h"
-#include "../AST/AST.h"
+#include "../../src/AST/AST.h"
+#include "../../src/extlib-constbv/constantbv.h"
 
 /*
  * Generates random (a op b = c) triples to check that solver.
@@ -17,9 +17,9 @@ using std::cerr;
 using namespace BEEV;
 using namespace CONSTANTBV;
 
-int width = 16;
-typedef uint16_t uns;
-typedef int16_t sig;
+int width = 64;
+typedef uint64_t uns;
+typedef int64_t sig;
 
 const bool debug = false;
 
@@ -38,7 +38,14 @@ uns getUnsignedResult(uns a, Kind k, uns b)
        else if (BVDIV == k)
        {
                return a / b;
+       }else if (BVLEFTSHIFT == k)
+       {
+               return (b > (sizeof(a) * 8) ? 0 : a << b);
        }
+       else if (BVRIGHTSHIFT == k)
+               {
+                       return (b > (sizeof(a) * 8) ? 0 : a << b);
+               }
        cerr << "not implemetned" << endl;
        exit(2);
 
@@ -68,6 +75,10 @@ sig getSignedResult(sig a, Kind k, sig b)
        {
                gold = a / b;
        }
+       else if (BVSRSHIFT == k)
+       {
+               return (b > (sizeof(a) * 8) ? 0 : a >> b);
+       }
        else
        {
                cerr << "not implemetned" << endl;
@@ -77,7 +88,7 @@ sig getSignedResult(sig a, Kind k, sig b)
 
 }
 
-void go(int count, uns a, uns b, uns result, char* name)
+void go(int count, uns a, uns b, uns result, const char* name)
 {
        cout << ":extrafuns ((a" << count << " BitVec[" << width << "])) " << endl;
        cout << ":extrafuns ((b" << count << " BitVec[" << width << "])) " << endl;
@@ -123,7 +134,7 @@ void testSolver(void)
                bS = rand();
        } while (bS == 0 || b == 0);
 
-       switch (rand() % 6)
+       switch (rand() % 9)
        {
                case 0:
                        go(0, a, b, getUnsignedResult(a, BVMULT, b), "bvmul");
@@ -143,6 +154,16 @@ void testSolver(void)
                case 5:
                        go(5, aS, bS, getSignedResult(aS, SBVMOD, bS), "bvsmod");
                        break;
+               case 6:
+                       go(5, aS, bS, getUnsignedResult(aS, BVLEFTSHIFT, bS), "bvshl");
+                       break;
+               case 7:
+                       go(5, aS, bS, getUnsignedResult(aS, BVRIGHTSHIFT, bS), "bvshl");
+                       break;
+               case 8:
+                       go(5, aS, bS, getSignedResult(aS, BVSRSHIFT, bS), "bvshl");
+                       break;
+
 
        }
        cout << ")" << endl;
@@ -164,12 +185,6 @@ int main(int argc, char**argv)
 
        BitVector_Boot();
 
-       if (false)
-       {
-               testConstEval(SBVMOD);
-               testConstEval(SBVREM);
-               testConstEval(SBVDIV);
-       }
        testSolver();
 
        return 0;

diff --git a/tests/generated_tests/runMulDivRem.sh b/tests/generated_tests/runMulDivRem.sh
new file mode 100755 (executable)
index 0000000..486bf1d
--- /dev/null
+++ b/tests/generated_tests/runMulDivRem.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+for i in {1..5000}
+do
+  ./muldiv > file
+  result=`stp -d -m file`
+  if [ $result != "sat" ]; then
+      echo "failed"  
+      exit
+      fi
+  echo $result
+done