diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/options.cpp | 41 | ||||
-rw-r--r-- | src/util/options.h | 30 | ||||
-rw-r--r-- | src/util/stats.cpp | 49 | ||||
-rw-r--r-- | src/util/stats.h | 59 |
4 files changed, 125 insertions, 54 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 diff --git a/src/util/options.h b/src/util/options.h index 32ce77a64..efbd48900 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -26,6 +26,7 @@ #include "util/exception.h" #include "util/language.h" +#include "util/tls.h" namespace CVC4 { @@ -39,13 +40,23 @@ public: struct CVC4_PUBLIC Options { + /** The current Options in effect */ + static CVC4_THREADLOCAL(const Options*) s_current; + + /** Get the current Options in effect */ + static inline const Options* current() { + return s_current; + } + + /** The name of the binary (e.g. "cvc4") */ std::string binary_name; + /** Whether to collect statistics during this run */ bool statistics; - std::istream* in; - std::ostream* out; - std::ostream* err; + std::istream* in; /*< The input stream to use */ + std::ostream* out; /*< The output stream to use */ + std::ostream* err; /*< The error stream to use */ /* -1 means no output */ /* 0 is normal (and default) -- warnings only */ @@ -117,8 +128,10 @@ struct CVC4_PUBLIC Options { /** Whether incemental solving (push/pop) */ bool incrementalSolving; - static bool rewriteArithEqualities; + /** Whether to rewrite equalities in arithmetic theory */ + bool rewriteArithEqualities; + /** The pivot rule for arithmetic */ typedef enum { MINIMUM, BREAK_TIES, MAXIMUM } ArithPivotRule; ArithPivotRule pivotRule; @@ -130,7 +143,14 @@ struct CVC4_PUBLIC Options { * suitable as an argument to printf. */ std::string getDescription() const; + /** + * Print overall command-line option usage message, prefixed by + * "msg"---which could be an error message causing the usage + * output in the first place, e.g. "no such option --foo" + */ static void printUsage(const std::string msg, std::ostream& out); + + /** Print help for the --lang command line option */ static void printLanguageHelp(std::ostream& out); /** @@ -156,6 +176,8 @@ inline std::ostream& operator<<(std::ostream& out, return out; } +std::ostream& operator<<(std::ostream& out, Options::ArithPivotRule rule); + }/* CVC4 namespace */ #endif /* __CVC4__OPTIONS_H */ diff --git a/src/util/stats.cpp b/src/util/stats.cpp index 5be9525a9..428f051e0 100644 --- a/src/util/stats.cpp +++ b/src/util/stats.cpp @@ -18,13 +18,33 @@ **/ #include "util/stats.h" +#include "expr/node_manager.h" +#include "expr/expr_manager_scope.h" using namespace CVC4; -StatisticsRegistry::StatSet StatisticsRegistry::d_registeredStats; - std::string Stat::s_delim(","); +StatisticsRegistry* StatisticsRegistry::current() { + return NodeManager::currentNM()->getStatisticsRegistry(); +} + +void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) { +#ifdef CVC4_STATISTICS_ON + StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats; + AlwaysAssert(registeredStats.find(s) == registeredStats.end()); + registeredStats.insert(s); +#endif /* CVC4_STATISTICS_ON */ +}/* StatisticsRegistry::registerStat() */ + +void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) { +#ifdef CVC4_STATISTICS_ON + StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats; + AlwaysAssert(registeredStats.find(s) != registeredStats.end()); + registeredStats.erase(s); +#endif /* CVC4_STATISTICS_ON */ +}/* StatisticsRegistry::unregisterStat() */ + void StatisticsRegistry::flushStatistics(std::ostream& out) { #ifdef CVC4_STATISTICS_ON for(StatSet::iterator i = d_registeredStats.begin(); @@ -34,5 +54,28 @@ void StatisticsRegistry::flushStatistics(std::ostream& out) { s->flushStat(out); out << std::endl; } -#endif +#endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::flushStatistics() */ + +StatisticsRegistry::const_iterator StatisticsRegistry::begin() { + return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.begin(); +}/* StatisticsRegistry::begin() */ + +StatisticsRegistry::const_iterator StatisticsRegistry::end() { + return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.end(); +}/* StatisticsRegistry::end() */ + +RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) : + d_em(&em), d_stat(stat) { + ExprManagerScope ems(*d_em); + StatisticsRegistry::registerStat(d_stat); +}/* RegisterStatistic::RegisterStatistic(ExprManager&, Stat*) */ + +RegisterStatistic::~RegisterStatistic() { + if(d_em != NULL) { + ExprManagerScope ems(*d_em); + StatisticsRegistry::unregisterStat(d_stat); + } else { + StatisticsRegistry::unregisterStat(d_stat); + } +}/* RegisterStatistic::~RegisterStatistic() */ diff --git a/src/util/stats.h b/src/util/stats.h index bf962d02b..53acc9b1b 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -42,6 +42,8 @@ namespace CVC4 { # define __CVC4_USE_STATISTICS false #endif +class ExprManager; + class CVC4_PUBLIC Stat; inline std::ostream& operator<<(std::ostream& os, const ::timespec& t); @@ -49,9 +51,6 @@ inline std::ostream& operator<<(std::ostream& os, const ::timespec& t); /** * The main statistics registry. This registry maintains the list of * currently active statistics and is able to "flush" them all. - * - * The statistics registry is only used statically; one does not - * construct a statistics registry. */ class CVC4_PUBLIC StatisticsRegistry { private: @@ -64,42 +63,42 @@ private: typedef std::set< Stat*, StatCmp > StatSet; /** The set of currently active statistics */ - static StatSet d_registeredStats; + StatSet d_registeredStats; - /** Private default constructor undefined (no construction permitted). */ - StatisticsRegistry() CVC4_UNDEFINED; /** Private copy constructor undefined (no copy permitted). */ StatisticsRegistry(const StatisticsRegistry&) CVC4_UNDEFINED; public: + /** Construct a statistics registry */ + StatisticsRegistry() { } + /** An iterator type over a set of statistics */ typedef StatSet::const_iterator const_iterator; + /** Get a pointer to the current statistics registry */ + static StatisticsRegistry* current(); + /** Flush all statistics to the given output stream. */ - static void flushStatistics(std::ostream& out); + void flushStatistics(std::ostream& out); /** Register a new statistic, making it active. */ - static inline void registerStat(Stat* s) throw(AssertionException); + static void registerStat(Stat* s) throw(AssertionException); /** Unregister an active statistic, making it inactive. */ - static inline void unregisterStat(Stat* s) throw(AssertionException); + static void unregisterStat(Stat* s) throw(AssertionException); /** * Get an iterator to the beginning of the range of the set of active * (registered) statistics. */ - static inline const_iterator begin() { - return d_registeredStats.begin(); - } + static const_iterator begin(); /** * Get an iterator to the end of the range of the set of active * (registered) statistics. */ - static inline const_iterator end() { - return d_registeredStats.end(); - } + static const_iterator end(); };/* class StatisticsRegistry */ @@ -175,24 +174,6 @@ inline bool StatisticsRegistry::StatCmp::operator()(const Stat* s1, return s1->getName() < s2->getName(); } -inline void StatisticsRegistry::registerStat(Stat* s) - throw(AssertionException) { - if(__CVC4_USE_STATISTICS) { - AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end()); - d_registeredStats.insert(s); - } -}/* StatisticsRegistry::registerStat() */ - - -inline void StatisticsRegistry::unregisterStat(Stat* s) - throw(AssertionException) { - if(__CVC4_USE_STATISTICS) { - AlwaysAssert(d_registeredStats.find(s) != d_registeredStats.end()); - d_registeredStats.erase(s); - } -}/* StatisticsRegistry::unregisterStat() */ - - /** * A class to represent a "read-only" data statistic of type T. Adds to * the Stat base class the pure virtual function getData(), which returns @@ -766,14 +747,20 @@ public: * registration and unregistration. */ class RegisterStatistic { + ExprManager* d_em; Stat* d_stat; public: RegisterStatistic(Stat* stat) : d_stat(stat) { + Assert(StatisticsRegistry::current() != NULL, + "You need to specify an expression manager " + "on which to set the statistic"); StatisticsRegistry::registerStat(d_stat); } - ~RegisterStatistic() { - StatisticsRegistry::unregisterStat(d_stat); - } + + RegisterStatistic(ExprManager& em, Stat* stat); + + ~RegisterStatistic(); + };/* class RegisterStatistic */ #undef __CVC4_USE_STATISTICS |