diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Makefile.am | 3 | ||||
-rw-r--r-- | src/util/channel.cpp | 2 | ||||
-rw-r--r-- | src/util/channel.h | 96 | ||||
-rw-r--r-- | src/util/hash.h | 16 | ||||
-rw-r--r-- | src/util/lemma_input_channel.h | 19 | ||||
-rw-r--r-- | src/util/lemma_output_channel.h | 46 | ||||
-rw-r--r-- | src/util/options.cpp | 96 | ||||
-rw-r--r-- | src/util/options.h | 41 | ||||
-rw-r--r-- | src/util/stats.cpp | 48 | ||||
-rw-r--r-- | src/util/stats.h | 230 |
10 files changed, 486 insertions, 111 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am index c5a20cd5d..3cb6ea16f 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -50,6 +50,9 @@ libutil_la_SOURCES = \ stats.cpp \ dynamic_array.h \ language.h \ + lemma_output_channel.h \ + channel.h \ + channel.cpp \ language.cpp \ ntuple.h \ recursion_breaker.h \ diff --git a/src/util/channel.cpp b/src/util/channel.cpp new file mode 100644 index 000000000..998550f8e --- /dev/null +++ b/src/util/channel.cpp @@ -0,0 +1,2 @@ +#include "channel.h" + diff --git a/src/util/channel.h b/src/util/channel.h new file mode 100644 index 000000000..1701feba9 --- /dev/null +++ b/src/util/channel.h @@ -0,0 +1,96 @@ + +#ifndef __CVC4__CHANNEL_H +#define __CVC4__CHANNEL_H + +#include <boost/circular_buffer.hpp> +#include <boost/thread/mutex.hpp> +#include <boost/thread/condition.hpp> +#include <boost/thread/thread.hpp> +#include <boost/call_traits.hpp> +#include <boost/progress.hpp> +#include <boost/bind.hpp> + + +namespace CVC4 { + +template <typename T> +class SharedChannel { +private: + int d_maxsize; // just call it size? +public: + SharedChannel() {} + SharedChannel(int maxsize) : d_maxsize(maxsize) {} + + /* Tries to add element and returns true if successful */ + virtual bool push(const T&) = 0; + + /* Removes an element from the channel */ + virtual T pop() = 0; + + /* */ + virtual bool empty() = 0; + + /* */ + virtual bool full() = 0; +}; + +/* +This code is from + +http://live.boost.org/doc/libs/1_46_1/libs/circular_buffer/doc/circular_buffer.html#boundedbuffer +*/ +template <typename T> +class SynchronizedSharedChannel: public SharedChannel<T> { +public: + typedef boost::circular_buffer<T> container_type; + typedef typename container_type::size_type size_type; + typedef typename container_type::value_type value_type; + typedef typename boost::call_traits<value_type>::param_type param_type; + + explicit SynchronizedSharedChannel(size_type capacity) : m_unread(0), m_container(capacity) {} + + bool push(param_type item){ + // param_type represents the "best" way to pass a parameter of type value_type to a method + + boost::mutex::scoped_lock lock(m_mutex); + m_not_full.wait(lock, boost::bind(&SynchronizedSharedChannel<value_type>::is_not_full, this)); + m_container.push_front(item); + ++m_unread; + lock.unlock(); + m_not_empty.notify_one(); + return true; + }//function definitions need to be moved to cpp + + value_type pop(){ + value_type ret; + boost::mutex::scoped_lock lock(m_mutex); + m_not_empty.wait(lock, boost::bind(&SynchronizedSharedChannel<value_type>::is_not_empty, this)); + ret = m_container[--m_unread]; + lock.unlock(); + m_not_full.notify_one(); + return ret; + } + + + bool empty() { return not is_not_empty(); } + bool full() { return not is_not_full(); } + +private: + SynchronizedSharedChannel(const SynchronizedSharedChannel&); // Disabled copy constructor + SynchronizedSharedChannel& operator = (const SynchronizedSharedChannel&); // Disabled assign operator + + bool is_not_empty() const { return m_unread > 0; } + bool is_not_full() const { return m_unread < m_container.capacity(); } + + size_type m_unread; + container_type m_container; + boost::mutex m_mutex; + boost::condition m_not_empty; + boost::condition m_not_full; +}; + +} + +#endif /* __CVC4__CHANNEL_H */ + + diff --git a/src/util/hash.h b/src/util/hash.h index 6183c5208..5f0189d44 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -26,6 +26,22 @@ namespace __gnu_cxx {} #include <ext/hash_map> + +namespace __gnu_cxx { + +#if __WORDSIZE == 32 +// on 32-bit, we need a specialization of hash for 64-bit values +template <> +struct hash<uint64_t> { + size_t operator()(uint64_t v) const { + return v; + } +};/* struct hash<uint64_t> */ +#endif /* 32-bit */ + +}/* __gnu_cxx namespace */ + +// hackish: treat hash stuff as if it were in std namespace namespace std { using namespace __gnu_cxx; } namespace CVC4 { diff --git a/src/util/lemma_input_channel.h b/src/util/lemma_input_channel.h new file mode 100644 index 000000000..1627711ee --- /dev/null +++ b/src/util/lemma_input_channel.h @@ -0,0 +1,19 @@ +#include "cvc4_public.h" + +#ifndef __CVC4__LEMMA_INPUT_CHANNEL_H +#define __CVC4__LEMMA_INPUT_CHANNEL_H + +#include "expr/expr.h" + +namespace CVC4 { + +class CVC4_PUBLIC LemmaInputChannel { +public: + virtual bool hasNewLemma() = 0; + virtual Expr getNewLemma() = 0; + +};/* class LemmaOutputChannel */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__LEMMA_INPUT_CHANNEL_H */ diff --git a/src/util/lemma_output_channel.h b/src/util/lemma_output_channel.h new file mode 100644 index 000000000..720dd6512 --- /dev/null +++ b/src/util/lemma_output_channel.h @@ -0,0 +1,46 @@ +/********************* */ +/*! \file lemma_output_channel.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 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 Mechanism for communication about new lemmas + ** + ** This file defines an interface for use by the theory and propositional + ** engines to communicate new lemmas to the "outside world," for example + ** for lemma sharing between threads. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__LEMMA_OUTPUT_CHANNEL_H +#define __CVC4__LEMMA_OUTPUT_CHANNEL_H + +#include "expr/expr.h" + +namespace CVC4 { + +/** + * This interface describes a mechanism for the propositional and theory + * engines to communicate with the "outside world" about new lemmas being + * discovered. + */ +class CVC4_PUBLIC LemmaOutputChannel { +public: + /** + * Notifies this output channel that there's a new lemma. + * The lemma may or may not be in CNF. + */ + virtual void notifyNewLemma(Expr lemma) = 0; +};/* class LemmaOutputChannel */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__LEMMA_OUTPUT_CHANNEL_H */ diff --git a/src/util/options.cpp b/src/util/options.cpp index d33064c73..e33fbc263 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -64,6 +64,9 @@ Options::Options() : verbosity(0), inputLanguage(language::input::LANG_AUTO), outputLanguage(language::output::LANG_AUTO), + help(false), + version(false), + languageHelp(false), parseOnly(false), preprocessOnly(false), semanticChecks(DO_SEMANTIC_CHECKS_BY_DEFAULT), @@ -71,6 +74,7 @@ Options::Options() : memoryMap(false), strictParsing(false), lazyDefinitionExpansion(false), + printWinner(false), simplificationMode(SIMPLIFICATION_MODE_BATCH), doStaticLearning(true), interactive(false), @@ -93,12 +97,23 @@ Options::Options() : arithPropagation(true), satRandomFreq(0.0), satRandomSeed(91648253),// Minisat's default value + satVarDecay(0.95), + satClauseDecay(0.999), + satRestartFirst(25), + satRestartInc(3.0), pivotRule(MINIMUM), arithPivotThreshold(16), arithPropagateMaxLength(16), ufSymmetryBreaker(false), ufSymmetryBreakerSetByUser(false), - dioSolver(true) + dioSolver(true), + lemmaOutputChannel(NULL), + lemmaInputChannel(NULL), + threads(2),// default should be 1 probably, but say 2 for now + threadArgv(), + thread_id(-1), + separateOutput(false), + sharingFilterByLength(-1) { } @@ -141,6 +156,7 @@ Additional CVC4 options:\n\ --no-type-checking never type check expressions\n\ --no-checking disable ALL semantic checks, including type checks\n\ --no-theory-registration disable theory reg (not safe for some theories)\n\ + --print-winner enable printing the winning thread (pcvc4 only)\n\ --trace | -t trace something (e.g. -t pushpop), can repeat\n\ --debug | -d debug something (e.g. -d arith), can repeat\n\ --show-debug-tags show all avalable tags for debugging\n\ @@ -157,13 +173,19 @@ Additional CVC4 options:\n\ --prop-row-length=N sets the maximum row length to be used in propagation\n\ --random-freq=P sets the frequency of random decisions in the sat solver(P=0.0 by default)\n\ --random-seed=S sets the random seed for the sat solver\n\ + --restart-int-base=I sets the base restart interval for the sat solver (I=25 by default)\n\ + --restart-int-inc=F sets the restart interval increase factor for the sat solver (F=3.0 by default)\n\ --disable-variable-removal enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\ --disable-arithmetic-propagation turns on arithmetic propagation\n\ --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al., CADE 2011) [on by default only for QF_UF]\n\ --disable-symmetry-breaker turns off UF symmetry breaker\n\ --disable-dio-solver turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)\n\ + --threads=N sets the number of solver threads\n\ + --threadN=string configures thread N (0..#threads-1)\n\ + --filter-lemma-length=N don't share lemmas strictly longer than N\n\ "; + #warning "Change CL options as --disable-variable-removal cannot do anything currently." static const string languageDescription = "\ @@ -322,8 +344,11 @@ enum OptionValue { REPLAY, REPLAY_LOG, PIVOT_RULE, + PRINT_WINNER, RANDOM_FREQUENCY, RANDOM_SEED, + SAT_RESTART_FIRST, + SAT_RESTART_INC, ARITHMETIC_VARIABLE_REMOVAL, ARITHMETIC_PROPAGATION, ARITHMETIC_PIVOT_THRESHOLD, @@ -331,6 +356,9 @@ enum OptionValue { ARITHMETIC_DIO_SOLVER, ENABLE_SYMMETRY_BREAKER, DISABLE_SYMMETRY_BREAKER, + PARALLEL_THREADS, + PARALLEL_SEPARATE_OUTPUT, + PORTFOLIO_FILTER_LENGTH, TIME_LIMIT, TIME_LIMIT_PER, RESOURCE_LIMIT, @@ -409,11 +437,17 @@ static struct option cmdlineOptions[] = { { "prop-row-length" , required_argument, NULL, ARITHMETIC_PROP_MAX_LENGTH }, { "random-freq" , required_argument, NULL, RANDOM_FREQUENCY }, { "random-seed" , required_argument, NULL, RANDOM_SEED }, + { "restart-int-base", required_argument, NULL, SAT_RESTART_FIRST }, + { "restart-int-inc", required_argument, NULL, SAT_RESTART_INC }, + { "print-winner", no_argument , NULL, PRINT_WINNER }, { "disable-variable-removal", no_argument, NULL, ARITHMETIC_VARIABLE_REMOVAL }, { "disable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION }, { "disable-dio-solver", no_argument, NULL, ARITHMETIC_DIO_SOLVER }, { "enable-symmetry-breaker", no_argument, NULL, ENABLE_SYMMETRY_BREAKER }, { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER }, + { "threads", required_argument, NULL, PARALLEL_THREADS }, + { "separate-output", no_argument, NULL, PARALLEL_SEPARATE_OUTPUT }, + { "filter-lemma-length", required_argument, NULL, PORTFOLIO_FILTER_LENGTH }, { "tlimit" , required_argument, NULL, TIME_LIMIT }, { "tlimit-per" , required_argument, NULL, TIME_LIMIT_PER }, { "rlimit" , required_argument, NULL, RESOURCE_LIMIT }, @@ -428,6 +462,13 @@ throw(OptionException) { const char *progName = argv[0]; int c; + // Reset getopt(), in the case of multiple calls. + // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0. + optind = 0; +#if HAVE_DECL_OPTRESET + optreset = 1; // on BSD getopt() (e.g. Mac OS), might also need this +#endif /* HAVE_DECL_OPTRESET */ + // find the base name of the program const char *x = strrchr(progName, '/'); if(x != NULL) { @@ -595,6 +636,10 @@ throw(OptionException) { memoryMap = true; break; + case PRINT_WINNER: + printWinner = true; + break; + case STRICT_PARSING: strictParsing = true; break; @@ -807,6 +852,26 @@ throw(OptionException) { optarg + "' is not between 0.0 and 1.0."); } break; + + case SAT_RESTART_FIRST: + { + int i = atoi(optarg); + if(i < 1) { + throw OptionException("--restart-int-base requires a number bigger than 1"); + } + satRestartFirst = i; + break; + } + + case SAT_RESTART_INC: + { + int i = atoi(optarg); + if(i < 1) { + throw OptionException("--restart-int-inc requires a number bigger than 1.0"); + } + satRestartInc = i; + } + break; case PIVOT_RULE: if(!strcmp(optarg, "min")) { @@ -905,11 +970,40 @@ throw(OptionException) { printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no"); exit(0); + case PARALLEL_THREADS: + threads = atoi(optarg); + break; + + case PARALLEL_SEPARATE_OUTPUT: + separateOutput = true; + break; + + case PORTFOLIO_FILTER_LENGTH: + sharingFilterByLength = atoi(optarg); + break; + case ':': throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument"); case '?': default: + if(optopt == 0 && + !strncmp(argv[optind - 1], "--thread", 8) && + strlen(argv[optind - 1]) > 8 && + isdigit(argv[optind - 1][8])) { + int tnum = atoi(argv[optind - 1] + 8); + threadArgv.resize(tnum + 1); + if(threadArgv[tnum] != "") { + threadArgv[tnum] += " "; + } + const char* p = strchr(argv[optind - 1] + 9, '='); + if(p == NULL) { // e.g., we have --thread0 "foo" + threadArgv[tnum] += argv[optind++]; + } else { // e.g., we have --thread0="foo" + threadArgv[tnum] += p + 1; + } + break; + } throw OptionException(string("can't understand option `") + argv[optind - 1] + "'"); } } diff --git a/src/util/options.h b/src/util/options.h index d04947b02..6b8054a13 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -27,8 +27,12 @@ #include "util/exception.h" #include "util/language.h" +#include "util/lemma_output_channel.h" +#include "util/lemma_input_channel.h" #include "util/tls.h" +#include <vector> + namespace CVC4 { class ExprStream; @@ -104,6 +108,9 @@ struct CVC4_PUBLIC Options { /** Should we expand function definitions lazily? */ bool lazyDefinitionExpansion; + /** Parallel Only: Whether the winner is printed at the end or not. */ + bool printWinner; + /** Enumeration of simplification modes (when to simplify). */ typedef enum { /** Simplify the assertions as they come in */ @@ -187,6 +194,18 @@ struct CVC4_PUBLIC Options { **/ double satRandomSeed; + /** Variable activity decay factor for Minisat */ + double satVarDecay; + + /** Clause activity decay factor for Minisat */ + double satClauseDecay; + + /** Base restart interval for Minisat */ + int satRestartFirst; + + /** Restart interval increase factor for Minisat */ + double satRestartInc; + /** The pivot rule for arithmetic */ typedef enum { MINIMUM, BREAK_TIES, MAXIMUM } ArithPivotRule; ArithPivotRule pivotRule; @@ -220,6 +239,28 @@ struct CVC4_PUBLIC Options { */ bool dioSolver; + /** The output channel to receive notfication events for new lemmas */ + LemmaOutputChannel* lemmaOutputChannel; + LemmaInputChannel* lemmaInputChannel; + + /** Total number of threads */ + int threads; + + /** Thread configuration (a string to be passed to parseOptions) */ + std::vector<std::string> threadArgv; + + /** Thread ID, for internal use in case of multi-threaded run */ + int thread_id; + + /** + * In multi-threaded setting print output of each thread at the + * end of run, separated by a divider ("----"). + **/ + bool separateOutput; + + /** Filter depending on length of lemma */ + int sharingFilterByLength; + Options(); /** diff --git a/src/util/stats.cpp b/src/util/stats.cpp index 474d8fa7a..709f80b04 100644 --- a/src/util/stats.cpp +++ b/src/util/stats.cpp @@ -31,6 +31,7 @@ using namespace CVC4; std::string Stat::s_delim(","); +std::string StatisticsRegistry::s_regDelim("::"); StatisticsRegistry* StatisticsRegistry::current() { return NodeManager::currentNM()->getStatisticsRegistry(); @@ -45,6 +46,14 @@ void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) { #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::registerStat() */ +void StatisticsRegistry::registerStat_(Stat* s) throw(AssertionException) +{ +#ifdef CVC4_STATISTICS_ON + AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end()); + d_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; @@ -54,17 +63,33 @@ void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) { #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::unregisterStat() */ -void StatisticsRegistry::flushStatistics(std::ostream& out) { +void StatisticsRegistry::unregisterStat_(Stat* s) throw(AssertionException) { +#ifdef CVC4_STATISTICS_ON + AlwaysAssert(d_registeredStats.find(s) != d_registeredStats.end()); + d_registeredStats.erase(s); +#endif /* CVC4_STATISTICS_ON */ +}/* StatisticsRegistry::unregisterStat_() */ + +void StatisticsRegistry::flushInformation(std::ostream& out) const { #ifdef CVC4_STATISTICS_ON for(StatSet::iterator i = d_registeredStats.begin(); i != d_registeredStats.end(); ++i) { Stat* s = *i; + if(d_name != "") { + out << d_name << s_regDelim; + } s->flushStat(out); out << std::endl; } #endif /* CVC4_STATISTICS_ON */ -}/* StatisticsRegistry::flushStatistics() */ +}/* StatisticsRegistry::flushInformation() */ + +void StatisticsRegistry::flushStat(std::ostream &out) const {; +#ifdef CVC4_STATISTICS_ON + flushInformation(out); +#endif /* CVC4_STATISTICS_ON */ +} StatisticsRegistry::const_iterator StatisticsRegistry::begin() { return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.begin(); @@ -93,16 +118,9 @@ void TimerStat::stop() { }/* TimerStat::stop() */ 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() */ + d_reg(NULL), + d_stat(stat) { + ExprManagerScope ems(em); + d_reg = StatisticsRegistry::current(); + d_reg->registerStat_(d_stat); +} diff --git a/src/util/stats.h b/src/util/stats.h index 719bbaab6..63e732305 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -2,7 +2,7 @@ /*! \file stats.h ** \verbatim ** Original author: taking - ** Major contributors: mdeters + ** Major contributors: mdeters, kshitij ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) @@ -47,84 +47,32 @@ class ExprManager; class CVC4_PUBLIC Stat; /** - * The main statistics registry. This registry maintains the list of - * currently active statistics and is able to "flush" them all. - */ -class CVC4_PUBLIC StatisticsRegistry { -private: - /** A helper class for comparing two statistics */ - struct StatCmp { - inline bool operator()(const Stat* s1, const Stat* s2) const; - };/* class StatisticsRegistry::StatCmp */ - - /** A type for a set of statistics */ - typedef std::set< Stat*, StatCmp > StatSet; - - /** The set of currently active statistics */ - StatSet d_registeredStats; - - /** 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. */ - void flushStatistics(std::ostream& out); - - /** Register a new statistic, making it active. */ - static void registerStat(Stat* s) throw(AssertionException); - - /** Unregister an active statistic, making it inactive. */ - static void unregisterStat(Stat* s) throw(AssertionException); - - /** - * Get an iterator to the beginning of the range of the set of active - * (registered) statistics. - */ - static const_iterator begin(); - - /** - * Get an iterator to the end of the range of the set of active - * (registered) statistics. - */ - static const_iterator end(); - -};/* class StatisticsRegistry */ - - -/** * The base class for all statistics. * - * This base class keeps the name of the statistic and declares two (pure) - * virtual functionss flushInformation() and getValue(). Derived classes - * must implement these functions and pass their name to the base class - * constructor. + * This base class keeps the name of the statistic and declares the (pure) + * virtual function flushInformation(). Derived classes must implement + * this function and pass their name to the base class constructor. * * This class also (statically) maintains the delimiter used to separate * the name and the value when statistics are output. */ class CVC4_PUBLIC Stat { private: - /** The name of this statistic */ - std::string d_name; - /** * The delimiter between name and value to use when outputting a * statistic. */ static std::string s_delim; +protected: + /** The name of this statistic */ + std::string d_name; + public: + /** Nullary constructor, does nothing */ + Stat() { } + /** * Construct a statistic with the given name. Debug builds of CVC4 * will throw an assertion exception if the given name contains the @@ -149,8 +97,10 @@ public: /** * Flush the name,value pair of this statistic to an output stream. * Uses the statistic delimiter string between name and value. + * + * May be redefined by a child class */ - void flushStat(std::ostream& out) const { + virtual void flushStat(std::ostream& out) const { if(__CVC4_USE_STATISTICS) { out << d_name << s_delim; flushInformation(out); @@ -163,21 +113,18 @@ public: } /** Get the value of this statistic as a string. */ - virtual std::string getValue() const = 0; + std::string getValue() const { + std::stringstream ss; + flushInformation(ss); + return ss.str(); + } };/* class Stat */ -inline bool StatisticsRegistry::StatCmp::operator()(const Stat* s1, - const Stat* s2) const { - return s1->getName() < s2->getName(); -} - /** * 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 - * type T, along with an implementation of getValue(), which converts the - * type T to a string using an existing stream insertion operator defined - * on T, and flushInformation(), which outputs the statistic value to an + * type T, and flushInformation(), which outputs the statistic value to an * output stream (using the same existing stream insertion operator). * * Template class T must have stream insertion operation defined: @@ -204,13 +151,6 @@ public: } } - /** Get the value of the statistic as a string. */ - std::string getValue() const { - std::stringstream ss; - ss << getData(); - return ss.str(); - } - };/* class ReadOnlyDataStat<T> */ @@ -480,20 +420,20 @@ private: * have seen so far. */ uint32_t d_count; + double d_sum; public: /** Construct an average statistic with the given name. */ AverageStat(const std::string& name) : - BackedStat<double>(name, 0.0), d_count(0) { + BackedStat<double>(name, 0.0), d_count(0), d_sum(0.0) { } /** Add an entry to the running-average calculation. */ void addEntry(double e) { if(__CVC4_USE_STATISTICS) { - double oldSum = d_count * getData(); ++d_count; - double newSum = oldSum + e; - setData(newSum / d_count); + d_sum += e; + setData(d_sum / d_count); } } @@ -535,13 +475,102 @@ public: return (*this); } - std::string getValue() const { - std::stringstream ss; - flushInformation(ss); - return ss.str(); +};/* class ListStat */ + +/****************************************************************************/ +/* Statistics Registry */ +/****************************************************************************/ + +/** + * The main statistics registry. This registry maintains the list of + * currently active statistics and is able to "flush" them all. + */ +class CVC4_PUBLIC StatisticsRegistry : public Stat { +private: + /** A helper class for comparing two statistics */ + struct StatCmp { + inline bool operator()(const Stat* s1, const Stat* s2) const; + };/* class StatisticsRegistry::StatCmp */ + + /** A type for a set of statistics */ + typedef std::set< Stat*, StatCmp > StatSet; + + /** The set of currently active statistics */ + StatSet d_registeredStats; + + /** Private copy constructor undefined (no copy permitted). */ + StatisticsRegistry(const StatisticsRegistry&) CVC4_UNDEFINED; + + static std::string s_regDelim; +public: + + /** Construct an nameless statistics registry */ + StatisticsRegistry() {} + + /** Construct a statistics registry */ + StatisticsRegistry(const std::string& name) throw(CVC4::AssertionException) : + Stat(name) { + if(__CVC4_USE_STATISTICS) { + AlwaysAssert(d_name.find(s_regDelim) == std::string::npos); + } } -};/* class ListStat */ + /** + * Set the name of this statistic registry, used as prefix during + * output. + * + * TODO: Get rid of this function once we have ability to set the + * name of StatisticsRegistry at creation time. + */ + void setName(const std::string& name) { + d_name = name; + } + + /** 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. */ + void flushInformation(std::ostream& out) const; + + /** Obsolete flushStatistics -- use flushInformation */ + //void flushStatistics(std::ostream& out) const; + + /** Overridden to avoid the name being printed */ + void flushStat(std::ostream &out) const; + + /** Register a new statistic, making it active. */ + static void registerStat(Stat* s) throw(AssertionException); + + /** Register a new statistic */ + void registerStat_(Stat* s) throw(AssertionException); + + /** Unregister an active statistic, making it inactive. */ + static void unregisterStat(Stat* s) throw(AssertionException); + + /** Unregister a new statistic */ + void unregisterStat_(Stat* s) throw(AssertionException); + + /** + * Get an iterator to the beginning of the range of the set of active + * (registered) statistics. + */ + static const_iterator begin(); + + /** + * Get an iterator to the end of the range of the set of active + * (registered) statistics. + */ + static const_iterator end(); + +};/* class StatisticsRegistry */ + +inline bool StatisticsRegistry::StatCmp::operator()(const Stat* s1, + const Stat* s2) const { + return s1->getName() < s2->getName(); +} /****************************************************************************/ /* Some utility functions for timespec */ @@ -753,19 +782,30 @@ public: * registration and unregistration. */ class CVC4_PUBLIC RegisterStatistic { - ExprManager* d_em; + StatisticsRegistry* d_reg; 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"); + RegisterStatistic(Stat* stat) : + d_reg(StatisticsRegistry::current()), + d_stat(stat) { + Assert(d_reg != NULL, "There is no current statistics registry!"); StatisticsRegistry::registerStat(d_stat); } + RegisterStatistic(StatisticsRegistry* reg, Stat* stat) : + d_reg(reg), + d_stat(stat) { + Assert(d_reg != NULL, + "You need to specify a statistics registry" + "on which to set the statistic"); + d_reg->registerStat_(d_stat); + } + RegisterStatistic(ExprManager& em, Stat* stat); - ~RegisterStatistic(); + ~RegisterStatistic() { + d_reg->unregisterStat_(d_stat); + } };/* class RegisterStatistic */ |