diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-01 00:56:42 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-01 00:56:42 +0000 |
commit | 159cb7ee8b6f28f3784a3f24b371760c2ab77f86 (patch) | |
tree | d510bfa3e4977b5c532d9ab82b6cd5d9581365a3 /src/util/options.cpp | |
parent | ceca24424da629db2e133f7864b0bac03ad44829 (diff) |
This commit is a merge from the "betterstats" branch, which:
* Makes Options an "omnipresent thread-local global" (like the notion
of the "current NodeManager" was already). Options::current() accesses
this structure.
* Removes Options from constructors and data structures everywhere
(this cleans up a lot of things).
* No longer uses StatisticsRegistry statically. An instance of the
registry is created and linked to a NodeManager.
* StatisticsRegistry::current() is similar to Options::current(), but
the pointer is stowed in the NodeManager (rather than stored)
* The static functions of StatisticsRegistry have been left, for backward
compatibility; they now use the "current" statistics registry.
* SmtEngine::getStatisticsRegistry() is a public accessor for the
registry; this is needed by main() to reach in and get the registry,
for flushing statistics at the end.
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 |