From f7e100672fbbca0c58035ac124f106e41cf36e8a Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 20 Feb 2012 03:54:20 +0000 Subject: [PATCH] Improvement. The bitblaster now handled signed div/mod/rem. They don't need to be removed before bitblasting. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1571 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/ArrayTransformer.cpp | 21 +------------------ .../NodeFactory/SimplifyingNodeFactory.cpp | 8 ------- .../constantBitP/ConstantBitPropagation.cpp | 7 ++----- src/to-sat/BitBlaster.cpp | 13 ++++++++++++ 4 files changed, 16 insertions(+), 33 deletions(-) diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp index 42eb09e..0507c7a 100644 --- a/src/AST/ArrayTransformer.cpp +++ b/src/AST/ArrayTransformer.cpp @@ -35,7 +35,7 @@ namespace BEEV TransformMap = new ASTNodeMap(100); ASTNode result = TransformFormula(form); -#ifndef NDEBUG +#if 0 { ASTNodeSet visited; assertTransformPostConditions(result,visited); @@ -49,7 +49,6 @@ namespace BEEV if (bm->UserFlags.stats_flag) printArrayStats(); - // This establishes equalities between every indexes, and a fresh variable. if (!bm->UserFlags.ackermannisation) { @@ -271,11 +270,6 @@ namespace BEEV const Kind k = term.GetKind(); - // Check the signed operations have been removed. - assert( SBVDIV != k); - assert( SBVMOD != k); - assert( SBVREM !=k); - // Check the array reads / writes have been removed assert( READ !=k ); assert( WRITE !=k); @@ -488,19 +482,6 @@ namespace BEEV } else result = term; - - if (SBVDIV == result.GetKind() - || SBVREM == result.GetKind() - || SBVMOD == result.GetKind()) - { - ASTNode r = TranslateSignedDivModRem(result,nf,bm); - if (r != result && bm->UserFlags.optimize_flag) - { - result = simp->SimplifyTerm_TopLevel(r); - } - else - result = r; - } } break; } diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp index 2c0379a..45871f3 100644 --- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp +++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp @@ -50,8 +50,6 @@ using BEEV::BVDIV; static bool debug_simplifyingNodeFactory = false; -static const bool translate_signed = true; - ASTNode SimplifyingNodeFactory::CreateNode(Kind kind, const ASTVec & children) { @@ -1311,8 +1309,6 @@ SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, const ASTVec & result = bm.CreateZeroConst(width); else if (children[1].GetKind() == BVUMINUS && children[1][0] == children[0]) result = bm.CreateZeroConst(width); - else if (translate_signed) - result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children), this, &bm); break; case BEEV::BVDIV: @@ -1350,8 +1346,6 @@ SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, const ASTVec & bm.CreateOneConst(width), bm.CreateZeroConst(width)); if (children[1].isConstant() && CONSTANTBV::BitVector_is_full(children[1].GetBVConst())) result = NodeFactory::CreateTerm(BVUMINUS, width, children[0]); - else if (translate_signed) - result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children), this, &bm); break; case SBVREM: @@ -1369,8 +1363,6 @@ SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, const ASTVec & result = NodeFactory::CreateTerm(SBVREM, width, children[0], children[1][0]); else if (children[0].GetKind() == BVUMINUS && children[0][0] == children[1]) result = bm.CreateZeroConst(width); - else if (translate_signed) - result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children), this, &bm); break; case BEEV::BVMOD: diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.cpp b/src/simplifier/constantBitP/ConstantBitPropagation.cpp index ae22989..0190a56 100644 --- a/src/simplifier/constantBitP/ConstantBitPropagation.cpp +++ b/src/simplifier/constantBitP/ConstantBitPropagation.cpp @@ -742,15 +742,12 @@ namespace simplifier result = bvSignedRemainderBothWays(children, output, n.GetSTPMgr()); mult_like=true; } - - // This propagator is very slow. It needs to be reimplemented. - #if 0 else if (k == SBVMOD) { - result = bvSignedModulusBothWays(children, output, n.GetSTPMgr()); + // This propagator is very slow. It needs to be reimplemented. + //result = bvSignedModulusBothWays(children, output, n.GetSTPMgr()); mult_like=true; } - #endif else diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp index dc798f2..9595663 100644 --- a/src/to-sat/BitBlaster.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -15,6 +15,7 @@ #include "../simplifier/constantBitP/ConstantBitPropagation.h" #include "../simplifier/constantBitP/NodeToFixedBitsMap.h" #include "../simplifier/simplifier.h" +#include "../AST/ArrayTransformer.h" namespace BEEV { @@ -347,6 +348,8 @@ namespace BEEV if (n.isConstant()) { + // This doesn't hold any longer because we convert BVSDIV and friends to ASTNodes. +#if 0 simplifier::constantBitP::NodeToFixedBitsMap::NodeToFixedBitsMapType::const_iterator it; it = cb->fixedMap->map->find(n); if (it == cb->fixedMap->map->end()) @@ -354,6 +357,7 @@ namespace BEEV cerr << n; assert(it != cb->fixedMap->map->end()); }assert(it->second->isTotallyFixed()); +#endif return; } @@ -829,6 +833,15 @@ namespace BEEV result = BBMult(mpcd1, mpcd2, support, term); break; } + case SBVREM: + case SBVMOD: + case SBVDIV: + { + ASTNode p = ArrayTransformer::TranslateSignedDivModRem(term,ASTNF,term.GetSTPMgr()); + result = BBTerm(p,support); + break; + } + case BVDIV: case BVMOD: { -- 2.47.3