From 15c47f9e575968f9c85730bd467b9fccc9e2082c Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 4 Jul 2010 08:25:47 +0000 Subject: [PATCH] Tiny speedup. Generate the encoding of multiplication slightly more efficiently. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@918 e59a4935-1847-0410-ae03-e826735625c1 --- src/to-sat/BitBlaster.cpp | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp index f43c207..a1729bb 100644 --- a/src/to-sat/BitBlaster.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -944,9 +944,20 @@ void BitBlaster::BBDivMod(const BBNodeVec &y, const BBNod BBNodeVec &q, BBNodeVec &r, unsigned int rwidth, BBNodeSet& support) { const unsigned int width = y.size(); const BBNodeVec zero = BBfill(width, nf->getFalse()); - const BBNodeVec one = BBInc(zero); + BBNodeVec one = zero; + one[0] = nf->getTrue(); - if (rwidth == 0) { + // check if y is already zero. + bool isZero=true; + for (int i =0; i < rwidth;i++) + if (y[i] != nf->getFalse()) + { + isZero = false; + break; + } + + + if (isZero || rwidth == 0) { // When we have shifted the entire width, y is guaranteed to be 0. q = zero; r = zero; -- 2.47.3