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