From e01c2678f710c149d44b5c2b188b3255a6e6a240 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 22 Dec 2011 04:47:32 +0000 Subject: [PATCH] Cleanup how the command line arguments are printed. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1442 e59a4935-1847-0410-ae03-e826735625c1 --- src/c_interface/c_interface.cpp | 36 +---------- src/main/Globals.cpp | 2 +- src/main/main.cpp | 105 ++++++++++++-------------------- 3 files changed, 44 insertions(+), 99 deletions(-) diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index 29d9ac7..93f6fcf 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -41,37 +41,7 @@ extern int smtparse(void*); void vc_setFlags(VC vc, char c, int param_value) { bmstar b = (bmstar)(((stpstar)vc)->bm); - std::string helpstring = - "Usage: stp [-option] [infile]\n\n"; - helpstring += - "STP version: " + BEEV::version + "\n\n"; - helpstring += - "-a : switch optimizations off (optimizations are ON by default)\n"; - helpstring += - "-c : construct counterexample\n"; - helpstring += - "-d : check counterexample\n"; - helpstring += - "-f : number of abstraction-refinement loops\n"; - helpstring += - "-h : help\n"; - helpstring += - "-m : use the SMTLIB parser\n"; - helpstring += - "-p : print counterexample\n"; - helpstring += - "-r : switch refinement off (optimizations are ON by default)\n"; - helpstring += - "-s : print function statistics\n"; - helpstring += - "-v : print nodes \n"; - helpstring += - "-w : switch wordlevel solver off (optimizations are ON by default)\n"; - helpstring += - "-x : flatten nested XORs\n"; - helpstring += - "-y : print counterexample in binary\n"; - + switch(c) { case 'a' : b->UserFlags.optimize_flag = false; @@ -85,7 +55,7 @@ void vc_setFlags(VC vc, char c, int param_value) { break; case 'h': fprintf(stderr,BEEV::usage,BEEV::prog); - cout << helpstring; + //cout << helpstring; //FatalError(""); //return -1; break; @@ -134,7 +104,7 @@ void vc_setFlags(VC vc, char c, int param_value) { std::string s = "C_interface: " \ "vc_setFlags: Unrecognized commandline flag:\n"; - s += helpstring; + //s += helpstring; BEEV::FatalError(s.c_str()); break; } diff --git a/src/main/Globals.cpp b/src/main/Globals.cpp index 5a91d71..57d8c88 100644 --- a/src/main/Globals.cpp +++ b/src/main/Globals.cpp @@ -34,5 +34,5 @@ namespace BEEV const char * prog = "stp"; int linenum = 1; const char * usage = "Usage: %s [-option] [infile]\n"; - std::string helpstring = "\n\n"; + std::string helpstring = "\n"; }; //end of namespace BEEV diff --git a/src/main/main.cpp b/src/main/main.cpp index 79474e5..4f45428 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -1,6 +1,6 @@ /******************************************************************** - * AUTHORS: Vijay Ganesh + * AUTHORS: Vijay Ganesh, Trevor Hansen * * BEGIN DATE: November, 2005 * @@ -121,72 +121,47 @@ int main(int argc, char ** argv) { //populate the help string helpstring += - "STP version : " + version + "\n\n"; - helpstring += - "-a : disable potentially size-increasing optimisations\n"; - helpstring += - "-b : print STP input back to cout\n"; - //helpstring += - // "-c : construct counterexample\n"; - helpstring += - "--cryptominisat : use cryptominisat2 as the solver\n"; - //helpstring += - // "-d : check counterexample\n"; - helpstring += - "--disable-cbitp : disable constant bit propagation\n"; - helpstring += - "--disable-simplify : disable all simplifications\n"; - helpstring += - "--exit-after-CNF : exit after the CNF has been generated\n"; - helpstring += - "-g : timeout (seconds until STP gives up)\n"; - helpstring += - "-h : help\n"; - helpstring += - "-i : Randomize STP's satisfiable output. Random_seed is an integer >= 0.\n"; - helpstring += - "-m : use the SMTLIB1 parser\n"; - helpstring += - "--minisat : use minisat 2.2 as the solver\n"; - helpstring += - "--oldstyle-refinement : Do abstraction-refinement outside the SAT solver.\n"; - helpstring += - "--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 += - "-p : print counterexample\n"; - helpstring += - "--print-back-CVC : print input in CVC format, then exit\n"; - helpstring += - "--print-back-SMTLIB2 : print input in SMT-LIB2 format, then exit\n"; - helpstring += - "--print-back-SMTLIB1 : print input in SMT-LIB1 format, then exit\n"; - helpstring += - "--print-back-GDL : print AiSee's graph format, then exit\n"; - helpstring += - "--print-back-dot : print dotty/neato's graph format, then exit\n"; - helpstring += - "-r : turn of abstraction-refinement of arrays.\n"; - helpstring += - "-s : print function statistics\n"; - helpstring += - "--simplifying-minisat : use simplifying-minisat 2.2 as the solver\n"; - helpstring += - "--SMTLIB1 : use the SMT-LIB1 format parser\n"; - helpstring += - "--SMTLIB2 : use the SMT-LIB2 format parser\n"; - helpstring += - "-t : print quick statistics\n"; - helpstring += - "-v : print nodes \n"; - helpstring += - "-w : switch wordlevel solver off (optimizations are ON by default)\n"; - //helpstring += - // "-x : flatten nested XORs\n"; - helpstring += + "STP version : " + version + "\n" + "--disable-simplify : disable all simplifications\n" + "-w : switch wordlevel solver off (optimizations are ON by default)\n" + "-a : disable potentially size-increasing optimisations\n" + "--disable-cbitp : disable constant bit propagation\n" + "\n" + "--cryptominisat : use cryptominisat2 as the solver\n" + "--simplifying-minisat : use simplifying-minisat 2.2 as the solver\n" + "--minisat : use minisat 2.2 as the solver\n" + "\n" + "--oldstyle-refinement : Do abstraction-refinement outside the SAT solver\n" + "-r : Eagerly encode array-read axioms (Ackermannistaion)\n" + "\n" + "-b : print STP input back to cout\n" + "--print-back-CVC : print input in CVC format, then exit\n" + "--print-back-SMTLIB2 : print input in SMT-LIB2 format, then exit\n" + "--print-back-SMTLIB1 : print input in SMT-LIB1 format, then exit\n" + "--print-back-GDL : print AiSee's graph format, then exit\n" + "--print-back-dot : print dotty/neato's graph format, then exit\n" + "\n" + "-m : use the SMTLIB1 parser\n" + "--SMTLIB1 : use the SMT-LIB1 format parser\n" + "--SMTLIB2 : use the SMT-LIB2 format parser\n" + "\n" + "--output-CNF : save the CNF into output_[0..n].cnf\n" + "--output-bench : save in ABC's bench format to output.bench\n" + "\n" + "--exit-after-CNF : exit after the CNF has been generated\n" + "-g : timeout (seconds until STP gives up)\n" + "-h : help\n" + "-i : Randomize STP's satisfiable output. Random_seed is an integer >= 0\n" + "-p : print counterexample\n" + "-s : print function statistics\n" + "-t : print quick statistics\n" + "-v : print nodes \n" "-y : print counterexample in binary\n"; + // "-x : flatten nested XORs\n" + // "-c : construct counterexample\n" + // "-d : check counterexample\n" + for(int i=1; i < argc;i++) { if(argv[i][0] == '-') -- 2.47.3