From d2178492470f701a833c29dae2d046194c45ca32 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Tue, 6 Jul 2010 05:03:02 +0000 Subject: [PATCH] * 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 --- scripts/Makefile.common | 4 ++++ src/AST/ASTmisc.cpp | 5 +++-- src/STPManager/UserDefinedFlags.h | 6 ++++++ src/simplifier/constantBitP/FixedBits.cpp | 10 +++++++--- src/simplifier/constantBitP/FixedBits.h | 2 +- src/simplifier/consteval.cpp | 3 ++- src/to-sat/BitBlaster.cpp | 6 ++++-- 7 files changed, 27 insertions(+), 9 deletions(-) diff --git a/scripts/Makefile.common b/scripts/Makefile.common index 89da27b..41e8b2c 100644 --- 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 8281cbd..3584b06 100644 --- 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 00eb60a..0265915 100644 --- 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 6304562..49368c9 100644 --- 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 e6cd072..6ded3d7 100644 --- 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 b4465f3..9b804fc 100644 --- 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 a62233e..814b8a2 100644 --- a/src/to-sat/BitBlaster.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -280,7 +280,9 @@ const BBNodeVec BitBlaster::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::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); -- 2.47.3