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 44e3958247cee0b0d55fd09ef8d673056b067f8d..0da30f95bcac2e0b5223352406c970ce9376f623 100644 (file)
--- 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)