From: Christopher L. Conway Date: Fri, 22 Oct 2010 22:50:33 +0000 (+0000) Subject: Merging main/getopt.cpp, main/usage.h, and smt/options.h in X-Git-Tag: cvc5-1.0.0~8789 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a486cdde94366aa6b4a1f558eecc0130ba25ad5e;p=cvc5.git Merging main/getopt.cpp, main/usage.h, and smt/options.h in util/options.h,cpp --- 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 -#include -#include -#include -#include -#include -#include - -#include - -#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 #include +#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 #include -#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" diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index f503efae2..5851f3990 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -21,10 +21,10 @@ #include "sat.h" #include "theory/theory_engine.h" -#include "util/decision_engine.h" #include "util/Assert.h" +#include "util/decision_engine.h" +#include "util/options.h" #include "util/output.h" -#include "smt/options.h" #include "util/result.h" #include diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 1c7c506ee..ecef29ac2 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -24,9 +24,9 @@ #define __CVC4__PROP_ENGINE_H #include "expr/node.h" -#include "util/result.h" #include "util/decision_engine.h" -#include "smt/options.h" +#include "util/options.h" +#include "util/result.h" namespace CVC4 { diff --git a/src/prop/sat.h b/src/prop/sat.h index 17bf447f8..550de5527 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -25,9 +25,9 @@ // Optional blocks below will be unconditionally included #define __CVC4_USE_MINISAT -#include "util/stats.h" #include "theory/theory.h" -#include "smt/options.h" +#include "util/options.h" +#include "util/stats.h" #ifdef __CVC4_USE_MINISAT diff --git a/src/smt/options.h b/src/smt/options.h deleted file mode 100644 index 73c38545f..000000000 --- a/src/smt/options.h +++ /dev/null @@ -1,140 +0,0 @@ -/********************* */ -/*! \file options.h - ** \verbatim - ** Original author: mdeters - ** Major contributors: cconway - ** Minor contributors (to current version): dejan - ** 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 Global (command-line, set-option, ...) parameters for SMT. - ** - ** Global (command-line, set-option, ...) parameters for SMT. - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__OPTIONS_H -#define __CVC4__OPTIONS_H - -#ifdef CVC4_DEBUG -# define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true -#else /* CVC4_DEBUG */ -# define USE_EARLY_TYPE_CHECKING_BY_DEFAULT false -#endif /* CVC4_DEBUG */ - -#include -#include - -#include "util/language.h" - -namespace CVC4 { - -struct CVC4_PUBLIC Options { - - std::string binary_name; - - bool statistics; - - std::ostream *out; - std::ostream *err; - - /* -1 means no output */ - /* 0 is normal (and default) -- warnings only */ - /* 1 is warnings + notices so the user doesn't get too bored */ - /* 2 is chatty, giving statistical things etc. */ - /* with 3, the solver is slowed down by all the scrolling */ - int verbosity; - - /** The input language */ - InputLanguage inputLanguage; - - /** Enumeration of UF implementation choices */ - typedef enum { TIM, MORGAN } UfImplementation; - - /** Which implementation of uninterpreted function theory to use */ - UfImplementation uf_implementation; - - /** Should we exit after parsing? */ - bool parseOnly; - - /** Should the parser do semantic checks? */ - bool semanticChecks; - - /** Should the parser memory-map file input? */ - bool memoryMap; - - /** Should we strictly enforce the language standard while parsing? */ - bool strictParsing; - - /** Should we expand function definitions lazily? */ - bool lazyDefinitionExpansion; - - /** Whether we're in interactive mode or not */ - bool interactive; - - /** - * Whether we're in interactive mode (or not) due to explicit user - * setting (if false, we inferred the proper default setting). - */ - bool interactiveSetByUser; - - /** Whether we support SmtEngine::getValue() for this run. */ - bool produceModels; - - /** Whether we support SmtEngine::getAssignment() for this run. */ - bool produceAssignments; - - /** Whether we do typechecking at all. */ - bool typeChecking; - - /** Whether we do typechecking at Expr creation time. */ - bool earlyTypeChecking; - - Options() : - binary_name(), - statistics(false), - out(0), - err(0), - verbosity(0), - inputLanguage(language::input::LANG_AUTO), - uf_implementation(MORGAN), - parseOnly(false), - semanticChecks(true), - memoryMap(false), - strictParsing(false), - lazyDefinitionExpansion(false), - interactive(false), - interactiveSetByUser(false), - produceModels(false), - produceAssignments(false), - typeChecking(true), - earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT) { - } -};/* struct Options */ - -inline std::ostream& operator<<(std::ostream& out, - Options::UfImplementation uf) { - switch(uf) { - case Options::TIM: - out << "TIM"; - break; - case Options::MORGAN: - out << "MORGAN"; - break; - default: - out << "UfImplementation:UNKNOWN![" << unsigned(uf) << "]"; - } - - return out; -} - -}/* CVC4 namespace */ - -#undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT - -#endif /* __CVC4__OPTIONS_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 149c3620d..81930a5ea 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -20,22 +20,22 @@ #include #include -#include "smt/smt_engine.h" -#include "smt/modal_exception.h" -#include "smt/bad_option_exception.h" -#include "smt/no_such_function_exception.h" -#include "context/context.h" #include "context/cdlist.h" #include "context/cdset.h" -#include "expr/expr.h" +#include "context/context.h" #include "expr/command.h" +#include "expr/expr.h" #include "expr/node_builder.h" -#include "util/output.h" -#include "util/exception.h" -#include "smt/options.h" -#include "util/configuration.h" #include "prop/prop_engine.h" +#include "smt/bad_option_exception.h" +#include "smt/modal_exception.h" +#include "smt/no_such_function_exception.h" +#include "smt/smt_engine.h" #include "theory/theory_engine.h" +#include "util/configuration.h" +#include "util/exception.h" +#include "util/options.h" +#include "util/output.h" using namespace std; using namespace CVC4; diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 0831a0447..35bfb0bcc 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -23,19 +23,19 @@ #include -#include "expr/expr.h" -#include "expr/expr_manager.h" +#include "context/cdlist_forward.h" #include "context/cdmap_forward.h" #include "context/cdset_forward.h" -#include "context/cdlist_forward.h" -#include "util/result.h" -#include "util/model.h" -#include "util/sexpr.h" -#include "util/hash.h" +#include "expr/expr.h" +#include "expr/expr_manager.h" +#include "smt/bad_option_exception.h" #include "smt/modal_exception.h" #include "smt/no_such_function_exception.h" -#include "smt/options.h" -#include "smt/bad_option_exception.h" +#include "util/hash.h" +#include "util/model.h" +#include "util/options.h" +#include "util/result.h" +#include "util/sexpr.h" // In terms of abstraction, this is below (and provides services to) // ValidityChecker and above (and requires the services of) @@ -47,7 +47,7 @@ template class NodeTemplate; typedef NodeTemplate Node; typedef NodeTemplate TNode; class NodeHashFunction; -class Command; + class TheoryEngine; class DecisionEngine; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 2fcfc9626..40debc7c7 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -19,13 +19,13 @@ #include #include -#include "theory/theory_engine.h" -#include "expr/node.h" #include "expr/attribute.h" -#include "theory/theory.h" +#include "expr/node.h" #include "expr/node_builder.h" -#include "smt/options.h" +#include "util/options.h" +#include "theory/theory.h" +#include "theory/theory_engine.h" #include "theory/builtin/theory_builtin.h" #include "theory/booleans/theory_bool.h" #include "theory/uf/theory_uf.h" diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 0bca372ca..7e08a29d5 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -23,10 +23,10 @@ #include "expr/node.h" #include "prop/prop_engine.h" -#include "smt/options.h" #include "theory/shared_term_manager.h" #include "theory/theory.h" #include "theory/theoryof_table.h" +#include "util/options.h" #include "util/stats.h" namespace CVC4 { diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 61c0bf885..e75735f82 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -18,6 +18,8 @@ libutil_la_SOURCES = \ hash.h \ bool.h \ model.h \ + options.h \ + options.cpp \ output.cpp \ output.h \ result.h \ diff --git a/src/util/options.cpp b/src/util/options.cpp new file mode 100644 index 000000000..f6d3c3092 --- /dev/null +++ b/src/util/options.cpp @@ -0,0 +1,396 @@ +/********************* */ +/*! \file options.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 +#include +#include +#include +#include +#include +#include + +#include + +#include "expr/expr.h" +#include "util/configuration.h" +#include "util/exception.h" +#include "util/language.h" +#include "util/options.h" +#include "util/output.h" + +#include "cvc4autoconfig.h" + +using namespace std; +using namespace CVC4; + +namespace CVC4 { + +static const string optionsDescription = "\ + --lang | -L force input language (default is `auto'; see --lang help)\n\ + --version | -V identify this CVC4 binary\n\ + --help | -h this command line reference\n\ + --parse-only exit after parsing input\n\ + --mmap memory map file input\n\ + --show-config show CVC4 static configuration\n\ + --segv-nospin don't spin on segfault waiting for gdb\n\ + --lazy-type-checking type check expressions only when necessary (default)\n\ + --eager-type-checking type check expressions immediately on creation\n\ + --no-type-checking never type check expressions\n\ + --no-checking disable ALL semantic checks, including type checks \n\ + --strict-parsing fail on non-conformant inputs (SMT2 only)\n\ + --verbose | -v increase verbosity (repeatable)\n\ + --quiet | -q decrease verbosity (repeatable)\n\ + --trace | -t tracing for something (e.g. --trace pushpop)\n\ + --debug | -d debugging for something (e.g. --debug arith), implies -t\n\ + --stats give statistics on exit\n\ + --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\ + --print-expr-types print types with variables when printing exprs\n\ + --uf=morgan|tim select uninterpreted function theory implementation\n\ + --interactive run interactively\n\ + --no-interactive do not run interactively\n\ + --produce-models support the get-value command\n\ + --produce-assignments support the get-assignment command\n\ + --lazy-definition-expansion expand define-fun lazily\n"; + +static const string languageDescription = "\ +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\ +"; + +string Options::getDescription() const { + return optionsDescription; +} + +void Options::printUsage(const string msg, std::ostream& out) { + out << msg << optionsDescription << endl << flush; + // printf(usage + options.getDescription(), options.binary_name.c_str()); + // printf(usage, binary_name.c_str()); +} + +void Options::printLanguageHelp(std::ostream& out) { + out << languageDescription << flush; +} + +/** + * 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! */ + + +/** Parse argc/argv and put the result into a CVC4::Options struct. */ +int Options::parseOptions(int argc, char* argv[]) +throw(OptionException) { + const char *progName = argv[0]; + int c; + + // find the base name of the program + const char *x = strrchr(progName, '/'); + if(x != NULL) { + progName = x + 1; + } + 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': + help = true; + break; + // options.printUsage(usage); + // exit(1); + + case 'V': + version = true; + break; + // fputs(Configuration::about().c_str(), stdout); + // exit(0); + + case 'v': + ++verbosity; + break; + + case 'q': + --verbosity; + break; + + case 'L': + if(!strcmp(optarg, "cvc4") || !strcmp(optarg, "pl")) { + inputLanguage = language::input::LANG_CVC4; + break; + } else if(!strcmp(optarg, "smtlib") || !strcmp(optarg, "smt")) { + inputLanguage = language::input::LANG_SMTLIB; + break; + } else if(!strcmp(optarg, "smtlib2") || !strcmp(optarg, "smt2")) { + inputLanguage = language::input::LANG_SMTLIB_V2; + break; + } else if(!strcmp(optarg, "auto")) { + inputLanguage = language::input::LANG_AUTO; + break; + } + + if(strcmp(optarg, "help")) { + throw OptionException(string("unknown language for --lang: `") + + optarg + "'. Try --lang help."); + } + + languageHelp = true; + break; + + case 't': + Trace.on(optarg); + break; + + case 'd': + Debug.on(optarg); + Trace.on(optarg); + break; + + case STATS: + statistics = true; + break; + + case SEGV_NOSPIN: + segvNoSpin = true; + break; + + case PARSE_ONLY: + parseOnly = true; + break; + + case NO_CHECKING: + semanticChecks = false; + typeChecking = false; + earlyTypeChecking = false; + break; + + case USE_MMAP: + memoryMap = true; + break; + + case STRICT_PARSING: + 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")) { + uf_implementation = Options::TIM; + } else if(!strcmp(optarg, "morgan")) { + 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: + lazyDefinitionExpansion = true; + break; + + case INTERACTIVE: + interactive = true; + interactiveSetByUser = true; + break; + + case NO_INTERACTIVE: + interactive = false; + interactiveSetByUser = true; + break; + + case PRODUCE_MODELS: + produceModels = true; + break; + + case PRODUCE_ASSIGNMENTS: + produceAssignments = true; + break; + + case NO_TYPE_CHECKING: + typeChecking = false; + earlyTypeChecking = false; + break; + + case LAZY_TYPE_CHECKING: + earlyTypeChecking = false; + break; + + case EAGER_TYPE_CHECKING: + typeChecking = true; + 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 namespace */ diff --git a/src/util/options.h b/src/util/options.h new file mode 100644 index 000000000..b56741fba --- /dev/null +++ b/src/util/options.h @@ -0,0 +1,181 @@ +/********************* */ +/*! \file options.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: cconway + ** Minor contributors (to current version): dejan + ** 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 Global (command-line, set-option, ...) parameters for SMT. + ** + ** Global (command-line, set-option, ...) parameters for SMT. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__OPTIONS_H +#define __CVC4__OPTIONS_H + +#ifdef CVC4_DEBUG +# define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true +#else /* CVC4_DEBUG */ +# define USE_EARLY_TYPE_CHECKING_BY_DEFAULT false +#endif /* CVC4_DEBUG */ + +#include +#include + +#include "exception.h" +#include "language.h" + +namespace CVC4 { + +/** 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 */ + +struct CVC4_PUBLIC Options { + + std::string binary_name; + + bool statistics; + + std::istream& in; + std::ostream& out; + std::ostream& err; + + /* -1 means no output */ + /* 0 is normal (and default) -- warnings only */ + /* 1 is warnings + notices so the user doesn't get too bored */ + /* 2 is chatty, giving statistical things etc. */ + /* with 3, the solver is slowed down by all the scrolling */ + int verbosity; + + /** The input language */ + InputLanguage inputLanguage; + + /** Enumeration of UF implementation choices */ + typedef enum { TIM, MORGAN } UfImplementation; + + /** Which implementation of uninterpreted function theory to use */ + UfImplementation uf_implementation; + + /** Should we print the help message? */ + bool help; + + /** Should we print the release information? */ + bool version; + + /** Should we print the language help information? */ + bool languageHelp; + + /** Should we exit after parsing? */ + bool parseOnly; + + /** Should the parser do semantic checks? */ + bool semanticChecks; + + /** Should the parser memory-map file input? */ + bool memoryMap; + + /** Should we strictly enforce the language standard while parsing? */ + bool strictParsing; + + /** Should we expand function definitions lazily? */ + bool lazyDefinitionExpansion; + + /** Whether we're in interactive mode or not */ + bool interactive; + + /** + * Whether we're in interactive mode (or not) due to explicit user + * setting (if false, we inferred the proper default setting). + */ + bool interactiveSetByUser; + + /** Whether we should "spin" on a SIG_SEGV. */ + bool segvNoSpin; + + /** Whether we support SmtEngine::getValue() for this run. */ + bool produceModels; + + /** Whether we support SmtEngine::getAssignment() for this run. */ + bool produceAssignments; + + /** Whether we do typechecking at all. */ + bool typeChecking; + + /** Whether we do typechecking at Expr creation time. */ + bool earlyTypeChecking; + + Options() : + binary_name(), + statistics(false), + in(std::cin), + out(std::cout), + err(std::cerr), + verbosity(0), + inputLanguage(language::input::LANG_AUTO), + uf_implementation(MORGAN), + parseOnly(false), + semanticChecks(true), + memoryMap(false), + strictParsing(false), + lazyDefinitionExpansion(false), + interactive(false), + interactiveSetByUser(false), + segvNoSpin(false), + produceModels(false), + produceAssignments(false), + typeChecking(true), + earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT) { + } + + /** + * Get a description of the command-line flags accepted by + * parseOptions. The returned string will be escaped so that it is + * suitable as an argument to printf. */ + std::string getDescription() const; + + static void printUsage(const std::string msg, std::ostream& out); + static void printLanguageHelp(std::ostream& out); + + /** + * Initialize the options based on the given command-line arguments. + */ + int parseOptions(int argc, char* argv[]) + throw(OptionException); +};/* struct Options */ + +inline std::ostream& operator<<(std::ostream& out, + Options::UfImplementation uf) { + switch(uf) { + case Options::TIM: + out << "TIM"; + break; + case Options::MORGAN: + out << "MORGAN"; + break; + default: + out << "UfImplementation:UNKNOWN![" << unsigned(uf) << "]"; + } + + return out; +} + + + +}/* CVC4 namespace */ + +#undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT + +#endif /* __CVC4__OPTIONS_H */ diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index b340beb50..cee8a6a64 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -30,7 +30,6 @@ #include "prop/prop_engine.h" #include "prop/sat.h" #include "smt/smt_engine.h" -#include "smt/options.h" #include "util/decision_engine.h" using namespace CVC4; diff --git a/test/unit/theory/shared_term_manager_black.h b/test/unit/theory/shared_term_manager_black.h index 5007f43ed..7340f6ae7 100644 --- a/test/unit/theory/shared_term_manager_black.h +++ b/test/unit/theory/shared_term_manager_black.h @@ -31,7 +31,7 @@ #include "context/context.h" #include "util/rational.h" #include "util/integer.h" -#include "smt/options.h" +#include "util/options.h" #include "util/Assert.h" using namespace CVC4; @@ -51,7 +51,6 @@ class SharedTermManagerBlack : public CxxTest::TestSuite { NodeManager* d_nm; NodeManagerScope* d_scope; TheoryEngine* d_theoryEngine; - Options d_options; public: @@ -61,7 +60,8 @@ public: d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); - d_theoryEngine = new TheoryEngine(d_ctxt, d_options); + Options options; + d_theoryEngine = new TheoryEngine(d_ctxt, options); } void tearDown() { diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 00766ec90..bd6ec515b 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -35,7 +35,7 @@ #include "context/context.h" #include "util/rational.h" #include "util/integer.h" -#include "smt/options.h" +#include "util/options.h" #include "util/Assert.h" using namespace CVC4; @@ -227,7 +227,6 @@ class TheoryEngineWhite : public CxxTest::TestSuite { FakeOutputChannel *d_nullChannel; FakeTheory *d_builtin, *d_bool, *d_uf, *d_arith, *d_arrays, *d_bv; TheoryEngine* d_theoryEngine; - Options d_options; public: @@ -248,7 +247,8 @@ public: d_bv = new FakeTheory(d_ctxt, *d_nullChannel, "BV"); // create the TheoryEngine - d_theoryEngine = new TheoryEngine(d_ctxt, d_options); + Options options; + d_theoryEngine = new TheoryEngine(d_ctxt, options); // insert our fake versions into the TheoryEngine's theoryOf table d_theoryEngine->d_theoryOfTable.