From 52ad34b1a264976aed7be2bf3d3de67f000a8897 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sat, 1 Aug 2009 18:04:12 +0000 Subject: [PATCH] I broke the division family in #100. Fixing. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@101 e59a4935-1847-0410-ae03-e826735625c1 --- AST/Transform.cpp | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/AST/Transform.cpp b/AST/Transform.cpp index 4d18cf8..baa9adb 100644 --- a/AST/Transform.cpp +++ b/AST/Transform.cpp @@ -318,26 +318,29 @@ ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm) Kind k = result.GetKind(); - if (SBVDIV == result.GetKind() || SBVREM == result.GetKind() || SBVMOD == result.GetKind()) + if (BVDIV == k || BVMOD == k || SBVDIV == k || SBVREM == k || SBVMOD == k) { - result = TranslateSignedDivModRem(result); - } + ASTNode bottom = result[1]; + + if (SBVDIV == result.GetKind() || SBVREM == result.GetKind() || SBVMOD == result.GetKind()) + { + result = TranslateSignedDivModRem(result); + } + + ////// Temporary hack so we don't get killed on the Spear benchmarks in SMTCOMP-2009 + // This is a difficult rule to introduce in other places because it's recursive. i.e. + // result is imbedded unchanged inside the result. It's not - ////// Temporary hack so we don't get killed on the Spear benchmarks in SMTCOMP-2009 - // This is a difficult rule to introduce in other places because it's recursive. i.e. - // result is imbedded unchanged inside the result. It's not - if (BVDIV==k || BVMOD==k || SBVDIV == k || SBVREM == k || SBVMOD == k) - { unsigned inputValueWidth = result.GetValueWidth(); ASTNode zero = CreateZeroConst(inputValueWidth); ASTNode one = CreateOneConst(inputValueWidth); - result = CreateTerm(ITE, inputValueWidth, CreateNode(EQ, zero, result[1]), one, result); + result = CreateTerm(ITE, inputValueWidth, CreateNode(EQ, zero, bottom), one, result); } + } //////////////////////////////////////////////////////////////////////////////////// break; - } } TransformMap[term] = result; -- 2.47.3