completed the cnf dumping feature. it works

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 3e710a3005277232dd1fde89b7059b995898ae48..623b6250381425518ab0826ee08349222fce36cc 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -28,7 +28,7 @@ namespace BEEV {
     MINISAT::Solver NewSolver;
     if(bm->UserFlags.print_cnf_flag)
       {
-       newS.needLibraryCNFFile("output.cnf");
+       NewSolver.needLibraryCNFFile(bm->UserFlags.cnf_dump_filename);
       }
 
 #endif

diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h
index 359df1f51bbceb599a983c0c05a0af61c14f3996..5fbb988983d33fdc0bb464d80c762b8a958f39ea 100644 (file)
--- a/src/STPManager/UserDefinedFlags.h
+++ b/src/STPManager/UserDefinedFlags.h
@@ -67,6 +67,7 @@ namespace BEEV
 
     //Flag that allows the printing of the DIMACS format of the input
     bool print_cnf_flag;
+    char * cnf_dump_filename;
 
     //flag to decide whether to print "valid/invalid" or not
     bool print_output_flag;
@@ -146,6 +147,7 @@ namespace BEEV
       //Flag that allows the printing of the DIMACS format of the
       //input
       print_cnf_flag = false;
+      cnf_dump_filename = (char*)"stp-input.cnf";
 
       //flag to decide whether to print "valid/invalid" or not
       print_output_flag = false;

diff --git a/src/main/main.cpp b/src/main/main.cpp
index f4e7ab4d299f5ddcfca16dae6b1cae9a9e3fed1c..9a2d45caf0177f5799713029393e676d962e47b6 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -91,6 +91,8 @@ int main(int argc, char ** argv) {
     "-h  : help\n";
   helpstring +=  
     "-i <random_seed>  : Randomize STP's satisfiable output. Random_seed is an integer >= 0.\n";
+  helpstring +=  
+    "-j <filename>  : CNF Dumping. Creates a DIMACS equivalent file of the input STP file\n";
   helpstring +=  
     "-m  : use the SMTLIB parser\n";
   helpstring +=  
@@ -169,6 +171,7 @@ int main(int argc, char ** argv) {
              break;
            case 'j':
              bm->UserFlags.print_cnf_flag = true;
+             bm->UserFlags.cnf_dump_filename = argv[++i];
              break;
             case 'n':
               bm->UserFlags.print_output_flag = true;