From fcf0581eb91a97a7a4a1e2a3ecb89ddf8b954f13 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 22 Dec 2011 05:12:52 +0000 Subject: [PATCH] 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 --- src/AST/AST.h | 1 + src/AST/ASTmisc.cpp | 70 +++++++++++++++++- src/c_interface/c_interface.cpp | 69 +----------------- src/main/main.cpp | 124 ++++++++------------------------ 4 files changed, 101 insertions(+), 163 deletions(-) diff --git a/src/AST/AST.h b/src/AST/AST.h index 81ed69b..7930ff1 100644 --- 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 84c1da0..b92a283 100644 --- 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 93f6fcf..9f082c4 100644 --- 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 4f45428..771a16e 100644 --- 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 : 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" @@ -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) -- 2.47.3