From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 25 Mar 2012 01:35:28 +0000 (+0000)
Subject: Improvement. If the numerator of a division contains leading zeroes, replace the... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=ecc15a0920f31591feb22b87623cb3bad77989b8;p=francis%2Fstp.git

Improvement. If the numerator of a division contains leading zeroes, replace the division with a concatenation. Thanks to Edward Schwartz for providing the test case to inspire this.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1604 e59a4935-1847-0410-ae03-e826735625c1
---

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index d667b8e..9551d9b 100644
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -2774,6 +2774,28 @@ namespace BEEV
             output = inputterm[0];
             break;
           }
+        unsigned int nlz=  numberOfLeadingZeroes(inputterm[0]);
+        if (nlz > 0)
+          {
+            nlz = std::min(inputValueWidth-1,nlz);
+            int rest = inputValueWidth-nlz;
+            ASTNode low = _bm->CreateBVConst(32,rest);
+            ASTNode high =_bm->CreateBVConst(32,inputValueWidth-1);
+
+            ASTNode cond = nf->CreateNode(EQ,_bm->CreateZeroConst(nlz),
+                           nf->CreateTerm(BVEXTRACT, nlz, inputterm[1], high,low));
+
+            ASTNode top = nf->CreateTerm(BVEXTRACT, rest, inputterm[0], _bm->CreateBVConst(32,rest-1),_bm->CreateZeroConst(32));
+            ASTNode bottom = nf->CreateTerm(BVEXTRACT, rest, inputterm[1], _bm->CreateBVConst(32,rest-1),_bm->CreateZeroConst(32));
+
+            ASTNode div = nf->CreateTerm(BVDIV,rest,top,bottom);
+            div = nf->CreateTerm(BVCONCAT,inputValueWidth,_bm->CreateZeroConst(inputValueWidth-rest),div);
+
+            output = nf->CreateTerm(ITE, inputValueWidth, cond, div, _bm->CreateZeroConst(inputValueWidth));
+            cerr << output;
+            break;
+          }
+
         ASTNode lessThan = SimplifyFormula(nf->CreateNode(BVLT, inputterm[0], inputterm[1]), false, NULL);
         if (lessThan == ASTTrue)
           output = _bm->CreateZeroConst(inputValueWidth);