]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commitdiff
Fix. remove the -j option. Which did nothing. It used to output a CNF from the conten...
authortrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Wed, 19 Jan 2011 06:03:03 +0000 (06:03 +0000)
committertrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Wed, 19 Jan 2011 06:03:03 +0000 (06:03 +0000)
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1081 e59a4935-1847-0410-ae03-e826735625c1

src/main/main.cpp

index e3c2e03b256dd467fc9831ae23069550b87c5945..e431b169c5797c0814edfa2e84b295cc78ba7510 100644 (file)
@@ -139,15 +139,15 @@ 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 +=
+  //    "-j <filename>          : CNF Dumping. Creates a DIMACS equivalent file of the input STP file\n";
   helpstring +=  
     "-m                     : use the SMTLIB1 parser\n";
   helpstring +=
     "--minisat              : use minisat 2.2 as the solver\n";
 
   helpstring +=  
-    "--output-CNF           : save the CNF into output.cnf\n";
+    "--output-CNF           : save the CNF into output_[0..n].cnf\n";
   helpstring +=  
     "--output-bench         : save in ABC's bench format to output.bench\n";
   helpstring +=  
@@ -359,8 +359,9 @@ int main(int argc, char ** argv) {
                }
              break;
            case 'j':
-             bm->UserFlags.print_cnf_flag = true;
-             bm->UserFlags.cnf_dump_filename = argv[++i];
+             // Used to output the CNF. No longer does.
+             //bm->UserFlags.print_cnf_flag = true;
+             //bm->UserFlags.cnf_dump_filename = argv[++i];
              break;
             case 'm':
               bm->UserFlags.smtlib1_parser_flag=true;