From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 25 Mar 2012 05:00:47 +0000 (+0000)
Subject: Improvement. Two extra simplifications for the bvmod
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=b1148470383ed4753b88a9cdb3e90b2a708c1ae8;p=francis%2Fstp.git

Improvement. Two extra simplifications for the bvmod

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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 44e3958..0da30f9 100644
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -2809,6 +2809,33 @@ namespace BEEV
             output = _bm->CreateZeroConst(inputValueWidth);
             break;
           }
+        if (inputterm[1] == _bm->CreateOneConst(inputValueWidth))
+          {
+            output = _bm->CreateZeroConst(inputValueWidth);
+            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(BVMOD,rest,top,bottom);
+           div = nf->CreateTerm(BVCONCAT,inputValueWidth,_bm->CreateZeroConst(inputValueWidth-rest),div);
+
+           output = nf->CreateTerm(ITE, inputValueWidth, cond, div, _bm->CreateZeroConst(inputValueWidth));
+           break;
+         }
+
         ASTNode lessThan = SimplifyFormula(nf->CreateNode(BVLT, inputterm[0], inputterm[1]), false, NULL);
 
         if (lessThan == ASTTrue)