summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/Makefile.am3
-rw-r--r--src/util/channel.cpp2
-rw-r--r--src/util/channel.h96
-rw-r--r--src/util/hash.h16
-rw-r--r--src/util/lemma_input_channel.h19
-rw-r--r--src/util/lemma_output_channel.h46
-rw-r--r--src/util/options.cpp96
-rw-r--r--src/util/options.h41
-rw-r--r--src/util/stats.cpp48
-rw-r--r--src/util/stats.h230
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback