From e2f89ce59c467a972ff6db40662a64b5f087a073 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Tue, 8 Jun 2010 11:28:27 +0000 Subject: [PATCH] Copy the cleaner new SplitEven_into_Oddnum_PowerOf2 function from bvsolverExp. I'm comparing the values from the old and new version of the function still. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@814 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/bvsolver.cpp | 26 +++++++++++++++++++++++--- src/simplifier/bvsolver.h | 5 ++++- 2 files changed, 27 insertions(+), 4 deletions(-) diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp index e0a80f6..3d74532 100644 --- a/src/simplifier/bvsolver.cpp +++ b/src/simplifier/bvsolver.cpp @@ -57,11 +57,31 @@ namespace BEEV FormulasAlreadySolvedMap[key] = value; } //end of UpdateAlreadySolvedMap() + //accepts an even number "in", and returns the location of + // the lowest bit that is turned on in that number. + void BVSolver::SplitEven_into_Oddnum_PowerOf2(const ASTNode& in, + unsigned int& number_shifts) { + assert (BVCONST == in.GetKind() && !_simp->BVConstIsOdd(in)); + + // location of the least significant bit turned on. + for (number_shifts = 0; number_shifts < in.GetValueWidth() + && !CONSTANTBV::BitVector_bit_test(in.GetBVConst(), number_shifts); number_shifts++) { + }; + assert(number_shifts >0); // shouldn't be odd. + +#ifndef NDEBUG + // check that old == new. + unsigned t_number_shifts=0; + SplitEven_into_Oddnum_PowerOf2_OLD(in,t_number_shifts); + assert(number_shifts == t_number_shifts); +#endif + } + //FIXME This is doing way more arithmetic than it needs to. //accepts an even number "in", and splits it into an odd number and //a power of 2. i.e " in = b.(2^k) ". returns the odd number, and //the power of two by reference - ASTNode BVSolver::SplitEven_into_Oddnum_PowerOf2(const ASTNode& in, + ASTNode BVSolver::SplitEven_into_Oddnum_PowerOf2_OLD(const ASTNode& in, unsigned int& number_shifts) { if (BVCONST != in.GetKind() || _simp->BVConstIsOdd(in)) @@ -767,7 +787,7 @@ namespace BEEV } ASTVec lhs_c = lhs.GetChildren(); - ASTNode odd; + //ASTNode odd; for (ASTVec::iterator it = lhs_c.begin(), itend = lhs_c.end(); it != itend; it++) @@ -789,7 +809,7 @@ namespace BEEV //we are gauranteed that if control is here then the monomial is //of the form 'a*x' or 'a', where 'a' is even ASTNode coeff = (BVCONST == itk) ? aaa : aaa[0]; - odd = SplitEven_into_Oddnum_PowerOf2(coeff, power_of_2); + SplitEven_into_Oddnum_PowerOf2(coeff, power_of_2); if (power_of_2 < power_of_2_lowest) { power_of_2_lowest = power_of_2; diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h index 91bd87d..310b8d6 100644 --- a/src/simplifier/bvsolver.h +++ b/src/simplifier/bvsolver.h @@ -105,7 +105,10 @@ namespace BEEV //Refer STP's CAV 2007 (or Clark Barrett's 1998 paper on //bit-vector arithmetic published in DAC 1998) paper for precise //understanding of the algorithm - ASTNode SplitEven_into_Oddnum_PowerOf2(const ASTNode& in, + void SplitEven_into_Oddnum_PowerOf2(const ASTNode& in, + unsigned int& number_shifts); + + ASTNode SplitEven_into_Oddnum_PowerOf2_OLD(const ASTNode& in, unsigned int& number_shifts); //Once a formula has been solved, then update the alreadysolvedmap -- 2.47.3