When encoding to CNF via ABC, use the simple mapping if there are more than 10M nodes...

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

diff --git a/src/to-sat/AIG/BBNodeManagerAIG.cpp b/src/to-sat/AIG/BBNodeManagerAIG.cpp
index f12473719253e00e30053d0dbfe1c9236b2ff125..db97940ad63a78d0cb1df39a19122979a4c24d09 100644 (file)
--- a/src/to-sat/AIG/BBNodeManagerAIG.cpp
+++ b/src/to-sat/AIG/BBNodeManagerAIG.cpp
@@ -56,7 +56,10 @@ namespace BEEV
               break;
           }
       }
-    cnfData = Cnf_Derive(aigMgr, 0);
+    if (aigMgr->nObjs[AIG_OBJ_AND] < 10000000)
+      cnfData = Cnf_Derive(aigMgr, 0);
+    else
+      cnfData = Cnf_DeriveSimple(aigMgr, 0);
 
     BBNodeManagerAIG::SymbolToBBNode::const_iterator it;