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

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 29d9ac7e0da7dd6eae6045abc90401c9bcbc1198..93f6fcfb30ff15b2215ae557541f5ba11b7636f2 100644 (file)
--- 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 5a91d716d36b4c5a8f4967fff64ac023bd9989c1..57d8c882e7a7f45365e484ef9cfc1970dfcac70d 100644 (file)
--- 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 79474e5d879d0fad5d74d304b5b2b4534a2fc15c..4f45428512b7c2cd5ae609057ce9b3c8406b1b41 100644 (file)
--- 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 <random_seed>       : 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 <random_seed>       : 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] == '-')