Reverting r465. Based on Stephen's example: stp-tests/crypto-tests/factoring-12bitsx1...

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

diff --git a/src/to-sat/BitBlastNew.cpp b/src/to-sat/BitBlastNew.cpp
index f6ba02a016c9cae50c34344e1f814c7e48e48b5d..f0db7d365351b7fa274864a4692c0dd12bc22926 100644 (file)
--- a/src/to-sat/BitBlastNew.cpp
+++ b/src/to-sat/BitBlastNew.cpp
@@ -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);