added cnf dumping facility

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index d04d5caedb795b07e014fa9cc03230413e3b1a8a..3e710a3005277232dd1fde89b7059b995898ae48 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -21,11 +21,16 @@ namespace BEEV {
                                            bm->CreateNode(NOT, query));
     
     //solver instantiated here
-#ifdef CORE
+#if defined CORE || defined CRYPTOMINISAT
     MINISAT::Solver NewSolver;
 #endif
-#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2
+#if defined CRYPTOMINISAT2
     MINISAT::Solver NewSolver;
+    if(bm->UserFlags.print_cnf_flag)
+      {
+       newS.needLibraryCNFFile("output.cnf");
+      }
+
 #endif
 #ifdef SIMP
     MINISAT::SimpSolver NewSolver;

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 6f44a3c889f35ae2ced27257117ed2e240574ea2..579fa5048fb3177bfdd1fb13c39a05502d2b328b 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -90,10 +90,6 @@ namespace BEEV
 #endif
       }
 
-    if(bm->UserFlags.print_cnf_flag)
-      {
-       //newSolver.cnfDump = true;
-      }
 #ifdef CRYPTOMINISAT
     newSolver.startClauseAdding();
 #endif