Cleanup some of the command line parsing.

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

diff --git a/src/AST/AST.h b/src/AST/AST.h
index 81ed69b2007f0c4d287883d500530399bdab64ae..7930ff1ddcaec2e5620747dcd46f687a909d0598 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -18,6 +18,7 @@
 
 namespace BEEV
 {
+  void process_argument(const char ch, STPMgr  *bm);
   void FatalError(const char * str, const ASTNode& a, int w = 0) __attribute__ ((noreturn));
   void FatalError(const char * str) __attribute__ ((noreturn));
   void SortByExprNum(ASTVec& c);

diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp
index 84c1da06b0e3818a8f623633cc85b1d3ba668c19..b92a28353b77a930eca6bd5b7e4de1fd743ae9c9 100644 (file)
--- a/src/AST/ASTmisc.cpp
+++ b/src/AST/ASTmisc.cpp
@@ -1,6 +1,6 @@
 // -*- c++ -*-
 /********************************************************************
- * AUTHORS: Vijay Ganesh
+ * AUTHORS: Vijay Ganesh, Trevor Hansen
  *
  * BEGIN DATE: November, 2005
  *
@@ -8,6 +8,7 @@
  ********************************************************************/
 
 #include "AST.h"
+#include "../STPManager/STPManager.h"
 
 namespace BEEV
 {
@@ -16,6 +17,73 @@ namespace BEEV
    * Universal Helper Functions                                   *
    ****************************************************************/
 
+  void process_argument(const char ch, STPMgr  *bm)
+  {
+    switch(ch)
+        {
+        case 'a' :
+          bm->UserFlags.optimize_flag = false;
+          break;
+        case 'c':
+          bm->UserFlags.construct_counterexample_flag = true;
+          break;
+        case 'd':
+          bm->UserFlags.construct_counterexample_flag = true;
+          bm->UserFlags.check_counterexample_flag = true;
+          break;
+
+        case 'h':
+          fprintf(stderr,usage,prog);
+          cout << helpstring;
+          exit(-1);
+          break;
+        case 'm':
+          bm->UserFlags.smtlib1_parser_flag=true;
+          bm->UserFlags.division_by_zero_returns_one_flag = true;
+                      if (bm->UserFlags.smtlib2_parser_flag)
+                              FatalError("Can't use both the smtlib and smtlib2 parsers");
+          break;
+        case 'n':
+          bm->UserFlags.print_output_flag = true;
+          break;
+        case 'p':
+          bm->UserFlags.print_counterexample_flag = true;
+          break;
+        case 'q':
+          bm->UserFlags.print_arrayval_declaredorder_flag = true;
+          break;
+        case 'r':
+          bm->UserFlags.arrayread_refinement_flag = false;
+          break;
+        case 's' :
+          bm->UserFlags.stats_flag = true;
+          break;
+        case 't':
+          bm->UserFlags.quick_statistics_flag = true;
+          break;
+        case 'v' :
+          bm->UserFlags.print_nodes_flag = true;
+          break;
+        case 'w':
+          bm->UserFlags.wordlevel_solve_flag = false;
+          break;
+        case 'x':
+          bm->UserFlags.xor_flatten_flag = true;
+          break;
+        case 'y':
+          bm->UserFlags.print_binary_flag = true;
+          break;
+        case 'z':
+          bm->UserFlags.print_sat_varorder_flag = true;
+          break;
+        default:
+          fprintf(stderr,usage,prog);
+          cout << helpstring;
+          exit(-1);
+          break;
+        }
+  }
+
   // Sort ASTNodes by expression numbers
   bool exprless(const ASTNode n1, const ASTNode n2)
   {

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 93f6fcfb30ff15b2215ae557541f5ba11b7636f2..9f082c45295711903c87ad893ad9cbb195d05fd2 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -40,74 +40,7 @@ extern int smtparse(void*);
 
 void vc_setFlags(VC vc, char c, int param_value) {
   bmstar b = (bmstar)(((stpstar)vc)->bm);
-
-
-  switch(c) {
-  case 'a' :
-    b->UserFlags.optimize_flag = false;
-    break;
-  case 'c':
-    b->UserFlags.construct_counterexample_flag = true;
-    break;
-  case 'd':
-    b->UserFlags.construct_counterexample_flag = true;
-    b->UserFlags.check_counterexample_flag = true;
-    break;
-  case 'h':
-    fprintf(stderr,BEEV::usage,BEEV::prog);
-    //cout << helpstring;
-    //FatalError("");
-    //return -1;
-    break;
-  case 'i':
-    b->UserFlags.random_seed_flag = true;
-    b->UserFlags.random_seed = param_value;
-    break;
-  case 'n':
-    b->UserFlags.print_output_flag = true;
-    break;
-  case 'm':
-    b->UserFlags.smtlib1_parser_flag=true;
-    b->UserFlags.division_by_zero_returns_one_flag = true;
-    break;
-  case 'p':
-    b->UserFlags.print_counterexample_flag = true;
-    break;
-  case 'q':
-    b->UserFlags.print_arrayval_declaredorder_flag = true;
-    break;
-  case 'r':
-    b->UserFlags.arrayread_refinement_flag = false;
-    break;
-  case 's' :
-    b->UserFlags.stats_flag = true;
-    break;
-  case 'u':
-    //b->UserFlags.arraywrite_refinement_flag = false;
-    break;
-  case 'v' :
-    b->UserFlags.print_nodes_flag = true;
-    break;
-  case 'w':
-    b->UserFlags.wordlevel_solve_flag = false;
-    break;
-  case 'x':
-    b->UserFlags.xor_flatten_flag = true;
-    break;
-  case 'y':
-    b->UserFlags.print_binary_flag = true;
-    break;
-  case 'z':
-    b->UserFlags.print_sat_varorder_flag = true;
-    break;
-  default:
-    std::string s = 
-      "C_interface: "                                                   \
-      "vc_setFlags: Unrecognized commandline flag:\n";
-    //s += helpstring;
-    BEEV::FatalError(s.c_str());
-    break;
-  }
+  process_argument(c, b);
 }
 
 void vc_setInterfaceFlags(VC vc, enum ifaceflag_t f, int param_value) {

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 4f45428512b7c2cd5ae609057ce9b3c8406b1b41..771a16eceb84dcd90a768cb6d178e3c1a364969a 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -80,6 +80,7 @@ static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000;
 
 typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB2,PRINT_BACK_SMTLIB1, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER, SMT_LIB2_FORMAT, SMT_LIB1_FORMAT, DISABLE_CBITP,EXIT_AFTER_CNF,USE_CRYPTOMINISAT_SOLVER,USE_MINISAT_SOLVER, DISABLE_SIMPLIFICATIONS, OLDSTYLE_REFINEMENT} OptionType;
 
+
 int main(int argc, char ** argv) {
   char * infile = NULL;
   extern FILE *cvcin;
@@ -149,7 +150,7 @@ int main(int argc, char ** argv) {
     "--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"
+    "-g <time_in_sec>       : 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"
@@ -297,99 +298,34 @@ int main(int argc, char ** argv) {
               cout << helpstring;
               return -1;
             }
-          switch(argv[i][1])
-            {
-            case 'a' :
-              bm->UserFlags.optimize_flag = false;
-              break;
-            case 'b':
-              onePrintBack = true;
-              bm->UserFlags.print_STPinput_back_flag = true;
-              break;
-            case 'c':
-              bm->UserFlags.construct_counterexample_flag = true;
-              break;
-            case 'd':
-              bm->UserFlags.construct_counterexample_flag = true;
-              bm->UserFlags.check_counterexample_flag = true;
-              break;
-            case 'g':
-              signal(SIGVTALRM, handle_time_out);
-              timeout.it_interval.tv_usec = 0;
-              timeout.it_interval.tv_sec  = 0;
-              timeout.it_value.tv_usec    = 0;
-              timeout.it_value.tv_sec     = atoi(argv[++i]);
-              setitimer(ITIMER_VIRTUAL, &timeout, NULL);
-              break;
-            case 'h':
-              fprintf(stderr,usage,prog);
-              cout << helpstring;
-              return -1;
-              break;
-           case 'i':
-             bm->UserFlags.random_seed_flag = true;
-              bm->UserFlags.random_seed = atoi(argv[++i]);
-             //cerr << "Random seed is: " << bm->UserFlags.random_seed << endl;
-             if(!(0 <= bm->UserFlags.random_seed))
-               {
-                 FatalError("Random Seed should be an integer >= 0\n");
-               }
-             break;
-           case 'j':
-             // 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;
-              bm->UserFlags.division_by_zero_returns_one_flag = true;
-                         if (bm->UserFlags.smtlib2_parser_flag)
-                                 FatalError("Can't use both the smtlib and smtlib2 parsers");
-
-              break;
-            case 'n':
-              bm->UserFlags.print_output_flag = true;
-              break;
-            case 'p':
-              bm->UserFlags.print_counterexample_flag = true;
-              break;
-            case 'q':
-              bm->UserFlags.print_arrayval_declaredorder_flag = true;
-              break;
-            case 'r':
-              bm->UserFlags.arrayread_refinement_flag = false;
-              break;
-            case 's' :
-              bm->UserFlags.stats_flag = true;
-              break;
-            case 't':
-              bm->UserFlags.quick_statistics_flag = true;
-              break;
-            case 'u':
-              //bm->UserFlags.arraywrite_refinement_flag = false;
-              break;
-            case 'v' :
-              bm->UserFlags.print_nodes_flag = true;
-              break;
-            case 'w':
-              bm->UserFlags.wordlevel_solve_flag = false;
-              break;
-            case 'x':
-              bm->UserFlags.xor_flatten_flag = true;
-              break;
-            case 'y':
-              bm->UserFlags.print_binary_flag = true;
-              break;            
-            case 'z':
-              bm->UserFlags.print_sat_varorder_flag = true;
-              break;
-            default:
-              fprintf(stderr,usage,prog);
-              cout << helpstring;
-              //FatalError("");
-              return -1;
-              break;
-            }
+
+      if (argv[i][1] == 'g')
+        {
+        signal(SIGVTALRM, handle_time_out);
+        timeout.it_interval.tv_usec = 0;
+        timeout.it_interval.tv_sec  = 0;
+        timeout.it_value.tv_usec    = 0;
+        timeout.it_value.tv_sec     = atoi(argv[++i]);
+        setitimer(ITIMER_VIRTUAL, &timeout, NULL);
+        }
+      else if (argv[i][1] == 'i')
+        {
+        bm->UserFlags.random_seed_flag = true;
+        bm->UserFlags.random_seed = atoi(argv[++i]);
+        //cerr << "Random seed is: " << bm->UserFlags.random_seed << endl;
+        if(!(0 <= bm->UserFlags.random_seed))
+          {
+            FatalError("Random Seed should be an integer >= 0\n");
+          }
+        }
+      else if (argv[i][1] == 'b')
+        {
+          onePrintBack = true;
+          bm->UserFlags.print_STPinput_back_flag = true;
+        }
+      else
+         process_argument(argv[i][1],bm);
+
         }
         } else {          
                if (NULL != infile)