From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 18 Aug 2010 07:25:11 +0000 (+0000)
Subject: Changes to inactive code. Use simple AIG simplifications on complex problems.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=7ce6c78e4f2c5e680f0990b64ff908c374500718;p=francis%2Fstp.git

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 ff1bd68..088349d 100644
--- 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 );