From 2e8105588fccbda060f6871c771b643a8eb259c1 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 27 Apr 2011 00:37:21 +0000 Subject: [PATCH] Remove signed division, modulus and remainder when creating nodes via the simplifying node factory. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1283 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/ArrayTransformer.cpp | 23 +++++++--------- src/AST/ArrayTransformer.h | 2 +- .../NodeFactory/SimplifyingNodeFactory.cpp | 27 ++++++++++++------- 3 files changed, 27 insertions(+), 25 deletions(-) diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp index 332fd69..4a8a3ba 100644 --- a/src/AST/ArrayTransformer.cpp +++ b/src/AST/ArrayTransformer.cpp @@ -52,7 +52,7 @@ namespace BEEV } //Translates signed BVDIV,BVMOD and BVREM into unsigned variety - ASTNode ArrayTransformer::TranslateSignedDivModRem(const ASTNode& in) + ASTNode ArrayTransformer::TranslateSignedDivModRem(const ASTNode& in, NodeFactory* nf, STPMgr *bm) { assert(in.GetChildren().size() ==2); @@ -99,11 +99,6 @@ namespace BEEV cond_dividend, nf->CreateTerm(BVUMINUS, len, modnode), modnode); - - //put everything together, simplify, and return - if (bm->UserFlags.optimize_flag) - return simp->SimplifyTerm_TopLevel(n); - else return n; } @@ -154,9 +149,6 @@ namespace BEEV nf->CreateTerm(BVPLUS, len, rev_node, divisor), rev_node); - if (bm->UserFlags.optimize_flag) - return simp->SimplifyTerm_TopLevel(n); - else return n; } else if (SBVDIV == in.GetKind()) @@ -200,15 +192,12 @@ namespace BEEV nf->CreateTerm(BVUMINUS, len, divnode), divnode); - if (bm->UserFlags.optimize_flag) - return simp->SimplifyTerm_TopLevel(n); - else return n; } FatalError("TranslateSignedDivModRem:"\ "input must be signed DIV/MOD/REM", in); - return ASTUndefined; + return bm->ASTUndefined; }//end of TranslateSignedDivModRem() @@ -452,7 +441,13 @@ namespace BEEV || SBVREM == result.GetKind() || SBVMOD == result.GetKind()) { - result = TranslateSignedDivModRem(result); + 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/ArrayTransformer.h b/src/AST/ArrayTransformer.h index 660ebd9..62d5d1b 100644 --- a/src/AST/ArrayTransformer.h +++ b/src/AST/ArrayTransformer.h @@ -85,7 +85,6 @@ namespace BEEV * Private Member Functions * ****************************************************************/ - ASTNode TranslateSignedDivModRem(const ASTNode& in); ASTNode TransformTerm(const ASTNode& inputterm); void assertTransformPostConditions(const ASTNode & term, ASTNodeSet& visited); @@ -94,6 +93,7 @@ namespace BEEV ASTNode TransformFormula(const ASTNode& form); public: + static ASTNode TranslateSignedDivModRem(const ASTNode& in, NodeFactory*nf, STPMgr *bm); //fill the arrayname_readindices vector if e0 is a READ(Arr,index) //and index is a BVCONST diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp index a3ef9b9..0fad759 100644 --- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp +++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp @@ -25,6 +25,7 @@ #include #include "SimplifyingNodeFactory.h" #include "../../simplifier/simplifier.h" +#include "../ArrayTransformer.h" #include using BEEV::Kind; @@ -977,12 +978,14 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, break; case BEEV::SBVMOD: - if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty( - children[1].GetBVConst())) - result = children[0]; - if (children[0] == children[1]) - result = bm.CreateZeroConst(width); - break; + if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty( + children[1].GetBVConst())) + result = children[0]; + else if (children[0] == children[1]) + result = bm.CreateZeroConst(width); + else + result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children),this,&bm); + break; case BEEV::BVDIV: @@ -993,23 +996,27 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, case BEEV::SBVDIV: if (children[1].isConstant() && children[1] == bm.CreateOneConst(width)) result = children[0]; + else + result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children),this,&bm); break; case BEEV::SBVREM: if (children[0] == children[1]) result = bm.CreateZeroConst(width); - if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty( + else if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty( children[0].GetBVConst())) result = bm.CreateZeroConst(width); - if (children[1].isConstant() && CONSTANTBV::BitVector_is_full( + else if (children[1].isConstant() && CONSTANTBV::BitVector_is_full( children[1].GetBVConst())) result = bm.CreateZeroConst(width); - if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty( + else if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty( children[1].GetBVConst())) result = children[0]; - if (children[1].isConstant() && bm.CreateOneConst(width) == children[1]) + else if (children[1].isConstant() && bm.CreateOneConst(width) == children[1]) result = bm.CreateZeroConst(width); + else + result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children),this,&bm); break; case BEEV::BVMOD: -- 2.47.3