bin_PROGRAMS = cvc4
cvc4_SOURCES = \
- getopt.cpp \
interactive_shell.h \
interactive_shell.cpp \
main.h \
+++ /dev/null
-/********************* */
-/*! \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 */
#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"
#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"
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.
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);
}
}
// 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
// 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;
StatisticsRegistry::registerStat(&s_statSatResult);
if(options.statistics) {
- StatisticsRegistry::flushStatistics(cerr);
+ StatisticsRegistry::flushStatistics(options.err);
}
StatisticsRegistry::unregisterStat(&s_statSatResult);
}
} 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);
}
#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;
*/
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();
#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"
#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 <utility>
#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 {
// 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
+++ /dev/null
-/********************* */
-/*! \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 <iostream>
-#include <string>
-
-#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 */
#include <string>
#include <sstream>
-#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;
#include <vector>
-#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)
typedef NodeTemplate<true> Node;
typedef NodeTemplate<false> TNode;
class NodeHashFunction;
-class Command;
+
class TheoryEngine;
class DecisionEngine;
#include <vector>
#include <list>
-#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"
#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 {
hash.h \
bool.h \
model.h \
+ options.h \
+ options.cpp \
output.cpp \
output.h \
result.h \
--- /dev/null
+/********************* */
+/*! \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 <cstdio>
+#include <cstdlib>
+#include <new>
+#include <unistd.h>
+#include <string.h>
+#include <stdint.h>
+#include <time.h>
+
+#include <getopt.h>
+
+#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 */
--- /dev/null
+/********************* */
+/*! \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 <iostream>
+#include <string>
+
+#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 */
#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;
#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;
NodeManager* d_nm;
NodeManagerScope* d_scope;
TheoryEngine* d_theoryEngine;
- Options d_options;
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() {
#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;
FakeOutputChannel *d_nullChannel;
FakeTheory *d_builtin, *d_bool, *d_uf, *d_arith, *d_arrays, *d_bv;
TheoryEngine* d_theoryEngine;
- Options d_options;
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.
projects / cvc5.git / commitdiff