From 066dc0bf33e4564f55294ab3ea3b509704bdb0ac Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 11 May 2011 04:24:39 +0000 Subject: [PATCH] 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 --- src/to-sat/AIG/ToCNFAIG.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) 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; -- 2.47.3