]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commitdiff
Reverting r465. Based on Stephen's example: stp-tests/crypto-tests/factoring-12bitsx1...
authortrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Sun, 25 Apr 2010 11:00:20 +0000 (11:00 +0000)
committertrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Sun, 25 Apr 2010 11:00:20 +0000 (11:00 +0000)
Confirming what Stephen identified, varying just the bvdiv encoding:

crypto2: 42sec vs 32sec
simplifying minisat: 65s vs 37s
core minisat: 65s vs 43s

However, r600 solved this problem the fastest I've seen: 14 seconds. But that was cryptominisat. Cryptominisat2 is now in the trunk. So I suspect that this reverts a change that made division faster on cryptominisat, but slowed it down on the others (including cryptominisat2).

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

src/to-sat/BitBlastNew.cpp

index f6ba02a016c9cae50c34344e1f814c7e48e48b5d..f0db7d365351b7fa274864a4692c0dd12bc22926 100644 (file)
@@ -610,7 +610,8 @@ void BitBlasterNew::BBDivMod(const BBNodeVec &y, const BBNodeVec &x,
                BBNodeVec notylessxrval = BBITE(yeqx, BBfill(width, nf->getFalse()),
                                ygtrxrval);
                // y < x <=> not x >= y.
-               BBNode ylessx = BBBVLE(y, x, false, true);
+               //BBNode ylessx = BBBVLE(y, x, false, true);
+               BBNode ylessx = nf->CreateNode(NOT, BBBVLE(x, y, false));
                // final values of q and r
                q = BBITE(ylessx, BBfill(width, nf->getFalse()), notylessxqval);
                r = BBITE(ylessx, y, notylessxrval);