Changes to inactive code. Use simple AIG simplifications on complex problems.

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

diff --git a/src/to-sat/AIG/BBNodeManagerAIG.cpp b/src/to-sat/AIG/BBNodeManagerAIG.cpp
index ff1bd68cb09e26a7bedad4e1d17930e98a705694..088349dfb209b1a166cc7d78aa3fc90d21a3d31c 100644 (file)
--- a/src/to-sat/AIG/BBNodeManagerAIG.cpp
+++ b/src/to-sat/AIG/BBNodeManagerAIG.cpp
@@ -28,10 +28,24 @@ namespace BEEV
           Aig_Man_t * pTemp;
           Dar_RwrPar_t Pars, * pPars = &Pars;
           Dar_ManDefaultRwrParams( pPars );
-          //pPars->fUpdateLevel =0;
-          //pPars->fUseZeros = 1;
 
-          for (int i=0; i < 3;i++)
+          // Assertion errors occur with this enabled.
+          // pPars->fUseZeros = 1;
+
+          // For mul63bit.smt2 with iterations =3 & nCutsMax = 8
+          // CNF generation was taking 139 seconds, solving 10 seconds.
+
+          // With nCutsMax =2, CNF generation takes 16 seconds, solving 10 seconds.
+          // The rewriting doesn't remove as many nodes of course..
+          int iterations = 3;
+          if (nodeCount > 1000000)
+          {
+            iterations =1;
+            pPars->nCutsMax=2;
+          }
+
+
+          for (int i=0; i < iterations;i++)
           {
             aigMgr = Aig_ManDup( pTemp = aigMgr, 0 );
             Aig_ManStop( pTemp );