From 394791604a62e19763a8a45328bc5177d91fabf9 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 18 Nov 2009 22:02:11 +0000 Subject: [PATCH] work on exprs, driver, util --- configure.ac | 56 +++++++++++++++- contrib/update-copyright.pl | 29 +++++--- src/expr/attr_type.h | 2 +- src/expr/expr.cpp | 10 +-- src/expr/expr_attribute.h | 6 +- src/expr/expr_builder.cpp | 77 +++++++++++++++++++--- src/expr/expr_builder.h | 12 +++- src/expr/expr_manager.cpp | 6 +- src/expr/expr_manager.h | 2 +- src/expr/expr_value.cpp | 2 +- src/expr/expr_value.h | 4 ++ src/include/cvc4_expr.h | 9 ++- src/main/Makefile.am | 7 +- src/main/about.h | 17 +++++ src/main/getopt.cpp | 128 ++++++++++++++++++++++++++++++++++++ src/main/main.cpp | 68 +++++++++++++++++++ src/main/main.h | 26 ++++++++ src/main/usage.h | 29 ++++++++ src/main/util.cpp | 44 +++++++++++++ src/util/options.h | 31 +++++++++ 20 files changed, 518 insertions(+), 47 deletions(-) create mode 100644 src/main/about.h create mode 100644 src/main/getopt.cpp create mode 100644 src/main/main.cpp create mode 100644 src/main/main.h create mode 100644 src/main/usage.h create mode 100644 src/main/util.cpp create mode 100644 src/util/options.h diff --git a/configure.ac b/configure.ac index 58fcdfac3..77c03ef2c 100644 --- a/configure.ac +++ b/configure.ac @@ -12,6 +12,25 @@ LT_INIT AC_LIBTOOL_WIN32_DLL +# Features requested by the user +AC_MSG_CHECKING([whether to do a debug build of CVC4]) +AC_ARG_ENABLE([debug], [AS_HELP_STRING([--enable-debug] ,[do a debug build of CVC4])]) +if test -z "${enable_debug+set}"; then + enable_debug=no +fi +AC_MSG_RESULT([$enable_debug]) + +AC_MSG_CHECKING([whether to include assertions in build]) +AC_ARG_ENABLE([assertions], [AS_HELP_STRING([--disable-assertions],[turn off assertions in build])]) +if test -z "${enable_assertions+set}"; then + enable_assertions=yes +fi +AC_MSG_RESULT([$enable_assertions]) + +if test "$enable_assertions" = no -a "$enable_debug" = yes; then + AC_MSG_FAILURE([when debugging is on, so must assertions be.]) +fi + # Checks for programs. AC_PROG_CC AC_PROG_CXX @@ -20,15 +39,16 @@ AC_PROG_LIBTOOL AM_PROG_LEX AC_PROG_YACC -AC_CHECK_PROG(DOXYGEN, doxygen, doxygen,) -if test "$DOXYGEN" = ''; then - echo 'WARNING: documentation targets require doxygen. Set your PATH appropriately or set DOXYGEN to point to a valid doxygen binary.' +AC_CHECK_PROG(DOXYGEN, doxygen, doxygen, []) +if test -z "$DOXYGEN"; then + AC_MSG_WARN([documentation targets require doxygen. Set your PATH appropriately or set DOXYGEN to point to a valid doxygen binary.]) fi # Checks for libraries. AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP not found, see http://gmplib.org/])]) # Checks for header files. +AC_CHECK_HEADERS([getopt.h unistd.h]) # Checks for typedefs, structures, and compiler characteristics. AC_HEADER_STDBOOL @@ -39,6 +59,17 @@ AC_TYPE_SIZE_T # Checks for library functions. +# Some definitions for config.h +if test "$enable_debug" = yes; then + AC_DEFINE([CVC4_DEBUG], [], [Whether or not to include debugging code.]) +fi + +if test "$enable_assertions" = yes; then + AC_DEFINE([CVC4_ASSERTIONS], [], [Whether or not assertions are enabled.]) +fi + +# Prepare configure output + AC_CONFIG_FILES([ Makefile contrib/Makefile @@ -54,4 +85,23 @@ AC_CONFIG_FILES([ src/parser/Makefile src/theory/Makefile ]) + AC_OUTPUT + +# Final information to the user +debug=debug +if test "$enable_debug" = no; then + debug=non-debug +fi +withassertions=with +if test "$enable_assertions" = no; then + withassertions=without +fi + +cat <; chomp; -die 'aborting operation' if !( $_ eq 'y' || $_ eq 'yes' || $_ eq 'Y' || $_ eq 'YES' ); + $_ = ; chomp; + die 'aborting operation' if !( $_ eq 'y' || $_ eq 'yes' || $_ eq 'Y' || $_ eq 'YES' ); + + $searchdirs[0] = 'src'; +} else { + @searchdirs = @ARGV; +} print "Updating sources...\n"; -recurse('src'); +recurse(shift @searchdirs) while $#searchdirs >= 0; sub recurse { my ($srcdir) = @_; + print "in dir $srcdir\n"; opendir(my $DIR, $srcdir); while(my $file = readdir $DIR) { next if !($file =~ /^[a-zA-Z]/); diff --git a/src/expr/attr_type.h b/src/expr/attr_type.h index d76bd742d..d24385f8e 100644 --- a/src/expr/attr_type.h +++ b/src/expr/attr_type.h @@ -12,7 +12,7 @@ #ifndef __CVC4_ATTR_TYPE_H #define __CVC4_ATTR_TYPE_H -#include "core/expr_attribute.h" +#include "expr_attribute.h" namespace CVC4 { diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index 5e422f349..b6484ef25 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -11,8 +11,8 @@ **/ #include "cvc4_expr.h" -#include "core/expr_value.h" -#include "core/expr_builder.h" +#include "expr_value.h" +#include "expr_builder.h" namespace CVC4 { @@ -44,11 +44,7 @@ Expr& Expr::operator=(const Expr& e) { return *this; } -ExprValue* Expr::operator->() { - return d_ev; -} - -const ExprValue* Expr::operator->() const { +ExprValue* Expr::operator->() const { return d_ev; } diff --git a/src/expr/expr_attribute.h b/src/expr/expr_attribute.h index b00882478..3525a8370 100644 --- a/src/expr/expr_attribute.h +++ b/src/expr/expr_attribute.h @@ -15,9 +15,9 @@ // TODO WARNING this file needs work ! #include -#include "core/config.h" -#include "core/context.h" -#include "core/cvc4_expr.h" +#include "config.h" +#include "context/context.h" +#include "cvc4_expr.h" namespace CVC4 { diff --git a/src/expr/expr_builder.cpp b/src/expr/expr_builder.cpp index 6491b7d44..2f7114a9b 100644 --- a/src/expr/expr_builder.cpp +++ b/src/expr/expr_builder.cpp @@ -9,9 +9,10 @@ ** **/ -#include "core/expr_builder.h" -#include "core/expr_manager.h" -#include "core/expr_value.h" +#include "expr_builder.h" +#include "expr_manager.h" +#include "expr_value.h" +#include "util/assert.h" using namespace std; @@ -26,6 +27,16 @@ ExprBuilder::ExprBuilder(const Expr& e) : d_em(ExprManager::currentEM()), d_kind d_children.u_arr[0] = v; } +ExprBuilder& ExprBuilder::reset(const ExprValue* ev) { + this->~ExprBuilder(); + d_kind = Kind(ev->d_kind); + d_used = false; + d_nchildren = ev->d_nchildren; + for(Expr::const_iterator i = ev->begin(); i != ev->end(); ++i) + addChild(i->d_ev); + return *this; +} + ExprBuilder::ExprBuilder(const ExprBuilder& eb) : d_em(eb.d_em), d_kind(eb.d_kind), d_used(eb.d_used), d_nchildren(eb.d_nchildren) { cvc4assert(!d_used); @@ -34,9 +45,9 @@ ExprBuilder::ExprBuilder(const ExprBuilder& eb) : d_em(eb.d_em), d_kind(eb.d_kin d_children.u_vec->reserve(d_nchildren + 5); copy(eb.d_children.u_vec->begin(), eb.d_children.u_vec->end(), back_inserter(*d_children.u_vec)); } else { - iterator j = d_children.u_arr; - for(iterator i = eb.d_children.u_arr; i != eb.d_children.u_arr + eb.d_nchildren; ++i, ++j) - *j = i->inc(); + ev_iterator j = d_children.u_arr; + for(ExprValue* const* i = eb.d_children.u_arr; i != eb.d_children.u_arr + eb.d_nchildren; ++i, ++j) + *j = (*i)->inc(); } } @@ -46,7 +57,7 @@ ExprBuilder::ExprBuilder(ExprManager* em) : d_em(em), d_kind(UNDEFINED_KIND), d_ ExprBuilder::ExprBuilder(ExprManager* em, Kind k) : d_em(em), d_kind(k), d_used(false), d_nchildren(0) { } -ExprBuilder::ExprBuilder(ExprManager* em, const Expr&) : d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) { +ExprBuilder::ExprBuilder(ExprManager* em, const Expr& e) : d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) { ExprValue *v = e->inc(); d_children.u_arr[0] = v; } @@ -55,8 +66,8 @@ ExprBuilder::~ExprBuilder() { if(d_nchildren > nchild_thresh) { delete d_children.u_vec; } else { - for(iterator i = d_children.u_arr; i != d_children.u_arr + d_nchildren; ++i) { - *i + for(ev_iterator i = d_children.u_arr; i != d_children.u_arr + d_nchildren; ++i) { + (*i)->dec(); } } } @@ -70,10 +81,20 @@ ExprBuilder& ExprBuilder::eqExpr(const Expr& right) { } ExprBuilder& ExprBuilder::notExpr() { + if(d_kind != UNDEFINED_KIND) + collapse(); + d_kind = NOT; + return *this; } // avoid double-negatives ExprBuilder& ExprBuilder::negate() { + if(d_kind == NOT) + return reset(d_children.u_arr[0]); + if(d_kind != UNDEFINED_KIND) + collapse(); + d_kind = NOT; + return *this; } ExprBuilder& ExprBuilder::andExpr(const Expr& right) { @@ -116,7 +137,43 @@ void ExprBuilder::addChild(const Expr& e) { if(d_nchildren == nchild_thresh) { vector* v = new vector(); v->reserve(nchild_thresh + 5); - + for(ExprValue** i = d_children.u_arr; i != d_children.u_arr + nchild_thresh; ++i) { + v->push_back(Expr(*i)); + i->dec(); + } + v.push_back(e); + d_children.u_vec = v; + ++d_nchildren; + } else if(d_nchildren > nchild_thresh) { + d_children.u_vec.push_back(e); + ++d_nchildren; + } else { + ExprValue *ev = e->d_ev; + d_children.u_arr[d_nchildren] = ev; + ev->inc(); + ++d_nchildren; + } + return *this; +} + +void ExprBuilder::addChild(const ExprValue* ev) { + if(d_nchildren == nchild_thresh) { + vector* v = new vector(); + v->reserve(nchild_thresh + 5); + for(ExprValue** i = d_children.u_arr; i != d_children.u_arr + nchild_thresh; ++i) { + v->push_back(Expr(*i)); + i->dec(); + } + v.push_back(Expr(ev)); + d_children.u_vec = v; + ++d_nchildren; + } else if(d_nchildren > nchild_thresh) { + d_children.u_vec.push_back(Expr(ev)); + ++d_nchildren; + } else { + d_children.u_arr[d_nchildren] = ev; + ev->inc(); + ++d_nchildren; } return *this; } diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h index fa08a3149..1104c17f5 100644 --- a/src/expr/expr_builder.h +++ b/src/expr/expr_builder.h @@ -13,8 +13,8 @@ #define __CVC4_EXPR_BUILDER_H #include -#include "core/expr_manager.h" -#include "core/kind.h" +#include "expr_manager.h" +#include "kind.h" namespace CVC4 { @@ -41,9 +41,15 @@ class ExprBuilder { std::vector* u_vec; } d_children; - void addChild(); + void addChild(const Expr&); + void addChild(const ExprValue*); void collapse(); + typedef ExprValue** ev_iterator; + typedef ExprValue const** const_ev_iterator; + + void reset(const ExprValue*); + public: ExprBuilder(); diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index 90f10d8f7..80091bef6 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -10,9 +10,9 @@ ** Expression manager implementation. **/ -#include "core/expr_builder.h" -#include "core/expr_manager.h" -#include "core/cvc4_expr.h" +#include "expr_builder.h" +#include "expr_manager.h" +#include "cvc4_expr.h" namespace CVC4 { diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index 048250485..7e0da01c6 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -14,7 +14,7 @@ #include #include "cvc4_expr.h" -#include "core/kind.h" +#include "kind.h" namespace CVC4 { diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp index ce4177a09..451538f3f 100644 --- a/src/expr/expr_value.cpp +++ b/src/expr/expr_value.cpp @@ -14,7 +14,7 @@ ** reference count on ExprValue instances and **/ -#include "core/expr_value.h" +#include "expr_value.h" namespace CVC4 { diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h index 5f90533ed..4b4b4f612 100644 --- a/src/expr/expr_value.h +++ b/src/expr/expr_value.h @@ -48,6 +48,10 @@ class ExprValue { Expr d_children[0]; friend class Expr; + friend class ExprBuilder; + + ExprValue* inc() { /* FIXME thread safety */ ++d_rc; return this; } + ExprValue* dec() { /* FIXME thread safety */ --d_rc; return this; } public: /** Hash this expression. diff --git a/src/include/cvc4_expr.h b/src/include/cvc4_expr.h index 17e7f4f82..3d7a35fc8 100644 --- a/src/include/cvc4_expr.h +++ b/src/include/cvc4_expr.h @@ -38,6 +38,9 @@ class Expr { * Increments the reference count. */ explicit Expr(ExprValue*); + typedef Expr* iterator; + typedef Expr const* const_iterator; + public: Expr(const Expr&); @@ -49,11 +52,7 @@ public: /** Access to the encapsulated expression. * @return the encapsulated expression. */ - ExprValue* operator->(); - - /** Const access to the encapsulated expression. - * @return the encapsulated expression [const]. */ - const ExprValue* operator->() const; + ExprValue* operator->() const; uint64_t hash() const; diff --git a/src/main/Makefile.am b/src/main/Makefile.am index e857c8245..3b2ccb05a 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -1,6 +1,9 @@ INCLUDES = -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -bin_BINARIES = cvc4 +bin_PROGRAMS = cvc4 -cvc4_SOURCES = +cvc4_SOURCES = \ + main.cpp \ + getopt.cpp \ + util.cpp diff --git a/src/main/about.h b/src/main/about.h new file mode 100644 index 000000000..f582debf0 --- /dev/null +++ b/src/main/about.h @@ -0,0 +1,17 @@ +#ifndef __CVC4_ABOUT_H +#define __CVC4_ABOUT_H + +namespace CVC4 { +namespace Main { + +const char about[] = "\ +This is a pre-release of CVC4.\n\ +Copyright (C) 2009 The ACSys Group\n\ + Courant Institute of Mathematical Sciences,\n\ + New York University\n\ +"; + +}/* CVC4::Main namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4_MAIN_H */ diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp new file mode 100644 index 000000000..5f32ccd77 --- /dev/null +++ b/src/main/getopt.cpp @@ -0,0 +1,128 @@ +#include +#include +#include +#include +#include +#include +#include + +#include + +#include "config.h" +#include "main.h" +#include "util/exception.h" +#include "usage.h" +#include "about.h" + +using namespace std; +using namespace CVC4; + +namespace CVC4 { +namespace Main { + +static const char lang_help[] = "\ +Languages currently supported 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\n\ +"; + +enum Language { + AUTO = 0, + PL, + SMTLIB, +};/* enum Language */ + +enum OptionValue { + SMTCOMP = 256, /* no clash with char options */ + STATS +};/* enum OptionValue */ + +static struct option cmdlineOptions[] = { + // name, has_arg, *flag, val + { "help" , no_argument , NULL, 'h' }, + { "version", no_argument , NULL, 'V' }, + { "verbose", no_argument , NULL, 'v' }, + { "quiet" , no_argument , NULL, 'q' }, + { "lang" , required_argument, NULL, 'L' }, + { "debug" , required_argument, NULL, 'd' }, + { "smtcomp", no_argument , NULL, SMTCOMP }, + { "stats" , no_argument , NULL, STATS } +}; + +int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(Exception*) { + 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; + opts->binary_name = string(progName); + + while((c = getopt_long(argc, argv, "+:hVvL:", cmdlineOptions, NULL)) != -1) { + switch(c) { + + case 'h': + printf(usage, opts->binary_name.c_str()); + exit(1); + break; + + case 'V': + fputs(about, stdout); + break; + + case 'v': + ++opts->verbosity; + break; + + case 'q': + --opts->verbosity; + break; + + case 'L': + if(!strcmp(argv[optind], "cvc4") || !strcmp(argv[optind], "pl")) { + opts->lang = PL; + break; + } else if(!strcmp(argv[optind], "smtlib") || !strcmp(argv[optind], "smt")) { + opts->lang = SMTLIB; + break; + } else if(!strcmp(argv[optind], "auto")) { + opts->lang = AUTO; + break; + } + + if(strcmp(argv[optind], "help")) + throw new OptionException(string("unknown language for --lang: `") + argv[optind] + "'. Try --lang help."); + + fputs(lang_help, stdout); + exit(1); + + case STATS: + opts->statistics = true; + break; + + case SMTCOMP: + // silences CVC4 (except "sat" or "unsat" or "unknown", forces smtlib input) + opts->smtcomp_mode = true; + opts->verbosity = -1; + opts->lang = SMTLIB; + break; + + case '?': + throw new OptionException(string("can't understand option: `") + argv[optind] + "'"); + + case ':': + throw new OptionException(string("option `") + argv[optind] + "' missing its required argument"); + + default: + throw new OptionException(string("can't understand option: `") + argv[optind] + "'"); + } + + } + + return optind; +} + +}/* CVC4::Main namespace */ +}/* CVC4 namespace */ diff --git a/src/main/main.cpp b/src/main/main.cpp new file mode 100644 index 000000000..4850d475f --- /dev/null +++ b/src/main/main.cpp @@ -0,0 +1,68 @@ +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include "config.h" +#include "main.h" +#include "usage.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::Main; + +int main(int argc, char *argv[]) { + struct Options opts; + + try { + cvc4_init(); + + int firstArgIndex = parseOptions(argc, argv, &opts); + + FILE *infile; + + if(firstArgIndex >= argc) { + infile = stdin; + } else if(argc > firstArgIndex + 1) { + throw new Exception("Too many input files specified."); + } else { + infile = fopen(argv[firstArgIndex], "r"); + if(!infile) { + throw new Exception(string("Could not open input file `") + argv[firstArgIndex] + "' for reading: " + strerror(errno)); + exit(1); + } + } + } catch(CVC4::Main::OptionException* e) { + if(opts.smtcomp_mode) { + printf("unknown"); + fflush(stdout); + } + fprintf(stderr, "CVC4 Error:\n%s\n\n", e->toString().c_str()); + printf(usage, opts.binary_name.c_str()); + exit(1); + } catch(CVC4::Exception* e) { + if(opts.smtcomp_mode) { + printf("unknown"); + fflush(stdout); + } + fprintf(stderr, "CVC4 Error:\n%s\n", e->toString().c_str()); + exit(1); + } catch(bad_alloc) { + if(opts.smtcomp_mode) { + printf("unknown"); + fflush(stdout); + } + fprintf(stderr, "CVC4 ran out of memory.\n"); + exit(1); + } catch(...) { + fprintf(stderr, "CVC4 threw an exception of unknown type.\n"); + exit(1); + } + + return 0; +} diff --git a/src/main/main.h b/src/main/main.h new file mode 100644 index 000000000..4101f4fe4 --- /dev/null +++ b/src/main/main.h @@ -0,0 +1,26 @@ +#include +#include +#include + +#include "config.h" +#include "util/exception.h" +#include "util/options.h" + +#ifndef __CVC4_MAIN_H +#define __CVC4_MAIN_H + +namespace CVC4 { +namespace Main { + +class OptionException : public CVC4::Exception { +public: + OptionException(const std::string& s) throw() : CVC4::Exception("Error in option parsing: " + s) {} +};/* class OptionException */ + +int parseOptions(int argc, char** argv, CVC4::Options*) throw(CVC4::Exception*); +void cvc4_init() throw(); + +}/* CVC4::Main namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4_MAIN_H */ diff --git a/src/main/usage.h b/src/main/usage.h new file mode 100644 index 000000000..971ba7640 --- /dev/null +++ b/src/main/usage.h @@ -0,0 +1,29 @@ +#ifndef __CVC4_USAGE_H +#define __CVC4_USAGE_H + +namespace CVC4 { +namespace Main { + +// no more % chars in here without being escaped; it's used as a +// printf() format string +const char usage[] = "\ +usage: %s [options] [input-file]\n\ +\n\ +Without an input file, or with `-', CVC4 reads from standard input.\n\ +\n\ +CVC4 options:\n\ + --lang | -L set input language (--lang help gives a list;\n\ + `auto' is default)\n\ + --version | -V identify this CVC4 binary\n\ + --help | -h this command line reference\n\ + --verbose | -v increase verbosity (repeatable)\n\ + --quiet | -q decrease verbosity (repeatable)\n\ + --debug | -d debugging for something (e.g. --debug arith)\n\ + --smtcomp competition mode (very quiet)\n\ + --stats give statistics on exit\n\ +"; + +}/* CVC4::Main namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4_USAGE_H */ diff --git a/src/main/util.cpp b/src/main/util.cpp new file mode 100644 index 000000000..da4d4b0c0 --- /dev/null +++ b/src/main/util.cpp @@ -0,0 +1,44 @@ +#include +#include +#include +#include +#include +#include + +#include "util/exception.h" +#include "config.h" + +using CVC4::Exception; +using namespace std; + +namespace CVC4 { +namespace Main { + +void sigint_handler(int sig, siginfo_t* info, void*) { + fprintf(stderr, "CVC4 interrupted by user.\n"); + exit(info->si_signo + 128); +} + +void segv_handler(int sig, siginfo_t* info, void*) { + fprintf(stderr, "CVC4 suffered a segfault.\n"); + exit(info->si_signo + 128); +} + +void cvc4_init() throw() { + struct sigaction act1; + act1.sa_sigaction = sigint_handler; + act1.sa_flags = SA_SIGINFO; + sigemptyset(&act1.sa_mask); + if(sigaction(SIGINT, &act1, NULL)) + throw new Exception(string("sigaction(SIGINT) failure: ") + strerror(errno)); + + struct sigaction act2; + act2.sa_sigaction = segv_handler; + act2.sa_flags = SA_SIGINFO; + sigemptyset(&act2.sa_mask); + if(sigaction(SIGSEGV, &act2, NULL)) + throw new Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno)); +} + +}/* CVC4::Main namespace */ +}/* CVC4 namespace */ diff --git a/src/util/options.h b/src/util/options.h new file mode 100644 index 000000000..f04b06f10 --- /dev/null +++ b/src/util/options.h @@ -0,0 +1,31 @@ +#ifndef __CVC4_OPTIONS_H +#define __CVC4_OPTIONS_H + +namespace CVC4 { + +struct Options { + std::string binary_name; + + bool smtcomp_mode; + bool statistics; + + /* -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; + + std::string lang; + + Options() : binary_name(), + smtcomp_mode(false), + statistics(false), + verbosity(0), + lang() + {} +};/* struct Options */ + +}/* CVC4 namespace */ + +#endif /* __CVC4_OPTIONS_H */ -- 2.30.2