diff options
Diffstat (limited to 'src/util/options.cpp')
| -rw-r--r-- | src/util/options.cpp | 41 |
1 files changed, 30 insertions, 11 deletions
diff --git a/src/util/options.cpp b/src/util/options.cpp index 1b73361c3..4bcc9a37d 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -40,6 +40,8 @@ using namespace CVC4; namespace CVC4 { +CVC4_THREADLOCAL(const Options*) Options::s_current = NULL; + #ifdef CVC4_DEBUG # define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true #else /* CVC4_DEBUG */ @@ -75,6 +77,7 @@ Options::Options() : typeChecking(DO_SEMANTIC_CHECKS_BY_DEFAULT), earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT), incrementalSolving(false), + rewriteArithEqualities(false), pivotRule(MINIMUM) { } @@ -88,9 +91,9 @@ static const string optionsDescription = "\ --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\ + --eager-type-checking type check expressions immediately on creation (debug builds only)\n\ --no-type-checking never type check expressions\n\ - --no-checking disable ALL semantic checks, including type checks \n\ + --no-checking disable ALL semantic checks, including type checks\n\ --no-theory-registration disable theory reg (not safe for some theories)\n\ --strict-parsing fail on non-conformant inputs (SMT2 only)\n\ --verbose | -v increase verbosity (repeatable)\n\ @@ -106,7 +109,8 @@ static const string optionsDescription = "\ --produce-models support the get-value command\n\ --produce-assignments support the get-assignment command\n\ --lazy-definition-expansion expand define-fun lazily\n\ - --rewrite-arithmetic-equalities rewrite (= x y) to (and (<= x y) (>= x y)) in arithmetic \n\ + --pivot-rule=RULE change the pivot rule (see --pivot-rule help)\n\ + --rewrite-arithmetic-equalities rewrite (= x y) to (and (<= x y) (>= x y)) in arithmetic\n\ --incremental enable incremental solving\n"; static const string languageDescription = "\ @@ -213,14 +217,14 @@ static struct option cmdlineOptions[] = { { "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}, - { "incremental", no_argument, NULL, INCREMENTAL}, + { "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 }, + { "incremental", no_argument, NULL, INCREMENTAL }, { "pivot-rule" , required_argument, NULL, PIVOT_RULE }, - { "rewrite-arithmetic-equalities" , no_argument, NULL, REWRITE_ARITHMETIC_EQUALITIES}, + { "rewrite-arithmetic-equalities", no_argument, NULL, REWRITE_ARITHMETIC_EQUALITIES }, { NULL , no_argument , NULL, '\0' } };/* if you add things to the above, please remember to update usage.h! */ @@ -484,8 +488,23 @@ throw(OptionException) { return optind; } -bool Options::rewriteArithEqualities = false; +std::ostream& operator<<(std::ostream& out, Options::ArithPivotRule rule) { + switch(rule) { + case Options::MINIMUM: + out << "MINIMUM"; + break; + case Options::BREAK_TIES: + out << "BREAK_TIES"; + break; + case Options::MAXIMUM: + out << "MAXIMUM"; + break; + default: + out << "ArithPivotRule!UNKNOWN"; + } + return out; +} #undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT #undef DO_SEMANTIC_CHECKS_BY_DEFAULT |