From f21cd8fa3bd1baef9e85e53edd27652273d59e00 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 19 Jan 2011 06:03:03 +0000 Subject: [PATCH] Fix. remove the -j option. Which did nothing. It used to output a CNF from the contents of cryptominisat's insides. Not from the other solvers. 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 | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/main/main.cpp b/src/main/main.cpp index e3c2e03..e431b16 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -139,15 +139,15 @@ int main(int argc, char ** argv) { "-h : help\n"; helpstring += "-i : Randomize STP's satisfiable output. Random_seed is an integer >= 0.\n"; - helpstring += - "-j : CNF Dumping. Creates a DIMACS equivalent file of the input STP file\n"; + //helpstring += + // "-j : 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; -- 2.47.3