* Interface changes for constant bit propagation. Not currently enabled.

* Add code to bitblast etc. for bvzx. BVZX can be created via the interface, and might not be simplified out before reaching the bitblaster.

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

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index 89da27b8aea547db0fd9a14ae72fd9d7a1347248..41e8b2cbd047b5e7c03446d7696e46cc0cc48b04 100644 (file)
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -37,6 +37,10 @@ ifeq ($(SAT),minisat)
   SOLVER_INCLUDE = $(TOP)/src/sat/core
 endif
 
+ifeq ($(WITHCBITP),yes)
+       CFLAGS_BASE += -DWITHCBITP
+endif
+
 # todo: These should be set by the config script of course..
 TEST_PREFIX=../../stp-tests/
 SHELL=/bin/bash

diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp
index 8281cbd2383e394f061f87605e074955530c7df9..3584b06f4ba8a8dd658c6afb4b38ec032d065d4a 100644 (file)
--- a/src/AST/ASTmisc.cpp
+++ b/src/AST/ASTmisc.cpp
@@ -299,16 +299,17 @@ bool containsArrayOps(const ASTNode&n)
               break;
             }
           case BVSX:
+          case BVZX:
                        //in BVSX(n[0],len), the length of the BVSX term must be
                        //greater than the length of n[0]
                        if (n[0].GetValueWidth() > n.GetValueWidth()) {
                                FatalError(
-                                               "BVTypeCheck: BVSX(t,bvsx_len) : length of 't' must be <= bvsx_len\n",
+                                               "BVTypeCheck: BV[SZ]X(t,bv[sz]x_len) : length of 't' must be <= bv[sz]x_len\n",
                                                n);
                        }
                        if ((v.size() != 2))
                                FatalError(
-                                               "BVTypeCheck:BVSX must have two arguments. The second is the new width\n",
+                                               "BVTypeCheck:BV[SZ]X must have two arguments. The second is the new width\n",
                                                n);
                        break;
 

diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h
index 00eb60a5d6314c5818c7c4385f6868d779f0256c..0265915155fd74fbcf13f4409683c8ae54e3ff11 100644 (file)
--- a/src/STPManager/UserDefinedFlags.h
+++ b/src/STPManager/UserDefinedFlags.h
@@ -113,6 +113,9 @@ namespace BEEV
 
     bool bitConstantProp_flag;
 
+
+    bool cBitP_propagateForDivisionByZero;
+
     // Available back-end SAT solvers.
     enum SATSolvers
       {
@@ -221,6 +224,9 @@ namespace BEEV
       // Should constant bit propagation be enabled?
       bitConstantProp_flag = true;
 
+      // given a/b = c, propagates that c<=a even if b may be zero.
+      cBitP_propagateForDivisionByZero =true;
+
     } //End of constructor for UserDefinedFlags
 
   }; //End of struct UserDefinedFlags

diff --git a/src/simplifier/constantBitP/FixedBits.cpp b/src/simplifier/constantBitP/FixedBits.cpp
index 6304562c9b87acff3385258fc1df0cd65b9f128e..49368c90bc7ab971941729b1d8faa68f5e907a00 100644 (file)
--- a/src/simplifier/constantBitP/FixedBits.cpp
+++ b/src/simplifier/constantBitP/FixedBits.cpp
@@ -1,6 +1,10 @@
 #include "../../AST/AST.h"
 #include "FixedBits.h"
-//#include "../../utility/MersenneTwister.h"
+
+#ifdef WITHCBITP
+  #include "MersenneTwister.h"
+#endif
+
 #include "ConstantBitP_Utility.h"
 
 // To reduce the memory I tried using the constantbv stuff. But because it is not
@@ -150,7 +154,7 @@ namespace simplifier
       return result;
     }
 
-#if 0
+#ifdef WITHCBITP
     // Getting a new random number is expensive. Not sure why.
     FixedBits FixedBits::createRandom(const int length, const int probabilityOfSetting, MTRand& trand)
       {
@@ -193,7 +197,7 @@ namespace simplifier
                     result.setValue(i, true);
                     break;
                     default:
-                    throw std::runtime_error(LOCATION "never.");
+                    BEEV::FatalError(LOCATION "never.");
 
                   }
                 randomV >>= 1;

diff --git a/src/simplifier/constantBitP/FixedBits.h b/src/simplifier/constantBitP/FixedBits.h
index e6cd0726df5b0ad0350fe9f014b0a383868c806b..6ded3d74895891d5fd20fcb83fae08eda317ac14 100644 (file)
--- a/src/simplifier/constantBitP/FixedBits.h
+++ b/src/simplifier/constantBitP/FixedBits.h
@@ -11,7 +11,7 @@ namespace BEEV
 {
   class ASTNode;
   typedef unsigned int * CBV;
-  extern bool disable_bitConstantProp;
+  void FatalError(const char * str);
 }
 
 namespace simplifier

diff --git a/src/simplifier/consteval.cpp b/src/simplifier/consteval.cpp
index b4465f3a24d588be0127e8418f22a48feda97f52..9b804fcc9a5ee81ced31c9b47353c19990db3bfb 100644 (file)
--- a/src/simplifier/consteval.cpp
+++ b/src/simplifier/consteval.cpp
@@ -88,6 +88,7 @@ namespace BEEV
           break;
         }
       case BVSX:
+      case BVZX:
         {
           output = CONSTANTBV::BitVector_Create(inputwidth, true);
           unsigned t0_width = t[0].GetValueWidth();
@@ -98,7 +99,7 @@ namespace BEEV
             }
           else
             {
-              bool topbit_sign = (CONSTANTBV::BitVector_Sign(tmp0) < 0);
+              bool topbit_sign = (k == BVSX)?(CONSTANTBV::BitVector_Sign(tmp0) < 0): false;
 
               if (topbit_sign)
                 {

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index a62233ef35d6d6e175279e9f4b7f2d75a1952f34..814b8a225303d744db0a79295a7e2570f5cce480 100644 (file)
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -280,7 +280,9 @@ const BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::BBTerm(const ASTNode& term, B
                break;
        }
 
-       case BVSX: {
+       case BVSX:
+       case BVZX:
+         {
                // Replicate high-order bit as many times as necessary.
                // Arg 0 is expression to be sign extended.
                const ASTNode& arg = term[0];
@@ -294,7 +296,7 @@ const BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::BBTerm(const ASTNode& term, B
                        break;
                } else {
                        //we need to sign extend
-                       const BBNode& msb = bbarg.back();
+                       const BBNode& msb = (k == BVSX) ?bbarg.back() : BBFalse;
 
                        BBNodeVec tmp_res(result_width);