From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 14 Feb 2011 01:14:05 +0000 (+0000)
Subject: Add --config options to enable CNF conversion via Tseitin, and AIG rewrites.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=d2808374c86a25888b1013fbf89fbdaec2097f44;p=francis%2Fstp.git

Add --config options to enable CNF conversion via Tseitin, and AIG rewrites.

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

diff --git a/src/to-sat/AIG/ToCNFAIG.cpp b/src/to-sat/AIG/ToCNFAIG.cpp
index ee36150..34ef47e 100644
--- a/src/to-sat/AIG/ToCNFAIG.cpp
+++ b/src/to-sat/AIG/ToCNFAIG.cpp
@@ -67,8 +67,7 @@ void ToCNFAIG::toCNF(const BBNodeAIG& top, Cnf_Dat_t*& cnfData,
 	if (uf.stats_flag)
 		cerr << "Nodes before AIG rewrite:" << nodeCount << endl;
 
-	if (!needAbsRef && uf.enable_AIG_rewrites_flag
-			&& mgr.aigMgr->nObjs[AIG_OBJ_AND] < 5000) {
+	if (!needAbsRef && uf.isSet("aig_rewrite","0")) {
 		Dar_LibStart();
 		Aig_Man_t * pTemp;
 		Dar_RwrPar_t Pars, *pPars = &Pars;
@@ -100,7 +99,7 @@ void ToCNFAIG::toCNF(const BBNodeAIG& top, Cnf_Dat_t*& cnfData,
 				break;
 		}
 	}
-	if (!needAbsRef && mgr.aigMgr->nObjs[AIG_OBJ_AND] < 2000000) {
+	if (!needAbsRef && mgr.aigMgr->nObjs[AIG_OBJ_AND] < 2000000 && !uf.isSet("simple-cnf","0")) {
 		cnfData = Cnf_Derive(mgr.aigMgr, 0);
 	} else {
 		cnfData = Cnf_DeriveSimple(mgr.aigMgr, 0);