diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-10-22 22:50:33 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-10-22 22:50:33 +0000 |
commit | a486cdde94366aa6b4a1f558eecc0130ba25ad5e (patch) | |
tree | 8931708b9046ec62c7bdd513de9de1e5a507aa53 /src/main | |
parent | 6dee1d9817d8e9209f0a681b7c601ec6b4b5014d (diff) |
Merging main/getopt.cpp, main/usage.h, and smt/options.h in
util/options.h,cpp
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/Makefile.am | 1 | ||||
-rw-r--r-- | src/main/getopt.cpp | 360 | ||||
-rw-r--r-- | src/main/main.cpp | 91 | ||||
-rw-r--r-- | src/main/main.h | 21 | ||||
-rw-r--r-- | src/main/util.cpp | 4 |
5 files changed, 71 insertions, 406 deletions
diff --git a/src/main/Makefile.am b/src/main/Makefile.am index b6cdbb1f4..05a451d52 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -6,7 +6,6 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas bin_PROGRAMS = cvc4 cvc4_SOURCES = \ - getopt.cpp \ interactive_shell.h \ interactive_shell.cpp \ main.h \ diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp deleted file mode 100644 index 25badb7e5..000000000 --- a/src/main/getopt.cpp +++ /dev/null @@ -1,360 +0,0 @@ -/********************* */ -/*! \file getopt.cpp - ** \verbatim - ** Original author: mdeters - ** Major contributors: cconway - ** Minor contributors (to current version): dejan, barrett - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Contains code for handling command-line options. - ** - ** Contains code for handling command-line options - **/ - -#include <cstdio> -#include <cstdlib> -#include <new> -#include <unistd.h> -#include <string.h> -#include <stdint.h> -#include <time.h> - -#include <getopt.h> - -#include "util/exception.h" -#include "util/configuration.h" -#include "util/output.h" -#include "smt/options.h" -#include "util/language.h" -#include "expr/expr.h" - -#include "cvc4autoconfig.h" -#include "main.h" -#include "usage.h" - -using namespace std; -using namespace CVC4; - -namespace CVC4 { -namespace main { - -static const char lang_help[] = "\ -Languages currently supported as arguments to the -L / --lang option:\n\ - auto attempt to automatically determine the input language\n\ - pl | cvc4 CVC4 presentation language\n\ - smt | smtlib SMT-LIB format 1.2\n\ - smt2 | smtlib2 SMT-LIB format 2.0\n\ -"; - -/** - * For the main getopt() routine, we need ways to switch on long - * options without clashing with short option characters. This is an - * enum of those long options. For long options (e.g. "--verbose") - * with a short option equivalent ("-v"), we use the single-letter - * short option; therefore, this enumeration starts at 256 to avoid - * any collision. - */ -enum OptionValue { - SMTCOMP = 256, /* no clash with char options */ - STATS, - SEGV_NOSPIN, - PARSE_ONLY, - NO_CHECKING, - USE_MMAP, - SHOW_CONFIG, - STRICT_PARSING, - DEFAULT_EXPR_DEPTH, - PRINT_EXPR_TYPES, - UF_THEORY, - LAZY_DEFINITION_EXPANSION, - INTERACTIVE, - NO_INTERACTIVE, - PRODUCE_MODELS, - PRODUCE_ASSIGNMENTS, - NO_TYPE_CHECKING, - LAZY_TYPE_CHECKING, - EAGER_TYPE_CHECKING, -};/* enum OptionValue */ - -/** - * This is a table of long options. By policy, each short option - * should have an equivalent long option (but the reverse isn't the - * case), so this table should thus contain all command-line options. - * - * Each option in this array has four elements: - * - * 1. the long option string - * 2. argument behavior for the option: - * no_argument - no argument permitted - * required_argument - an argument is expected - * optional_argument - an argument is permitted but not required - * 3. this is a pointer to an int which is set to the 4th entry of the - * array if the option is present; or NULL, in which case - * getopt_long() returns the 4th entry - * 4. the return value for getopt_long() when this long option (or the - * value to set the 3rd entry to; see #3) - * - * If you add something here, you should add it in src/main/usage.h - * also, to document it. - * - * If you add something that has a short option equivalent, you should - * add it to the getopt_long() call in parseOptions(). - */ -static struct option cmdlineOptions[] = { - // name, has_arg, *flag, val - { "verbose" , no_argument , NULL, 'v' }, - { "quiet" , no_argument , NULL, 'q' }, - { "debug" , required_argument, NULL, 'd' }, - { "trace" , required_argument, NULL, 't' }, - { "stats" , no_argument , NULL, STATS }, - { "no-checking", no_argument , NULL, NO_CHECKING }, - { "show-config", no_argument , NULL, SHOW_CONFIG }, - { "segv-nospin", no_argument , NULL, SEGV_NOSPIN }, - { "help" , no_argument , NULL, 'h' }, - { "version" , no_argument , NULL, 'V' }, - { "about" , no_argument , NULL, 'V' }, - { "lang" , required_argument, NULL, 'L' }, - { "parse-only" , no_argument , NULL, PARSE_ONLY }, - { "mmap" , no_argument , NULL, USE_MMAP }, - { "strict-parsing", no_argument , NULL, STRICT_PARSING }, - { "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH }, - { "print-expr-types", no_argument , NULL, PRINT_EXPR_TYPES }, - { "uf" , required_argument, NULL, UF_THEORY }, - { "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION }, - { "interactive", no_argument , NULL, INTERACTIVE }, - { "no-interactive", no_argument , NULL, NO_INTERACTIVE }, - { "produce-models", no_argument , NULL, PRODUCE_MODELS}, - { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS}, - { "no-type-checking", no_argument, NULL, NO_TYPE_CHECKING}, - { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING}, - { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING}, - { NULL , no_argument , NULL, '\0' } -};/* if you add things to the above, please remember to update usage.h! */ - -/** Full argv[0] */ -const char *progPath; - -/** Just the basename component of argv[0] */ -const char *progName; - -/** Parse argc/argv and put the result into a CVC4::Options struct. */ -int parseOptions(int argc, char* argv[], CVC4::Options* opts) -throw(OptionException) { - progPath = progName = argv[0]; - int c; - - // find the base name of the program - const char *x = strrchr(progName, '/'); - if(x != NULL) { - progName = x + 1; - } - opts->binary_name = string(progName); - - // The strange string in this call is the short option string. The - // initial '+' means that option processing stops as soon as a - // non-option argument is encountered. The initial ':' indicates - // that getopt_long() should return ':' instead of '?' for a missing - // option argument. Then, each letter is a valid short option for - // getopt_long(), and if it's encountered, getopt_long() returns - // that character. A ':' after an option character means an - // argument is required; two colons indicates an argument is - // optional; no colons indicate an argument is not permitted. - // cmdlineOptions specifies all the long-options and the return - // value for getopt_long() should they be encountered. - while((c = getopt_long(argc, argv, - "+:hVvqL:d:t:", - cmdlineOptions, NULL)) != -1) { - switch(c) { - - case 'h': - printf(usage, opts->binary_name.c_str()); - exit(1); - - case 'V': - fputs(Configuration::about().c_str(), stdout); - exit(0); - - case 'v': - ++opts->verbosity; - break; - - case 'q': - --opts->verbosity; - break; - - case 'L': - if(!strcmp(optarg, "cvc4") || !strcmp(optarg, "pl")) { - opts->inputLanguage = language::input::LANG_CVC4; - break; - } else if(!strcmp(optarg, "smtlib") || !strcmp(optarg, "smt")) { - opts->inputLanguage = language::input::LANG_SMTLIB; - break; - } else if(!strcmp(optarg, "smtlib2") || !strcmp(optarg, "smt2")) { - opts->inputLanguage = language::input::LANG_SMTLIB_V2; - break; - } else if(!strcmp(optarg, "auto")) { - opts->inputLanguage = language::input::LANG_AUTO; - break; - } - - if(strcmp(optarg, "help")) { - throw OptionException(string("unknown language for --lang: `") + - optarg + "'. Try --lang help."); - } - - fputs(lang_help, stdout); - exit(1); - - case 't': - Trace.on(optarg); - break; - - case 'd': - Debug.on(optarg); - Trace.on(optarg); - break; - - case STATS: - opts->statistics = true; - break; - - case SEGV_NOSPIN: - segvNoSpin = true; - break; - - case PARSE_ONLY: - opts->parseOnly = true; - break; - - case NO_CHECKING: - opts->semanticChecks = false; - opts->typeChecking = false; - opts->earlyTypeChecking = false; - break; - - case USE_MMAP: - opts->memoryMap = true; - break; - - case STRICT_PARSING: - opts->strictParsing = true; - break; - - case DEFAULT_EXPR_DEPTH: - { - int depth = atoi(optarg); - Debug.getStream() << Expr::setdepth(depth); - Trace.getStream() << Expr::setdepth(depth); - Notice.getStream() << Expr::setdepth(depth); - Chat.getStream() << Expr::setdepth(depth); - Message.getStream() << Expr::setdepth(depth); - Warning.getStream() << Expr::setdepth(depth); - } - break; - - case PRINT_EXPR_TYPES: - { - Debug.getStream() << Expr::printtypes(true); - Trace.getStream() << Expr::printtypes(true); - Notice.getStream() << Expr::printtypes(true); - Chat.getStream() << Expr::printtypes(true); - Message.getStream() << Expr::printtypes(true); - Warning.getStream() << Expr::printtypes(true); - } - break; - - case UF_THEORY: - { - if(!strcmp(optarg, "tim")) { - opts->uf_implementation = Options::TIM; - } else if(!strcmp(optarg, "morgan")) { - opts->uf_implementation = Options::MORGAN; - } else if(!strcmp(optarg, "help")) { - printf("UF implementations available:\n"); - printf("tim\n"); - printf("morgan\n"); - exit(1); - } else { - throw OptionException(string("unknown option for --uf: `") + - optarg + "'. Try --uf help."); - } - } - break; - - case LAZY_DEFINITION_EXPANSION: - opts->lazyDefinitionExpansion = true; - break; - - case INTERACTIVE: - opts->interactive = true; - opts->interactiveSetByUser = true; - break; - - case NO_INTERACTIVE: - opts->interactive = false; - opts->interactiveSetByUser = true; - break; - - case PRODUCE_MODELS: - opts->produceModels = true; - break; - - case PRODUCE_ASSIGNMENTS: - opts->produceAssignments = true; - break; - - case NO_TYPE_CHECKING: - opts->typeChecking = false; - opts->earlyTypeChecking = false; - break; - - case LAZY_TYPE_CHECKING: - opts->earlyTypeChecking = false; - break; - - case EAGER_TYPE_CHECKING: - opts->typeChecking = true; - opts->earlyTypeChecking = true; - break; - - case SHOW_CONFIG: - fputs(Configuration::about().c_str(), stdout); - printf("\n"); - printf("version : %s\n", Configuration::getVersionString().c_str()); - printf("\n"); - printf("library : %u.%u.%u\n", - Configuration::getVersionMajor(), - Configuration::getVersionMinor(), - Configuration::getVersionRelease()); - printf("\n"); - printf("debug code : %s\n", Configuration::isDebugBuild() ? "yes" : "no"); - printf("tracing : %s\n", Configuration::isTracingBuild() ? "yes" : "no"); - printf("muzzled : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no"); - printf("assertions : %s\n", Configuration::isAssertionBuild() ? "yes" : "no"); - printf("coverage : %s\n", Configuration::isCoverageBuild() ? "yes" : "no"); - printf("profiling : %s\n", Configuration::isProfilingBuild() ? "yes" : "no"); - printf("competition: %s\n", Configuration::isCompetitionBuild() ? "yes" : "no"); - exit(0); - - case '?': - throw OptionException(string("can't understand option `") + argv[optind - 1] + "'"); - - case ':': - throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument"); - - default: - throw OptionException(string("can't understand option:") + argv[optind - 1] + "'"); - } - - } - - return optind; -} - -}/* CVC4::main namespace */ -}/* CVC4 namespace */ diff --git a/src/main/main.cpp b/src/main/main.cpp index 8ed938351..544c6fd29 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -28,7 +28,6 @@ #include "cvc4autoconfig.h" #include "main.h" #include "interactive_shell.h" -#include "usage.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "parser/parser_exception.h" @@ -37,8 +36,8 @@ #include "expr/command.h" #include "util/Assert.h" #include "util/configuration.h" +#include "util/options.h" #include "util/output.h" -#include "smt/options.h" #include "util/result.h" #include "util/stats.h" @@ -47,14 +46,41 @@ using namespace CVC4; using namespace CVC4::parser; using namespace CVC4::main; -namespace CVC4 { - namespace main { - struct Options options; - }/* CVC4::main namespace */ -}/* CVC4 namespace */ - int runCvc4(int argc, char* argv[]); void doCommand(SmtEngine&, Command*); +void printUsage(); + +namespace CVC4 { + namespace main {/* Global options variable */ + Options options; + + /** Full argv[0] */ + const char *progPath; + + /** Just the basename component of argv[0] */ + const char *progName; + } +} + + +// no more % chars in here without being escaped; it's used as a +// printf() format string +const string usageMessage = "\ +usage: %s [options] [input-file]\n\ +\n\ +Without an input file, or with `-', CVC4 reads from standard input.\n\ +\n\ +CVC4 options:\n"; + +void printUsage() { + stringstream ss; + ss << "usage: " << options.binary_name << " [options] [input-file]" << endl + << endl + << "Without an input file, or with `-', CVC4 reads from standard input." << endl + << endl + << "CVC4 options:" << endl; + Options::printUsage( ss.str(), options.out ); +} /** * CVC4's main() routine is just an exception-safe wrapper around CVC4. @@ -68,34 +94,34 @@ int main(int argc, char* argv[]) { return runCvc4(argc, argv); } catch(OptionException& e) { #ifdef CVC4_COMPETITION_MODE - cout << "unknown" << endl; + options.out << "unknown" << endl; #endif cerr << "CVC4 Error:" << endl << e << endl; - printf(usage, options.binary_name.c_str()); + printUsage(); exit(1); } catch(Exception& e) { #ifdef CVC4_COMPETITION_MODE - cout << "unknown" << endl; + options.out << "unknown" << endl; #endif - cerr << "CVC4 Error:" << endl << e << endl; + options.err << "CVC4 Error:" << endl << e << endl; if(options.statistics) { - StatisticsRegistry::flushStatistics(cerr); + StatisticsRegistry::flushStatistics(options.err); } exit(1); } catch(bad_alloc) { #ifdef CVC4_COMPETITION_MODE - cout << "unknown" << endl; + options.out << "unknown" << endl; #endif - cerr << "CVC4 ran out of memory." << endl; + options.err << "CVC4 ran out of memory." << endl; if(options.statistics) { - StatisticsRegistry::flushStatistics(cerr); + StatisticsRegistry::flushStatistics(options.err); } exit(1); } catch(...) { #ifdef CVC4_COMPETITION_MODE - cout << "unknown" << endl; + options.out << "unknown" << endl; #endif - cerr << "CVC4 threw an exception of unknown type." << endl; + options.err << "CVC4 threw an exception of unknown type." << endl; exit(1); } } @@ -106,12 +132,29 @@ int runCvc4(int argc, char* argv[]) { // Initialize the signal handlers cvc4_init(); + progPath = argv[0]; + // Parse the options - int firstArgIndex = parseOptions(argc, argv, &options); + int firstArgIndex = options.parseOptions(argc, argv); + + progName = options.binary_name.c_str(); + + if( options.help ) { + printUsage(); + exit(1); + } else if( options.languageHelp ) { + Options::printLanguageHelp(options.out); + exit(1); + } else if( options.version ) { + options.out << Configuration::about().c_str() << flush; + exit(0); + } + + segvNoSpin = options.segvNoSpin; // If in competition mode, set output stream option to flush immediately #ifdef CVC4_COMPETITION_MODE - cout << unitbuf; + options.out << unitbuf; #endif // We only accept one input file @@ -201,7 +244,7 @@ int runCvc4(int argc, char* argv[]) { // Parse and execute commands until we are done Command* cmd; if( options.interactive ) { - InteractiveShell shell(cin,cout,parserBuilder); + InteractiveShell shell(options.in,options.out,parserBuilder); while((cmd = shell.readCommand())) { doCommand(smt,cmd); delete cmd; @@ -237,7 +280,7 @@ int runCvc4(int argc, char* argv[]) { StatisticsRegistry::registerStat(&s_statSatResult); if(options.statistics) { - StatisticsRegistry::flushStatistics(cerr); + StatisticsRegistry::flushStatistics(options.err); } StatisticsRegistry::unregisterStat(&s_statSatResult); @@ -261,11 +304,11 @@ void doCommand(SmtEngine& smt, Command* cmd) { } } else { if(options.verbosity > 0) { - cout << "Invoking: " << *cmd << endl; + options.out << "Invoking: " << *cmd << endl; } if(options.verbosity >= 0) { - cmd->invoke(&smt, cout); + cmd->invoke(&smt, options.out); } else { cmd->invoke(&smt); } diff --git a/src/main/main.h b/src/main/main.h index 350578ffa..b6a8bcfb1 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -19,26 +19,16 @@ #include <exception> #include <string> +#include "util/options.h" #include "cvc4autoconfig.h" -#include "util/exception.h" #ifndef __CVC4__MAIN__MAIN_H #define __CVC4__MAIN__MAIN_H namespace CVC4 { -struct Options; - namespace main { -/** Class representing an option-parsing exception. */ -class OptionException : public CVC4::Exception { -public: - OptionException(const std::string& s) throw() : - CVC4::Exception("Error in option parsing: " + s) { - } -};/* class OptionException */ - /** Full argv[0] */ extern const char *progPath; @@ -52,14 +42,7 @@ extern const char *progName; */ extern bool segvNoSpin; -/** - * Keep a copy of the options around globally, so that signal handlers can - * access it. - */ -extern struct Options options; - -/** Parse argc/argv and put the result into a CVC4::Options struct. */ -int parseOptions(int argc, char** argv, CVC4::Options*) throw(OptionException); +extern Options options; /** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. */ void cvc4_init() throw(); diff --git a/src/main/util.cpp b/src/main/util.cpp index 70cb85c93..4ec1c1bee 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -23,9 +23,9 @@ #include <string.h> #include <signal.h> -#include "util/exception.h" -#include "smt/options.h" #include "util/Assert.h" +#include "util/exception.h" +#include "util/options.h" #include "util/stats.h" #include "cvc4autoconfig.h" |