From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 11 May 2011 04:24:39 +0000 (+0000)
Subject: No longer default to the simple CNF generator for big AIGs, i.e >=2Million nodes... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=066dc0bf33e4564f55294ab3ea3b509704bdb0ac;p=francis%2Fstp.git

No longer default to the simple CNF generator for big AIGs, i.e >=2Million nodes. We used to do this because of a bug(?) now fixed in ABC.

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

diff --git a/src/to-sat/AIG/ToCNFAIG.cpp b/src/to-sat/AIG/ToCNFAIG.cpp
index 34ef47e..4b8b702 100644
--- a/src/to-sat/AIG/ToCNFAIG.cpp
+++ b/src/to-sat/AIG/ToCNFAIG.cpp
@@ -99,10 +99,15 @@ void ToCNFAIG::toCNF(const BBNodeAIG& top, Cnf_Dat_t*& cnfData,
 				break;
 		}
 	}
-	if (!needAbsRef && mgr.aigMgr->nObjs[AIG_OBJ_AND] < 2000000 && !uf.isSet("simple-cnf","0")) {
+	if (!needAbsRef &&  !uf.isSet("simple-cnf","0")) {
 		cnfData = Cnf_Derive(mgr.aigMgr, 0);
+		if (uf.stats_flag)
+		  cerr << "advanced CNF" << endl;
 	} else {
 		cnfData = Cnf_DeriveSimple(mgr.aigMgr, 0);
+                if (uf.stats_flag)
+                  cerr << "simple CNF" << endl;
+
 	}
 
 	BBNodeManagerAIG::SymbolToBBNode::const_iterator it;