No longer default to the simple CNF generator for big AIGs, i.e >=2Million nodes...

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 34ef47e6bc464612cecf3a36b276123202b49e09..4b8b702aa55d02c4f8d3820bd7db37a7efb4797a 100644 (file)
--- 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;