Improvement. If the numerator of a division contains leading zeroes, replace the...

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 d667b8ec9186edf219a38329f42a044947074106..9551d9b199ac44663a66e833e5eb101f1baf7f13 100644 (file)
--- 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);