- The functionality the get the StatisticsRegistry attached to the SmtEngine was previously through StatisticsRegistry::current(). This is the dominant StatisticsRegistry in the code. (There is another StatisticsRegistry attached to the NodeManager.) Having this be a static function on StatisticsRegistry requires the use of an SmtEngine in the wrong compilation unit.
- Usages of StatisticsRegistry::current() that were visible in prop/{bvminisat,minisat} has been removed. A pointer to the relevant StatisticsRegistry should be passed instead into the constructor.
- The function StatisticsRegistry::current() has been replaced by SmtScope::currentStatisticsRegistry(). SmtScope is in the libcvc4 package, where SmtEngine is available in the compilation unit.
- The function smtStatisticsRegistry() is a synonym for SmtScope::currentStatisticsRegistry() in smt/smt_statistics_registry.h. This header has fewer include dependencies than the one for SmtScope.
- Correspondingly, the static functions StatisticsRegistry::{registerStat, unregisterStat} have been removed. One should instead use smtStatisticsRegistry()->{registerStat,unregisterStat} instead.
- The KEEP_STATISTIC macro has been moved into smt/smt_statistics_registry.h.
- Documents the reason StatisticsRegistry is CVC4_PUBLIC. This lets me remove the warning I added.
- Removing most operators for timespec from statistics_registry.h file. These a bit error prone in clang.
- Most of the really confusing ifdef's in util/statistics_registry.h are gone.
smt/smt_globals.h \
smt/model_postprocessor.cpp \
smt/model_postprocessor.h \
- smt/smt_options_handler.cpp \
- smt/smt_options_handler.h \
smt/smt_engine_scope.cpp \
smt/smt_engine_scope.h \
+ smt/smt_options_handler.cpp \
+ smt/smt_options_handler.h \
+ smt/smt_statistics_registry.cpp \
+ smt/smt_statistics_registry.h \
smt/command_list.cpp \
smt/command_list.h \
smt/boolean_terms.h \
%include "util/regexp.i"
%include "util/result.i"
%include "util/sexpr.i"
+%include "util/statistics.i"
%include "util/subrange_bound.i"
%include "util/tuple.i"
%include "util/unsafe_interrupt_exception.i"
%include "expr/uninterpreted_constant.i"
-%include "expr/statistics.i"
%include "expr/array_store_all.i"
%include "expr/ascription_type.i"
%include "expr/emptyset.i"
#include "options/decision_options.h"
#include "theory/rewriter.h"
#include "smt_util/ite_removal.h"
-
+#include "smt/smt_statistics_registry.h"
namespace CVC4 {
d_childCache(uc),
d_weightCache(uc),
d_startIndexCache(c) {
- StatisticsRegistry::registerStat(&d_helfulness);
- StatisticsRegistry::registerStat(&d_giveup);
- StatisticsRegistry::registerStat(&d_timestat);
+ smtStatisticsRegistry()->registerStat(&d_helfulness);
+ smtStatisticsRegistry()->registerStat(&d_giveup);
+ smtStatisticsRegistry()->registerStat(&d_timestat);
Trace("decision") << "Justification heuristic enabled" << std::endl;
}
JustificationHeuristic::~JustificationHeuristic() throw() {
- StatisticsRegistry::unregisterStat(&d_helfulness);
- StatisticsRegistry::unregisterStat(&d_giveup);
- StatisticsRegistry::unregisterStat(&d_timestat);
+ smtStatisticsRegistry()->unregisterStat(&d_helfulness);
+ smtStatisticsRegistry()->unregisterStat(&d_giveup);
+ smtStatisticsRegistry()->unregisterStat(&d_timestat);
}
CVC4::prop::SatLiteral JustificationHeuristic::getNext(bool &stopSearch)
-I@builddir@/.. -I@srcdir@/../include -I@srcdir@/..
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
-#noinst_LTLIBRARIES = libexpr.la libstatistics.la
noinst_LTLIBRARIES = libexpr.la
-# libstatistics_la_CPPFLAGS = $(CPPFLAGS) $(AM_CPPFLAGS) -D__BUILDING_STATISTICS_FOR_EXPORT
-# libstatistics_la_SOURCES = \
-# statistics_registry.h \
-# statistics_registry.cpp
-
-# EXTRA_libstatistics_la_DEPENDENCIES = \
-# builts
-
# For some reason statistics were in libutil. No idea why though.
libexpr_la_SOURCES = \
- statistics.cpp \
- statistics.h \
- statistics_registry.cpp \
- statistics_registry.h \
array.h \
array_store_all.cpp \
array_store_all.h \
expr_stream.i \
expr_manager.i \
symbol_table.i \
- statistics.i \
type.i \
kind.i \
expr.i \
#include <map>
#include "expr/node_manager.h"
-#include "expr/statistics_registry.h"
#include "expr/variable_type_map.h"
#include "options/options.h"
+#include "util/statistics_registry.h"
${includes}
stringstream statName; \
statName << "expr::ExprManager::" << kind; \
d_exprStatistics[kind] = new IntStat(statName.str(), 0); \
- d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatistics[kind]); \
+ d_nodeManager->getStatisticsRegistry()->registerStat(d_exprStatistics[kind]); \
} \
++ *(d_exprStatistics[kind]); \
}
statName << "expr::ExprManager::" << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":" << type; \
} \
d_exprStatisticsVars[type] = new IntStat(statName.str(), 0); \
- d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatisticsVars[type]); \
+ d_nodeManager->getStatisticsRegistry()->registerStat(d_exprStatisticsVars[type]); \
} \
++ *(d_exprStatisticsVars[type]); \
}
#ifdef CVC4_STATISTICS_ON
for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
if (d_exprStatistics[i] != NULL) {
- d_nodeManager->getStatisticsRegistry()->unregisterStat_(d_exprStatistics[i]);
+ d_nodeManager->getStatisticsRegistry()->unregisterStat(d_exprStatistics[i]);
delete d_exprStatistics[i];
d_exprStatistics[i] = NULL;
}
}
for (unsigned i = 0; i < LAST_TYPE; ++ i) {
if (d_exprStatisticsVars[i] != NULL) {
- d_nodeManager->getStatisticsRegistry()->unregisterStat_(d_exprStatisticsVars[i]);
+ d_nodeManager->getStatisticsRegistry()->unregisterStat(d_exprStatisticsVars[i]);
delete d_exprStatisticsVars[i];
d_exprStatisticsVars[i] = NULL;
}
}
}
-StatisticsRegistry* ExprManager::getStatisticsRegistry() throw() {
- return d_nodeManager->getStatisticsRegistry();
-}
-
const Options& ExprManager::getOptions() const {
return d_nodeManager->getOptions();
}
#include "expr/expr.h"
#include "expr/kind.h"
#include "expr/type.h"
-#include "expr/statistics.h"
+#include "util/statistics.h"
#include "util/subrange_bound.h"
${includes}
class Options;
class IntStat;
struct ExprManagerMapCollection;
-class StatisticsRegistry;
class ResourceManager;
namespace expr {
}/* CVC4::expr::pickle namespace */
}/* CVC4::expr namespace */
-namespace stats {
- StatisticsRegistry* getStatisticsRegistry(ExprManager*);
-}/* CVC4::stats namespace */
-
class CVC4_PUBLIC ExprManager {
private:
/** The internal node manager */
/** NodeManager reaches in to get the NodeManager */
friend class NodeManager;
- /** Statistics reach in to get the StatisticsRegistry */
- friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(ExprManager*);
-
- /** Get the underlying statistics registry. */
- StatisticsRegistry* getStatisticsRegistry() throw();
-
// undefined, private copy constructor and assignment op (disallow copy)
ExprManager(const ExprManager&) CVC4_UNDEFINED;
ExprManager& operator=(const ExprManager&) CVC4_UNDEFINED;
#include "options/options.h"
#include "options/smt_options.h"
#include "expr/resource_manager.h"
-#include "expr/statistics_registry.h"
+#include "util/statistics_registry.h"
using namespace std;
+++ /dev/null
-/********************* */
-/*! \file statistics.cpp
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include <typeinfo>
-
-#include "expr/statistics.h"
-#include "expr/statistics_registry.h" // for details about class Stat
-
-
-namespace CVC4 {
-
-std::string StatisticsBase::s_regDelim("::");
-
-bool StatisticsBase::StatCmp::operator()(const Stat* s1, const Stat* s2) const {
- return s1->getName() < s2->getName();
-}
-
-StatisticsBase::iterator::value_type StatisticsBase::iterator::operator*() const {
- return std::make_pair((*d_it)->getName(), (*d_it)->getValue());
-}
-
-StatisticsBase::StatisticsBase() :
- d_prefix(),
- d_stats() {
-}
-
-StatisticsBase::StatisticsBase(const StatisticsBase& stats) :
- d_prefix(stats.d_prefix),
- d_stats() {
-}
-
-StatisticsBase& StatisticsBase::operator=(const StatisticsBase& stats) {
- d_prefix = stats.d_prefix;
- return *this;
-}
-
-void Statistics::copyFrom(const StatisticsBase& stats) {
- // This is ugly, but otherwise we have to introduce a "friend" relation for
- // Base to its derived class (really obnoxious).
- StatSet::const_iterator i_begin = ((const Statistics*) &stats)->d_stats.begin();
- StatSet::const_iterator i_end = ((const Statistics*) &stats)->d_stats.end();
- for(StatSet::const_iterator i = i_begin; i != i_end; ++i) {
- SExprStat* p = new SExprStat((*i)->getName(), (*i)->getValue());
- d_stats.insert(p);
- }
-}
-
-void Statistics::clear() {
- for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) {
- delete *i;
- }
- d_stats.clear();
-}
-
-Statistics::Statistics(const StatisticsBase& stats) :
- StatisticsBase(stats) {
- copyFrom(stats);
-}
-
-Statistics::Statistics(const Statistics& stats) :
- StatisticsBase(stats) {
- copyFrom(stats);
-}
-
-Statistics::~Statistics() {
- clear();
-}
-
-Statistics& Statistics::operator=(const StatisticsBase& stats) {
- clear();
- this->StatisticsBase::operator=(stats);
- copyFrom(stats);
-
- return *this;
-}
-
-Statistics& Statistics::operator=(const Statistics& stats) {
- return this->operator=((const StatisticsBase&)stats);
-}
-
-StatisticsBase::const_iterator StatisticsBase::begin() const {
- return iterator(d_stats.begin());
-}
-
-StatisticsBase::const_iterator StatisticsBase::end() const {
- return iterator(d_stats.end());
-}
-
-void StatisticsBase::flushInformation(std::ostream &out) const {
-#ifdef CVC4_STATISTICS_ON
- for(StatSet::iterator i = d_stats.begin();
- i != d_stats.end();
- ++i) {
- Stat* s = *i;
- if(d_prefix != "") {
- out << d_prefix << s_regDelim;
- }
- s->flushStat(out);
- out << std::endl;
- }
-#endif /* CVC4_STATISTICS_ON */
-}
-
-SExpr StatisticsBase::getStatistic(std::string name) const {
- SExpr value;
- IntStat s(name, 0);
- StatSet::iterator i = d_stats.find(&s);
- if(i != d_stats.end()) {
- return (*i)->getValue();
- } else {
- return SExpr();
- }
-}
-
-void StatisticsBase::setPrefix(const std::string& prefix) {
- d_prefix = prefix;
-}
-
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file statistics.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__STATISTICS_H
-#define __CVC4__STATISTICS_H
-
-#include <iterator>
-#include <ostream>
-#include <set>
-#include <string>
-#include <utility>
-
-#include "util/sexpr.h"
-
-namespace CVC4 {
-
-class Stat;
-
-class CVC4_PUBLIC StatisticsBase {
-protected:
-
- static std::string s_regDelim;
-
- /** A helper class for comparing two statistics */
- struct StatCmp {
- bool operator()(const Stat* s1, const Stat* s2) const;
- };/* struct StatisticsRegistry::StatCmp */
-
- /** A type for a set of statistics */
- typedef std::set< Stat*, StatCmp > StatSet;
-
- std::string d_prefix;
-
- /** The set of statistics in this object */
- StatSet d_stats;
-
- StatisticsBase();
- StatisticsBase(const StatisticsBase& stats);
- StatisticsBase& operator=(const StatisticsBase& stats);
-
-public:
-
- virtual ~StatisticsBase() { }
-
- class CVC4_PUBLIC iterator : public std::iterator< std::input_iterator_tag, std::pair<std::string, SExpr> > {
- StatSet::iterator d_it;
-
- iterator(StatSet::iterator it) : d_it(it) { }
-
- friend class StatisticsBase;
-
- public:
- iterator() : d_it() { }
- iterator(const iterator& it) : d_it(it.d_it) { }
- value_type operator*() const;
- iterator& operator++() { ++d_it; return *this; }
- iterator operator++(int) { iterator old = *this; ++d_it; return old; }
- bool operator==(const iterator& i) const { return d_it == i.d_it; }
- bool operator!=(const iterator& i) const { return d_it != i.d_it; }
- };/* class StatisticsBase::iterator */
-
- /** An iterator type over a set of statistics. */
- typedef iterator const_iterator;
-
- /** Set the output prefix for this set of statistics. */
- virtual void setPrefix(const std::string& prefix);
-
- /** Flush all statistics to the given output stream. */
- void flushInformation(std::ostream& out) const;
-
- /** Get the value of a named statistic. */
- SExpr getStatistic(std::string name) const;
-
- /**
- * Get an iterator to the beginning of the range of the set of
- * statistics.
- */
- const_iterator begin() const;
-
- /**
- * Get an iterator to the end of the range of the set of statistics.
- */
- const_iterator end() const;
-
-};/* class StatisticsBase */
-
-class CVC4_PUBLIC Statistics : public StatisticsBase {
- void clear();
- void copyFrom(const StatisticsBase&);
-
-public:
-
- /**
- * Override the copy constructor to do a "deep" copy of statistics
- * values.
- */
- Statistics(const StatisticsBase& stats);
- Statistics(const Statistics& stats);
-
- ~Statistics();
-
- /**
- * Override the assignment operator to do a "deep" copy of statistics
- * values.
- */
- Statistics& operator=(const StatisticsBase& stats);
- Statistics& operator=(const Statistics& stats);
-
-};/* class Statistics */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__STATISTICS_H */
+++ /dev/null
-%{
-#include "expr/statistics.h"
-
-#ifdef SWIGJAVA
-
-#include "bindings/java_iterator_adapter.h"
-#include "bindings/java_stream_adapters.h"
-
-#endif /* SWIGJAVA */
-%}
-
-%rename(assign) CVC4::Statistics::operator=(const StatisticsBase&);
-%rename(assign) CVC4::Statistics::operator=(const Statistics& stats);
-
-#ifdef SWIGJAVA
-
-// Instead of StatisticsBase::begin() and end(), create an
-// iterator() method on the Java side that returns a Java-style
-// Iterator.
-%ignore CVC4::StatisticsBase::begin();
-%ignore CVC4::StatisticsBase::end();
-%ignore CVC4::StatisticsBase::begin() const;
-%ignore CVC4::StatisticsBase::end() const;
-%extend CVC4::StatisticsBase {
- CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> iterator() {
- return CVC4::JavaIteratorAdapter<CVC4::StatisticsBase>(*$self);
- }
-}
-
-// StatisticsBase is "iterable" on the Java side
-%typemap(javainterfaces) CVC4::StatisticsBase "java.lang.Iterable<Object[]>";
-
-// the JavaIteratorAdapter should not be public, and implements Iterator
-%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> "class";
-%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> "java.util.Iterator<Object[]>";
-// add some functions to the Java side (do it here because there's no way to do these in C++)
-%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> "
- public void remove() {
- throw new java.lang.UnsupportedOperationException();
- }
-
- public Object[] next() {
- if(hasNext()) {
- return getNext();
- } else {
- throw new java.util.NoSuchElementException();
- }
- }
-"
-// getNext() just allows C++ iterator access from Java-side next(), make it private
-%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::StatisticsBase>::getNext() "private";
-
-// map the types appropriately. for statistics, the "payload" of the iterator is an Object[].
-// These Object arrays are always of two elements, the first is a String and the second an
-// SExpr. (On the C++ side, it is a std::pair<std::string, SExpr>.)
-%typemap(jni) CVC4::StatisticsBase::const_iterator::value_type "jobjectArray";
-%typemap(jtype) CVC4::StatisticsBase::const_iterator::value_type "java.lang.Object[]";
-%typemap(jstype) CVC4::StatisticsBase::const_iterator::value_type "java.lang.Object[]";
-%typemap(javaout) CVC4::StatisticsBase::const_iterator::value_type { return $jnicall; }
-%typemap(out) CVC4::StatisticsBase::const_iterator::value_type {
- $result = jenv->NewObjectArray(2, jenv->FindClass("java/lang/Object"), $null);
- jenv->SetObjectArrayElement($result, 0, jenv->NewStringUTF($1.first.c_str()));
- jclass clazz = jenv->FindClass("edu/nyu/acsys/CVC4/SExpr");
- jmethodID methodid = jenv->GetMethodID(clazz, "<init>", "(JZ)V");
- jenv->SetObjectArrayElement($result, 1, jenv->NewObject(clazz, methodid, reinterpret_cast<long>(new CVC4::SExpr($1.second)), true));
- };
-
-#endif /* SWIGJAVA */
-
-%include "expr/statistics.h"
-
-#ifdef SWIGJAVA
-
-%include "bindings/java_iterator_adapter.h"
-%include "bindings/java_stream_adapters.h"
-
-%template(JavaIteratorAdapter_StatisticsBase) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase>;
-
-#endif /* SWIGJAVA */
+++ /dev/null
-/********************* */
-/*! \file statistics_registry.cpp
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Kshitij Bansal, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "expr/statistics_registry.h"
-
-#include "base/cvc4_assert.h"
-#include "expr/expr_manager.h"
-#include "lib/clock_gettime.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
-
-
-#ifdef CVC4_STATISTICS_ON
-# define __CVC4_USE_STATISTICS true
-#else
-# define __CVC4_USE_STATISTICS false
-#endif
-
-#warning "TODO: Make StatisticsRegistry non-public again."
-#warning "TODO: Make TimerStat non-public again."
-
-namespace CVC4 {
-
-/** Construct a statistics registry */
-StatisticsRegistry::StatisticsRegistry(const std::string& name)
- throw(CVC4::IllegalArgumentException) :
- Stat(name) {
-
- d_prefix = name;
- if(__CVC4_USE_STATISTICS) {
- PrettyCheckArgument(d_name.find(s_regDelim) == std::string::npos, name,
- "StatisticsRegistry names cannot contain the string \"%s\"",
- s_regDelim.c_str());
- }
-}
-
-namespace stats {
-
-// This is a friend of SmtEngine, just to reach in and get it.
-// this isn't a class function because then there's a cyclic
-// dependence.
-inline StatisticsRegistry* getStatisticsRegistry(SmtEngine* smt) {
- return smt->d_statisticsRegistry;
-}
-
-inline StatisticsRegistry* getStatisticsRegistry(ExprManager* em) {
- return em->getStatisticsRegistry();
-}
-
-}/* CVC4::stats namespace */
-
-StatisticsRegistry* StatisticsRegistry::current() {
- return stats::getStatisticsRegistry(smt::currentSmtEngine());
-}
-
-void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentException) {
-#ifdef CVC4_STATISTICS_ON
- StatSet& stats = current()->d_stats;
- PrettyCheckArgument(stats.find(s) == stats.end(), s,
- "Statistic `%s' was already registered with this registry.",
- s->getName().c_str());
- stats.insert(s);
-#endif /* CVC4_STATISTICS_ON */
-}/* StatisticsRegistry::registerStat() */
-
-void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException) {
-#ifdef CVC4_STATISTICS_ON
- StatSet& stats = current()->d_stats;
- PrettyCheckArgument(stats.find(s) != stats.end(), s,
- "Statistic `%s' was not registered with this registry.",
- s->getName().c_str());
- stats.erase(s);
-#endif /* CVC4_STATISTICS_ON */
-}/* StatisticsRegistry::unregisterStat() */
-
-void StatisticsRegistry::registerStat_(Stat* s) throw(CVC4::IllegalArgumentException) {
-#ifdef CVC4_STATISTICS_ON
- PrettyCheckArgument(d_stats.find(s) == d_stats.end(), s);
- d_stats.insert(s);
-#endif /* CVC4_STATISTICS_ON */
-}/* StatisticsRegistry::registerStat_() */
-
-void StatisticsRegistry::unregisterStat_(Stat* s) throw(CVC4::IllegalArgumentException) {
-#ifdef CVC4_STATISTICS_ON
- PrettyCheckArgument(d_stats.find(s) != d_stats.end(), s);
- d_stats.erase(s);
-#endif /* CVC4_STATISTICS_ON */
-}/* StatisticsRegistry::unregisterStat_() */
-
-void StatisticsRegistry::flushStat(std::ostream &out) const {
-#ifdef CVC4_STATISTICS_ON
- flushInformation(out);
-#endif /* CVC4_STATISTICS_ON */
-}
-
-void StatisticsRegistry::flushInformation(std::ostream &out) const {
-#ifdef CVC4_STATISTICS_ON
- this->StatisticsBase::flushInformation(out);
-#endif /* CVC4_STATISTICS_ON */
-}
-
-void TimerStat::start() {
- if(__CVC4_USE_STATISTICS) {
- PrettyCheckArgument(!d_running, *this, "timer already running");
- clock_gettime(CLOCK_MONOTONIC, &d_start);
- d_running = true;
- }
-}/* TimerStat::start() */
-
-void TimerStat::stop() {
- if(__CVC4_USE_STATISTICS) {
- PrettyCheckArgument(d_running, *this, "timer not running");
- ::timespec end;
- clock_gettime(CLOCK_MONOTONIC, &end);
- d_data += end - d_start;
- d_running = false;
- }
-}/* TimerStat::stop() */
-
-bool TimerStat::running() const {
- return d_running;
-}/* TimerStat::running() */
-
-timespec TimerStat::getData() const {
- ::timespec data = d_data;
- if(__CVC4_USE_STATISTICS && d_running) {
- ::timespec end;
- clock_gettime(CLOCK_MONOTONIC, &end);
- data += end - d_start;
- }
- return data;
-}
-
-SExpr TimerStat::getValue() const {
- ::timespec data = d_data;
- if(__CVC4_USE_STATISTICS && d_running) {
- ::timespec end;
- clock_gettime(CLOCK_MONOTONIC, &end);
- data += end - d_start;
- }
- std::stringstream ss;
- ss << std::fixed << std::setprecision(8) << data;
- return SExpr(Rational::fromDecimal(ss.str()));
-}/* TimerStat::getValue() */
-
-RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) :
- d_reg(stats::getStatisticsRegistry(&em)),
- d_stat(stat) {
- d_reg->registerStat_(d_stat);
-}
-
-RegisterStatistic::RegisterStatistic(SmtEngine& smt, Stat* stat) :
- d_reg(stats::getStatisticsRegistry(&smt)),
- d_stat(stat) {
- d_reg->registerStat_(d_stat);
-}
-
-
-
-}/* CVC4 namespace */
-
-#undef __CVC4_USE_STATISTICS
+++ /dev/null
-/********************* */
-/*! \file statistics_registry.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Tim King
- ** Minor contributors (to current version): Kshitij Bansal
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Statistics utility classes
- **
- ** Statistics utility classes, including classes for holding (and referring
- ** to) statistics, the statistics registry, and some other associated
- ** classes.
- **/
-
-#include "cvc4_private_library.h"
-
-#ifndef __CVC4__STATISTICS_REGISTRY_H
-#define __CVC4__STATISTICS_REGISTRY_H
-
-#include <stdint.h>
-
-#include <cassert>
-#include <ctime>
-#include <iomanip>
-#include <map>
-#include <sstream>
-#include <vector>
-
-#include "base/exception.h"
-#include "expr/statistics.h"
-#include "lib/clock_gettime.h"
-
-namespace CVC4 {
-
-#ifdef CVC4_STATISTICS_ON
-# define __CVC4_USE_STATISTICS true
-#else
-# define __CVC4_USE_STATISTICS false
-#endif
-
-class ExprManager;
-class SmtEngine;
-
-/**
- * The base class for all statistics.
- *
- * 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 Stat {
-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
- * statistic delimiter string.
- */
- Stat(const std::string& name) throw(CVC4::IllegalArgumentException) :
- d_name(name) {
- if(__CVC4_USE_STATISTICS) {
- CheckArgument(d_name.find(", ") == std::string::npos, name,
- "Statistics names cannot include a comma (',')");
- }
- }
-
- /** Destruct a statistic. This base-class version does nothing. */
- virtual ~Stat() {}
-
- /**
- * Flush the value of this statistic to an output stream. Should
- * finish the output with an end-of-line character.
- */
- virtual void flushInformation(std::ostream& out) const = 0;
-
- /**
- * 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
- */
- virtual void flushStat(std::ostream& out) const {
- if(__CVC4_USE_STATISTICS) {
- out << d_name << ", ";
- flushInformation(out);
- }
- }
-
- /** Get the name of this statistic. */
- const std::string& getName() const {
- return d_name;
- }
-
- /** Get the value of this statistic as a string. */
- virtual SExpr getValue() const {
- std::stringstream ss;
- flushInformation(ss);
- return SExpr(ss.str());
- }
-
-};/* class Stat */
-
-// A generic way of making a SExpr from templated stats code.
-// for example, the uint64_t version ensures that we create
-// Integer-SExprs for ReadOnlyDataStats (like those inside
-// Minisat) without having to specialize the entire
-// ReadOnlyDataStat class template.
-template <class T>
-inline SExpr mkSExpr(const T& x) {
- std::stringstream ss;
- ss << x;
- return SExpr(ss.str());
-}
-
-template <>
-inline SExpr mkSExpr(const uint64_t& x) {
- return SExpr(Integer(x));
-}
-
-template <>
-inline SExpr mkSExpr(const int64_t& x) {
- return SExpr(Integer(x));
-}
-
-template <>
-inline SExpr mkSExpr(const int& x) {
- return SExpr(Integer(x));
-}
-
-template <>
-inline SExpr mkSExpr(const Integer& x) {
- return SExpr(x);
-}
-
-template <>
-inline SExpr mkSExpr(const double& x) {
- // roundabout way to get a Rational from a double
- std::stringstream ss;
- ss << std::fixed << std::setprecision(8) << x;
- return SExpr(Rational::fromDecimal(ss.str()));
-}
-
-template <>
-inline SExpr mkSExpr(const Rational& x) {
- return SExpr(x);
-}
-
-/**
- * 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, 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:
- * std::ostream& operator<<(std::ostream&, const T&)
- */
-template <class T>
-class ReadOnlyDataStat : public Stat {
-public:
- /** The "payload" type of this data statistic (that is, T). */
- typedef T payload_t;
-
- /** Construct a read-only data statistic with the given name. */
- ReadOnlyDataStat(const std::string& name) :
- Stat(name) {
- }
-
- /** Get the value of the statistic. */
- virtual T getData() const = 0;
-
- /** Flush the value of the statistic to the given output stream. */
- void flushInformation(std::ostream& out) const {
- if(__CVC4_USE_STATISTICS) {
- out << getData();
- }
- }
-
- SExpr getValue() const {
- return mkSExpr(getData());
- }
-
-};/* class ReadOnlyDataStat<T> */
-
-
-/**
- * A data statistic class. This class extends a read-only data statistic
- * with assignment (the statistic can be set as well as read). This class
- * adds to the read-only case a pure virtual function setData(), thus
- * providing the basic interface for a data statistic: getData() to get the
- * statistic value, and setData() to set it.
- *
- * As with the read-only data statistic class, template class T must have
- * stream insertion operation defined:
- * std::ostream& operator<<(std::ostream&, const T&)
- */
-template <class T>
-class DataStat : public ReadOnlyDataStat<T> {
-public:
-
- /** Construct a data statistic with the given name. */
- DataStat(const std::string& name) :
- ReadOnlyDataStat<T>(name) {
- }
-
- /** Set the data statistic. */
- virtual void setData(const T&) = 0;
-
-};/* class DataStat<T> */
-
-
-/**
- * A data statistic that references a data cell of type T,
- * implementing getData() by referencing that memory cell, and
- * setData() by reassigning the statistic to point to the new
- * data cell. The referenced data cell is kept as a const
- * reference, meaning the referenced data is never actually
- * modified by this class (it must be externally modified for
- * a reference statistic to make sense). A common use for
- * this type of statistic is to output a statistic that is kept
- * outside the statistics package (for example, one that's kept
- * by a theory implementation for internal heuristic purposes,
- * which is important to keep even if statistics are turned off).
- *
- * Template class T must have an assignment operator=().
- */
-template <class T>
-class ReferenceStat : public DataStat<T> {
-private:
- /** The referenced data cell */
- const T* d_data;
-
-public:
- /**
- * Construct a reference stat with the given name and a reference
- * to NULL.
- */
- ReferenceStat(const std::string& name) :
- DataStat<T>(name),
- d_data(NULL) {
- }
-
- /**
- * Construct a reference stat with the given name and a reference to
- * the given data.
- */
- ReferenceStat(const std::string& name, const T& data) :
- DataStat<T>(name),
- d_data(NULL) {
- setData(data);
- }
-
- /** Set this reference statistic to refer to the given data cell. */
- void setData(const T& t) {
- if(__CVC4_USE_STATISTICS) {
- d_data = &t;
- }
- }
-
- /** Get the value of the referenced data cell. */
- T getData() const {
- return *d_data;
- }
-
-};/* class ReferenceStat<T> */
-
-
-/**
- * A data statistic that keeps a T and sets it with setData().
- *
- * Template class T must have an operator=() and a copy constructor.
- */
-template <class T>
-class BackedStat : public DataStat<T> {
-protected:
- /** The internally-kept statistic value */
- T d_data;
-
-public:
-
- /** Construct a backed statistic with the given name and initial value. */
- BackedStat(const std::string& name, const T& init) :
- DataStat<T>(name),
- d_data(init) {
- }
-
- /** Set the underlying data value to the given value. */
- void setData(const T& t) {
- if(__CVC4_USE_STATISTICS) {
- d_data = t;
- }
- }
-
- /** Identical to setData(). */
- BackedStat<T>& operator=(const T& t) {
- if(__CVC4_USE_STATISTICS) {
- d_data = t;
- }
- return *this;
- }
-
- /** Get the underlying data value. */
- T getData() const {
- return d_data;
- }
-
-};/* class BackedStat<T> */
-
-
-/**
- * A wrapper Stat for another Stat.
- *
- * This type of Stat is useful in cases where a module (like the
- * CongruenceClosure module) might keep its own statistics, but might
- * be instantiated in many contexts by many clients. This makes such
- * a statistic inappopriate to register with the StatisticsRegistry
- * directly, as all would be output with the same name (and may be
- * unregistered too quickly anyway). A WrappedStat allows the calling
- * client (say, TheoryUF) to wrap the Stat from the client module,
- * giving it a globally unique name.
- */
-template <class Stat>
-class WrappedStat : public ReadOnlyDataStat<typename Stat::payload_t> {
- typedef typename Stat::payload_t T;
-
- const ReadOnlyDataStat<T>& d_stat;
-
- /** Private copy constructor undefined (no copy permitted). */
- WrappedStat(const WrappedStat&) CVC4_UNDEFINED;
- /** Private assignment operator undefined (no copy permitted). */
- WrappedStat<T>& operator=(const WrappedStat&) CVC4_UNDEFINED;
-
-public:
-
- /**
- * Construct a wrapped statistic with the given name that wraps the
- * given statistic.
- */
- WrappedStat(const std::string& name, const ReadOnlyDataStat<T>& stat) :
- ReadOnlyDataStat<T>(name),
- d_stat(stat) {
- }
-
- /** Get the data of the underlying (wrapped) statistic. */
- T getData() const {
- return d_stat.getData();
- }
-
- SExpr getValue() const {
- return d_stat.getValue();
- }
-
-};/* class WrappedStat<T> */
-
-/**
- * A backed integer-valued (64-bit signed) statistic.
- * This doesn't functionally differ from its base class BackedStat<int64_t>,
- * except for adding convenience functions for dealing with integers.
- */
-class IntStat : public BackedStat<int64_t> {
-public:
-
- /**
- * Construct an integer-valued statistic with the given name and
- * initial value.
- */
- IntStat(const std::string& name, int64_t init) :
- BackedStat<int64_t>(name, init) {
- }
-
- /** Increment the underlying integer statistic. */
- IntStat& operator++() {
- if(__CVC4_USE_STATISTICS) {
- ++d_data;
- }
- return *this;
- }
-
- /** Increment the underlying integer statistic by the given amount. */
- IntStat& operator+=(int64_t val) {
- if(__CVC4_USE_STATISTICS) {
- d_data += val;
- }
- return *this;
- }
-
- /** Keep the maximum of the current statistic value and the given one. */
- void maxAssign(int64_t val) {
- if(__CVC4_USE_STATISTICS) {
- if(d_data < val) {
- d_data = val;
- }
- }
- }
-
- /** Keep the minimum of the current statistic value and the given one. */
- void minAssign(int64_t val) {
- if(__CVC4_USE_STATISTICS) {
- if(d_data > val) {
- d_data = val;
- }
- }
- }
-
- SExpr getValue() const {
- return SExpr(Integer(d_data));
- }
-
-};/* class IntStat */
-
-template <class T>
-class SizeStat : public Stat {
-private:
- const T& d_sized;
-public:
- SizeStat(const std::string&name, const T& sized) :
- Stat(name), d_sized(sized) {}
- ~SizeStat() {}
-
- void flushInformation(std::ostream& out) const {
- out << d_sized.size();
- }
-
- SExpr getValue() const {
- return SExpr(Integer(d_sized.size()));
- }
-
-};/* class SizeStat */
-
-/**
- * The value for an AverageStat is the running average of (e1, e_2, ..., e_n),
- * (e1 + e_2 + ... + e_n)/n,
- * where e_i is an entry added by an addEntry(e_i) call.
- * The value is initially always 0.
- * (This is to avoid making parsers confused.)
- *
- * A call to setData() will change the running average but not reset the
- * running count, so should generally be avoided. Call addEntry() to add
- * an entry to the average calculation.
- */
-class AverageStat : public BackedStat<double> {
-private:
- /**
- * The number of accumulations of the running average that we
- * 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), d_sum(0.0) {
- }
-
- /** Add an entry to the running-average calculation. */
- void addEntry(double e) {
- if(__CVC4_USE_STATISTICS) {
- ++d_count;
- d_sum += e;
- setData(d_sum / d_count);
- }
- }
-
- SExpr getValue() const {
- std::stringstream ss;
- ss << std::fixed << std::setprecision(8) << d_data;
- return SExpr(Rational::fromDecimal(ss.str()));
- }
-
-};/* class AverageStat */
-
-/** A statistic that contains a SExpr. */
-class SExprStat : public Stat {
-private:
- SExpr d_data;
-
-public:
-
- /**
- * Construct a SExpr-valued statistic with the given name and
- * initial value.
- */
- SExprStat(const std::string& name, const SExpr& init) :
- Stat(name), d_data(init){}
-
- virtual void flushInformation(std::ostream& out) const {
- out << d_data << std::endl;
- }
-
- SExpr getValue() const {
- return d_data;
- }
-
-};/* class SExprStat */
-
-template <class T>
-class ListStat : public Stat {
-private:
- typedef std::vector<T> List;
- List d_list;
-public:
-
- /**
- * Construct an integer-valued statistic with the given name and
- * initial value.
- */
- ListStat(const std::string& name) : Stat(name) {}
- ~ListStat() {}
-
- void flushInformation(std::ostream& out) const{
- if(__CVC4_USE_STATISTICS) {
- typename List::const_iterator i = d_list.begin(), end = d_list.end();
- out << "[";
- if(i != end){
- out << *i;
- ++i;
- for(; i != end; ++i){
- out << ", " << *i;
- }
- }
- out << "]";
- }
- }
-
- ListStat& operator<<(const T& val){
- if(__CVC4_USE_STATISTICS) {
- d_list.push_back(val);
- }
- return (*this);
- }
-
-};/* class ListStat */
-
-template <class T>
-class HistogramStat : public Stat {
-private:
- typedef std::map<T, unsigned int> Histogram;
- Histogram d_hist;
-public:
-
- /** Construct a histogram of a stream of entries. */
- HistogramStat(const std::string& name) : Stat(name) {}
- ~HistogramStat() {}
-
- void flushInformation(std::ostream& out) const{
- if(__CVC4_USE_STATISTICS) {
- typename Histogram::const_iterator i = d_hist.begin();
- typename Histogram::const_iterator end = d_hist.end();
- out << "[";
- while(i != end){
- const T& key = (*i).first;
- unsigned int count = (*i).second;
- out << "("<<key<<" : "<<count<< ")";
- ++i;
- if(i != end){
- out << ", ";
- }
- }
- out << "]";
- }
- }
-
- HistogramStat& operator<<(const T& val){
- if(__CVC4_USE_STATISTICS) {
- if(d_hist.find(val) == d_hist.end()){
- d_hist.insert(std::make_pair(val,0));
- }
- d_hist[val]++;
- }
- return (*this);
- }
-
-};/* class HistogramStat */
-
-/****************************************************************************/
-/* 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 StatisticsBase, public Stat {
-private:
-
- /** Private copy constructor undefined (no copy permitted). */
- StatisticsRegistry(const StatisticsRegistry&) CVC4_UNDEFINED;
-
-public:
-
- /** Construct an nameless statistics registry */
- StatisticsRegistry() {}
-
- /** Construct a statistics registry */
- StatisticsRegistry(const std::string& name)
- throw(CVC4::IllegalArgumentException);
-
- /**
- * Set the name of this statistic registry, used as prefix during
- * output. (This version overrides StatisticsBase::setPrefix().)
- */
- void setPrefix(const std::string& name) {
- d_prefix = d_name = name;
- }
-
-#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST))
- /** Get a pointer to the current statistics registry */
- static StatisticsRegistry* current();
-#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) */
-
- /** Overridden to avoid the name being printed */
- void flushStat(std::ostream &out) const;
-
- virtual void flushInformation(std::ostream& out) const;
-
- SExpr getValue() const {
- std::vector<SExpr> v;
- for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) {
- std::vector<SExpr> w;
- w.push_back(SExpr((*i)->getName()));
- w.push_back((*i)->getValue());
- v.push_back(SExpr(w));
- }
- return SExpr(v);
- }
-
-#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST))
- /** Register a new statistic, making it active. */
- static void registerStat(Stat* s) throw(CVC4::IllegalArgumentException);
-
- /** Unregister an active statistic, making it inactive. */
- static void unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException);
-#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB) */
-
- /** Register a new statistic */
- void registerStat_(Stat* s) throw(CVC4::IllegalArgumentException);
-
- /** Unregister a new statistic */
- void unregisterStat_(Stat* s) throw(CVC4::IllegalArgumentException);
-
-};/* class StatisticsRegistry */
-
-}/* CVC4 namespace */
-
-/****************************************************************************/
-/* Some utility functions for timespec */
-/****************************************************************************/
-
-inline std::ostream& operator<<(std::ostream& os, const timespec& t);
-
-/** Compute the sum of two timespecs. */
-inline timespec& operator+=(timespec& a, const timespec& b) {
- using namespace CVC4;
- // assumes a.tv_nsec and b.tv_nsec are in range
- const long nsec_per_sec = 1000000000L; // one thousand million
- CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a);
- CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b);
- a.tv_sec += b.tv_sec;
- long nsec = a.tv_nsec + b.tv_nsec;
- assert(nsec >= 0);
- if(nsec < 0) {
- nsec += nsec_per_sec;
- --a.tv_sec;
- }
- if(nsec >= nsec_per_sec) {
- nsec -= nsec_per_sec;
- ++a.tv_sec;
- }
- assert(nsec >= 0 && nsec < nsec_per_sec);
- a.tv_nsec = nsec;
- return a;
-}
-
-/** Compute the difference of two timespecs. */
-inline timespec& operator-=(timespec& a, const timespec& b) {
- using namespace CVC4;
- // assumes a.tv_nsec and b.tv_nsec are in range
- const long nsec_per_sec = 1000000000L; // one thousand million
- CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a);
- CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b);
- a.tv_sec -= b.tv_sec;
- long nsec = a.tv_nsec - b.tv_nsec;
- if(nsec < 0) {
- nsec += nsec_per_sec;
- --a.tv_sec;
- }
- if(nsec >= nsec_per_sec) {
- nsec -= nsec_per_sec;
- ++a.tv_sec;
- }
- assert(nsec >= 0 && nsec < nsec_per_sec);
- a.tv_nsec = nsec;
- return a;
-}
-
-/** Add two timespecs. */
-inline timespec operator+(const timespec& a, const timespec& b) {
- timespec result = a;
- return result += b;
-}
-
-/** Subtract two timespecs. */
-inline timespec operator-(const timespec& a, const timespec& b) {
- timespec result = a;
- return result -= b;
-}
-
-/** Compare two timespecs for equality. */
-inline bool operator==(const timespec& a, const timespec& b) {
- // assumes a.tv_nsec and b.tv_nsec are in range
- return a.tv_sec == b.tv_sec && a.tv_nsec == b.tv_nsec;
-}
-
-/** Compare two timespecs for disequality. */
-inline bool operator!=(const timespec& a, const timespec& b) {
- // assumes a.tv_nsec and b.tv_nsec are in range
- return !(a == b);
-}
-
-/** Compare two timespecs, returning true iff a < b. */
-inline bool operator<(const timespec& a, const timespec& b) {
- // assumes a.tv_nsec and b.tv_nsec are in range
- return a.tv_sec < b.tv_sec ||
- (a.tv_sec == b.tv_sec && a.tv_nsec < b.tv_nsec);
-}
-
-/** Compare two timespecs, returning true iff a > b. */
-inline bool operator>(const timespec& a, const timespec& b) {
- // assumes a.tv_nsec and b.tv_nsec are in range
- return a.tv_sec > b.tv_sec ||
- (a.tv_sec == b.tv_sec && a.tv_nsec > b.tv_nsec);
-}
-
-/** Compare two timespecs, returning true iff a <= b. */
-inline bool operator<=(const timespec& a, const timespec& b) {
- // assumes a.tv_nsec and b.tv_nsec are in range
- return !(a > b);
-}
-
-/** Compare two timespecs, returning true iff a >= b. */
-inline bool operator>=(const timespec& a, const timespec& b) {
- // assumes a.tv_nsec and b.tv_nsec are in range
- return !(a < b);
-}
-
-/** Output a timespec on an output stream. */
-inline std::ostream& operator<<(std::ostream& os, const timespec& t) {
- // assumes t.tv_nsec is in range
- return os << t.tv_sec << "."
- << std::setfill('0') << std::setw(9) << std::right << t.tv_nsec;
-}
-
-namespace CVC4 {
-
-class CodeTimer;
-
-/**
- * A timer statistic. The timer can be started and stopped
- * arbitrarily, like a stopwatch; the value of the statistic at the
- * end is the accumulated time over all (start,stop) pairs.
- */
-class CVC4_PUBLIC TimerStat : public BackedStat<timespec> {
-
- // strange: timespec isn't placed in 'std' namespace ?!
- /** The last start time of this timer */
- timespec d_start;
-
- /** Whether this timer is currently running */
- bool d_running;
-
-public:
-
- typedef CVC4::CodeTimer CodeTimer;
-
- /**
- * Construct a timer statistic with the given name. Newly-constructed
- * timers have a 0.0 value and are not running.
- */
- TimerStat(const std::string& name) :
- BackedStat< timespec >(name, timespec()),
- d_running(false) {
- /* timespec is POD and so may not be initialized to zero;
- * here, ensure it is */
- d_data.tv_sec = d_data.tv_nsec = 0;
- }
-
- /** Start the timer. */
- void start();
-
- /**
- * Stop the timer and update the statistic value with the
- * accumulated time.
- */
- void stop();
-
- /** If the timer is currently running */
- bool running() const;
-
- timespec getData() const;
-
- SExpr getValue() const;
-
-};/* class TimerStat */
-
-/**
- * Utility class to make it easier to call stop() at the end of a
- * code block. When constructed, it starts the timer. When
- * destructed, it stops the timer.
- */
-class CodeTimer {
- TimerStat& d_timer;
- bool d_reentrant;
-
- /** Private copy constructor undefined (no copy permitted). */
- CodeTimer(const CodeTimer& timer) CVC4_UNDEFINED;
- /** Private assignment operator undefined (no copy permitted). */
- CodeTimer& operator=(const CodeTimer& timer) CVC4_UNDEFINED;
-
-public:
- CodeTimer(TimerStat& timer, bool allow_reentrant = false) : d_timer(timer), d_reentrant(false) {
- if(!allow_reentrant || !(d_reentrant = d_timer.running())) {
- d_timer.start();
- }
- }
- ~CodeTimer() {
- if(!d_reentrant) {
- d_timer.stop();
- }
- }
-};/* class CodeTimer */
-
-/**
- * To use a statistic, you need to declare it, initialize it in your
- * constructor, register it in your constructor, and deregister it in
- * your destructor. Instead, this macro does it all for you (and
- * therefore also keeps the statistic type, field name, and output
- * string all in the same place in your class's header. Its use is
- * like in this example, which takes the place of the declaration of a
- * statistics field "d_checkTimer":
- *
- * KEEP_STATISTIC(TimerStat, d_checkTimer, "theory::uf::checkTime");
- *
- * If any args need to be passed to the constructor, you can specify
- * them after the string.
- *
- * The macro works by creating a nested class type, derived from the
- * statistic type you give it, which declares a registry-aware
- * constructor/destructor pair.
- */
-#define KEEP_STATISTIC(_StatType, _StatField, _StatName, _CtorArgs...) \
- struct Statistic_##_StatField : public _StatType { \
- Statistic_##_StatField() : _StatType(_StatName, ## _CtorArgs) { \
- StatisticsRegistry::registerStat(this); \
- } \
- ~Statistic_##_StatField() { \
- StatisticsRegistry::unregisterStat(this); \
- } \
- } _StatField
-
-/**
- * Resource-acquisition-is-initialization idiom for statistics
- * registry. Useful for stack-based statistics (like in the driver).
- * Generally, for statistics kept in a member field of class, it's
- * better to use the above KEEP_STATISTIC(), which does declaration of
- * the member, construction of the statistic, and
- * registration/unregistration. This RAII class only does
- * registration and unregistration.
- */
-class RegisterStatistic {
-
- StatisticsRegistry* d_reg;
- Stat* d_stat;
-
-public:
-
-#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST))
- RegisterStatistic(Stat* stat) :
- d_reg(StatisticsRegistry::current()),
- d_stat(stat) {
- if(d_reg != NULL) {
- throw CVC4::Exception("There is no current statistics registry!");
- }
- StatisticsRegistry::registerStat(d_stat);
- }
-#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) */
-
- RegisterStatistic(StatisticsRegistry* reg, Stat* stat) :
- d_reg(reg),
- d_stat(stat) {
- CheckArgument(reg != NULL, reg,
- "You need to specify a statistics registry"
- "on which to set the statistic");
- d_reg->registerStat_(d_stat);
- }
-
- RegisterStatistic(ExprManager& em, Stat* stat);
-
- RegisterStatistic(SmtEngine& smt, Stat* stat);
-
- ~RegisterStatistic() {
- d_reg->unregisterStat_(d_stat);
- }
-
-};/* class RegisterStatistic */
-
-#undef __CVC4_USE_STATISTICS
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__STATISTICS_REGISTRY_H */
#include <string>
#include "expr/expr_manager.h"
-#include "expr/statistics_registry.h"
#include "options/options.h"
#include "smt/smt_engine.h"
#include "smt_util/command.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace main {
assert(d_threadOptions.size() == d_numThreads);
d_statLastWinner.setData(d_lastWinner);
- d_stats.registerStat_(&d_statLastWinner);
- d_stats.registerStat_(&d_statWaitTime);
+ d_stats.registerStat(&d_statLastWinner);
+ d_stats.registerStat(&d_statWaitTime);
/* Duplication, individualization */
d_exprMgrs.push_back(&d_exprMgr);
d_exprMgrs.clear();
d_smts.clear();
- d_stats.unregisterStat_(&d_statLastWinner);
- d_stats.unregisterStat_(&d_statWaitTime);
+ d_stats.unregisterStat(&d_statLastWinner);
+ d_stats.unregisterStat(&d_statWaitTime);
}
void CommandExecutorPortfolio::lemmaSharingInit()
#include "base/output.h"
#include "expr/expr_iomanip.h"
#include "expr/expr_manager.h"
-#include "expr/statistics_registry.h"
#include "main/command_executor.h"
#ifdef PORTFOLIO_BUILD
#include "smt_util/command.h"
#include "util/configuration.h"
#include "util/result.h"
+#include "util/statistics_registry.h"
using namespace std;
using namespace CVC4;
#include "base/output.h"
#include "expr/expr_manager.h"
-#include "expr/statistics.h"
#include "main/command_executor.h"
#include "main/interactive_shell.h"
#include "options/base_options.h"
#include "smt_util/command.h"
#include "util/configuration.h"
#include "util/result.h"
+#include "util/statistics.h"
using namespace std;
using namespace CVC4;
#include "base/tls.h"
#include "cvc4autoconfig.h"
#include "expr/expr_manager.h"
-#include "expr/statistics.h"
-#include "expr/statistics_registry.h"
#include "options/options.h"
#include "smt/smt_engine.h"
+#include "util/statistics.h"
+#include "util/statistics_registry.h"
#ifndef __CVC4__MAIN__MAIN_H
#define __CVC4__MAIN__MAIN_H
#include <boost/exception_ptr.hpp>
#include "base/output.h"
-#include "expr/statistics_registry.h"
#include "options/options.h"
#include "smt/smt_engine.h"
#include "util/result.h"
-
+#include "util/statistics_registry.h"
namespace CVC4 {
#include <boost/function.hpp>
#include <utility>
-#include "expr/statistics_registry.h"
#include "options/options.h"
#include "smt/smt_engine.h"
#include "smt_util/command.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
#include "base/exception.h"
#include "base/tls.h"
#include "cvc4autoconfig.h"
-#include "expr/statistics.h"
#include "main/command_executor.h"
#include "main/main.h"
#include "options/base_options.h"
#include "options/options.h"
#include "smt/smt_engine.h"
+#include "util/statistics.h"
using CVC4::Exception;
using namespace std;
**/
#include "prop/bvminisat/bvminisat.h"
+
#include "prop/bvminisat/simp/SimpSolver.h"
+#include "util/statistics_registry.h"
-using namespace CVC4;
-using namespace prop;
+namespace CVC4 {
+namespace prop {
-BVMinisatSatSolver::BVMinisatSatSolver(context::Context* mainSatContext, const std::string& name)
+BVMinisatSatSolver::BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name)
: context::ContextNotifyObj(mainSatContext, false),
d_minisat(new BVMinisat::SimpSolver(mainSatContext)),
d_minisatNotify(0),
d_assertionsCount(0),
d_assertionsRealCount(mainSatContext, 0),
d_lastPropagation(mainSatContext, 0),
- d_statistics(name)
+ d_statistics(registry, name)
{
- d_statistics.init(d_minisat);
+ d_statistics.init(d_minisat);
}
// Satistics for BVMinisatSatSolver
-BVMinisatSatSolver::Statistics::Statistics(const std::string& prefix) :
- d_statStarts("theory::bv::"+prefix+"bvminisat::starts"),
- d_statDecisions("theory::bv::"+prefix+"bvminisat::decisions"),
- d_statRndDecisions("theory::bv::"+prefix+"bvminisat::rnd_decisions"),
- d_statPropagations("theory::bv::"+prefix+"bvminisat::propagations"),
- d_statConflicts("theory::bv::"+prefix+"bvminisat::conflicts"),
- d_statClausesLiterals("theory::bv::"+prefix+"bvminisat::clauses_literals"),
- d_statLearntsLiterals("theory::bv::"+prefix+"bvminisat::learnts_literals"),
- d_statMaxLiterals("theory::bv::"+prefix+"bvminisat::max_literals"),
- d_statTotLiterals("theory::bv::"+prefix+"bvminisat::tot_literals"),
- d_statEliminatedVars("theory::bv::"+prefix+"bvminisat::eliminated_vars"),
- d_statCallsToSolve("theory::bv::"+prefix+"bvminisat::calls_to_solve", 0),
- d_statSolveTime("theory::bv::"+prefix+"bvminisat::solve_time", 0),
- d_registerStats(!prefix.empty())
+BVMinisatSatSolver::Statistics::Statistics(StatisticsRegistry* registry, const std::string& prefix)
+ : d_registry(registry),
+ d_statStarts("theory::bv::"+prefix+"bvminisat::starts"),
+ d_statDecisions("theory::bv::"+prefix+"bvminisat::decisions"),
+ d_statRndDecisions("theory::bv::"+prefix+"bvminisat::rnd_decisions"),
+ d_statPropagations("theory::bv::"+prefix+"bvminisat::propagations"),
+ d_statConflicts("theory::bv::"+prefix+"bvminisat::conflicts"),
+ d_statClausesLiterals("theory::bv::"+prefix+"bvminisat::clauses_literals"),
+ d_statLearntsLiterals("theory::bv::"+prefix+"bvminisat::learnts_literals"),
+ d_statMaxLiterals("theory::bv::"+prefix+"bvminisat::max_literals"),
+ d_statTotLiterals("theory::bv::"+prefix+"bvminisat::tot_literals"),
+ d_statEliminatedVars("theory::bv::"+prefix+"bvminisat::eliminated_vars"),
+ d_statCallsToSolve("theory::bv::"+prefix+"bvminisat::calls_to_solve", 0),
+ d_statSolveTime("theory::bv::"+prefix+"bvminisat::solve_time", 0),
+ d_registerStats(!prefix.empty())
{
- if (!d_registerStats)
+ if (!d_registerStats){
return;
+ }
- StatisticsRegistry::registerStat(&d_statStarts);
- StatisticsRegistry::registerStat(&d_statDecisions);
- StatisticsRegistry::registerStat(&d_statRndDecisions);
- StatisticsRegistry::registerStat(&d_statPropagations);
- StatisticsRegistry::registerStat(&d_statConflicts);
- StatisticsRegistry::registerStat(&d_statClausesLiterals);
- StatisticsRegistry::registerStat(&d_statLearntsLiterals);
- StatisticsRegistry::registerStat(&d_statMaxLiterals);
- StatisticsRegistry::registerStat(&d_statTotLiterals);
- StatisticsRegistry::registerStat(&d_statEliminatedVars);
- StatisticsRegistry::registerStat(&d_statCallsToSolve);
- StatisticsRegistry::registerStat(&d_statSolveTime);
+ d_registry->registerStat(&d_statStarts);
+ d_registry->registerStat(&d_statDecisions);
+ d_registry->registerStat(&d_statRndDecisions);
+ d_registry->registerStat(&d_statPropagations);
+ d_registry->registerStat(&d_statConflicts);
+ d_registry->registerStat(&d_statClausesLiterals);
+ d_registry->registerStat(&d_statLearntsLiterals);
+ d_registry->registerStat(&d_statMaxLiterals);
+ d_registry->registerStat(&d_statTotLiterals);
+ d_registry->registerStat(&d_statEliminatedVars);
+ d_registry->registerStat(&d_statCallsToSolve);
+ d_registry->registerStat(&d_statSolveTime);
}
BVMinisatSatSolver::Statistics::~Statistics() {
- if (!d_registerStats)
+ if (!d_registerStats){
return;
- StatisticsRegistry::unregisterStat(&d_statStarts);
- StatisticsRegistry::unregisterStat(&d_statDecisions);
- StatisticsRegistry::unregisterStat(&d_statRndDecisions);
- StatisticsRegistry::unregisterStat(&d_statPropagations);
- StatisticsRegistry::unregisterStat(&d_statConflicts);
- StatisticsRegistry::unregisterStat(&d_statClausesLiterals);
- StatisticsRegistry::unregisterStat(&d_statLearntsLiterals);
- StatisticsRegistry::unregisterStat(&d_statMaxLiterals);
- StatisticsRegistry::unregisterStat(&d_statTotLiterals);
- StatisticsRegistry::unregisterStat(&d_statEliminatedVars);
- StatisticsRegistry::unregisterStat(&d_statCallsToSolve);
- StatisticsRegistry::unregisterStat(&d_statSolveTime);
+ }
+ d_registry->unregisterStat(&d_statStarts);
+ d_registry->unregisterStat(&d_statDecisions);
+ d_registry->unregisterStat(&d_statRndDecisions);
+ d_registry->unregisterStat(&d_statPropagations);
+ d_registry->unregisterStat(&d_statConflicts);
+ d_registry->unregisterStat(&d_statClausesLiterals);
+ d_registry->unregisterStat(&d_statLearntsLiterals);
+ d_registry->unregisterStat(&d_statMaxLiterals);
+ d_registry->unregisterStat(&d_statTotLiterals);
+ d_registry->unregisterStat(&d_statEliminatedVars);
+ d_registry->unregisterStat(&d_statCallsToSolve);
+ d_registry->unregisterStat(&d_statSolveTime);
}
void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){
- if (!d_registerStats)
+ if (!d_registerStats){
return;
-
+ }
+
d_statStarts.setData(minisat->starts);
d_statDecisions.setData(minisat->decisions);
d_statRndDecisions.setData(minisat->rnd_decisions);
d_statTotLiterals.setData(minisat->tot_literals);
d_statEliminatedVars.setData(minisat->eliminated_vars);
}
+
+} /* namespace CVC4::prop */
+} /* namespace CVC4 */
#pragma once
-#include "prop/sat_solver.h"
-#include "prop/bvminisat/simp/SimpSolver.h"
#include "context/cdo.h"
+#include "prop/bvminisat/simp/SimpSolver.h"
+#include "prop/sat_solver.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace prop {
public:
- BVMinisatSatSolver() :
- ContextNotifyObj(NULL, false),
- d_assertionsRealCount(NULL, (unsigned)0),
- d_lastPropagation(NULL, (unsigned)0),
- d_statistics("")
- { Unreachable(); }
- BVMinisatSatSolver(context::Context* mainSatContext, const std::string& name = "");
+ BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name = "");
~BVMinisatSatSolver() throw(AssertionException);
void setNotify(Notify* notify);
void markUnremovable(SatLiteral lit);
void interrupt();
-
+
SatValue solve();
SatValue solve(long unsigned int&);
void getUnsatCore(SatClause& unsatCore);
void explain(SatLiteral lit, std::vector<SatLiteral>& explanation);
SatValue assertAssumption(SatLiteral lit, bool propagate);
-
+
void popAssumption();
+private:
+ /* Disable the default constructor. */
+ BVMinisatSatSolver() CVC4_UNUSED;
+
class Statistics {
public:
+ StatisticsRegistry* d_registry;
ReferenceStat<uint64_t> d_statStarts, d_statDecisions;
ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations;
ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals;
IntStat d_statCallsToSolve;
BackedStat<double> d_statSolveTime;
bool d_registerStats;
- Statistics(const std::string& prefix);
+ Statistics(StatisticsRegistry* registry, const std::string& prefix);
~Statistics();
void init(BVMinisat::SimpSolver* minisat);
};
#define BVMinisat_SimpSolver_h
#include "context/context.h"
-#include "expr/statistics_registry.h"
#include "prop/bvminisat/core/Solver.h"
#include "prop/bvminisat/mtl/Queue.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace BVMinisat {
#include "options/prop_options.h"
#include "options/smt_options.h"
#include "prop/minisat/simp/SimpSolver.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace prop {
//// DPllMinisatSatSolver
-MinisatSatSolver::MinisatSatSolver() :
+MinisatSatSolver::MinisatSatSolver(StatisticsRegistry* registry) :
d_minisat(NULL),
- d_context(NULL)
+ d_context(NULL),
+ d_statistics(registry)
{}
MinisatSatSolver::~MinisatSatSolver() throw()
/// Statistics for MinisatSatSolver
-MinisatSatSolver::Statistics::Statistics() :
- d_statStarts("sat::starts"),
- d_statDecisions("sat::decisions"),
- d_statRndDecisions("sat::rnd_decisions"),
- d_statPropagations("sat::propagations"),
- d_statConflicts("sat::conflicts"),
- d_statClausesLiterals("sat::clauses_literals"),
- d_statLearntsLiterals("sat::learnts_literals"),
- d_statMaxLiterals("sat::max_literals"),
- d_statTotLiterals("sat::tot_literals")
+MinisatSatSolver::Statistics::Statistics(StatisticsRegistry* registry) :
+ d_registry(registry),
+ d_statStarts("sat::starts"),
+ d_statDecisions("sat::decisions"),
+ d_statRndDecisions("sat::rnd_decisions"),
+ d_statPropagations("sat::propagations"),
+ d_statConflicts("sat::conflicts"),
+ d_statClausesLiterals("sat::clauses_literals"),
+ d_statLearntsLiterals("sat::learnts_literals"),
+ d_statMaxLiterals("sat::max_literals"),
+ d_statTotLiterals("sat::tot_literals")
{
- StatisticsRegistry::registerStat(&d_statStarts);
- StatisticsRegistry::registerStat(&d_statDecisions);
- StatisticsRegistry::registerStat(&d_statRndDecisions);
- StatisticsRegistry::registerStat(&d_statPropagations);
- StatisticsRegistry::registerStat(&d_statConflicts);
- StatisticsRegistry::registerStat(&d_statClausesLiterals);
- StatisticsRegistry::registerStat(&d_statLearntsLiterals);
- StatisticsRegistry::registerStat(&d_statMaxLiterals);
- StatisticsRegistry::registerStat(&d_statTotLiterals);
+ d_registry->registerStat(&d_statStarts);
+ d_registry->registerStat(&d_statDecisions);
+ d_registry->registerStat(&d_statRndDecisions);
+ d_registry->registerStat(&d_statPropagations);
+ d_registry->registerStat(&d_statConflicts);
+ d_registry->registerStat(&d_statClausesLiterals);
+ d_registry->registerStat(&d_statLearntsLiterals);
+ d_registry->registerStat(&d_statMaxLiterals);
+ d_registry->registerStat(&d_statTotLiterals);
}
+
MinisatSatSolver::Statistics::~Statistics() {
- StatisticsRegistry::unregisterStat(&d_statStarts);
- StatisticsRegistry::unregisterStat(&d_statDecisions);
- StatisticsRegistry::unregisterStat(&d_statRndDecisions);
- StatisticsRegistry::unregisterStat(&d_statPropagations);
- StatisticsRegistry::unregisterStat(&d_statConflicts);
- StatisticsRegistry::unregisterStat(&d_statClausesLiterals);
- StatisticsRegistry::unregisterStat(&d_statLearntsLiterals);
- StatisticsRegistry::unregisterStat(&d_statMaxLiterals);
- StatisticsRegistry::unregisterStat(&d_statTotLiterals);
+ d_registry->unregisterStat(&d_statStarts);
+ d_registry->unregisterStat(&d_statDecisions);
+ d_registry->unregisterStat(&d_statRndDecisions);
+ d_registry->unregisterStat(&d_statPropagations);
+ d_registry->unregisterStat(&d_statConflicts);
+ d_registry->unregisterStat(&d_statClausesLiterals);
+ d_registry->unregisterStat(&d_statLearntsLiterals);
+ d_registry->unregisterStat(&d_statMaxLiterals);
+ d_registry->unregisterStat(&d_statTotLiterals);
}
+
void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){
d_statStarts.setData(d_minisat->starts);
d_statDecisions.setData(d_minisat->decisions);
#include "prop/sat_solver.h"
#include "prop/minisat/simp/SimpSolver.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace prop {
class MinisatSatSolver : public DPLLSatSolverInterface {
-
- /** The SatSolver used */
- Minisat::SimpSolver* d_minisat;
-
- /** Context we will be using to synchronize the sat solver */
- context::Context* d_context;
-
- void setupOptions();
-
public:
- MinisatSatSolver();
+ MinisatSatSolver(StatisticsRegistry* registry);
~MinisatSatSolver() throw();
;
bool isDecision(SatVariable decn) const;
+private:
+
+ /** The SatSolver used */
+ Minisat::SimpSolver* d_minisat;
+
+ /** Context we will be using to synchronize the sat solver */
+ context::Context* d_context;
+
+ void setupOptions();
+
class Statistics {
private:
+ StatisticsRegistry* d_registry;
ReferenceStat<uint64_t> d_statStarts, d_statDecisions;
ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations;
ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals;
ReferenceStat<uint64_t> d_statLearntsLiterals, d_statMaxLiterals;
ReferenceStat<uint64_t> d_statTotLiterals;
public:
- Statistics();
+ Statistics(StatisticsRegistry* registry);
~Statistics();
void init(Minisat::SimpSolver* d_minisat);
};/* class MinisatSatSolver::Statistics */
#include "prop/sat_solver.h"
#include "prop/sat_solver_factory.h"
#include "prop/theory_proxy.h"
+#include "smt/smt_statistics_registry.h"
#include "smt_util/command.h"
#include "theory/theory_engine.h"
#include "theory/theory_registrar.h"
Debug("prop") << "Constructing the PropEngine" << endl;
- d_satSolver = SatSolverFactory::createDPLLMinisat();
+ d_satSolver = SatSolverFactory::createDPLLMinisat(smtStatisticsRegistry());
d_registrar = new theory::TheoryRegistrar(d_theoryEngine);
d_cnfStream = new CVC4::prop::TseitinCnfStream
#include <string>
#include "context/cdlist.h"
+#include "context/context.h"
#include "expr/node.h"
-#include "expr/statistics_registry.h"
#include "prop/sat_solver_types.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace prop {
virtual void notify(SatClause& clause) = 0;
virtual void spendResource(unsigned ammount) = 0;
virtual void safePoint(unsigned ammount) = 0;
-
+
};/* class BVSatSolverInterface::Notify */
virtual void setNotify(Notify* notify) = 0;
**/
#include "prop/sat_solver_factory.h"
+
#include "prop/minisat/minisat.h"
#include "prop/bvminisat/bvminisat.h"
namespace CVC4 {
namespace prop {
-BVSatSolverInterface* SatSolverFactory::createMinisat(context::Context* mainSatContext, const std::string& name) {
- return new BVMinisatSatSolver(mainSatContext, name);
+BVSatSolverInterface* SatSolverFactory::createMinisat(context::Context* mainSatContext, StatisticsRegistry* registry, const std::string& name) {
+ return new BVMinisatSatSolver(registry, mainSatContext, name);
}
-DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat() {
- return new MinisatSatSolver();
+DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(StatisticsRegistry* registry) {
+ return new MinisatSatSolver(registry);
}
} /* CVC4::prop namespace */
#include <string>
#include <vector>
+#include "context/context.h"
#include "prop/sat_solver.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace prop {
class SatSolverFactory {
public:
- static BVSatSolverInterface* createMinisat(context::Context* mainSatContext, const std::string& name = "");
- static DPLLSatSolverInterface* createDPLLMinisat();
+ static BVSatSolverInterface* createMinisat(context::Context* mainSatContext, StatisticsRegistry* registry, const std::string& name = "");
+ static DPLLSatSolverInterface* createDPLLMinisat(StatisticsRegistry* registry);
};/* class SatSolverFactory */
#include "context/context.h"
#include "decision/decision_engine.h"
#include "expr/expr_stream.h"
-#include "expr/statistics_registry.h"
#include "options/decision_options.h"
#include "prop/cnf_stream.h"
#include "prop/prop_engine.h"
#include "smt_util/lemma_input_channel.h"
#include "smt_util/lemma_output_channel.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/rewriter.h"
#include "theory/theory_engine.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace prop {
d_decisionEngine(decisionEngine),
d_theoryEngine(theoryEngine),
d_globals(globals),
- d_queue(context)
-{}
+ d_queue(context),
+ d_replayedDecisions("prop::theoryproxy::replayedDecisions", 0)
+{
+ smtStatisticsRegistry()->registerStat(&d_replayedDecisions);
+}
TheoryProxy::~TheoryProxy() {
/* nothing to do for now */
+ smtStatisticsRegistry()->unregisterStat(&d_replayedDecisions);
}
/** The lemma input channel we are using. */
#include "context/cdqueue.h"
#include "expr/node.h"
-#include "expr/statistics_registry.h"
#include "prop/sat_solver.h"
#include "smt/smt_globals.h"
#include "smt_util/lemma_output_channel.h"
#include "smt_util/lemma_input_channel.h"
#include "theory/theory.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
/**
* Statistic: the number of replayed decisions (via --replay).
*/
- KEEP_STATISTIC(IntStat, d_replayedDecisions,
- "prop::theoryproxy::replayedDecisions", 0);
+ IntStat d_replayedDecisions;
+
};/* class SatSolver */
}/* CVC4::prop namespace */
d_resourceUnitsUsed("smt::SmtEngine::resourceUnitsUsed")
{
- StatisticsRegistry::registerStat(&d_definitionExpansionTime);
- StatisticsRegistry::registerStat(&d_rewriteBooleanTermsTime);
- StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime);
- StatisticsRegistry::registerStat(&d_miplibPassTime);
- StatisticsRegistry::registerStat(&d_numMiplibAssertionsRemoved);
- StatisticsRegistry::registerStat(&d_numConstantProps);
- StatisticsRegistry::registerStat(&d_staticLearningTime);
- StatisticsRegistry::registerStat(&d_simpITETime);
- StatisticsRegistry::registerStat(&d_unconstrainedSimpTime);
- StatisticsRegistry::registerStat(&d_iteRemovalTime);
- StatisticsRegistry::registerStat(&d_theoryPreprocessTime);
- StatisticsRegistry::registerStat(&d_rewriteApplyToConstTime);
- StatisticsRegistry::registerStat(&d_cnfConversionTime);
- StatisticsRegistry::registerStat(&d_numAssertionsPre);
- StatisticsRegistry::registerStat(&d_numAssertionsPost);
- StatisticsRegistry::registerStat(&d_checkModelTime);
- StatisticsRegistry::registerStat(&d_checkProofTime);
- StatisticsRegistry::registerStat(&d_checkUnsatCoreTime);
- StatisticsRegistry::registerStat(&d_solveTime);
- StatisticsRegistry::registerStat(&d_pushPopTime);
- StatisticsRegistry::registerStat(&d_processAssertionsTime);
- StatisticsRegistry::registerStat(&d_simplifiedToFalse);
- StatisticsRegistry::registerStat(&d_resourceUnitsUsed);
+ smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime);
+ smtStatisticsRegistry()->registerStat(&d_rewriteBooleanTermsTime);
+ smtStatisticsRegistry()->registerStat(&d_nonclausalSimplificationTime);
+ smtStatisticsRegistry()->registerStat(&d_miplibPassTime);
+ smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved);
+ smtStatisticsRegistry()->registerStat(&d_numConstantProps);
+ smtStatisticsRegistry()->registerStat(&d_staticLearningTime);
+ smtStatisticsRegistry()->registerStat(&d_simpITETime);
+ smtStatisticsRegistry()->registerStat(&d_unconstrainedSimpTime);
+ smtStatisticsRegistry()->registerStat(&d_iteRemovalTime);
+ smtStatisticsRegistry()->registerStat(&d_theoryPreprocessTime);
+ smtStatisticsRegistry()->registerStat(&d_rewriteApplyToConstTime);
+ smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
+ smtStatisticsRegistry()->registerStat(&d_numAssertionsPre);
+ smtStatisticsRegistry()->registerStat(&d_numAssertionsPost);
+ smtStatisticsRegistry()->registerStat(&d_checkModelTime);
+ smtStatisticsRegistry()->registerStat(&d_checkProofTime);
+ smtStatisticsRegistry()->registerStat(&d_checkUnsatCoreTime);
+ smtStatisticsRegistry()->registerStat(&d_solveTime);
+ smtStatisticsRegistry()->registerStat(&d_pushPopTime);
+ smtStatisticsRegistry()->registerStat(&d_processAssertionsTime);
+ smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse);
+ smtStatisticsRegistry()->registerStat(&d_resourceUnitsUsed);
}
~SmtEngineStatistics() {
- StatisticsRegistry::unregisterStat(&d_definitionExpansionTime);
- StatisticsRegistry::unregisterStat(&d_rewriteBooleanTermsTime);
- StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime);
- StatisticsRegistry::unregisterStat(&d_miplibPassTime);
- StatisticsRegistry::unregisterStat(&d_numMiplibAssertionsRemoved);
- StatisticsRegistry::unregisterStat(&d_numConstantProps);
- StatisticsRegistry::unregisterStat(&d_staticLearningTime);
- StatisticsRegistry::unregisterStat(&d_simpITETime);
- StatisticsRegistry::unregisterStat(&d_unconstrainedSimpTime);
- StatisticsRegistry::unregisterStat(&d_iteRemovalTime);
- StatisticsRegistry::unregisterStat(&d_theoryPreprocessTime);
- StatisticsRegistry::unregisterStat(&d_rewriteApplyToConstTime);
- StatisticsRegistry::unregisterStat(&d_cnfConversionTime);
- StatisticsRegistry::unregisterStat(&d_numAssertionsPre);
- StatisticsRegistry::unregisterStat(&d_numAssertionsPost);
- StatisticsRegistry::unregisterStat(&d_checkModelTime);
- StatisticsRegistry::unregisterStat(&d_checkProofTime);
- StatisticsRegistry::unregisterStat(&d_checkUnsatCoreTime);
- StatisticsRegistry::unregisterStat(&d_solveTime);
- StatisticsRegistry::unregisterStat(&d_pushPopTime);
- StatisticsRegistry::unregisterStat(&d_processAssertionsTime);
- StatisticsRegistry::unregisterStat(&d_simplifiedToFalse);
- StatisticsRegistry::unregisterStat(&d_resourceUnitsUsed);
+ smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime);
+ smtStatisticsRegistry()->unregisterStat(&d_rewriteBooleanTermsTime);
+ smtStatisticsRegistry()->unregisterStat(&d_nonclausalSimplificationTime);
+ smtStatisticsRegistry()->unregisterStat(&d_miplibPassTime);
+ smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved);
+ smtStatisticsRegistry()->unregisterStat(&d_numConstantProps);
+ smtStatisticsRegistry()->unregisterStat(&d_staticLearningTime);
+ smtStatisticsRegistry()->unregisterStat(&d_simpITETime);
+ smtStatisticsRegistry()->unregisterStat(&d_unconstrainedSimpTime);
+ smtStatisticsRegistry()->unregisterStat(&d_iteRemovalTime);
+ smtStatisticsRegistry()->unregisterStat(&d_theoryPreprocessTime);
+ smtStatisticsRegistry()->unregisterStat(&d_rewriteApplyToConstTime);
+ smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
+ smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre);
+ smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPost);
+ smtStatisticsRegistry()->unregisterStat(&d_checkModelTime);
+ smtStatisticsRegistry()->unregisterStat(&d_checkProofTime);
+ smtStatisticsRegistry()->unregisterStat(&d_checkUnsatCoreTime);
+ smtStatisticsRegistry()->unregisterStat(&d_solveTime);
+ smtStatisticsRegistry()->unregisterStat(&d_pushPopTime);
+ smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime);
+ smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse);
+ smtStatisticsRegistry()->unregisterStat(&d_resourceUnitsUsed);
}
};/* struct SmtEngineStatistics */
#include "context/cdlist_forward.h"
#include "expr/expr.h"
#include "expr/expr_manager.h"
-#include "expr/statistics.h"
#include "options/options.h"
#include "proof/unsat_core.h"
#include "smt/logic_exception.h"
#include "util/proof.h"
#include "util/result.h"
#include "util/sexpr.h"
+#include "util/statistics.h"
#include "util/unsafe_interrupt_exception.h"
// In terms of abstraction, this is below (and provides services to)
#include "base/cvc4_assert.h"
#include "base/output.h"
-#include "expr/statistics_registry.h"
#include "smt/smt_engine.h"
#include "util/configuration_private.h"
+#include "util/statistics_registry.h"
using namespace CVC4;
using namespace std;
s_smtEngine_current = d_oldSmtEngine;
Debug("current") << "smt scope: returning to " << s_smtEngine_current << std::endl;
}
+
+ /**
+ * This returns the StatisticsRegistry attached to the currently in scope
+ * SmtEngine.
+ */
+ static StatisticsRegistry* currentStatisticsRegistry() {
+ Assert(smtEngineInScope());
+ return s_smtEngine_current->d_statisticsRegistry;
+ }
+
};/* class SmtScope */
+
}/* CVC4::smt namespace */
}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file smt_statistic_registry.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Accessor for the SmtEngine's StatisticsRegistry.
+ **
+ ** Accessor for the SmtEngine's StatisticsRegistry.
+ **/
+
+
+#include "smt/smt_statistics_registry.h"
+
+#include "smt/smt_engine_scope.h"
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+
+StatisticsRegistry* smtStatisticsRegistry() {
+ return smt::SmtScope::currentStatisticsRegistry();
+}
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file smt_statistic_registry.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Accessor for the SmtEngine's StatisticsRegistry.
+ **
+ ** Accessor for the SmtEngine's StatisticsRegistry.
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+
+/**
+ * This returns the StatisticsRegistry attached to the currently in scope
+ * SmtEngine. This is a synonym for smt::SmtScope::currentStatisticsRegistry().
+ */
+StatisticsRegistry* smtStatisticsRegistry();
+
+
+/**
+ * To use a statistic, you need to declare it, initialize it in your
+ * constructor, register it in your constructor, and deregister it in
+ * your destructor. Instead, this macro does it all for you (and
+ * therefore also keeps the statistic type, field name, and output
+ * string all in the same place in your class's header. Its use is
+ * like in this example, which takes the place of the declaration of a
+ * statistics field "d_checkTimer":
+ *
+ * KEEP_STATISTIC(TimerStat, d_checkTimer, "theory::uf::checkTime");
+ *
+ * If any args need to be passed to the constructor, you can specify
+ * them after the string.
+ *
+ * The macro works by creating a nested class type, derived from the
+ * statistic type you give it, which declares a registry-aware
+ * constructor/destructor pair.
+ */
+#define KEEP_STATISTIC(_StatType, _StatField, _StatName, _CtorArgs...) \
+ struct Statistic_##_StatField : public _StatType { \
+ Statistic_##_StatField() : _StatType(_StatName, ## _CtorArgs) { \
+ smtStatisticsRegistry()->registerStat(this); \
+ } \
+ ~Statistic_##_StatField() { \
+ smtStatisticsRegistry()->unregisterStat(this); \
+ } \
+ } _StatField
+
+
+}/* CVC4 namespace */
** [[ Add lengthier description here ]]
** \todo document this file
**/
+#include "theory/arith/approx_simplex.h"
#include <cfloat>
#include <cmath>
#include "base/output.h"
#include "cvc4autoconfig.h"
-#include "theory/arith/approx_simplex.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/arith/constraint.h"
#include "theory/arith/cut_log.h"
#include "theory/arith/matrix.h"
, d_gaussianElimConstruct("z::approx::gaussianElimConstruct::calls",0)
, d_averageGuesses("z::approx::averageGuesses")
{
- // StatisticsRegistry::registerStat(&d_relaxCalls);
- // StatisticsRegistry::registerStat(&d_relaxUnknowns);
- // StatisticsRegistry::registerStat(&d_relaxFeasible);
- // StatisticsRegistry::registerStat(&d_relaxInfeasible);
- // StatisticsRegistry::registerStat(&d_relaxPivotsExhausted);
-
- // StatisticsRegistry::registerStat(&d_mipCalls);
- // StatisticsRegistry::registerStat(&d_mipUnknowns);
- // StatisticsRegistry::registerStat(&d_mipBingo);
- // StatisticsRegistry::registerStat(&d_mipClosed);
- // StatisticsRegistry::registerStat(&d_mipBranchesExhausted);
- // StatisticsRegistry::registerStat(&d_mipPivotsExhausted);
- // StatisticsRegistry::registerStat(&d_mipExecExhausted);
-
-
- // StatisticsRegistry::registerStat(&d_gmiGen);
- // StatisticsRegistry::registerStat(&d_gmiReplay);
- // StatisticsRegistry::registerStat(&d_mipGen);
- // StatisticsRegistry::registerStat(&d_mipReplay);
-
- StatisticsRegistry::registerStat(&d_branchMaxDepth);
- //StatisticsRegistry::registerStat(&d_branchTotal);
- //StatisticsRegistry::registerStat(&d_branchCuts);
- StatisticsRegistry::registerStat(&d_branchesMaxOnAVar);
-
- StatisticsRegistry::registerStat(&d_gaussianElimConstructTime);
- StatisticsRegistry::registerStat(&d_gaussianElimConstruct);
-
- StatisticsRegistry::registerStat(&d_averageGuesses);
+ // smtStatisticsRegistry()->registerStat(&d_relaxCalls);
+ // smtStatisticsRegistry()->registerStat(&d_relaxUnknowns);
+ // smtStatisticsRegistry()->registerStat(&d_relaxFeasible);
+ // smtStatisticsRegistry()->registerStat(&d_relaxInfeasible);
+ // smtStatisticsRegistry()->registerStat(&d_relaxPivotsExhausted);
+
+ // smtStatisticsRegistry()->registerStat(&d_mipCalls);
+ // smtStatisticsRegistry()->registerStat(&d_mipUnknowns);
+ // smtStatisticsRegistry()->registerStat(&d_mipBingo);
+ // smtStatisticsRegistry()->registerStat(&d_mipClosed);
+ // smtStatisticsRegistry()->registerStat(&d_mipBranchesExhausted);
+ // smtStatisticsRegistry()->registerStat(&d_mipPivotsExhausted);
+ // smtStatisticsRegistry()->registerStat(&d_mipExecExhausted);
+
+
+ // smtStatisticsRegistry()->registerStat(&d_gmiGen);
+ // smtStatisticsRegistry()->registerStat(&d_gmiReplay);
+ // smtStatisticsRegistry()->registerStat(&d_mipGen);
+ // smtStatisticsRegistry()->registerStat(&d_mipReplay);
+
+ smtStatisticsRegistry()->registerStat(&d_branchMaxDepth);
+ //smtStatisticsRegistry()->registerStat(&d_branchTotal);
+ //smtStatisticsRegistry()->registerStat(&d_branchCuts);
+ smtStatisticsRegistry()->registerStat(&d_branchesMaxOnAVar);
+
+ smtStatisticsRegistry()->registerStat(&d_gaussianElimConstructTime);
+ smtStatisticsRegistry()->registerStat(&d_gaussianElimConstruct);
+
+ smtStatisticsRegistry()->registerStat(&d_averageGuesses);
}
ApproximateStatistics::~ApproximateStatistics(){
- // StatisticsRegistry::unregisterStat(&d_relaxCalls);
- // StatisticsRegistry::unregisterStat(&d_relaxUnknowns);
- // StatisticsRegistry::unregisterStat(&d_relaxFeasible);
- // StatisticsRegistry::unregisterStat(&d_relaxInfeasible);
- // StatisticsRegistry::unregisterStat(&d_relaxPivotsExhausted);
-
- // StatisticsRegistry::unregisterStat(&d_mipCalls);
- // StatisticsRegistry::unregisterStat(&d_mipUnknowns);
- // StatisticsRegistry::unregisterStat(&d_mipBingo);
- // StatisticsRegistry::unregisterStat(&d_mipClosed);
- // StatisticsRegistry::unregisterStat(&d_mipBranchesExhausted);
- // StatisticsRegistry::unregisterStat(&d_mipPivotsExhausted);
- // StatisticsRegistry::unregisterStat(&d_mipExecExhausted);
-
-
- // StatisticsRegistry::unregisterStat(&d_gmiGen);
- // StatisticsRegistry::unregisterStat(&d_gmiReplay);
- // StatisticsRegistry::unregisterStat(&d_mipGen);
- // StatisticsRegistry::unregisterStat(&d_mipReplay);
-
- StatisticsRegistry::unregisterStat(&d_branchMaxDepth);
- //StatisticsRegistry::unregisterStat(&d_branchTotal);
- //StatisticsRegistry::unregisterStat(&d_branchCuts);
- StatisticsRegistry::unregisterStat(&d_branchesMaxOnAVar);
-
- StatisticsRegistry::unregisterStat(&d_gaussianElimConstructTime);
- StatisticsRegistry::unregisterStat(&d_gaussianElimConstruct);
-
- StatisticsRegistry::unregisterStat(&d_averageGuesses);
+ // smtStatisticsRegistry()->unregisterStat(&d_relaxCalls);
+ // smtStatisticsRegistry()->unregisterStat(&d_relaxUnknowns);
+ // smtStatisticsRegistry()->unregisterStat(&d_relaxFeasible);
+ // smtStatisticsRegistry()->unregisterStat(&d_relaxInfeasible);
+ // smtStatisticsRegistry()->unregisterStat(&d_relaxPivotsExhausted);
+
+ // smtStatisticsRegistry()->unregisterStat(&d_mipCalls);
+ // smtStatisticsRegistry()->unregisterStat(&d_mipUnknowns);
+ // smtStatisticsRegistry()->unregisterStat(&d_mipBingo);
+ // smtStatisticsRegistry()->unregisterStat(&d_mipClosed);
+ // smtStatisticsRegistry()->unregisterStat(&d_mipBranchesExhausted);
+ // smtStatisticsRegistry()->unregisterStat(&d_mipPivotsExhausted);
+ // smtStatisticsRegistry()->unregisterStat(&d_mipExecExhausted);
+
+
+ // smtStatisticsRegistry()->unregisterStat(&d_gmiGen);
+ // smtStatisticsRegistry()->unregisterStat(&d_gmiReplay);
+ // smtStatisticsRegistry()->unregisterStat(&d_mipGen);
+ // smtStatisticsRegistry()->unregisterStat(&d_mipReplay);
+
+ smtStatisticsRegistry()->unregisterStat(&d_branchMaxDepth);
+ //smtStatisticsRegistry()->unregisterStat(&d_branchTotal);
+ //smtStatisticsRegistry()->unregisterStat(&d_branchCuts);
+ smtStatisticsRegistry()->unregisterStat(&d_branchesMaxOnAVar);
+
+ smtStatisticsRegistry()->unregisterStat(&d_gaussianElimConstructTime);
+ smtStatisticsRegistry()->unregisterStat(&d_gaussianElimConstruct);
+
+ smtStatisticsRegistry()->unregisterStat(&d_averageGuesses);
}
Integer ApproximateSimplex::s_defaultMaxDenom(1<<26);
#pragma once
#include <vector>
-#include "expr/statistics_registry.h"
#include "theory/arith/arithvar.h"
#include "theory/arith/delta_rational.h"
#include "util/dense_map.h"
#include "util/rational.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
#include "expr/convenience_node_builders.h"
#include "expr/expr.h"
#include "options/arith_options.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/arith/arith_static_learner.h"
#include "theory/arith/arith_utilities.h"
#include "theory/arith/normal_form.h"
d_iteMinMaxApplications("theory::arith::iteMinMaxApplications", 0),
d_iteConstantApplications("theory::arith::iteConstantApplications", 0)
{
- StatisticsRegistry::registerStat(&d_iteMinMaxApplications);
- StatisticsRegistry::registerStat(&d_iteConstantApplications);
+ smtStatisticsRegistry()->registerStat(&d_iteMinMaxApplications);
+ smtStatisticsRegistry()->registerStat(&d_iteConstantApplications);
}
ArithStaticLearner::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_iteMinMaxApplications);
- StatisticsRegistry::unregisterStat(&d_iteConstantApplications);
+ smtStatisticsRegistry()->unregisterStat(&d_iteMinMaxApplications);
+ smtStatisticsRegistry()->unregisterStat(&d_iteConstantApplications);
}
void ArithStaticLearner::staticLearning(TNode n, NodeBuilder<>& learned){
#include "context/cdtrail_hashmap.h"
#include "context/context.h"
-#include "expr/statistics_registry.h"
#include "theory/arith/arith_utilities.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
** [[ Add lengthier description here ]]
** \todo document this file
**/
+#include "theory/arith/attempt_solution_simplex.h"
#include "base/output.h"
#include "options/arith_options.h"
-#include "theory/arith/attempt_solution_simplex.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/arith/constraint.h"
using namespace std;
d_queueTime("theory::arith::attempt::queueTime"),
d_conflicts("theory::arith::attempt::conflicts", 0)
{
- StatisticsRegistry::registerStat(&d_searchTime);
- StatisticsRegistry::registerStat(&d_queueTime);
- StatisticsRegistry::registerStat(&d_conflicts);
+ smtStatisticsRegistry()->registerStat(&d_searchTime);
+ smtStatisticsRegistry()->registerStat(&d_queueTime);
+ smtStatisticsRegistry()->registerStat(&d_conflicts);
}
AttemptSolutionSDP::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_searchTime);
- StatisticsRegistry::unregisterStat(&d_queueTime);
- StatisticsRegistry::unregisterStat(&d_conflicts);
+ smtStatisticsRegistry()->unregisterStat(&d_searchTime);
+ smtStatisticsRegistry()->unregisterStat(&d_queueTime);
+ smtStatisticsRegistry()->unregisterStat(&d_conflicts);
}
bool AttemptSolutionSDP::matchesNewValue(const DenseMap<DeltaRational>& nv, ArithVar v) const{
#pragma once
-#include "expr/statistics_registry.h"
#include "theory/arith/simplex.h"
#include "theory/arith/approx_simplex.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-
** [[ Add lengthier description here ]]
** \todo document this file
**/
+#include "theory/arith/congruence_manager.h"
#include "base/output.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/arith/arith_utilities.h"
-#include "theory/arith/congruence_manager.h"
#include "theory/arith/constraint.h"
namespace CVC4 {
d_propagateConstraints("theory::arith::congruence::propagateConstraints", 0),
d_conflicts("theory::arith::congruence::conflicts", 0)
{
- StatisticsRegistry::registerStat(&d_watchedVariables);
- StatisticsRegistry::registerStat(&d_watchedVariableIsZero);
- StatisticsRegistry::registerStat(&d_watchedVariableIsNotZero);
- StatisticsRegistry::registerStat(&d_equalsConstantCalls);
- StatisticsRegistry::registerStat(&d_propagations);
- StatisticsRegistry::registerStat(&d_propagateConstraints);
- StatisticsRegistry::registerStat(&d_conflicts);
+ smtStatisticsRegistry()->registerStat(&d_watchedVariables);
+ smtStatisticsRegistry()->registerStat(&d_watchedVariableIsZero);
+ smtStatisticsRegistry()->registerStat(&d_watchedVariableIsNotZero);
+ smtStatisticsRegistry()->registerStat(&d_equalsConstantCalls);
+ smtStatisticsRegistry()->registerStat(&d_propagations);
+ smtStatisticsRegistry()->registerStat(&d_propagateConstraints);
+ smtStatisticsRegistry()->registerStat(&d_conflicts);
}
ArithCongruenceManager::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_watchedVariables);
- StatisticsRegistry::unregisterStat(&d_watchedVariableIsZero);
- StatisticsRegistry::unregisterStat(&d_watchedVariableIsNotZero);
- StatisticsRegistry::unregisterStat(&d_equalsConstantCalls);
- StatisticsRegistry::unregisterStat(&d_propagations);
- StatisticsRegistry::unregisterStat(&d_propagateConstraints);
- StatisticsRegistry::unregisterStat(&d_conflicts);
+ smtStatisticsRegistry()->unregisterStat(&d_watchedVariables);
+ smtStatisticsRegistry()->unregisterStat(&d_watchedVariableIsZero);
+ smtStatisticsRegistry()->unregisterStat(&d_watchedVariableIsNotZero);
+ smtStatisticsRegistry()->unregisterStat(&d_equalsConstantCalls);
+ smtStatisticsRegistry()->unregisterStat(&d_propagations);
+ smtStatisticsRegistry()->unregisterStat(&d_propagateConstraints);
+ smtStatisticsRegistry()->unregisterStat(&d_conflicts);
}
ArithCongruenceManager::ArithCongruenceNotify::ArithCongruenceNotify(ArithCongruenceManager& acm)
#include "context/cdo.h"
#include "context/cdtrail_queue.h"
#include "context/context.h"
-#include "expr/statistics_registry.h"
#include "theory/arith/arithvar.h"
#include "theory/arith/constraint_forward.h"
#include "theory/arith/partial_model.h"
#include "theory/uf/equality_engine.h"
#include "util/dense_map.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
** [[ Add lengthier description here ]]
** \todo document this file
**/
+#include "theory/arith/constraint.h"
#include <ostream>
#include <algorithm>
#include "base/output.h"
#include "proof/proof.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/arith/arith_utilities.h"
-#include "theory/arith/constraint.h"
#include "theory/arith/normal_form.h"
d_unatePropagateCalls("theory::arith::cd::unatePropagateCalls", 0),
d_unatePropagateImplications("theory::arith::cd::unatePropagateImplications", 0)
{
- StatisticsRegistry::registerStat(&d_unatePropagateCalls);
- StatisticsRegistry::registerStat(&d_unatePropagateImplications);
+ smtStatisticsRegistry()->registerStat(&d_unatePropagateCalls);
+ smtStatisticsRegistry()->registerStat(&d_unatePropagateImplications);
}
+
ConstraintDatabase::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_unatePropagateCalls);
- StatisticsRegistry::unregisterStat(&d_unatePropagateImplications);
+ smtStatisticsRegistry()->unregisterStat(&d_unatePropagateCalls);
+ smtStatisticsRegistry()->unregisterStat(&d_unatePropagateImplications);
}
void ConstraintDatabase::deleteConstraintAndNegation(ConstraintP c){
#include <vector>
#include "expr/kind.h"
-#include "expr/statistics_registry.h"
#include "theory/arith/arithvar.h"
#include "theory/arith/constraint_forward.h"
#include "util/dense_map.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
**
** A Diophantine equation solver for the theory of arithmetic.
**/
+#include "theory/arith/dio_solver.h"
#include <iostream>
#include "base/output.h"
#include "options/arith_options.h"
-#include "theory/arith/dio_solver.h"
+#include "smt/smt_statistics_registry.h"
using namespace std;
d_conflictTimer("theory::arith::dio::conflictTimer"),
d_cutTimer("theory::arith::dio::cutTimer")
{
- StatisticsRegistry::registerStat(&d_conflictCalls);
- StatisticsRegistry::registerStat(&d_cutCalls);
+ smtStatisticsRegistry()->registerStat(&d_conflictCalls);
+ smtStatisticsRegistry()->registerStat(&d_cutCalls);
- StatisticsRegistry::registerStat(&d_cuts);
- StatisticsRegistry::registerStat(&d_conflicts);
+ smtStatisticsRegistry()->registerStat(&d_cuts);
+ smtStatisticsRegistry()->registerStat(&d_conflicts);
- StatisticsRegistry::registerStat(&d_conflictTimer);
- StatisticsRegistry::registerStat(&d_cutTimer);
+ smtStatisticsRegistry()->registerStat(&d_conflictTimer);
+ smtStatisticsRegistry()->registerStat(&d_cutTimer);
}
DioSolver::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_conflictCalls);
- StatisticsRegistry::unregisterStat(&d_cutCalls);
+ smtStatisticsRegistry()->unregisterStat(&d_conflictCalls);
+ smtStatisticsRegistry()->unregisterStat(&d_cutCalls);
- StatisticsRegistry::unregisterStat(&d_cuts);
- StatisticsRegistry::unregisterStat(&d_conflicts);
+ smtStatisticsRegistry()->unregisterStat(&d_cuts);
+ smtStatisticsRegistry()->unregisterStat(&d_conflicts);
- StatisticsRegistry::unregisterStat(&d_conflictTimer);
- StatisticsRegistry::unregisterStat(&d_cutTimer);
+ smtStatisticsRegistry()->unregisterStat(&d_conflictTimer);
+ smtStatisticsRegistry()->unregisterStat(&d_cutTimer);
}
bool DioSolver::queueConditions(TrailIndex t){
#include "context/cdo.h"
#include "context/cdqueue.h"
#include "context/context.h"
-#include "expr/statistics_registry.h"
#include "theory/arith/normal_form.h"
#include "theory/arith/partial_model.h"
#include "util/rational.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
** [[ Add lengthier description here ]]
** \todo document this file
**/
+#include "theory/arith/dual_simplex.h"
#include "base/output.h"
#include "options/arith_options.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/arith/constraint.h"
-#include "theory/arith/dual_simplex.h"
+
using namespace std;
d_searchTime("theory::arith::dual::searchTime"),
d_finalCheckPivotCounter("theory::arith::dual::lastPivots", pivots)
{
- StatisticsRegistry::registerStat(&d_statUpdateConflicts);
- StatisticsRegistry::registerStat(&d_processSignalsTime);
- StatisticsRegistry::registerStat(&d_simplexConflicts);
- StatisticsRegistry::registerStat(&d_recentViolationCatches);
- StatisticsRegistry::registerStat(&d_searchTime);
- StatisticsRegistry::registerStat(&d_finalCheckPivotCounter);
+ smtStatisticsRegistry()->registerStat(&d_statUpdateConflicts);
+ smtStatisticsRegistry()->registerStat(&d_processSignalsTime);
+ smtStatisticsRegistry()->registerStat(&d_simplexConflicts);
+ smtStatisticsRegistry()->registerStat(&d_recentViolationCatches);
+ smtStatisticsRegistry()->registerStat(&d_searchTime);
+ smtStatisticsRegistry()->registerStat(&d_finalCheckPivotCounter);
}
DualSimplexDecisionProcedure::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_statUpdateConflicts);
- StatisticsRegistry::unregisterStat(&d_processSignalsTime);
- StatisticsRegistry::unregisterStat(&d_simplexConflicts);
- StatisticsRegistry::unregisterStat(&d_recentViolationCatches);
- StatisticsRegistry::unregisterStat(&d_searchTime);
- StatisticsRegistry::unregisterStat(&d_finalCheckPivotCounter);
+ smtStatisticsRegistry()->unregisterStat(&d_statUpdateConflicts);
+ smtStatisticsRegistry()->unregisterStat(&d_processSignalsTime);
+ smtStatisticsRegistry()->unregisterStat(&d_simplexConflicts);
+ smtStatisticsRegistry()->unregisterStat(&d_recentViolationCatches);
+ smtStatisticsRegistry()->unregisterStat(&d_searchTime);
+ smtStatisticsRegistry()->unregisterStat(&d_finalCheckPivotCounter);
}
Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
#pragma once
-#include "expr/statistics_registry.h"
#include "theory/arith/simplex.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-
** \todo document this file
**/
-
#include "theory/arith/error_set.h"
+
+#include "smt/smt_statistics_registry.h"
#include "theory/arith/constraint.h"
using namespace std;
d_enqueuesCollectionDuplicates("theory::arith::pqueue::enqueuesCollectionDuplicates", 0),
d_enqueuesVarOrderModeDuplicates("theory::arith::pqueue::enqueuesVarOrderModeDuplicates", 0)
{
- StatisticsRegistry::registerStat(&d_enqueues);
- StatisticsRegistry::registerStat(&d_enqueuesCollection);
- StatisticsRegistry::registerStat(&d_enqueuesDiffMode);
- StatisticsRegistry::registerStat(&d_enqueuesVarOrderMode);
- StatisticsRegistry::registerStat(&d_enqueuesCollectionDuplicates);
- StatisticsRegistry::registerStat(&d_enqueuesVarOrderModeDuplicates);
+ smtStatisticsRegistry()->registerStat(&d_enqueues);
+ smtStatisticsRegistry()->registerStat(&d_enqueuesCollection);
+ smtStatisticsRegistry()->registerStat(&d_enqueuesDiffMode);
+ smtStatisticsRegistry()->registerStat(&d_enqueuesVarOrderMode);
+ smtStatisticsRegistry()->registerStat(&d_enqueuesCollectionDuplicates);
+ smtStatisticsRegistry()->registerStat(&d_enqueuesVarOrderModeDuplicates);
}
ErrorSet::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_enqueues);
- StatisticsRegistry::unregisterStat(&d_enqueuesCollection);
- StatisticsRegistry::unregisterStat(&d_enqueuesDiffMode);
- StatisticsRegistry::unregisterStat(&d_enqueuesVarOrderMode);
- StatisticsRegistry::unregisterStat(&d_enqueuesCollectionDuplicates);
- StatisticsRegistry::unregisterStat(&d_enqueuesVarOrderModeDuplicates);
+ smtStatisticsRegistry()->unregisterStat(&d_enqueues);
+ smtStatisticsRegistry()->unregisterStat(&d_enqueuesCollection);
+ smtStatisticsRegistry()->unregisterStat(&d_enqueuesDiffMode);
+ smtStatisticsRegistry()->unregisterStat(&d_enqueuesVarOrderMode);
+ smtStatisticsRegistry()->unregisterStat(&d_enqueuesCollectionDuplicates);
+ smtStatisticsRegistry()->unregisterStat(&d_enqueuesVarOrderModeDuplicates);
}
ErrorSet::ErrorSet(ArithVariables& vars, TableauSizes tabSizes, BoundCountingLookup lookups):
#include <vector>
-#include "expr/statistics_registry.h"
#include "options/arith_heuristic_pivot_rule.h"
#include "theory/arith/arithvar.h"
#include "theory/arith/bound_counts.h"
#include "theory/arith/partial_model.h"
#include "theory/arith/tableau_sizes.h"
#include "util/bin_heap.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
#include "theory/arith/fc_simplex.h"
#include "base/output.h"
-#include "expr/statistics_registry.h"
#include "options/arith_options.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/arith/constraint.h"
+#include "util/statistics_registry.h"
using namespace std;
d_selectUpdateForPrimal("theory::arith::FC::selectUpdateForPrimal"),
d_finalCheckPivotCounter("theory::arith::FC::lastPivots", pivots)
{
- StatisticsRegistry::registerStat(&d_initialSignalsTime);
- StatisticsRegistry::registerStat(&d_initialConflicts);
+ smtStatisticsRegistry()->registerStat(&d_initialSignalsTime);
+ smtStatisticsRegistry()->registerStat(&d_initialConflicts);
- StatisticsRegistry::registerStat(&d_fcFoundUnsat);
- StatisticsRegistry::registerStat(&d_fcFoundSat);
- StatisticsRegistry::registerStat(&d_fcMissed);
+ smtStatisticsRegistry()->registerStat(&d_fcFoundUnsat);
+ smtStatisticsRegistry()->registerStat(&d_fcFoundSat);
+ smtStatisticsRegistry()->registerStat(&d_fcMissed);
- StatisticsRegistry::registerStat(&d_fcTimer);
- StatisticsRegistry::registerStat(&d_fcFocusConstructionTimer);
+ smtStatisticsRegistry()->registerStat(&d_fcTimer);
+ smtStatisticsRegistry()->registerStat(&d_fcFocusConstructionTimer);
- StatisticsRegistry::registerStat(&d_selectUpdateForDualLike);
- StatisticsRegistry::registerStat(&d_selectUpdateForPrimal);
+ smtStatisticsRegistry()->registerStat(&d_selectUpdateForDualLike);
+ smtStatisticsRegistry()->registerStat(&d_selectUpdateForPrimal);
- StatisticsRegistry::registerStat(&d_finalCheckPivotCounter);
+ smtStatisticsRegistry()->registerStat(&d_finalCheckPivotCounter);
}
FCSimplexDecisionProcedure::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_initialSignalsTime);
- StatisticsRegistry::unregisterStat(&d_initialConflicts);
+ smtStatisticsRegistry()->unregisterStat(&d_initialSignalsTime);
+ smtStatisticsRegistry()->unregisterStat(&d_initialConflicts);
- StatisticsRegistry::unregisterStat(&d_fcFoundUnsat);
- StatisticsRegistry::unregisterStat(&d_fcFoundSat);
- StatisticsRegistry::unregisterStat(&d_fcMissed);
+ smtStatisticsRegistry()->unregisterStat(&d_fcFoundUnsat);
+ smtStatisticsRegistry()->unregisterStat(&d_fcFoundSat);
+ smtStatisticsRegistry()->unregisterStat(&d_fcMissed);
- StatisticsRegistry::unregisterStat(&d_fcTimer);
- StatisticsRegistry::unregisterStat(&d_fcFocusConstructionTimer);
+ smtStatisticsRegistry()->unregisterStat(&d_fcTimer);
+ smtStatisticsRegistry()->unregisterStat(&d_fcFocusConstructionTimer);
- StatisticsRegistry::unregisterStat(&d_selectUpdateForDualLike);
- StatisticsRegistry::unregisterStat(&d_selectUpdateForPrimal);
+ smtStatisticsRegistry()->unregisterStat(&d_selectUpdateForDualLike);
+ smtStatisticsRegistry()->unregisterStat(&d_selectUpdateForPrimal);
- StatisticsRegistry::unregisterStat(&d_finalCheckPivotCounter);
+ smtStatisticsRegistry()->unregisterStat(&d_finalCheckPivotCounter);
}
Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){
#include <stdint.h>
-#include "expr/statistics_registry.h"
#include "theory/arith/simplex.h"
#include "util/dense_map.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-
**
** This implements the LinearEqualityModule.
**/
-
+#include "theory/arith/linear_equality.h"
#include "base/output.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/arith/constraint.h"
-#include "theory/arith/linear_equality.h"
+
using namespace std;
d_weakenTime("theory::arith::weakening::time"),
d_forceTime("theory::arith::forcing::time")
{
- StatisticsRegistry::registerStat(&d_statPivots);
- StatisticsRegistry::registerStat(&d_statUpdates);
+ smtStatisticsRegistry()->registerStat(&d_statPivots);
+ smtStatisticsRegistry()->registerStat(&d_statUpdates);
- StatisticsRegistry::registerStat(&d_pivotTime);
- StatisticsRegistry::registerStat(&d_adjTime);
+ smtStatisticsRegistry()->registerStat(&d_pivotTime);
+ smtStatisticsRegistry()->registerStat(&d_adjTime);
- StatisticsRegistry::registerStat(&d_weakeningAttempts);
- StatisticsRegistry::registerStat(&d_weakeningSuccesses);
- StatisticsRegistry::registerStat(&d_weakenings);
- StatisticsRegistry::registerStat(&d_weakenTime);
- StatisticsRegistry::registerStat(&d_forceTime);
+ smtStatisticsRegistry()->registerStat(&d_weakeningAttempts);
+ smtStatisticsRegistry()->registerStat(&d_weakeningSuccesses);
+ smtStatisticsRegistry()->registerStat(&d_weakenings);
+ smtStatisticsRegistry()->registerStat(&d_weakenTime);
+ smtStatisticsRegistry()->registerStat(&d_forceTime);
}
LinearEqualityModule::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_statPivots);
- StatisticsRegistry::unregisterStat(&d_statUpdates);
- StatisticsRegistry::unregisterStat(&d_pivotTime);
- StatisticsRegistry::unregisterStat(&d_adjTime);
+ smtStatisticsRegistry()->unregisterStat(&d_statPivots);
+ smtStatisticsRegistry()->unregisterStat(&d_statUpdates);
+ smtStatisticsRegistry()->unregisterStat(&d_pivotTime);
+ smtStatisticsRegistry()->unregisterStat(&d_adjTime);
- StatisticsRegistry::unregisterStat(&d_weakeningAttempts);
- StatisticsRegistry::unregisterStat(&d_weakeningSuccesses);
- StatisticsRegistry::unregisterStat(&d_weakenings);
- StatisticsRegistry::unregisterStat(&d_weakenTime);
- StatisticsRegistry::unregisterStat(&d_forceTime);
+ smtStatisticsRegistry()->unregisterStat(&d_weakeningAttempts);
+ smtStatisticsRegistry()->unregisterStat(&d_weakeningSuccesses);
+ smtStatisticsRegistry()->unregisterStat(&d_weakenings);
+ smtStatisticsRegistry()->unregisterStat(&d_weakenTime);
+ smtStatisticsRegistry()->unregisterStat(&d_forceTime);
}
void LinearEqualityModule::includeBoundUpdate(ArithVar v, const BoundsInfo& prev){
#pragma once
-#include "expr/statistics_registry.h"
#include "options/arith_options.h"
#include "theory/arith/arithvar.h"
#include "theory/arith/constraint_forward.h"
#include "theory/arith/simplex_update.h"
#include "theory/arith/tableau.h"
#include "util/maybe.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
#include <algorithm>
#include "base/output.h"
-#include "expr/statistics_registry.h"
#include "options/arith_options.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/arith/constraint.h"
-
+#include "util/statistics_registry.h"
using namespace std;
d_selectUpdateForSOI("theory::arith::SOI::selectSOI"),
d_finalCheckPivotCounter("theory::arith::SOI::lastPivots", pivots)
{
- StatisticsRegistry::registerStat(&d_initialSignalsTime);
- StatisticsRegistry::registerStat(&d_initialConflicts);
+ smtStatisticsRegistry()->registerStat(&d_initialSignalsTime);
+ smtStatisticsRegistry()->registerStat(&d_initialConflicts);
- StatisticsRegistry::registerStat(&d_soiFoundUnsat);
- StatisticsRegistry::registerStat(&d_soiFoundSat);
- StatisticsRegistry::registerStat(&d_soiMissed);
+ smtStatisticsRegistry()->registerStat(&d_soiFoundUnsat);
+ smtStatisticsRegistry()->registerStat(&d_soiFoundSat);
+ smtStatisticsRegistry()->registerStat(&d_soiMissed);
- StatisticsRegistry::registerStat(&d_soiConflicts);
- StatisticsRegistry::registerStat(&d_hasToBeMinimal);
- StatisticsRegistry::registerStat(&d_maybeNotMinimal);
+ smtStatisticsRegistry()->registerStat(&d_soiConflicts);
+ smtStatisticsRegistry()->registerStat(&d_hasToBeMinimal);
+ smtStatisticsRegistry()->registerStat(&d_maybeNotMinimal);
- StatisticsRegistry::registerStat(&d_soiTimer);
- StatisticsRegistry::registerStat(&d_soiFocusConstructionTimer);
+ smtStatisticsRegistry()->registerStat(&d_soiTimer);
+ smtStatisticsRegistry()->registerStat(&d_soiFocusConstructionTimer);
- StatisticsRegistry::registerStat(&d_soiConflictMinimization);
+ smtStatisticsRegistry()->registerStat(&d_soiConflictMinimization);
- StatisticsRegistry::registerStat(&d_selectUpdateForSOI);
+ smtStatisticsRegistry()->registerStat(&d_selectUpdateForSOI);
- StatisticsRegistry::registerStat(&d_finalCheckPivotCounter);
+ smtStatisticsRegistry()->registerStat(&d_finalCheckPivotCounter);
}
SumOfInfeasibilitiesSPD::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_initialSignalsTime);
- StatisticsRegistry::unregisterStat(&d_initialConflicts);
+ smtStatisticsRegistry()->unregisterStat(&d_initialSignalsTime);
+ smtStatisticsRegistry()->unregisterStat(&d_initialConflicts);
- StatisticsRegistry::unregisterStat(&d_soiFoundUnsat);
- StatisticsRegistry::unregisterStat(&d_soiFoundSat);
- StatisticsRegistry::unregisterStat(&d_soiMissed);
+ smtStatisticsRegistry()->unregisterStat(&d_soiFoundUnsat);
+ smtStatisticsRegistry()->unregisterStat(&d_soiFoundSat);
+ smtStatisticsRegistry()->unregisterStat(&d_soiMissed);
- StatisticsRegistry::unregisterStat(&d_soiConflicts);
- StatisticsRegistry::unregisterStat(&d_hasToBeMinimal);
- StatisticsRegistry::unregisterStat(&d_maybeNotMinimal);
+ smtStatisticsRegistry()->unregisterStat(&d_soiConflicts);
+ smtStatisticsRegistry()->unregisterStat(&d_hasToBeMinimal);
+ smtStatisticsRegistry()->unregisterStat(&d_maybeNotMinimal);
- StatisticsRegistry::unregisterStat(&d_soiTimer);
- StatisticsRegistry::unregisterStat(&d_soiFocusConstructionTimer);
+ smtStatisticsRegistry()->unregisterStat(&d_soiTimer);
+ smtStatisticsRegistry()->unregisterStat(&d_soiFocusConstructionTimer);
- StatisticsRegistry::unregisterStat(&d_soiConflictMinimization);
+ smtStatisticsRegistry()->unregisterStat(&d_soiConflictMinimization);
- StatisticsRegistry::unregisterStat(&d_selectUpdateForSOI);
- StatisticsRegistry::unregisterStat(&d_finalCheckPivotCounter);
+ smtStatisticsRegistry()->unregisterStat(&d_selectUpdateForSOI);
+ smtStatisticsRegistry()->unregisterStat(&d_finalCheckPivotCounter);
}
Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){
#include <stdint.h>
-#include "expr/statistics_registry.h"
#include "theory/arith/simplex.h"
#include "util/dense_map.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-
#include "theory/arith/theory_arith.h"
#include "options/smt_options.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/arith/infer_bounds.h"
#include "theory/arith/theory_arith_private.h"
const LogicInfo& logicInfo, SmtGlobals* globals)
: Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, globals)
, d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo))
-{}
+ , d_ppRewriteTimer("theory::arith::ppRewriteTimer")
+{
+ smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer);
+}
TheoryArith::~TheoryArith(){
+ smtStatisticsRegistry()->unregisterStat(&d_ppRewriteTimer);
delete d_internal;
}
TheoryArithPrivate* d_internal;
- KEEP_STATISTIC(TimerStat, d_ppRewriteTimer, "theory::arith::ppRewriteTimer");
+ TimerStat d_ppRewriteTimer;
public:
TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out,
#include "expr/metakind.h"
#include "expr/node.h"
#include "expr/node_builder.h"
-#include "expr/statistics_registry.h"
#include "options/arith_options.h"
#include "options/smt_options.h" // for incrementalSolving()
#include "smt/logic_exception.h"
#include "smt/logic_request.h"
+#include "smt/smt_statistics_registry.h"
#include "smt_util/boolean_simplification.h"
#include "theory/arith/approx_simplex.h"
#include "theory/arith/arith_ite_utils.h"
#include "util/integer.h"
#include "util/rational.h"
#include "util/result.h"
+#include "util/statistics_registry.h"
using namespace std;
using namespace CVC4::kind;
, d_mipProofsSuccessful("theory::arith::z::mip::proofs::successful", 0)
, d_numBranchesFailed("theory::arith::z::mip::branch::proof::failed", 0)
{
- StatisticsRegistry::registerStat(&d_statAssertUpperConflicts);
- StatisticsRegistry::registerStat(&d_statAssertLowerConflicts);
-
- StatisticsRegistry::registerStat(&d_statUserVariables);
- StatisticsRegistry::registerStat(&d_statAuxiliaryVariables);
- StatisticsRegistry::registerStat(&d_statDisequalitySplits);
- StatisticsRegistry::registerStat(&d_statDisequalityConflicts);
- StatisticsRegistry::registerStat(&d_simplifyTimer);
- StatisticsRegistry::registerStat(&d_staticLearningTimer);
-
- StatisticsRegistry::registerStat(&d_presolveTime);
- StatisticsRegistry::registerStat(&d_newPropTime);
-
- StatisticsRegistry::registerStat(&d_externalBranchAndBounds);
-
- StatisticsRegistry::registerStat(&d_initialTableauSize);
- StatisticsRegistry::registerStat(&d_currSetToSmaller);
- StatisticsRegistry::registerStat(&d_smallerSetToCurr);
- StatisticsRegistry::registerStat(&d_restartTimer);
-
- StatisticsRegistry::registerStat(&d_boundComputationTime);
- StatisticsRegistry::registerStat(&d_boundComputations);
- StatisticsRegistry::registerStat(&d_boundPropagations);
-
- StatisticsRegistry::registerStat(&d_unknownChecks);
- StatisticsRegistry::registerStat(&d_maxUnknownsInARow);
- StatisticsRegistry::registerStat(&d_avgUnknownsInARow);
- StatisticsRegistry::registerStat(&d_revertsOnConflicts);
- StatisticsRegistry::registerStat(&d_commitsOnConflicts);
- StatisticsRegistry::registerStat(&d_nontrivialSatChecks);
-
-
- StatisticsRegistry::registerStat(&d_satPivots);
- StatisticsRegistry::registerStat(&d_unsatPivots);
- StatisticsRegistry::registerStat(&d_unknownPivots);
-
- StatisticsRegistry::registerStat(&d_replayLogRecCount);
- StatisticsRegistry::registerStat(&d_replayLogRecConflictEscalation);
- StatisticsRegistry::registerStat(&d_replayLogRecEarlyExit);
- StatisticsRegistry::registerStat(&d_replayBranchCloseFailures);
- StatisticsRegistry::registerStat(&d_replayLeafCloseFailures);
- StatisticsRegistry::registerStat(&d_replayBranchSkips);
- StatisticsRegistry::registerStat(&d_mirCutsAttempted);
- StatisticsRegistry::registerStat(&d_gmiCutsAttempted);
- StatisticsRegistry::registerStat(&d_branchCutsAttempted);
- StatisticsRegistry::registerStat(&d_cutsReconstructed);
- StatisticsRegistry::registerStat(&d_cutsProven);
- StatisticsRegistry::registerStat(&d_cutsProofFailed);
- StatisticsRegistry::registerStat(&d_cutsReconstructionFailed);
- StatisticsRegistry::registerStat(&d_mipReplayLemmaCalls);
- StatisticsRegistry::registerStat(&d_mipExternalCuts);
- StatisticsRegistry::registerStat(&d_mipExternalBranch);
-
- StatisticsRegistry::registerStat(&d_inSolveInteger);
- StatisticsRegistry::registerStat(&d_branchesExhausted);
- StatisticsRegistry::registerStat(&d_execExhausted);
- StatisticsRegistry::registerStat(&d_pivotsExhausted);
- StatisticsRegistry::registerStat(&d_panicBranches);
- StatisticsRegistry::registerStat(&d_relaxCalls);
- StatisticsRegistry::registerStat(&d_relaxLinFeas);
- StatisticsRegistry::registerStat(&d_relaxLinFeasFailures);
- StatisticsRegistry::registerStat(&d_relaxLinInfeas);
- StatisticsRegistry::registerStat(&d_relaxLinInfeasFailures);
- StatisticsRegistry::registerStat(&d_relaxLinExhausted);
- StatisticsRegistry::registerStat(&d_relaxOthers);
-
- StatisticsRegistry::registerStat(&d_applyRowsDeleted);
-
- StatisticsRegistry::registerStat(&d_replaySimplexTimer);
- StatisticsRegistry::registerStat(&d_replayLogTimer);
- StatisticsRegistry::registerStat(&d_solveIntTimer);
- StatisticsRegistry::registerStat(&d_solveRealRelaxTimer);
-
- StatisticsRegistry::registerStat(&d_solveIntCalls);
- StatisticsRegistry::registerStat(&d_solveStandardEffort);
-
- StatisticsRegistry::registerStat(&d_approxDisabled);
-
- StatisticsRegistry::registerStat(&d_replayAttemptFailed);
-
- StatisticsRegistry::registerStat(&d_cutsRejectedDuringReplay);
- StatisticsRegistry::registerStat(&d_cutsRejectedDuringLemmas);
-
- StatisticsRegistry::registerStat(&d_solveIntModelsAttempts);
- StatisticsRegistry::registerStat(&d_solveIntModelsSuccessful);
- StatisticsRegistry::registerStat(&d_mipTimer);
- StatisticsRegistry::registerStat(&d_lpTimer);
- StatisticsRegistry::registerStat(&d_mipProofsAttempted);
- StatisticsRegistry::registerStat(&d_mipProofsSuccessful);
- StatisticsRegistry::registerStat(&d_numBranchesFailed);
+ smtStatisticsRegistry()->registerStat(&d_statAssertUpperConflicts);
+ smtStatisticsRegistry()->registerStat(&d_statAssertLowerConflicts);
+
+ smtStatisticsRegistry()->registerStat(&d_statUserVariables);
+ smtStatisticsRegistry()->registerStat(&d_statAuxiliaryVariables);
+ smtStatisticsRegistry()->registerStat(&d_statDisequalitySplits);
+ smtStatisticsRegistry()->registerStat(&d_statDisequalityConflicts);
+ smtStatisticsRegistry()->registerStat(&d_simplifyTimer);
+ smtStatisticsRegistry()->registerStat(&d_staticLearningTimer);
+
+ smtStatisticsRegistry()->registerStat(&d_presolveTime);
+ smtStatisticsRegistry()->registerStat(&d_newPropTime);
+
+ smtStatisticsRegistry()->registerStat(&d_externalBranchAndBounds);
+
+ smtStatisticsRegistry()->registerStat(&d_initialTableauSize);
+ smtStatisticsRegistry()->registerStat(&d_currSetToSmaller);
+ smtStatisticsRegistry()->registerStat(&d_smallerSetToCurr);
+ smtStatisticsRegistry()->registerStat(&d_restartTimer);
+
+ smtStatisticsRegistry()->registerStat(&d_boundComputationTime);
+ smtStatisticsRegistry()->registerStat(&d_boundComputations);
+ smtStatisticsRegistry()->registerStat(&d_boundPropagations);
+
+ smtStatisticsRegistry()->registerStat(&d_unknownChecks);
+ smtStatisticsRegistry()->registerStat(&d_maxUnknownsInARow);
+ smtStatisticsRegistry()->registerStat(&d_avgUnknownsInARow);
+ smtStatisticsRegistry()->registerStat(&d_revertsOnConflicts);
+ smtStatisticsRegistry()->registerStat(&d_commitsOnConflicts);
+ smtStatisticsRegistry()->registerStat(&d_nontrivialSatChecks);
+
+
+ smtStatisticsRegistry()->registerStat(&d_satPivots);
+ smtStatisticsRegistry()->registerStat(&d_unsatPivots);
+ smtStatisticsRegistry()->registerStat(&d_unknownPivots);
+
+ smtStatisticsRegistry()->registerStat(&d_replayLogRecCount);
+ smtStatisticsRegistry()->registerStat(&d_replayLogRecConflictEscalation);
+ smtStatisticsRegistry()->registerStat(&d_replayLogRecEarlyExit);
+ smtStatisticsRegistry()->registerStat(&d_replayBranchCloseFailures);
+ smtStatisticsRegistry()->registerStat(&d_replayLeafCloseFailures);
+ smtStatisticsRegistry()->registerStat(&d_replayBranchSkips);
+ smtStatisticsRegistry()->registerStat(&d_mirCutsAttempted);
+ smtStatisticsRegistry()->registerStat(&d_gmiCutsAttempted);
+ smtStatisticsRegistry()->registerStat(&d_branchCutsAttempted);
+ smtStatisticsRegistry()->registerStat(&d_cutsReconstructed);
+ smtStatisticsRegistry()->registerStat(&d_cutsProven);
+ smtStatisticsRegistry()->registerStat(&d_cutsProofFailed);
+ smtStatisticsRegistry()->registerStat(&d_cutsReconstructionFailed);
+ smtStatisticsRegistry()->registerStat(&d_mipReplayLemmaCalls);
+ smtStatisticsRegistry()->registerStat(&d_mipExternalCuts);
+ smtStatisticsRegistry()->registerStat(&d_mipExternalBranch);
+
+ smtStatisticsRegistry()->registerStat(&d_inSolveInteger);
+ smtStatisticsRegistry()->registerStat(&d_branchesExhausted);
+ smtStatisticsRegistry()->registerStat(&d_execExhausted);
+ smtStatisticsRegistry()->registerStat(&d_pivotsExhausted);
+ smtStatisticsRegistry()->registerStat(&d_panicBranches);
+ smtStatisticsRegistry()->registerStat(&d_relaxCalls);
+ smtStatisticsRegistry()->registerStat(&d_relaxLinFeas);
+ smtStatisticsRegistry()->registerStat(&d_relaxLinFeasFailures);
+ smtStatisticsRegistry()->registerStat(&d_relaxLinInfeas);
+ smtStatisticsRegistry()->registerStat(&d_relaxLinInfeasFailures);
+ smtStatisticsRegistry()->registerStat(&d_relaxLinExhausted);
+ smtStatisticsRegistry()->registerStat(&d_relaxOthers);
+
+ smtStatisticsRegistry()->registerStat(&d_applyRowsDeleted);
+
+ smtStatisticsRegistry()->registerStat(&d_replaySimplexTimer);
+ smtStatisticsRegistry()->registerStat(&d_replayLogTimer);
+ smtStatisticsRegistry()->registerStat(&d_solveIntTimer);
+ smtStatisticsRegistry()->registerStat(&d_solveRealRelaxTimer);
+
+ smtStatisticsRegistry()->registerStat(&d_solveIntCalls);
+ smtStatisticsRegistry()->registerStat(&d_solveStandardEffort);
+
+ smtStatisticsRegistry()->registerStat(&d_approxDisabled);
+
+ smtStatisticsRegistry()->registerStat(&d_replayAttemptFailed);
+
+ smtStatisticsRegistry()->registerStat(&d_cutsRejectedDuringReplay);
+ smtStatisticsRegistry()->registerStat(&d_cutsRejectedDuringLemmas);
+
+ smtStatisticsRegistry()->registerStat(&d_solveIntModelsAttempts);
+ smtStatisticsRegistry()->registerStat(&d_solveIntModelsSuccessful);
+ smtStatisticsRegistry()->registerStat(&d_mipTimer);
+ smtStatisticsRegistry()->registerStat(&d_lpTimer);
+ smtStatisticsRegistry()->registerStat(&d_mipProofsAttempted);
+ smtStatisticsRegistry()->registerStat(&d_mipProofsSuccessful);
+ smtStatisticsRegistry()->registerStat(&d_numBranchesFailed);
}
TheoryArithPrivate::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts);
- StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts);
-
- StatisticsRegistry::unregisterStat(&d_statUserVariables);
- StatisticsRegistry::unregisterStat(&d_statAuxiliaryVariables);
- StatisticsRegistry::unregisterStat(&d_statDisequalitySplits);
- StatisticsRegistry::unregisterStat(&d_statDisequalityConflicts);
- StatisticsRegistry::unregisterStat(&d_simplifyTimer);
- StatisticsRegistry::unregisterStat(&d_staticLearningTimer);
-
- StatisticsRegistry::unregisterStat(&d_presolveTime);
- StatisticsRegistry::unregisterStat(&d_newPropTime);
-
- StatisticsRegistry::unregisterStat(&d_externalBranchAndBounds);
-
- StatisticsRegistry::unregisterStat(&d_initialTableauSize);
- StatisticsRegistry::unregisterStat(&d_currSetToSmaller);
- StatisticsRegistry::unregisterStat(&d_smallerSetToCurr);
- StatisticsRegistry::unregisterStat(&d_restartTimer);
-
- StatisticsRegistry::unregisterStat(&d_boundComputationTime);
- StatisticsRegistry::unregisterStat(&d_boundComputations);
- StatisticsRegistry::unregisterStat(&d_boundPropagations);
-
- StatisticsRegistry::unregisterStat(&d_unknownChecks);
- StatisticsRegistry::unregisterStat(&d_maxUnknownsInARow);
- StatisticsRegistry::unregisterStat(&d_avgUnknownsInARow);
- StatisticsRegistry::unregisterStat(&d_revertsOnConflicts);
- StatisticsRegistry::unregisterStat(&d_commitsOnConflicts);
- StatisticsRegistry::unregisterStat(&d_nontrivialSatChecks);
-
- StatisticsRegistry::unregisterStat(&d_satPivots);
- StatisticsRegistry::unregisterStat(&d_unsatPivots);
- StatisticsRegistry::unregisterStat(&d_unknownPivots);
-
- StatisticsRegistry::unregisterStat(&d_replayLogRecCount);
- StatisticsRegistry::unregisterStat(&d_replayLogRecConflictEscalation);
- StatisticsRegistry::unregisterStat(&d_replayLogRecEarlyExit);
- StatisticsRegistry::unregisterStat(&d_replayBranchCloseFailures);
- StatisticsRegistry::unregisterStat(&d_replayLeafCloseFailures);
- StatisticsRegistry::unregisterStat(&d_replayBranchSkips);
- StatisticsRegistry::unregisterStat(&d_mirCutsAttempted);
- StatisticsRegistry::unregisterStat(&d_gmiCutsAttempted);
- StatisticsRegistry::unregisterStat(&d_branchCutsAttempted);
- StatisticsRegistry::unregisterStat(&d_cutsReconstructed);
- StatisticsRegistry::unregisterStat(&d_cutsProven);
- StatisticsRegistry::unregisterStat(&d_cutsProofFailed);
- StatisticsRegistry::unregisterStat(&d_cutsReconstructionFailed);
- StatisticsRegistry::unregisterStat(&d_mipReplayLemmaCalls);
- StatisticsRegistry::unregisterStat(&d_mipExternalCuts);
- StatisticsRegistry::unregisterStat(&d_mipExternalBranch);
-
-
- StatisticsRegistry::unregisterStat(&d_inSolveInteger);
- StatisticsRegistry::unregisterStat(&d_branchesExhausted);
- StatisticsRegistry::unregisterStat(&d_execExhausted);
- StatisticsRegistry::unregisterStat(&d_pivotsExhausted);
- StatisticsRegistry::unregisterStat(&d_panicBranches);
- StatisticsRegistry::unregisterStat(&d_relaxCalls);
- StatisticsRegistry::unregisterStat(&d_relaxLinFeas);
- StatisticsRegistry::unregisterStat(&d_relaxLinFeasFailures);
- StatisticsRegistry::unregisterStat(&d_relaxLinInfeas);
- StatisticsRegistry::unregisterStat(&d_relaxLinInfeasFailures);
- StatisticsRegistry::unregisterStat(&d_relaxLinExhausted);
- StatisticsRegistry::unregisterStat(&d_relaxOthers);
-
- StatisticsRegistry::unregisterStat(&d_applyRowsDeleted);
-
- StatisticsRegistry::unregisterStat(&d_replaySimplexTimer);
- StatisticsRegistry::unregisterStat(&d_replayLogTimer);
- StatisticsRegistry::unregisterStat(&d_solveIntTimer);
- StatisticsRegistry::unregisterStat(&d_solveRealRelaxTimer);
-
- StatisticsRegistry::unregisterStat(&d_solveIntCalls);
- StatisticsRegistry::unregisterStat(&d_solveStandardEffort);
-
- StatisticsRegistry::unregisterStat(&d_approxDisabled);
-
- StatisticsRegistry::unregisterStat(&d_replayAttemptFailed);
-
- StatisticsRegistry::unregisterStat(&d_cutsRejectedDuringReplay);
- StatisticsRegistry::unregisterStat(&d_cutsRejectedDuringLemmas);
-
-
- StatisticsRegistry::unregisterStat(&d_solveIntModelsAttempts);
- StatisticsRegistry::unregisterStat(&d_solveIntModelsSuccessful);
- StatisticsRegistry::unregisterStat(&d_mipTimer);
- StatisticsRegistry::unregisterStat(&d_lpTimer);
- StatisticsRegistry::unregisterStat(&d_mipProofsAttempted);
- StatisticsRegistry::unregisterStat(&d_mipProofsSuccessful);
- StatisticsRegistry::unregisterStat(&d_numBranchesFailed);
+ smtStatisticsRegistry()->unregisterStat(&d_statAssertUpperConflicts);
+ smtStatisticsRegistry()->unregisterStat(&d_statAssertLowerConflicts);
+
+ smtStatisticsRegistry()->unregisterStat(&d_statUserVariables);
+ smtStatisticsRegistry()->unregisterStat(&d_statAuxiliaryVariables);
+ smtStatisticsRegistry()->unregisterStat(&d_statDisequalitySplits);
+ smtStatisticsRegistry()->unregisterStat(&d_statDisequalityConflicts);
+ smtStatisticsRegistry()->unregisterStat(&d_simplifyTimer);
+ smtStatisticsRegistry()->unregisterStat(&d_staticLearningTimer);
+
+ smtStatisticsRegistry()->unregisterStat(&d_presolveTime);
+ smtStatisticsRegistry()->unregisterStat(&d_newPropTime);
+
+ smtStatisticsRegistry()->unregisterStat(&d_externalBranchAndBounds);
+
+ smtStatisticsRegistry()->unregisterStat(&d_initialTableauSize);
+ smtStatisticsRegistry()->unregisterStat(&d_currSetToSmaller);
+ smtStatisticsRegistry()->unregisterStat(&d_smallerSetToCurr);
+ smtStatisticsRegistry()->unregisterStat(&d_restartTimer);
+
+ smtStatisticsRegistry()->unregisterStat(&d_boundComputationTime);
+ smtStatisticsRegistry()->unregisterStat(&d_boundComputations);
+ smtStatisticsRegistry()->unregisterStat(&d_boundPropagations);
+
+ smtStatisticsRegistry()->unregisterStat(&d_unknownChecks);
+ smtStatisticsRegistry()->unregisterStat(&d_maxUnknownsInARow);
+ smtStatisticsRegistry()->unregisterStat(&d_avgUnknownsInARow);
+ smtStatisticsRegistry()->unregisterStat(&d_revertsOnConflicts);
+ smtStatisticsRegistry()->unregisterStat(&d_commitsOnConflicts);
+ smtStatisticsRegistry()->unregisterStat(&d_nontrivialSatChecks);
+
+ smtStatisticsRegistry()->unregisterStat(&d_satPivots);
+ smtStatisticsRegistry()->unregisterStat(&d_unsatPivots);
+ smtStatisticsRegistry()->unregisterStat(&d_unknownPivots);
+
+ smtStatisticsRegistry()->unregisterStat(&d_replayLogRecCount);
+ smtStatisticsRegistry()->unregisterStat(&d_replayLogRecConflictEscalation);
+ smtStatisticsRegistry()->unregisterStat(&d_replayLogRecEarlyExit);
+ smtStatisticsRegistry()->unregisterStat(&d_replayBranchCloseFailures);
+ smtStatisticsRegistry()->unregisterStat(&d_replayLeafCloseFailures);
+ smtStatisticsRegistry()->unregisterStat(&d_replayBranchSkips);
+ smtStatisticsRegistry()->unregisterStat(&d_mirCutsAttempted);
+ smtStatisticsRegistry()->unregisterStat(&d_gmiCutsAttempted);
+ smtStatisticsRegistry()->unregisterStat(&d_branchCutsAttempted);
+ smtStatisticsRegistry()->unregisterStat(&d_cutsReconstructed);
+ smtStatisticsRegistry()->unregisterStat(&d_cutsProven);
+ smtStatisticsRegistry()->unregisterStat(&d_cutsProofFailed);
+ smtStatisticsRegistry()->unregisterStat(&d_cutsReconstructionFailed);
+ smtStatisticsRegistry()->unregisterStat(&d_mipReplayLemmaCalls);
+ smtStatisticsRegistry()->unregisterStat(&d_mipExternalCuts);
+ smtStatisticsRegistry()->unregisterStat(&d_mipExternalBranch);
+
+
+ smtStatisticsRegistry()->unregisterStat(&d_inSolveInteger);
+ smtStatisticsRegistry()->unregisterStat(&d_branchesExhausted);
+ smtStatisticsRegistry()->unregisterStat(&d_execExhausted);
+ smtStatisticsRegistry()->unregisterStat(&d_pivotsExhausted);
+ smtStatisticsRegistry()->unregisterStat(&d_panicBranches);
+ smtStatisticsRegistry()->unregisterStat(&d_relaxCalls);
+ smtStatisticsRegistry()->unregisterStat(&d_relaxLinFeas);
+ smtStatisticsRegistry()->unregisterStat(&d_relaxLinFeasFailures);
+ smtStatisticsRegistry()->unregisterStat(&d_relaxLinInfeas);
+ smtStatisticsRegistry()->unregisterStat(&d_relaxLinInfeasFailures);
+ smtStatisticsRegistry()->unregisterStat(&d_relaxLinExhausted);
+ smtStatisticsRegistry()->unregisterStat(&d_relaxOthers);
+
+ smtStatisticsRegistry()->unregisterStat(&d_applyRowsDeleted);
+
+ smtStatisticsRegistry()->unregisterStat(&d_replaySimplexTimer);
+ smtStatisticsRegistry()->unregisterStat(&d_replayLogTimer);
+ smtStatisticsRegistry()->unregisterStat(&d_solveIntTimer);
+ smtStatisticsRegistry()->unregisterStat(&d_solveRealRelaxTimer);
+
+ smtStatisticsRegistry()->unregisterStat(&d_solveIntCalls);
+ smtStatisticsRegistry()->unregisterStat(&d_solveStandardEffort);
+
+ smtStatisticsRegistry()->unregisterStat(&d_approxDisabled);
+
+ smtStatisticsRegistry()->unregisterStat(&d_replayAttemptFailed);
+
+ smtStatisticsRegistry()->unregisterStat(&d_cutsRejectedDuringReplay);
+ smtStatisticsRegistry()->unregisterStat(&d_cutsRejectedDuringLemmas);
+
+
+ smtStatisticsRegistry()->unregisterStat(&d_solveIntModelsAttempts);
+ smtStatisticsRegistry()->unregisterStat(&d_solveIntModelsSuccessful);
+ smtStatisticsRegistry()->unregisterStat(&d_mipTimer);
+ smtStatisticsRegistry()->unregisterStat(&d_lpTimer);
+ smtStatisticsRegistry()->unregisterStat(&d_mipProofsAttempted);
+ smtStatisticsRegistry()->unregisterStat(&d_mipProofsSuccessful);
+ smtStatisticsRegistry()->unregisterStat(&d_numBranchesFailed);
}
bool complexityBelow(const DenseMap<Rational>& row, uint32_t cap){
#include "expr/metakind.h"
#include "expr/node.h"
#include "expr/node_builder.h"
-#include "expr/statistics_registry.h"
#include "options/arith_options.h"
#include "smt/logic_exception.h"
#include "smt_util/boolean_simplification.h"
#include "util/integer.h"
#include "util/rational.h"
#include "util/result.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
#include "theory/arrays/array_info.h"
+#include "smt/smt_statistics_registry.h"
+
namespace CVC4 {
namespace theory {
namespace arrays {
+ArrayInfo::ArrayInfo(context::Context* c, Backtracker<TNode>* b)
+ : ct(c), bck(b), info_map(),
+ d_mergeInfoTimer("theory::arrays::mergeInfoTimer"),
+ d_avgIndexListLength("theory::arrays::avgIndexListLength"),
+ d_avgStoresListLength("theory::arrays::avgStoresListLength"),
+ d_avgInStoresListLength("theory::arrays::avgInStoresListLength"),
+ d_listsCount("theory::arrays::listsCount",0),
+ d_callsMergeInfo("theory::arrays::callsMergeInfo",0),
+ d_maxList("theory::arrays::maxList",0),
+ d_tableSize("theory::arrays::infoTableSize", info_map) {
+ emptyList = new(true) CTNodeList(ct);
+ emptyInfo = new Info(ct, bck);
+ smtStatisticsRegistry()->registerStat(&d_mergeInfoTimer);
+ smtStatisticsRegistry()->registerStat(&d_avgIndexListLength);
+ smtStatisticsRegistry()->registerStat(&d_avgStoresListLength);
+ smtStatisticsRegistry()->registerStat(&d_avgInStoresListLength);
+ smtStatisticsRegistry()->registerStat(&d_listsCount);
+ smtStatisticsRegistry()->registerStat(&d_callsMergeInfo);
+ smtStatisticsRegistry()->registerStat(&d_maxList);
+ smtStatisticsRegistry()->registerStat(&d_tableSize);
+}
+
+ArrayInfo::~ArrayInfo() {
+ CNodeInfoMap::iterator it = info_map.begin();
+ for( ; it != info_map.end(); it++ ) {
+ if((*it).second!= emptyInfo) {
+ delete (*it).second;
+ }
+ }
+ emptyList->deleteSelf();
+ delete emptyInfo;
+ smtStatisticsRegistry()->unregisterStat(&d_mergeInfoTimer);
+ smtStatisticsRegistry()->unregisterStat(&d_avgIndexListLength);
+ smtStatisticsRegistry()->unregisterStat(&d_avgStoresListLength);
+ smtStatisticsRegistry()->unregisterStat(&d_avgInStoresListLength);
+ smtStatisticsRegistry()->unregisterStat(&d_listsCount);
+ smtStatisticsRegistry()->unregisterStat(&d_callsMergeInfo);
+ smtStatisticsRegistry()->unregisterStat(&d_maxList);
+ smtStatisticsRegistry()->unregisterStat(&d_tableSize);
+}
+
bool inList(const CTNodeList* l, const TNode el) {
CTNodeList::const_iterator it = l->begin();
for ( ; it!= l->end(); it ++) {
#include "context/cdlist.h"
#include "context/cdhashmap.h"
#include "expr/node.h"
-#include "expr/statistics_registry.h"
#include "util/ntuple.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
d_callsMergeInfo("theory::arrays::callsMergeInfo",0),
d_maxList("theory::arrays::maxList",0),
d_tableSize("theory::arrays::infoTableSize", info_map) {
- StatisticsRegistry::registerStat(&d_mergeInfoTimer);
- StatisticsRegistry::registerStat(&d_avgIndexListLength);
- StatisticsRegistry::registerStat(&d_avgStoresListLength);
- StatisticsRegistry::registerStat(&d_avgInStoresListLength);
- StatisticsRegistry::registerStat(&d_listsCount);
- StatisticsRegistry::registerStat(&d_callsMergeInfo);
- StatisticsRegistry::registerStat(&d_maxList);
- StatisticsRegistry::registerStat(&d_tableSize);
+ currentStatisticsRegistry()->registerStat(&d_mergeInfoTimer);
+ currentStatisticsRegistry()->registerStat(&d_avgIndexListLength);
+ currentStatisticsRegistry()->registerStat(&d_avgStoresListLength);
+ currentStatisticsRegistry()->registerStat(&d_avgInStoresListLength);
+ currentStatisticsRegistry()->registerStat(&d_listsCount);
+ currentStatisticsRegistry()->registerStat(&d_callsMergeInfo);
+ currentStatisticsRegistry()->registerStat(&d_maxList);
+ currentStatisticsRegistry()->registerStat(&d_tableSize);
}*/
- ArrayInfo(context::Context* c, Backtracker<TNode>* b): ct(c), bck(b), info_map(),
- d_mergeInfoTimer("theory::arrays::mergeInfoTimer"),
- d_avgIndexListLength("theory::arrays::avgIndexListLength"),
- d_avgStoresListLength("theory::arrays::avgStoresListLength"),
- d_avgInStoresListLength("theory::arrays::avgInStoresListLength"),
- d_listsCount("theory::arrays::listsCount",0),
- d_callsMergeInfo("theory::arrays::callsMergeInfo",0),
- d_maxList("theory::arrays::maxList",0),
- d_tableSize("theory::arrays::infoTableSize", info_map) {
- emptyList = new(true) CTNodeList(ct);
- emptyInfo = new Info(ct, bck);
- StatisticsRegistry::registerStat(&d_mergeInfoTimer);
- StatisticsRegistry::registerStat(&d_avgIndexListLength);
- StatisticsRegistry::registerStat(&d_avgStoresListLength);
- StatisticsRegistry::registerStat(&d_avgInStoresListLength);
- StatisticsRegistry::registerStat(&d_listsCount);
- StatisticsRegistry::registerStat(&d_callsMergeInfo);
- StatisticsRegistry::registerStat(&d_maxList);
- StatisticsRegistry::registerStat(&d_tableSize);
- }
+ ArrayInfo(context::Context* c, Backtracker<TNode>* b);
- ~ArrayInfo() {
- CNodeInfoMap::iterator it = info_map.begin();
- for( ; it != info_map.end(); it++ ) {
- if((*it).second!= emptyInfo) {
- delete (*it).second;
- }
- }
- emptyList->deleteSelf();
- delete emptyInfo;
- StatisticsRegistry::unregisterStat(&d_mergeInfoTimer);
- StatisticsRegistry::unregisterStat(&d_avgIndexListLength);
- StatisticsRegistry::unregisterStat(&d_avgStoresListLength);
- StatisticsRegistry::unregisterStat(&d_avgInStoresListLength);
- StatisticsRegistry::unregisterStat(&d_listsCount);
- StatisticsRegistry::unregisterStat(&d_callsMergeInfo);
- StatisticsRegistry::unregisterStat(&d_maxList);
- StatisticsRegistry::unregisterStat(&d_tableSize);
- };
+ ~ArrayInfo();
/**
* adds the node a to the map if it does not exist
#include "options/arrays_options.h"
#include "options/smt_options.h"
#include "smt/logic_exception.h"
+#include "smt/smt_statistics_registry.h"
#include "smt_util/command.h"
#include "theory/rewriter.h"
#include "theory/theory_model.h"
d_arrayMerges(c),
d_inCheckModel(false)
{
- StatisticsRegistry::registerStat(&d_numRow);
- StatisticsRegistry::registerStat(&d_numExt);
- StatisticsRegistry::registerStat(&d_numProp);
- StatisticsRegistry::registerStat(&d_numExplain);
- StatisticsRegistry::registerStat(&d_numNonLinear);
- StatisticsRegistry::registerStat(&d_numSharedArrayVarSplits);
- StatisticsRegistry::registerStat(&d_numGetModelValSplits);
- StatisticsRegistry::registerStat(&d_numGetModelValConflicts);
- StatisticsRegistry::registerStat(&d_numSetModelValSplits);
- StatisticsRegistry::registerStat(&d_numSetModelValConflicts);
+ smtStatisticsRegistry()->registerStat(&d_numRow);
+ smtStatisticsRegistry()->registerStat(&d_numExt);
+ smtStatisticsRegistry()->registerStat(&d_numProp);
+ smtStatisticsRegistry()->registerStat(&d_numExplain);
+ smtStatisticsRegistry()->registerStat(&d_numNonLinear);
+ smtStatisticsRegistry()->registerStat(&d_numSharedArrayVarSplits);
+ smtStatisticsRegistry()->registerStat(&d_numGetModelValSplits);
+ smtStatisticsRegistry()->registerStat(&d_numGetModelValConflicts);
+ smtStatisticsRegistry()->registerStat(&d_numSetModelValSplits);
+ smtStatisticsRegistry()->registerStat(&d_numSetModelValConflicts);
d_true = NodeManager::currentNM()->mkConst<bool>(true);
d_false = NodeManager::currentNM()->mkConst<bool>(false);
it2->second->deleteSelf();
}
delete d_constReadsContext;
- StatisticsRegistry::unregisterStat(&d_numRow);
- StatisticsRegistry::unregisterStat(&d_numExt);
- StatisticsRegistry::unregisterStat(&d_numProp);
- StatisticsRegistry::unregisterStat(&d_numExplain);
- StatisticsRegistry::unregisterStat(&d_numNonLinear);
- StatisticsRegistry::unregisterStat(&d_numSharedArrayVarSplits);
- StatisticsRegistry::unregisterStat(&d_numGetModelValSplits);
- StatisticsRegistry::unregisterStat(&d_numGetModelValConflicts);
- StatisticsRegistry::unregisterStat(&d_numSetModelValSplits);
- StatisticsRegistry::unregisterStat(&d_numSetModelValConflicts);
+ smtStatisticsRegistry()->unregisterStat(&d_numRow);
+ smtStatisticsRegistry()->unregisterStat(&d_numExt);
+ smtStatisticsRegistry()->unregisterStat(&d_numProp);
+ smtStatisticsRegistry()->unregisterStat(&d_numExplain);
+ smtStatisticsRegistry()->unregisterStat(&d_numNonLinear);
+ smtStatisticsRegistry()->unregisterStat(&d_numSharedArrayVarSplits);
+ smtStatisticsRegistry()->unregisterStat(&d_numGetModelValSplits);
+ smtStatisticsRegistry()->unregisterStat(&d_numGetModelValConflicts);
+ smtStatisticsRegistry()->unregisterStat(&d_numSetModelValSplits);
+ smtStatisticsRegistry()->unregisterStat(&d_numSetModelValConflicts);
}
void TheoryArrays::setMasterEqualityEngine(eq::EqualityEngine* eq) {
#include "context/cdhashmap.h"
#include "context/cdhashset.h"
#include "context/cdqueue.h"
-#include "expr/statistics_registry.h"
#include "theory/arrays/array_info.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
#include "options/bv_options.h"
#include "smt_util/dump.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/rewriter.h"
, d_numArgsSkolemized("theory::bv::AbstractioModule::NumArgsSkolemized", 0)
, d_abstractionTime("theory::bv::AbstractioModule::AbstractionTime")
{
- StatisticsRegistry::registerStat(&d_numFunctionsAbstracted);
- StatisticsRegistry::registerStat(&d_numArgsSkolemized);
- StatisticsRegistry::registerStat(&d_abstractionTime);
+ smtStatisticsRegistry()->registerStat(&d_numFunctionsAbstracted);
+ smtStatisticsRegistry()->registerStat(&d_numArgsSkolemized);
+ smtStatisticsRegistry()->registerStat(&d_abstractionTime);
}
AbstractionModule::Statistics::~Statistics() {
- StatisticsRegistry::unregisterStat(&d_numFunctionsAbstracted);
- StatisticsRegistry::unregisterStat(&d_numArgsSkolemized);
- StatisticsRegistry::unregisterStat(&d_abstractionTime);
+ smtStatisticsRegistry()->unregisterStat(&d_numFunctionsAbstracted);
+ smtStatisticsRegistry()->unregisterStat(&d_numArgsSkolemized);
+ smtStatisticsRegistry()->unregisterStat(&d_abstractionTime);
}
#include <ext/hash_set>
#include "expr/node.h"
-#include "expr/statistics_registry.h"
#include "theory/substitutions.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
, d_cnfConversionTime("theory::bv::AigBitblaster::cnfConversionTime")
, d_solveTime("theory::bv::AigBitblaster::solveTime")
{
- StatisticsRegistry::registerStat(&d_numClauses);
- StatisticsRegistry::registerStat(&d_numVariables);
- StatisticsRegistry::registerStat(&d_simplificationTime);
- StatisticsRegistry::registerStat(&d_cnfConversionTime);
- StatisticsRegistry::registerStat(&d_solveTime);
+ smtStatisticsRegistry()->registerStat(&d_numClauses);
+ smtStatisticsRegistry()->registerStat(&d_numVariables);
+ smtStatisticsRegistry()->registerStat(&d_simplificationTime);
+ smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
+ smtStatisticsRegistry()->registerStat(&d_solveTime);
}
AigBitblaster::Statistics::~Statistics() {
- StatisticsRegistry::unregisterStat(&d_numClauses);
- StatisticsRegistry::unregisterStat(&d_numVariables);
- StatisticsRegistry::unregisterStat(&d_simplificationTime);
- StatisticsRegistry::unregisterStat(&d_cnfConversionTime);
- StatisticsRegistry::unregisterStat(&d_solveTime);
+ smtStatisticsRegistry()->unregisterStat(&d_numClauses);
+ smtStatisticsRegistry()->unregisterStat(&d_numVariables);
+ smtStatisticsRegistry()->unregisterStat(&d_simplificationTime);
+ smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
+ smtStatisticsRegistry()->unregisterStat(&d_solveTime);
}
#else // CVC4_USE_ABC
**/
#include "theory/bv/bv_quick_check.h"
-#include "theory/bv/theory_bv_utils.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/bv/bitblaster_template.h"
+#include "theory/bv/theory_bv_utils.h"
using namespace CVC4;
using namespace CVC4::theory;
, d_finalPeriod("theory::bv::"+name+"::QuickXplain::FinalPeriod", 0)
, d_avgMinimizationRatio("theory::bv::"+name+"::QuickXplain::AvgMinRatio")
{
- StatisticsRegistry::registerStat(&d_xplainTime);
- StatisticsRegistry::registerStat(&d_numSolved);
- StatisticsRegistry::registerStat(&d_numUnknown);
- StatisticsRegistry::registerStat(&d_numUnknownWasUnsat);
- StatisticsRegistry::registerStat(&d_numConflictsMinimized);
- StatisticsRegistry::registerStat(&d_finalPeriod);
- StatisticsRegistry::registerStat(&d_avgMinimizationRatio);
+ smtStatisticsRegistry()->registerStat(&d_xplainTime);
+ smtStatisticsRegistry()->registerStat(&d_numSolved);
+ smtStatisticsRegistry()->registerStat(&d_numUnknown);
+ smtStatisticsRegistry()->registerStat(&d_numUnknownWasUnsat);
+ smtStatisticsRegistry()->registerStat(&d_numConflictsMinimized);
+ smtStatisticsRegistry()->registerStat(&d_finalPeriod);
+ smtStatisticsRegistry()->registerStat(&d_avgMinimizationRatio);
}
QuickXPlain::Statistics::~Statistics() {
- StatisticsRegistry::unregisterStat(&d_xplainTime);
- StatisticsRegistry::unregisterStat(&d_numSolved);
- StatisticsRegistry::unregisterStat(&d_numUnknown);
- StatisticsRegistry::unregisterStat(&d_numUnknownWasUnsat);
- StatisticsRegistry::unregisterStat(&d_numConflictsMinimized);
- StatisticsRegistry::unregisterStat(&d_finalPeriod);
- StatisticsRegistry::unregisterStat(&d_avgMinimizationRatio);
+ smtStatisticsRegistry()->unregisterStat(&d_xplainTime);
+ smtStatisticsRegistry()->unregisterStat(&d_numSolved);
+ smtStatisticsRegistry()->unregisterStat(&d_numUnknown);
+ smtStatisticsRegistry()->unregisterStat(&d_numUnknownWasUnsat);
+ smtStatisticsRegistry()->unregisterStat(&d_numConflictsMinimized);
+ smtStatisticsRegistry()->unregisterStat(&d_finalPeriod);
+ smtStatisticsRegistry()->unregisterStat(&d_avgMinimizationRatio);
}
-
#include "context/cdo.h"
#include "expr/node.h"
-#include "expr/statistics_registry.h"
#include "prop/sat_solver_types.h"
#include "theory/bv/theory_bv_utils.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
**
** Algebraic solver.
**/
+#include "theory/bv/bv_subtheory_algebraic.h"
#include "options/bv_options.h"
#include "smt_util/boolean_simplification.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/bv/bv_quick_check.h"
-#include "theory/bv/bv_subtheory_algebraic.h"
#include "theory/bv/theory_bv.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/theory_model.h"
, d_solveTime("theory::bv::AlgebraicSolver::SolveTime")
, d_useHeuristic("theory::bv::AlgebraicSolver::UseHeuristic", 0.2)
{
- StatisticsRegistry::registerStat(&d_numCallstoCheck);
- StatisticsRegistry::registerStat(&d_numSimplifiesToTrue);
- StatisticsRegistry::registerStat(&d_numSimplifiesToFalse);
- StatisticsRegistry::registerStat(&d_numUnsat);
- StatisticsRegistry::registerStat(&d_numSat);
- StatisticsRegistry::registerStat(&d_numUnknown);
- StatisticsRegistry::registerStat(&d_solveTime);
- StatisticsRegistry::registerStat(&d_useHeuristic);
+ smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
+ smtStatisticsRegistry()->registerStat(&d_numSimplifiesToTrue);
+ smtStatisticsRegistry()->registerStat(&d_numSimplifiesToFalse);
+ smtStatisticsRegistry()->registerStat(&d_numUnsat);
+ smtStatisticsRegistry()->registerStat(&d_numSat);
+ smtStatisticsRegistry()->registerStat(&d_numUnknown);
+ smtStatisticsRegistry()->registerStat(&d_solveTime);
+ smtStatisticsRegistry()->registerStat(&d_useHeuristic);
}
AlgebraicSolver::Statistics::~Statistics() {
- StatisticsRegistry::unregisterStat(&d_numCallstoCheck);
- StatisticsRegistry::unregisterStat(&d_numSimplifiesToTrue);
- StatisticsRegistry::unregisterStat(&d_numSimplifiesToFalse);
- StatisticsRegistry::unregisterStat(&d_numUnsat);
- StatisticsRegistry::unregisterStat(&d_numSat);
- StatisticsRegistry::unregisterStat(&d_numUnknown);
- StatisticsRegistry::unregisterStat(&d_solveTime);
- StatisticsRegistry::unregisterStat(&d_useHeuristic);
+ smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck);
+ smtStatisticsRegistry()->unregisterStat(&d_numSimplifiesToTrue);
+ smtStatisticsRegistry()->unregisterStat(&d_numSimplifiesToFalse);
+ smtStatisticsRegistry()->unregisterStat(&d_numUnsat);
+ smtStatisticsRegistry()->unregisterStat(&d_numSat);
+ smtStatisticsRegistry()->unregisterStat(&d_numUnknown);
+ smtStatisticsRegistry()->unregisterStat(&d_solveTime);
+ smtStatisticsRegistry()->unregisterStat(&d_useHeuristic);
}
bool hasExpensiveBVOperatorsRec(TNode fact, TNodeSet& seen) {
#include "decision/decision_attributes.h"
#include "options/decision_options.h"
#include "options/bv_options.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/bv/abstraction.h"
#include "theory/bv/bitblaster_template.h"
#include "theory/bv/bv_quick_check.h"
: d_numCallstoCheck("theory::bv::BitblastSolver::NumCallsToCheck", 0)
, d_numBBLemmas("theory::bv::BitblastSolver::NumTimesLemmasBB", 0)
{
- StatisticsRegistry::registerStat(&d_numCallstoCheck);
- StatisticsRegistry::registerStat(&d_numBBLemmas);
+ smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
+ smtStatisticsRegistry()->registerStat(&d_numBBLemmas);
}
BitblastSolver::Statistics::~Statistics() {
- StatisticsRegistry::unregisterStat(&d_numCallstoCheck);
- StatisticsRegistry::unregisterStat(&d_numBBLemmas);
+ smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck);
+ smtStatisticsRegistry()->unregisterStat(&d_numBBLemmas);
}
void BitblastSolver::setAbstraction(AbstractionModule* abs) {
#include "options/bv_options.h"
#include "options/smt_options.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/bv/slicer.h"
#include "theory/bv/theory_bv.h"
#include "theory/bv/theory_bv_utils.h"
: d_numCallstoCheck("theory::bv::CoreSolver::NumCallsToCheck", 0)
, d_slicerEnabled("theory::bv::CoreSolver::SlicerEnabled", false)
{
- StatisticsRegistry::registerStat(&d_numCallstoCheck);
- StatisticsRegistry::registerStat(&d_slicerEnabled);
+ smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
+ smtStatisticsRegistry()->registerStat(&d_slicerEnabled);
}
CoreSolver::Statistics::~Statistics() {
- StatisticsRegistry::unregisterStat(&d_numCallstoCheck);
- StatisticsRegistry::unregisterStat(&d_slicerEnabled);
+ smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck);
+ smtStatisticsRegistry()->unregisterStat(&d_slicerEnabled);
}
#include "theory/bv/bv_subtheory_inequality.h"
#include "options/smt_options.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/bv/theory_bv.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/theory_model.h"
InequalitySolver::Statistics::Statistics()
: d_numCallstoCheck("theory::bv::InequalitySolver::NumCallsToCheck", 0)
{
- StatisticsRegistry::registerStat(&d_numCallstoCheck);
+ smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
}
InequalitySolver::Statistics::~Statistics() {
- StatisticsRegistry::unregisterStat(&d_numCallstoCheck);
+ smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck);
}
**
** \brief Preprocessing pass that lifts bit-vectors of size 1 to booleans.
**
- ** Preprocessing pass that lifts bit-vectors of size 1 to booleans.
+ ** Preprocessing pass that lifts bit-vectors of size 1 to booleans.
**/
#include "theory/bv/bv_to_bool.h"
#include "smt_util/node_visitor.h"
+#include "smt/smt_statistics_registry.h"
using namespace std;
using namespace CVC4;
{}
void BvToBoolPreprocessor::addToLiftCache(TNode term, Node new_term) {
- Assert (new_term != Node());
+ Assert (new_term != Node());
Assert (!hasLiftCache(term));
Assert (term.getType() == new_term.getType());
d_liftCache[term] = new_term;
, d_numAtomsLifted("theory::bv::BvToBoolPreprocess::NumberOfAtomsLifted", 0)
, d_numTermsForcedLifted("theory::bv::BvToBoolPreprocess::NumberOfTermsForcedLifted", 0)
{
- StatisticsRegistry::registerStat(&d_numTermsLifted);
- StatisticsRegistry::registerStat(&d_numAtomsLifted);
- StatisticsRegistry::registerStat(&d_numTermsForcedLifted);
+ smtStatisticsRegistry()->registerStat(&d_numTermsLifted);
+ smtStatisticsRegistry()->registerStat(&d_numAtomsLifted);
+ smtStatisticsRegistry()->registerStat(&d_numTermsForcedLifted);
}
BvToBoolPreprocessor::Statistics::~Statistics() {
- StatisticsRegistry::unregisterStat(&d_numTermsLifted);
- StatisticsRegistry::unregisterStat(&d_numAtomsLifted);
- StatisticsRegistry::unregisterStat(&d_numTermsForcedLifted);
+ smtStatisticsRegistry()->unregisterStat(&d_numTermsLifted);
+ smtStatisticsRegistry()->unregisterStat(&d_numAtomsLifted);
+ smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLifted);
}
**
** \brief Preprocessing pass that lifts bit-vectors of size 1 to booleans.
**
- ** Preprocessing pass that lifts bit-vectors of size 1 to booleans.
+ ** Preprocessing pass that lifts bit-vectors of size 1 to booleans.
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__BV__BV_TO_BOOL_H
#define __CVC4__THEORY__BV__BV_TO_BOOL_H
-#include "expr/statistics_registry.h"
#include "theory/bv/theory_bv_utils.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
namespace bv {
-typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap;
+typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap;
class BvToBoolPreprocessor {
#include "options/bv_options.h"
#include "prop/cnf_stream.h"
#include "prop/sat_solver_factory.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/bv/bitblaster_template.h"
#include "theory/bv/theory_bv.h"
#include "theory/theory_model.h"
d_bitblastingRegistrar = new BitblastingRegistrar(this);
d_nullContext = new context::Context();
- d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "EagerBitblaster");
+ d_satSolver = prop::SatSolverFactory::createMinisat(
+ d_nullContext, smtStatisticsRegistry(), "EagerBitblaster");
d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar,
d_nullContext, d_bv->globals());
#include "prop/cnf_stream.h"
#include "prop/sat_solver.h"
#include "prop/sat_solver_factory.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/bv/abstraction.h"
#include "theory/bv/theory_bv.h"
#include "theory/rewriter.h"
, d_name(name)
, d_statistics(name) {
- d_satSolver = prop::SatSolverFactory::createMinisat(c, name);
+ d_satSolver = prop::SatSolverFactory::createMinisat(
+ c, smtStatisticsRegistry(), name);
d_nullRegistrar = new prop::NullRegistrar();
d_nullContext = new context::Context();
d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar,
d_numBitblastingPropagations("theory::bv::"+prefix+"::NumberOfBitblastingPropagations", 0),
d_bitblastTimer("theory::bv::"+prefix+"::BitblastTimer")
{
- StatisticsRegistry::registerStat(&d_numTermClauses);
- StatisticsRegistry::registerStat(&d_numAtomClauses);
- StatisticsRegistry::registerStat(&d_numTerms);
- StatisticsRegistry::registerStat(&d_numAtoms);
- StatisticsRegistry::registerStat(&d_numExplainedPropagations);
- StatisticsRegistry::registerStat(&d_numBitblastingPropagations);
- StatisticsRegistry::registerStat(&d_bitblastTimer);
+ smtStatisticsRegistry()->registerStat(&d_numTermClauses);
+ smtStatisticsRegistry()->registerStat(&d_numAtomClauses);
+ smtStatisticsRegistry()->registerStat(&d_numTerms);
+ smtStatisticsRegistry()->registerStat(&d_numAtoms);
+ smtStatisticsRegistry()->registerStat(&d_numExplainedPropagations);
+ smtStatisticsRegistry()->registerStat(&d_numBitblastingPropagations);
+ smtStatisticsRegistry()->registerStat(&d_bitblastTimer);
}
TLazyBitblaster::Statistics::~Statistics() {
- StatisticsRegistry::unregisterStat(&d_numTermClauses);
- StatisticsRegistry::unregisterStat(&d_numAtomClauses);
- StatisticsRegistry::unregisterStat(&d_numTerms);
- StatisticsRegistry::unregisterStat(&d_numAtoms);
- StatisticsRegistry::unregisterStat(&d_numExplainedPropagations);
- StatisticsRegistry::unregisterStat(&d_numBitblastingPropagations);
- StatisticsRegistry::unregisterStat(&d_bitblastTimer);
+ smtStatisticsRegistry()->unregisterStat(&d_numTermClauses);
+ smtStatisticsRegistry()->unregisterStat(&d_numAtomClauses);
+ smtStatisticsRegistry()->unregisterStat(&d_numTerms);
+ smtStatisticsRegistry()->unregisterStat(&d_numAtoms);
+ smtStatisticsRegistry()->unregisterStat(&d_numExplainedPropagations);
+ smtStatisticsRegistry()->unregisterStat(&d_numBitblastingPropagations);
+ smtStatisticsRegistry()->unregisterStat(&d_bitblastTimer);
}
bool TLazyBitblaster::MinisatNotify::notify(prop::SatLiteral lit) {
invalidateModelCache();
// recreate sat solver
- d_satSolver = prop::SatSolverFactory::createMinisat(d_ctx);
+ d_satSolver = prop::SatSolverFactory::createMinisat(
+ d_ctx, smtStatisticsRegistry());
d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar,
d_nullContext, d_bv->globals());
**
** Bitvector theory.
**/
+#include "theory/bv/slicer.h"
#include "options/bv_options.h"
-#include "theory/bv/slicer.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/rewriter.h"
d_avgFindDepth("theory::bv::slicer::AverageFindDepth"),
d_numAddedEqualities("theory::bv::slicer::NumberOfEqualitiesAdded", Slicer::d_numAddedEqualities)
{
- StatisticsRegistry::registerStat(&d_numRepresentatives);
- StatisticsRegistry::registerStat(&d_numSplits);
- StatisticsRegistry::registerStat(&d_numMerges);
- StatisticsRegistry::registerStat(&d_avgFindDepth);
- StatisticsRegistry::registerStat(&d_numAddedEqualities);
+ smtStatisticsRegistry()->registerStat(&d_numRepresentatives);
+ smtStatisticsRegistry()->registerStat(&d_numSplits);
+ smtStatisticsRegistry()->registerStat(&d_numMerges);
+ smtStatisticsRegistry()->registerStat(&d_avgFindDepth);
+ smtStatisticsRegistry()->registerStat(&d_numAddedEqualities);
}
UnionFind::Statistics::~Statistics() {
- StatisticsRegistry::unregisterStat(&d_numRepresentatives);
- StatisticsRegistry::unregisterStat(&d_numSplits);
- StatisticsRegistry::unregisterStat(&d_numMerges);
- StatisticsRegistry::unregisterStat(&d_avgFindDepth);
- StatisticsRegistry::unregisterStat(&d_numAddedEqualities);
+ smtStatisticsRegistry()->unregisterStat(&d_numRepresentatives);
+ smtStatisticsRegistry()->unregisterStat(&d_numSplits);
+ smtStatisticsRegistry()->unregisterStat(&d_numMerges);
+ smtStatisticsRegistry()->unregisterStat(&d_avgFindDepth);
+ smtStatisticsRegistry()->unregisterStat(&d_numAddedEqualities);
}
#include <ext/hash_map>
#include "expr/node.h"
-#include "expr/statistics_registry.h"
#include "theory/bv/theory_bv_utils.h"
#include "util/bitvector.h"
#include "util/index.h"
-
+#include "util/statistics_registry.h"
#ifndef __CVC4__THEORY__BV__SLICER_BV_H
#define __CVC4__THEORY__BV__SLICER_BV_H
#include "options/bv_options.h"
#include "options/smt_options.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/bv/abstraction.h"
#include "theory/bv/bv_eager_solver.h"
#include "theory/bv/bv_subtheory_algebraic.h"
d_weightComputationTimer("theory::bv::weightComputationTimer"),
d_numMultSlice("theory::bv::NumMultSliceApplied", 0)
{
- StatisticsRegistry::registerStat(&d_avgConflictSize);
- StatisticsRegistry::registerStat(&d_solveSubstitutions);
- StatisticsRegistry::registerStat(&d_solveTimer);
- StatisticsRegistry::registerStat(&d_numCallsToCheckFullEffort);
- StatisticsRegistry::registerStat(&d_numCallsToCheckStandardEffort);
- StatisticsRegistry::registerStat(&d_weightComputationTimer);
- StatisticsRegistry::registerStat(&d_numMultSlice);
+ smtStatisticsRegistry()->registerStat(&d_avgConflictSize);
+ smtStatisticsRegistry()->registerStat(&d_solveSubstitutions);
+ smtStatisticsRegistry()->registerStat(&d_solveTimer);
+ smtStatisticsRegistry()->registerStat(&d_numCallsToCheckFullEffort);
+ smtStatisticsRegistry()->registerStat(&d_numCallsToCheckStandardEffort);
+ smtStatisticsRegistry()->registerStat(&d_weightComputationTimer);
+ smtStatisticsRegistry()->registerStat(&d_numMultSlice);
}
TheoryBV::Statistics::~Statistics() {
- StatisticsRegistry::unregisterStat(&d_avgConflictSize);
- StatisticsRegistry::unregisterStat(&d_solveSubstitutions);
- StatisticsRegistry::unregisterStat(&d_solveTimer);
- StatisticsRegistry::unregisterStat(&d_numCallsToCheckFullEffort);
- StatisticsRegistry::unregisterStat(&d_numCallsToCheckStandardEffort);
- StatisticsRegistry::unregisterStat(&d_weightComputationTimer);
- StatisticsRegistry::unregisterStat(&d_numMultSlice);
+ smtStatisticsRegistry()->unregisterStat(&d_avgConflictSize);
+ smtStatisticsRegistry()->unregisterStat(&d_solveSubstitutions);
+ smtStatisticsRegistry()->unregisterStat(&d_solveTimer);
+ smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckFullEffort);
+ smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckStandardEffort);
+ smtStatisticsRegistry()->unregisterStat(&d_weightComputationTimer);
+ smtStatisticsRegistry()->unregisterStat(&d_numMultSlice);
}
Node TheoryBV::getBVDivByZero(Kind k, unsigned width) {
#include "context/cdhashset.h"
#include "context/cdlist.h"
#include "context/context.h"
-#include "expr/statistics_registry.h"
#include "smt/smt_globals.h"
#include "theory/bv/bv_subtheory.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/theory.h"
#include "util/hash.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
#include <sstream>
#include "context/context.h"
-#include "expr/statistics_registry.h"
#include "smt_util/command.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/theory.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
// /** Constructor */
// RuleStatistics()
// : d_ruleApplications(getStatName("theory::bv::RewriteRules::count"), 0) {
- // StatisticsRegistry::registerStat(&d_ruleApplications);
+ // currentStatisticsRegistry()->registerStat(&d_ruleApplications);
// }
// /** Destructor */
void TheoryBVRewriter::init() {
// s_allRules = new AllRewriteRules;
// d_rewriteTimer = new TimerStat("theory::bv::rewriteTimer");
- // StatisticsRegistry::registerStat(d_rewriteTimer);
+ // smtStatisticsRegistry()->registerStat(d_rewriteTimer);
initializeRewrites();
}
void TheoryBVRewriter::shutdown() {
// delete s_allRules;
- // StatisticsRegistry::unregisterStat(d_rewriteTimer);
+ // smtStatisticsRegistry()->unregisterStat(d_rewriteTimer);
//delete d_rewriteTimer;
}
#ifndef __CVC4__THEORY__BV__THEORY_BV_REWRITER_H
#define __CVC4__THEORY__BV__THEORY_BV_REWRITER_H
-#include "expr/statistics_registry.h"
#include "theory/rewriter.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
** Kim, Somenzi, Jin. Efficient Term-ITE Conversion for SMT. FMCAD 2009.
** Burch, Jerry. Techniques for Verifying Superscalar Microprocessors. DAC '96
**/
-
-
#include "theory/ite_utilities.h"
+
#include <utility>
+
+#include "smt/smt_statistics_registry.h"
#include "theory/rewriter.h"
#include "theory/theory.h"
d_compressCalls("ite-simp::compressCalls", 0),
d_skolemsAdded("ite-simp::skolems", 0)
{
- StatisticsRegistry::registerStat(&d_compressCalls);
- StatisticsRegistry::registerStat(&d_skolemsAdded);
+ smtStatisticsRegistry()->registerStat(&d_compressCalls);
+ smtStatisticsRegistry()->registerStat(&d_skolemsAdded);
}
ITECompressor::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_compressCalls);
- StatisticsRegistry::unregisterStat(&d_skolemsAdded);
+ smtStatisticsRegistry()->unregisterStat(&d_compressCalls);
+ smtStatisticsRegistry()->unregisterStat(&d_skolemsAdded);
}
Node ITECompressor::push_back_boolean(Node original, Node compressed){
d_simpITEVisits("ite-simp::simpITE.visits", 0),
d_inSmaller("ite-simp::inSmaller")
{
- StatisticsRegistry::registerStat(&d_maxNonConstantsFolded);
- StatisticsRegistry::registerStat(&d_unexpected);
- StatisticsRegistry::registerStat(&d_unsimplified);
- StatisticsRegistry::registerStat(&d_exactMatchFold);
- StatisticsRegistry::registerStat(&d_binaryPredFold);
- StatisticsRegistry::registerStat(&d_specialEqualityFolds);
- StatisticsRegistry::registerStat(&d_simpITEVisits);
- StatisticsRegistry::registerStat(&d_inSmaller);
+ smtStatisticsRegistry()->registerStat(&d_maxNonConstantsFolded);
+ smtStatisticsRegistry()->registerStat(&d_unexpected);
+ smtStatisticsRegistry()->registerStat(&d_unsimplified);
+ smtStatisticsRegistry()->registerStat(&d_exactMatchFold);
+ smtStatisticsRegistry()->registerStat(&d_binaryPredFold);
+ smtStatisticsRegistry()->registerStat(&d_specialEqualityFolds);
+ smtStatisticsRegistry()->registerStat(&d_simpITEVisits);
+ smtStatisticsRegistry()->registerStat(&d_inSmaller);
}
ITESimplifier::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_maxNonConstantsFolded);
- StatisticsRegistry::unregisterStat(&d_unexpected);
- StatisticsRegistry::unregisterStat(&d_unsimplified);
- StatisticsRegistry::unregisterStat(&d_exactMatchFold);
- StatisticsRegistry::unregisterStat(&d_binaryPredFold);
- StatisticsRegistry::unregisterStat(&d_specialEqualityFolds);
- StatisticsRegistry::unregisterStat(&d_simpITEVisits);
- StatisticsRegistry::unregisterStat(&d_inSmaller);
+ smtStatisticsRegistry()->unregisterStat(&d_maxNonConstantsFolded);
+ smtStatisticsRegistry()->unregisterStat(&d_unexpected);
+ smtStatisticsRegistry()->unregisterStat(&d_unsimplified);
+ smtStatisticsRegistry()->unregisterStat(&d_exactMatchFold);
+ smtStatisticsRegistry()->unregisterStat(&d_binaryPredFold);
+ smtStatisticsRegistry()->unregisterStat(&d_specialEqualityFolds);
+ smtStatisticsRegistry()->unregisterStat(&d_simpITEVisits);
+ smtStatisticsRegistry()->unregisterStat(&d_inSmaller);
}
bool ITESimplifier::isConstantIte(TNode e){
#include <vector>
#include "expr/node.h"
-#include "expr/statistics_registry.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
#include "expr/datatype.h"
#include "options/quantifiers_options.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/term_database.h"
d_cegqi_lemmas_refine("CegInstantiation::cegqi_lemmas_refine", 0),
d_cegqi_si_lemmas("CegInstantiation::cegqi_lemmas_si", 0)
{
- StatisticsRegistry::registerStat(&d_cegqi_lemmas_ce);
- StatisticsRegistry::registerStat(&d_cegqi_lemmas_refine);
- StatisticsRegistry::registerStat(&d_cegqi_si_lemmas);
+ smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_ce);
+ smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_refine);
+ smtStatisticsRegistry()->registerStat(&d_cegqi_si_lemmas);
}
CegInstantiation::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_cegqi_lemmas_ce);
- StatisticsRegistry::unregisterStat(&d_cegqi_lemmas_refine);
- StatisticsRegistry::unregisterStat(&d_cegqi_si_lemmas);
+ smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_ce);
+ smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_refine);
+ smtStatisticsRegistry()->unregisterStat(&d_cegqi_si_lemmas);
}
#ifndef __CVC4__CEG_INSTANTIATOR_H
#define __CVC4__CEG_INSTANTIATOR_H
-#include "expr/statistics_registry.h"
#include "theory/quantifiers_engine.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
#ifndef __CVC4__INST_STRATEGY_CBQI_H
#define __CVC4__INST_STRATEGY_CBQI_H
-#include "expr/statistics_registry.h"
#include "theory/arith/arithvar.h"
#include "theory/quantifiers/ceg_instantiator.h"
#include "theory/quantifiers/instantiation_engine.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
#include "context/context.h"
#include "context/context_mm.h"
-#include "expr/statistics_registry.h"
#include "theory/quantifiers/instantiation_engine.h"
#include "theory/quantifiers/trigger.h"
#include "theory/quantifiers_engine.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
d_eval_lits("QModelBuilderIG::Eval_Lits", 0 ),
d_eval_lits_unknown("QModelBuilderIG::Eval_Lits_Unknown", 0 )
{
- StatisticsRegistry::registerStat(&d_num_quants_init);
- StatisticsRegistry::registerStat(&d_num_partial_quants_init);
- StatisticsRegistry::registerStat(&d_init_inst_gen_lemmas);
- StatisticsRegistry::registerStat(&d_inst_gen_lemmas);
- StatisticsRegistry::registerStat(&d_eval_formulas);
- StatisticsRegistry::registerStat(&d_eval_uf_terms);
- StatisticsRegistry::registerStat(&d_eval_lits);
- StatisticsRegistry::registerStat(&d_eval_lits_unknown);
+ smtStatisticsRegistry()->registerStat(&d_num_quants_init);
+ smtStatisticsRegistry()->registerStat(&d_num_partial_quants_init);
+ smtStatisticsRegistry()->registerStat(&d_init_inst_gen_lemmas);
+ smtStatisticsRegistry()->registerStat(&d_inst_gen_lemmas);
+ smtStatisticsRegistry()->registerStat(&d_eval_formulas);
+ smtStatisticsRegistry()->registerStat(&d_eval_uf_terms);
+ smtStatisticsRegistry()->registerStat(&d_eval_lits);
+ smtStatisticsRegistry()->registerStat(&d_eval_lits_unknown);
}
QModelBuilderIG::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_num_quants_init);
- StatisticsRegistry::unregisterStat(&d_num_partial_quants_init);
- StatisticsRegistry::unregisterStat(&d_init_inst_gen_lemmas);
- StatisticsRegistry::unregisterStat(&d_inst_gen_lemmas);
- StatisticsRegistry::unregisterStat(&d_eval_formulas);
- StatisticsRegistry::unregisterStat(&d_eval_uf_terms);
- StatisticsRegistry::unregisterStat(&d_eval_lits);
- StatisticsRegistry::unregisterStat(&d_eval_lits_unknown);
+ smtStatisticsRegistry()->unregisterStat(&d_num_quants_init);
+ smtStatisticsRegistry()->unregisterStat(&d_num_partial_quants_init);
+ smtStatisticsRegistry()->unregisterStat(&d_init_inst_gen_lemmas);
+ smtStatisticsRegistry()->unregisterStat(&d_inst_gen_lemmas);
+ smtStatisticsRegistry()->unregisterStat(&d_eval_formulas);
+ smtStatisticsRegistry()->unregisterStat(&d_eval_uf_terms);
+ smtStatisticsRegistry()->unregisterStat(&d_eval_lits);
+ smtStatisticsRegistry()->unregisterStat(&d_eval_lits_unknown);
}
bool QModelBuilderIG::isQuantifierActive( Node f ){
d_exh_inst_lemmas("ModelEngine::Instantiations_Exhaustive", 0 ),
d_mbqi_inst_lemmas("ModelEngine::Instantiations_Mbqi", 0 )
{
- StatisticsRegistry::registerStat(&d_inst_rounds);
- StatisticsRegistry::registerStat(&d_exh_inst_lemmas);
- StatisticsRegistry::registerStat(&d_mbqi_inst_lemmas);
+ smtStatisticsRegistry()->registerStat(&d_inst_rounds);
+ smtStatisticsRegistry()->registerStat(&d_exh_inst_lemmas);
+ smtStatisticsRegistry()->registerStat(&d_mbqi_inst_lemmas);
}
ModelEngine::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_inst_rounds);
- StatisticsRegistry::unregisterStat(&d_exh_inst_lemmas);
- StatisticsRegistry::unregisterStat(&d_mbqi_inst_lemmas);
+ smtStatisticsRegistry()->unregisterStat(&d_inst_rounds);
+ smtStatisticsRegistry()->unregisterStat(&d_exh_inst_lemmas);
+ smtStatisticsRegistry()->unregisterStat(&d_mbqi_inst_lemmas);
}
#include <vector>
#include "options/quantifiers_options.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/quantifiers/quant_util.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/trigger.h"
d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ),
d_entailment_checks("QuantConflictFind::Entailment_Checks",0)
{
- StatisticsRegistry::registerStat(&d_inst_rounds);
- StatisticsRegistry::registerStat(&d_conflict_inst);
- StatisticsRegistry::registerStat(&d_prop_inst);
- StatisticsRegistry::registerStat(&d_entailment_checks);
+ smtStatisticsRegistry()->registerStat(&d_inst_rounds);
+ smtStatisticsRegistry()->registerStat(&d_conflict_inst);
+ smtStatisticsRegistry()->registerStat(&d_prop_inst);
+ smtStatisticsRegistry()->registerStat(&d_entailment_checks);
}
QuantConflictFind::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_inst_rounds);
- StatisticsRegistry::unregisterStat(&d_conflict_inst);
- StatisticsRegistry::unregisterStat(&d_prop_inst);
- StatisticsRegistry::unregisterStat(&d_entailment_checks);
+ smtStatisticsRegistry()->unregisterStat(&d_inst_rounds);
+ smtStatisticsRegistry()->unregisterStat(&d_conflict_inst);
+ smtStatisticsRegistry()->unregisterStat(&d_prop_inst);
+ smtStatisticsRegistry()->unregisterStat(&d_entailment_checks);
}
TNode QuantConflictFind::getZero( Kind k ) {
#include <map>
#include "context/cdhashmap.h"
-#include "expr/statistics_registry.h"
#include "theory/theory.h"
#include "util/hash.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
class TheoryEngine;
#include "options/quantifiers_options.h"
#include "options/uf_options.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/arrays/theory_arrays.h"
#include "theory/datatypes/theory_datatypes.h"
#include "theory/quantifiers/alpha_equivalence.h"
}
QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te):
-d_te( te ),
-d_lemmas_produced_c(u),
-d_skolemized(u),
-d_presolve(u, true),
-d_presolve_in(u),
-d_presolve_cache(u),
-d_presolve_cache_wq(u),
-d_presolve_cache_wic(u){
+ d_te( te ),
+ d_lemmas_produced_c(u),
+ d_skolemized(u),
+ d_presolve(u, true),
+ d_presolve_in(u),
+ d_presolve_cache(u),
+ d_presolve_cache_wq(u),
+ d_presolve_cache_wic(u){
d_eq_query = new EqualityQueryQuantifiersEngine( this );
d_term_db = new quantifiers::TermDb( c, u, this );
d_tr_trie = new inst::TriggerTrie;
}
void QuantifiersEngine::check( Theory::Effort e ){
- CodeTimer codeTimer(d_time);
+ CodeTimer codeTimer(d_statistics.d_time);
if( !getMasterEqualityEngine()->consistent() ){
Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl;
return;
}
void QuantifiersEngine::propagate( Theory::Effort level ){
- CodeTimer codeTimer(d_time);
+ CodeTimer codeTimer(d_statistics.d_time);
for( int i=0; i<(int)d_modules.size(); i++ ){
d_modules[i]->propagate( level );
}
}
-QuantifiersEngine::Statistics::Statistics():
- d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
- d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
- d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
- d_instantiations("QuantifiersEngine::Instantiations_Total", 0),
- d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0),
- d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0),
- d_triggers("QuantifiersEngine::Triggers", 0),
- d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
- d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
- d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0),
- d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0),
- d_red_lte_partial_inst("QuantifiersEngine::Reductions_Lte_Partial_Inst", 0),
- d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0),
- d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0),
- d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0),
- d_instantiations_cbqi_arith("QuantifiersEngine::Instantiations_Cbqi_Arith", 0)
+QuantifiersEngine::Statistics::Statistics()
+ : d_time("theory::QuantifiersEngine::time"),
+ d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
+ d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
+ d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
+ d_instantiations("QuantifiersEngine::Instantiations_Total", 0),
+ d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0),
+ d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0),
+ d_triggers("QuantifiersEngine::Triggers", 0),
+ d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
+ d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
+ d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0),
+ d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0),
+ d_red_lte_partial_inst("QuantifiersEngine::Reductions_Lte_Partial_Inst", 0),
+ d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0),
+ d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0),
+ d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0),
+ d_instantiations_cbqi_arith("QuantifiersEngine::Instantiations_Cbqi_Arith", 0)
{
- StatisticsRegistry::registerStat(&d_num_quant);
- StatisticsRegistry::registerStat(&d_instantiation_rounds);
- StatisticsRegistry::registerStat(&d_instantiation_rounds_lc);
- StatisticsRegistry::registerStat(&d_instantiations);
- StatisticsRegistry::registerStat(&d_inst_duplicate);
- StatisticsRegistry::registerStat(&d_inst_duplicate_eq);
- StatisticsRegistry::registerStat(&d_triggers);
- StatisticsRegistry::registerStat(&d_simple_triggers);
- StatisticsRegistry::registerStat(&d_multi_triggers);
- StatisticsRegistry::registerStat(&d_multi_trigger_instantiations);
- StatisticsRegistry::registerStat(&d_red_alpha_equiv);
- StatisticsRegistry::registerStat(&d_red_lte_partial_inst);
- StatisticsRegistry::registerStat(&d_instantiations_user_patterns);
- StatisticsRegistry::registerStat(&d_instantiations_auto_gen);
- StatisticsRegistry::registerStat(&d_instantiations_guess);
- StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith);
+ smtStatisticsRegistry()->registerStat(&d_time);
+ smtStatisticsRegistry()->registerStat(&d_num_quant);
+ smtStatisticsRegistry()->registerStat(&d_instantiation_rounds);
+ smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc);
+ smtStatisticsRegistry()->registerStat(&d_instantiations);
+ smtStatisticsRegistry()->registerStat(&d_inst_duplicate);
+ smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq);
+ smtStatisticsRegistry()->registerStat(&d_triggers);
+ smtStatisticsRegistry()->registerStat(&d_simple_triggers);
+ smtStatisticsRegistry()->registerStat(&d_multi_triggers);
+ smtStatisticsRegistry()->registerStat(&d_multi_trigger_instantiations);
+ smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv);
+ smtStatisticsRegistry()->registerStat(&d_red_lte_partial_inst);
+ smtStatisticsRegistry()->registerStat(&d_instantiations_user_patterns);
+ smtStatisticsRegistry()->registerStat(&d_instantiations_auto_gen);
+ smtStatisticsRegistry()->registerStat(&d_instantiations_guess);
+ smtStatisticsRegistry()->registerStat(&d_instantiations_cbqi_arith);
}
QuantifiersEngine::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_num_quant);
- StatisticsRegistry::unregisterStat(&d_instantiation_rounds);
- StatisticsRegistry::unregisterStat(&d_instantiation_rounds_lc);
- StatisticsRegistry::unregisterStat(&d_instantiations);
- StatisticsRegistry::unregisterStat(&d_inst_duplicate);
- StatisticsRegistry::unregisterStat(&d_inst_duplicate_eq);
- StatisticsRegistry::unregisterStat(&d_triggers);
- StatisticsRegistry::unregisterStat(&d_simple_triggers);
- StatisticsRegistry::unregisterStat(&d_multi_triggers);
- StatisticsRegistry::unregisterStat(&d_multi_trigger_instantiations);
- StatisticsRegistry::unregisterStat(&d_red_alpha_equiv);
- StatisticsRegistry::unregisterStat(&d_red_lte_partial_inst);
- StatisticsRegistry::unregisterStat(&d_instantiations_user_patterns);
- StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen);
- StatisticsRegistry::unregisterStat(&d_instantiations_guess);
- StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith);
+ smtStatisticsRegistry()->unregisterStat(&d_time);
+ smtStatisticsRegistry()->unregisterStat(&d_num_quant);
+ smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds);
+ smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc);
+ smtStatisticsRegistry()->unregisterStat(&d_instantiations);
+ smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate);
+ smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq);
+ smtStatisticsRegistry()->unregisterStat(&d_triggers);
+ smtStatisticsRegistry()->unregisterStat(&d_simple_triggers);
+ smtStatisticsRegistry()->unregisterStat(&d_multi_triggers);
+ smtStatisticsRegistry()->unregisterStat(&d_multi_trigger_instantiations);
+ smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv);
+ smtStatisticsRegistry()->unregisterStat(&d_red_lte_partial_inst);
+ smtStatisticsRegistry()->unregisterStat(&d_instantiations_user_patterns);
+ smtStatisticsRegistry()->unregisterStat(&d_instantiations_auto_gen);
+ smtStatisticsRegistry()->unregisterStat(&d_instantiations_guess);
+ smtStatisticsRegistry()->unregisterStat(&d_instantiations_cbqi_arith);
}
eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){
#include "context/cdchunk_list.h"
#include "context/cdhashset.h"
#include "expr/attribute.h"
-#include "expr/statistics_registry.h"
#include "options/quantifiers_modes.h"
#include "theory/quantifiers/inst_match.h"
#include "theory/quantifiers/quant_util.h"
#include "theory/theory.h"
#include "util/hash.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
NodeList d_presolve_cache;
BoolList d_presolve_cache_wq;
BoolList d_presolve_cache_wic;
-private:
- KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time");
+
public:
QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te);
~QuantifiersEngine();
/** statistics class */
class Statistics {
public:
+ TimerStat d_time;
IntStat d_num_quant;
IntStat d_instantiation_rounds;
IntStat d_instantiation_rounds_lc;
std::map< Node, int > d_rep_score;
/** reset count */
int d_reset_count;
-private:
+
/** node contains */
Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache );
/** get score */
#include "expr/resource_manager.h"
#include "theory/theory.h"
-#include "theory/rewriter_tables.h"
#include "smt/smt_engine_scope.h"
+#include "smt/smt_statistics_registry.h"
+#include "theory/rewriter_tables.h"
+
using namespace std;
#include "expr/emptyset.h"
#include "options/sets_options.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/sets/expr_patterns.h" // ONLY included here
#include "theory/sets/scrutinize.h"
#include "theory/sets/theory_sets.h"
, d_memberLemmas("theory::sets::lemmas::member", 0)
, d_disequalityLemmas("theory::sets::lemmas::disequality", 0)
{
- StatisticsRegistry::registerStat(&d_getModelValueTime);
- StatisticsRegistry::registerStat(&d_memberLemmas);
- StatisticsRegistry::registerStat(&d_disequalityLemmas);
+ smtStatisticsRegistry()->registerStat(&d_getModelValueTime);
+ smtStatisticsRegistry()->registerStat(&d_memberLemmas);
+ smtStatisticsRegistry()->registerStat(&d_disequalityLemmas);
}
TheorySetsPrivate::Statistics::~Statistics() {
- StatisticsRegistry::unregisterStat(&d_getModelValueTime);
- StatisticsRegistry::unregisterStat(&d_memberLemmas);
- StatisticsRegistry::unregisterStat(&d_disequalityLemmas);
+ smtStatisticsRegistry()->unregisterStat(&d_getModelValueTime);
+ smtStatisticsRegistry()->unregisterStat(&d_memberLemmas);
+ smtStatisticsRegistry()->unregisterStat(&d_disequalityLemmas);
}
** \todo document this file
**/
-
#include "theory/shared_terms_database.h"
+
+#include "smt/smt_statistics_registry.h"
#include "theory/theory_engine.h"
using namespace std;
, d_theoryEngine(theoryEngine)
, d_inConflict(context, false)
{
- StatisticsRegistry::registerStat(&d_statSharedTerms);
+ smtStatisticsRegistry()->registerStat(&d_statSharedTerms);
}
SharedTermsDatabase::~SharedTermsDatabase() throw(AssertionException)
{
- StatisticsRegistry::unregisterStat(&d_statSharedTerms);
+ smtStatisticsRegistry()->unregisterStat(&d_statSharedTerms);
}
void SharedTermsDatabase::addEqualityToPropagate(TNode equality) {
#include "context/cdhashset.h"
#include "expr/node.h"
-#include "expr/statistics_registry.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
#include "expr/kind.h"
#include "options/strings_options.h"
#include "smt/logic_exception.h"
+#include "smt/smt_statistics_registry.h"
#include "smt_util/command.h"
#include "theory/rewriter.h"
#include "theory/strings/theory_strings_rewriter.h"
d_loop_lemmas("TheoryStrings::NumOfLoops", 0),
d_new_skolems("TheoryStrings::NumOfNewSkolems", 0)
{
- StatisticsRegistry::registerStat(&d_splits);
- StatisticsRegistry::registerStat(&d_eq_splits);
- StatisticsRegistry::registerStat(&d_deq_splits);
- StatisticsRegistry::registerStat(&d_loop_lemmas);
- StatisticsRegistry::registerStat(&d_new_skolems);
+ smtStatisticsRegistry()->registerStat(&d_splits);
+ smtStatisticsRegistry()->registerStat(&d_eq_splits);
+ smtStatisticsRegistry()->registerStat(&d_deq_splits);
+ smtStatisticsRegistry()->registerStat(&d_loop_lemmas);
+ smtStatisticsRegistry()->registerStat(&d_new_skolems);
}
TheoryStrings::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_splits);
- StatisticsRegistry::unregisterStat(&d_eq_splits);
- StatisticsRegistry::unregisterStat(&d_deq_splits);
- StatisticsRegistry::unregisterStat(&d_loop_lemmas);
- StatisticsRegistry::unregisterStat(&d_new_skolems);
+ smtStatisticsRegistry()->unregisterStat(&d_splits);
+ smtStatisticsRegistry()->unregisterStat(&d_eq_splits);
+ smtStatisticsRegistry()->unregisterStat(&d_deq_splits);
+ smtStatisticsRegistry()->unregisterStat(&d_loop_lemmas);
+ smtStatisticsRegistry()->unregisterStat(&d_new_skolems);
}
}/* CVC4::theory::strings namespace */
#include <vector>
#include "base/cvc4_assert.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/substitutions.h"
#include "theory/quantifiers_engine.h"
return os;
}/* ostream& operator<<(ostream&, Theory::Effort) */
+Theory::Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext,
+ OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo,
+ SmtGlobals* globals) throw()
+ : d_id(id)
+ , d_satContext(satContext)
+ , d_userContext(userContext)
+ , d_logicInfo(logicInfo)
+ , d_facts(satContext)
+ , d_factsHead(satContext, 0)
+ , d_sharedTermsIndex(satContext, 0)
+ , d_careGraph(NULL)
+ , d_quantEngine(NULL)
+ , d_checkTime(statName(id, "checkTime"))
+ , d_computeCareGraphTime(statName(id, "computeCareGraphTime"))
+ , d_sharedTerms(satContext)
+ , d_out(&out)
+ , d_valuation(valuation)
+ , d_proofEnabled(false)
+ , d_globals(globals)
+{
+ smtStatisticsRegistry()->registerStat(&d_checkTime);
+ smtStatisticsRegistry()->registerStat(&d_computeCareGraphTime);
+}
+
Theory::~Theory() {
- StatisticsRegistry::unregisterStat(&d_checkTime);
- StatisticsRegistry::unregisterStat(&d_computeCareGraphTime);
+ smtStatisticsRegistry()->unregisterStat(&d_checkTime);
+ smtStatisticsRegistry()->unregisterStat(&d_computeCareGraphTime);
}
TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) {
#include "context/cdo.h"
#include "context/context.h"
#include "expr/node.h"
-#include "expr/statistics_registry.h"
#include "lib/ffs.h"
#include "options/options.h"
#include "options/theory_options.h"
#include "theory/logic_info.h"
#include "theory/output_channel.h"
#include "theory/valuation.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
*/
Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext,
OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo,
- SmtGlobals* globals) throw()
- : d_id(id)
- , d_satContext(satContext)
- , d_userContext(userContext)
- , d_logicInfo(logicInfo)
- , d_facts(satContext)
- , d_factsHead(satContext, 0)
- , d_sharedTermsIndex(satContext, 0)
- , d_careGraph(NULL)
- , d_quantEngine(NULL)
- , d_checkTime(statName(id, "checkTime"))
- , d_computeCareGraphTime(statName(id, "computeCareGraphTime"))
- , d_sharedTerms(satContext)
- , d_out(&out)
- , d_valuation(valuation)
- , d_proofEnabled(false)
- , d_globals(globals)
- {
- StatisticsRegistry::registerStat(&d_checkTime);
- StatisticsRegistry::registerStat(&d_computeCareGraphTime);
- }
+ SmtGlobals* globals) throw();
/**
* This is called at shutdown time by the TheoryEngine, just before
using namespace std;
-using namespace CVC4;
using namespace CVC4::theory;
+namespace CVC4 {
+
void TheoryEngine::finishInit() {
PROOF (ProofManager::initTheoryProof(); );
d_curr_model = new theory::TheoryModel(userContext, "DefaultModel", true);
d_curr_model_builder = new theory::TheoryEngineModelBuilder(this);
- StatisticsRegistry::registerStat(&d_combineTheoriesTime);
+ smtStatisticsRegistry()->registerStat(&d_combineTheoriesTime);
d_true = NodeManager::currentNM()->mkConst<bool>(true);
d_false = NodeManager::currentNM()->mkConst<bool>(false);
d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor());
- StatisticsRegistry::registerStat(&d_arithSubstitutionsAdded);
+ smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded);
}
TheoryEngine::~TheoryEngine() {
delete d_masterEqualityEngine;
- StatisticsRegistry::unregisterStat(&d_combineTheoriesTime);
+ smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime);
delete d_unconstrainedSimp;
delete d_iteUtilities;
- StatisticsRegistry::unregisterStat(&d_arithSubstitutionsAdded);
+ smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded);
}
void TheoryEngine::interrupt() throw(ModalException) {
void TheoryEngine::spendResource(unsigned ammount) {
d_resourceManager->spendResource(ammount);
}
+
+TheoryEngine::Statistics::Statistics(theory::TheoryId theory):
+ conflicts(mkName("theory<", theory, ">::conflicts"), 0),
+ propagations(mkName("theory<", theory, ">::propagations"), 0),
+ lemmas(mkName("theory<", theory, ">::lemmas"), 0),
+ requirePhase(mkName("theory<", theory, ">::requirePhase"), 0),
+ flipDecision(mkName("theory<", theory, ">::flipDecision"), 0),
+ restartDemands(mkName("theory<", theory, ">::restartDemands"), 0)
+{
+ smtStatisticsRegistry()->registerStat(&conflicts);
+ smtStatisticsRegistry()->registerStat(&propagations);
+ smtStatisticsRegistry()->registerStat(&lemmas);
+ smtStatisticsRegistry()->registerStat(&requirePhase);
+ smtStatisticsRegistry()->registerStat(&flipDecision);
+ smtStatisticsRegistry()->registerStat(&restartDemands);
+}
+
+TheoryEngine::Statistics::~Statistics() {
+ smtStatisticsRegistry()->unregisterStat(&conflicts);
+ smtStatisticsRegistry()->unregisterStat(&propagations);
+ smtStatisticsRegistry()->unregisterStat(&lemmas);
+ smtStatisticsRegistry()->unregisterStat(&requirePhase);
+ smtStatisticsRegistry()->unregisterStat(&flipDecision);
+ smtStatisticsRegistry()->unregisterStat(&restartDemands);
+}
+
+}/* CVC4 namespace */
#include "base/cvc4_assert.h"
#include "context/cdhashset.h"
#include "expr/node.h"
-#include "expr/statistics_registry.h"
#include "options/options.h"
#include "options/smt_options.h"
#include "prop/prop_engine.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
#include "theory/valuation.h"
+#include "util/statistics_registry.h"
#include "util/unsafe_interrupt_exception.h"
namespace CVC4 {
IntStat conflicts, propagations, lemmas, requirePhase, flipDecision, restartDemands;
- Statistics(theory::TheoryId theory):
- conflicts(mkName("theory<", theory, ">::conflicts"), 0),
- propagations(mkName("theory<", theory, ">::propagations"), 0),
- lemmas(mkName("theory<", theory, ">::lemmas"), 0),
- requirePhase(mkName("theory<", theory, ">::requirePhase"), 0),
- flipDecision(mkName("theory<", theory, ">::flipDecision"), 0),
- restartDemands(mkName("theory<", theory, ">::restartDemands"), 0)
- {
- StatisticsRegistry::registerStat(&conflicts);
- StatisticsRegistry::registerStat(&propagations);
- StatisticsRegistry::registerStat(&lemmas);
- StatisticsRegistry::registerStat(&requirePhase);
- StatisticsRegistry::registerStat(&flipDecision);
- StatisticsRegistry::registerStat(&restartDemands);
- }
-
- ~Statistics() {
- StatisticsRegistry::unregisterStat(&conflicts);
- StatisticsRegistry::unregisterStat(&propagations);
- StatisticsRegistry::unregisterStat(&lemmas);
- StatisticsRegistry::unregisterStat(&requirePhase);
- StatisticsRegistry::unregisterStat(&flipDecision);
- StatisticsRegistry::unregisterStat(&restartDemands);
- }
+ Statistics(theory::TheoryId theory);
+ ~Statistics();
};/* class TheoryEngine::Statistics */
inline bool isTheoryEnabled(theory::TheoryId theoryId) const {
return d_logicInfo.isTheoryEnabled(theoryId);
}
-
+
/**
* Returns the equality status of the two terms, from the theory
* that owns the domain type. The types of a and b must be the same.
* Print solution for synthesis conjectures found by ce_guided_instantiation module
*/
void printSynthSolution( std::ostream& out );
-
+
/**
* Forwards an entailment check according to the given theoryOfMode.
* See theory.h for documentation on entailmentCheck().
SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; }
theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; }
-
+
RemoveITE* getIteRemover() { return &d_iteRemover; }
SortInference* getSortInference() { return &d_sortInfer; }
-
+
/** Prints the assertions to the debug stream */
void printAssertions(const char* tag);
#include "theory/uf/equality_engine.h"
+#include "smt/smt_statistics_registry.h"
+
namespace CVC4 {
namespace theory {
namespace eq {
+EqualityEngine::Statistics::Statistics(std::string name)
+ : mergesCount(name + "::mergesCount", 0),
+ termsCount(name + "::termsCount", 0),
+ functionTermsCount(name + "::functionTermsCount", 0),
+ constantTermsCount(name + "::constantTermsCount", 0)
+{
+ smtStatisticsRegistry()->registerStat(&mergesCount);
+ smtStatisticsRegistry()->registerStat(&termsCount);
+ smtStatisticsRegistry()->registerStat(&functionTermsCount);
+ smtStatisticsRegistry()->registerStat(&constantTermsCount);
+}
+
+EqualityEngine::Statistics::~Statistics() {
+ smtStatisticsRegistry()->unregisterStat(&mergesCount);
+ smtStatisticsRegistry()->unregisterStat(&termsCount);
+ smtStatisticsRegistry()->unregisterStat(&functionTermsCount);
+ smtStatisticsRegistry()->unregisterStat(&constantTermsCount);
+}
+
+
/**
* Data used in the BFS search through the equality graph.
*/
} // Namespace uf
} // Namespace theory
} // Namespace CVC4
-
#include "context/cdo.h"
#include "expr/kind_map.h"
#include "expr/node.h"
-#include "expr/statistics_registry.h"
#include "theory/rewriter.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine_types.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
/** Number of constant terms managed by the system */
IntStat constantTermsCount;
- Statistics(std::string name)
- : mergesCount(name + "::mergesCount", 0),
- termsCount(name + "::termsCount", 0),
- functionTermsCount(name + "::functionTermsCount", 0),
- constantTermsCount(name + "::constantTermsCount", 0)
- {
- StatisticsRegistry::registerStat(&mergesCount);
- StatisticsRegistry::registerStat(&termsCount);
- StatisticsRegistry::registerStat(&functionTermsCount);
- StatisticsRegistry::registerStat(&constantTermsCount);
- }
+ Statistics(std::string name);
- ~Statistics() {
- StatisticsRegistry::unregisterStat(&mergesCount);
- StatisticsRegistry::unregisterStat(&termsCount);
- StatisticsRegistry::unregisterStat(&functionTermsCount);
- StatisticsRegistry::unregisterStat(&constantTermsCount);
- }
+ ~Statistics();
};/* struct EqualityEngine::statistics */
private:
} // Namespace eq
} // Namespace theory
} // Namespace CVC4
-
#include "context/context.h"
#include "expr/node.h"
#include "expr/node_builder.h"
-#include "expr/statistics_registry.h"
+#include "smt/smt_statistics_registry.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
d_totality_lemmas("StrongSolverTheoryUF::Totality_Lemmas", 0),
d_max_model_size("StrongSolverTheoryUF::Max_Model_Size", 1)
{
- StatisticsRegistry::registerStat(&d_clique_conflicts);
- StatisticsRegistry::registerStat(&d_clique_lemmas);
- StatisticsRegistry::registerStat(&d_split_lemmas);
- StatisticsRegistry::registerStat(&d_disamb_term_lemmas);
- StatisticsRegistry::registerStat(&d_sym_break_lemmas);
- StatisticsRegistry::registerStat(&d_totality_lemmas);
- StatisticsRegistry::registerStat(&d_max_model_size);
+ smtStatisticsRegistry()->registerStat(&d_clique_conflicts);
+ smtStatisticsRegistry()->registerStat(&d_clique_lemmas);
+ smtStatisticsRegistry()->registerStat(&d_split_lemmas);
+ smtStatisticsRegistry()->registerStat(&d_disamb_term_lemmas);
+ smtStatisticsRegistry()->registerStat(&d_sym_break_lemmas);
+ smtStatisticsRegistry()->registerStat(&d_totality_lemmas);
+ smtStatisticsRegistry()->registerStat(&d_max_model_size);
}
StrongSolverTheoryUF::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_clique_conflicts);
- StatisticsRegistry::unregisterStat(&d_clique_lemmas);
- StatisticsRegistry::unregisterStat(&d_split_lemmas);
- StatisticsRegistry::unregisterStat(&d_disamb_term_lemmas);
- StatisticsRegistry::unregisterStat(&d_sym_break_lemmas);
- StatisticsRegistry::unregisterStat(&d_totality_lemmas);
- StatisticsRegistry::unregisterStat(&d_max_model_size);
+ smtStatisticsRegistry()->unregisterStat(&d_clique_conflicts);
+ smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas);
+ smtStatisticsRegistry()->unregisterStat(&d_split_lemmas);
+ smtStatisticsRegistry()->unregisterStat(&d_disamb_term_lemmas);
+ smtStatisticsRegistry()->unregisterStat(&d_sym_break_lemmas);
+ smtStatisticsRegistry()->unregisterStat(&d_totality_lemmas);
+ smtStatisticsRegistry()->unregisterStat(&d_max_model_size);
}
DisequalityPropagator::Statistics::Statistics():
d_propagations("StrongSolverTheoryUF::Disequality_Propagations", 0)
{
- StatisticsRegistry::registerStat(& d_propagations);
+ smtStatisticsRegistry()->registerStat(& d_propagations);
}
DisequalityPropagator::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(& d_propagations);
+ smtStatisticsRegistry()->unregisterStat(& d_propagations);
}
#include "context/cdhashmap.h"
#include "context/context.h"
#include "context/context_mm.h"
-#include "expr/statistics_registry.h"
#include "theory/theory.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
#include "theory/unconstrained_simplifier.h"
+
#include "theory/rewriter.h"
#include "theory/logic_info.h"
+#include "smt/smt_statistics_registry.h"
using namespace std;
using namespace CVC4;
: d_numUnconstrainedElim("preprocessor::number of unconstrained elims", 0),
d_context(context), d_substitutions(context), d_logicInfo(logicInfo)
{
- StatisticsRegistry::registerStat(&d_numUnconstrainedElim);
+ smtStatisticsRegistry()->registerStat(&d_numUnconstrainedElim);
}
UnconstrainedSimplifier::~UnconstrainedSimplifier()
{
- StatisticsRegistry::unregisterStat(&d_numUnconstrainedElim);
+ smtStatisticsRegistry()->unregisterStat(&d_numUnconstrainedElim);
}
#include <utility>
#include "expr/node.h"
-#include "expr/statistics_registry.h"
#include "theory/substitutions.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
sexpr.h \
smt2_quote_string.cpp \
smt2_quote_string.h \
+ statistics.cpp \
+ statistics.h \
+ statistics_registry.cpp \
+ statistics_registry.h \
subrange_bound.cpp \
subrange_bound.h \
tuple.h \
regexp.i \
result.i \
sexpr.i \
+ statistics.i \
subrange_bound.i \
tuple.i \
unsafe_interrupt_exception.i
--- /dev/null
+/********************* */
+/*! \file statistics.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "util/statistics.h"
+
+#include <typeinfo>
+
+#include "util/statistics_registry.h" // for details about class Stat
+
+
+namespace CVC4 {
+
+std::string StatisticsBase::s_regDelim("::");
+
+bool StatisticsBase::StatCmp::operator()(const Stat* s1, const Stat* s2) const {
+ return s1->getName() < s2->getName();
+}
+
+StatisticsBase::iterator::value_type StatisticsBase::iterator::operator*() const {
+ return std::make_pair((*d_it)->getName(), (*d_it)->getValue());
+}
+
+StatisticsBase::StatisticsBase() :
+ d_prefix(),
+ d_stats() {
+}
+
+StatisticsBase::StatisticsBase(const StatisticsBase& stats) :
+ d_prefix(stats.d_prefix),
+ d_stats() {
+}
+
+StatisticsBase& StatisticsBase::operator=(const StatisticsBase& stats) {
+ d_prefix = stats.d_prefix;
+ return *this;
+}
+
+void Statistics::copyFrom(const StatisticsBase& stats) {
+ // This is ugly, but otherwise we have to introduce a "friend" relation for
+ // Base to its derived class (really obnoxious).
+ StatSet::const_iterator i_begin = ((const Statistics*) &stats)->d_stats.begin();
+ StatSet::const_iterator i_end = ((const Statistics*) &stats)->d_stats.end();
+ for(StatSet::const_iterator i = i_begin; i != i_end; ++i) {
+ SExprStat* p = new SExprStat((*i)->getName(), (*i)->getValue());
+ d_stats.insert(p);
+ }
+}
+
+void Statistics::clear() {
+ for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) {
+ delete *i;
+ }
+ d_stats.clear();
+}
+
+Statistics::Statistics(const StatisticsBase& stats) :
+ StatisticsBase(stats) {
+ copyFrom(stats);
+}
+
+Statistics::Statistics(const Statistics& stats) :
+ StatisticsBase(stats) {
+ copyFrom(stats);
+}
+
+Statistics::~Statistics() {
+ clear();
+}
+
+Statistics& Statistics::operator=(const StatisticsBase& stats) {
+ clear();
+ this->StatisticsBase::operator=(stats);
+ copyFrom(stats);
+
+ return *this;
+}
+
+Statistics& Statistics::operator=(const Statistics& stats) {
+ return this->operator=((const StatisticsBase&)stats);
+}
+
+StatisticsBase::const_iterator StatisticsBase::begin() const {
+ return iterator(d_stats.begin());
+}
+
+StatisticsBase::const_iterator StatisticsBase::end() const {
+ return iterator(d_stats.end());
+}
+
+void StatisticsBase::flushInformation(std::ostream &out) const {
+#ifdef CVC4_STATISTICS_ON
+ for(StatSet::iterator i = d_stats.begin();
+ i != d_stats.end();
+ ++i) {
+ Stat* s = *i;
+ if(d_prefix != "") {
+ out << d_prefix << s_regDelim;
+ }
+ s->flushStat(out);
+ out << std::endl;
+ }
+#endif /* CVC4_STATISTICS_ON */
+}
+
+SExpr StatisticsBase::getStatistic(std::string name) const {
+ SExpr value;
+ IntStat s(name, 0);
+ StatSet::iterator i = d_stats.find(&s);
+ if(i != d_stats.end()) {
+ return (*i)->getValue();
+ } else {
+ return SExpr();
+ }
+}
+
+void StatisticsBase::setPrefix(const std::string& prefix) {
+ d_prefix = prefix;
+}
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file statistics.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__STATISTICS_H
+#define __CVC4__STATISTICS_H
+
+#include <iterator>
+#include <ostream>
+#include <set>
+#include <string>
+#include <utility>
+
+#include "util/sexpr.h"
+
+namespace CVC4 {
+
+class Stat;
+
+class CVC4_PUBLIC StatisticsBase {
+protected:
+
+ static std::string s_regDelim;
+
+ /** A helper class for comparing two statistics */
+ struct StatCmp {
+ bool operator()(const Stat* s1, const Stat* s2) const;
+ };/* struct StatisticsRegistry::StatCmp */
+
+ /** A type for a set of statistics */
+ typedef std::set< Stat*, StatCmp > StatSet;
+
+ std::string d_prefix;
+
+ /** The set of statistics in this object */
+ StatSet d_stats;
+
+ StatisticsBase();
+ StatisticsBase(const StatisticsBase& stats);
+ StatisticsBase& operator=(const StatisticsBase& stats);
+
+public:
+
+ virtual ~StatisticsBase() { }
+
+ class CVC4_PUBLIC iterator : public std::iterator< std::input_iterator_tag, std::pair<std::string, SExpr> > {
+ StatSet::iterator d_it;
+
+ iterator(StatSet::iterator it) : d_it(it) { }
+
+ friend class StatisticsBase;
+
+ public:
+ iterator() : d_it() { }
+ iterator(const iterator& it) : d_it(it.d_it) { }
+ value_type operator*() const;
+ iterator& operator++() { ++d_it; return *this; }
+ iterator operator++(int) { iterator old = *this; ++d_it; return old; }
+ bool operator==(const iterator& i) const { return d_it == i.d_it; }
+ bool operator!=(const iterator& i) const { return d_it != i.d_it; }
+ };/* class StatisticsBase::iterator */
+
+ /** An iterator type over a set of statistics. */
+ typedef iterator const_iterator;
+
+ /** Set the output prefix for this set of statistics. */
+ virtual void setPrefix(const std::string& prefix);
+
+ /** Flush all statistics to the given output stream. */
+ void flushInformation(std::ostream& out) const;
+
+ /** Get the value of a named statistic. */
+ SExpr getStatistic(std::string name) const;
+
+ /**
+ * Get an iterator to the beginning of the range of the set of
+ * statistics.
+ */
+ const_iterator begin() const;
+
+ /**
+ * Get an iterator to the end of the range of the set of statistics.
+ */
+ const_iterator end() const;
+
+};/* class StatisticsBase */
+
+class CVC4_PUBLIC Statistics : public StatisticsBase {
+ void clear();
+ void copyFrom(const StatisticsBase&);
+
+public:
+
+ /**
+ * Override the copy constructor to do a "deep" copy of statistics
+ * values.
+ */
+ Statistics(const StatisticsBase& stats);
+ Statistics(const Statistics& stats);
+
+ ~Statistics();
+
+ /**
+ * Override the assignment operator to do a "deep" copy of statistics
+ * values.
+ */
+ Statistics& operator=(const StatisticsBase& stats);
+ Statistics& operator=(const Statistics& stats);
+
+};/* class Statistics */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__STATISTICS_H */
--- /dev/null
+%{
+#include "util/statistics.h"
+
+#ifdef SWIGJAVA
+
+#include "bindings/java_iterator_adapter.h"
+#include "bindings/java_stream_adapters.h"
+
+#endif /* SWIGJAVA */
+%}
+
+%rename(assign) CVC4::Statistics::operator=(const StatisticsBase&);
+%rename(assign) CVC4::Statistics::operator=(const Statistics& stats);
+
+#ifdef SWIGJAVA
+
+// Instead of StatisticsBase::begin() and end(), create an
+// iterator() method on the Java side that returns a Java-style
+// Iterator.
+%ignore CVC4::StatisticsBase::begin();
+%ignore CVC4::StatisticsBase::end();
+%ignore CVC4::StatisticsBase::begin() const;
+%ignore CVC4::StatisticsBase::end() const;
+%extend CVC4::StatisticsBase {
+ CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> iterator() {
+ return CVC4::JavaIteratorAdapter<CVC4::StatisticsBase>(*$self);
+ }
+}
+
+// StatisticsBase is "iterable" on the Java side
+%typemap(javainterfaces) CVC4::StatisticsBase "java.lang.Iterable<Object[]>";
+
+// the JavaIteratorAdapter should not be public, and implements Iterator
+%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> "class";
+%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> "java.util.Iterator<Object[]>";
+// add some functions to the Java side (do it here because there's no way to do these in C++)
+%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> "
+ public void remove() {
+ throw new java.lang.UnsupportedOperationException();
+ }
+
+ public Object[] next() {
+ if(hasNext()) {
+ return getNext();
+ } else {
+ throw new java.util.NoSuchElementException();
+ }
+ }
+"
+// getNext() just allows C++ iterator access from Java-side next(), make it private
+%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::StatisticsBase>::getNext() "private";
+
+// map the types appropriately. for statistics, the "payload" of the iterator is an Object[].
+// These Object arrays are always of two elements, the first is a String and the second an
+// SExpr. (On the C++ side, it is a std::pair<std::string, SExpr>.)
+%typemap(jni) CVC4::StatisticsBase::const_iterator::value_type "jobjectArray";
+%typemap(jtype) CVC4::StatisticsBase::const_iterator::value_type "java.lang.Object[]";
+%typemap(jstype) CVC4::StatisticsBase::const_iterator::value_type "java.lang.Object[]";
+%typemap(javaout) CVC4::StatisticsBase::const_iterator::value_type { return $jnicall; }
+%typemap(out) CVC4::StatisticsBase::const_iterator::value_type {
+ $result = jenv->NewObjectArray(2, jenv->FindClass("java/lang/Object"), $null);
+ jenv->SetObjectArrayElement($result, 0, jenv->NewStringUTF($1.first.c_str()));
+ jclass clazz = jenv->FindClass("edu/nyu/acsys/CVC4/SExpr");
+ jmethodID methodid = jenv->GetMethodID(clazz, "<init>", "(JZ)V");
+ jenv->SetObjectArrayElement($result, 1, jenv->NewObject(clazz, methodid, reinterpret_cast<long>(new CVC4::SExpr($1.second)), true));
+ };
+
+#endif /* SWIGJAVA */
+
+%include "util/statistics.h"
+
+#ifdef SWIGJAVA
+
+%include "bindings/java_iterator_adapter.h"
+%include "bindings/java_stream_adapters.h"
+
+%template(JavaIteratorAdapter_StatisticsBase) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase>;
+
+#endif /* SWIGJAVA */
--- /dev/null
+/********************* */
+/*! \file statistics_registry.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): Kshitij Bansal, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "util/statistics_registry.h"
+
+#include "base/cvc4_assert.h"
+#include "lib/clock_gettime.h"
+
+
+#ifdef CVC4_STATISTICS_ON
+# define __CVC4_USE_STATISTICS true
+#else
+# define __CVC4_USE_STATISTICS false
+#endif
+
+
+/****************************************************************************/
+/* Some utility functions for timespec */
+/****************************************************************************/
+namespace CVC4 {
+
+/** Compute the sum of two timespecs. */
+inline timespec& operator+=(timespec& a, const timespec& b) {
+ using namespace CVC4;
+ // assumes a.tv_nsec and b.tv_nsec are in range
+ const long nsec_per_sec = 1000000000L; // one thousand million
+ CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a);
+ CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b);
+ a.tv_sec += b.tv_sec;
+ long nsec = a.tv_nsec + b.tv_nsec;
+ assert(nsec >= 0);
+ if(nsec < 0) {
+ nsec += nsec_per_sec;
+ --a.tv_sec;
+ }
+ if(nsec >= nsec_per_sec) {
+ nsec -= nsec_per_sec;
+ ++a.tv_sec;
+ }
+ assert(nsec >= 0 && nsec < nsec_per_sec);
+ a.tv_nsec = nsec;
+ return a;
+}
+
+/** Compute the difference of two timespecs. */
+inline timespec& operator-=(timespec& a, const timespec& b) {
+ using namespace CVC4;
+ // assumes a.tv_nsec and b.tv_nsec are in range
+ const long nsec_per_sec = 1000000000L; // one thousand million
+ CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a);
+ CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b);
+ a.tv_sec -= b.tv_sec;
+ long nsec = a.tv_nsec - b.tv_nsec;
+ if(nsec < 0) {
+ nsec += nsec_per_sec;
+ --a.tv_sec;
+ }
+ if(nsec >= nsec_per_sec) {
+ nsec -= nsec_per_sec;
+ ++a.tv_sec;
+ }
+ assert(nsec >= 0 && nsec < nsec_per_sec);
+ a.tv_nsec = nsec;
+ return a;
+}
+
+/** Add two timespecs. */
+inline timespec operator+(const timespec& a, const timespec& b) {
+ timespec result = a;
+ return result += b;
+}
+
+/** Subtract two timespecs. */
+inline timespec operator-(const timespec& a, const timespec& b) {
+ timespec result = a;
+ return result -= b;
+}
+
+/**
+ * Compare two timespecs for equality.
+ * This must be kept in sync with the copy in test/util/stats_black.h
+ */
+inline bool operator==(const timespec& a, const timespec& b) {
+ // assumes a.tv_nsec and b.tv_nsec are in range
+ return a.tv_sec == b.tv_sec && a.tv_nsec == b.tv_nsec;
+}
+
+/** Compare two timespecs for disequality. */
+inline bool operator!=(const timespec& a, const timespec& b) {
+ // assumes a.tv_nsec and b.tv_nsec are in range
+ return !(a == b);
+}
+
+/** Compare two timespecs, returning true iff a < b. */
+inline bool operator<(const timespec& a, const timespec& b) {
+ // assumes a.tv_nsec and b.tv_nsec are in range
+ return a.tv_sec < b.tv_sec ||
+ (a.tv_sec == b.tv_sec && a.tv_nsec < b.tv_nsec);
+}
+
+/** Compare two timespecs, returning true iff a > b. */
+inline bool operator>(const timespec& a, const timespec& b) {
+ // assumes a.tv_nsec and b.tv_nsec are in range
+ return a.tv_sec > b.tv_sec ||
+ (a.tv_sec == b.tv_sec && a.tv_nsec > b.tv_nsec);
+}
+
+/** Compare two timespecs, returning true iff a <= b. */
+inline bool operator<=(const timespec& a, const timespec& b) {
+ // assumes a.tv_nsec and b.tv_nsec are in range
+ return !(a > b);
+}
+
+/** Compare two timespecs, returning true iff a >= b. */
+inline bool operator>=(const timespec& a, const timespec& b) {
+ // assumes a.tv_nsec and b.tv_nsec are in range
+ return !(a < b);
+}
+
+/** Output a timespec on an output stream. */
+std::ostream& operator<<(std::ostream& os, const timespec& t) {
+ // assumes t.tv_nsec is in range
+ return os << t.tv_sec << "."
+ << std::setfill('0') << std::setw(9) << std::right << t.tv_nsec;
+}
+
+
+/** Construct a statistics registry */
+StatisticsRegistry::StatisticsRegistry(const std::string& name)
+ throw(CVC4::IllegalArgumentException) :
+ Stat(name) {
+
+ d_prefix = name;
+ if(__CVC4_USE_STATISTICS) {
+ PrettyCheckArgument(d_name.find(s_regDelim) == std::string::npos, name,
+ "StatisticsRegistry names cannot contain the string \"%s\"",
+ s_regDelim.c_str());
+ }
+}
+
+void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentException) {
+#ifdef CVC4_STATISTICS_ON
+ PrettyCheckArgument(d_stats.find(s) == d_stats.end(), s,
+ "Statistic `%s' was not registered with this registry.",
+ s->getName().c_str());
+ d_stats.insert(s);
+#endif /* CVC4_STATISTICS_ON */
+}/* StatisticsRegistry::registerStat_() */
+
+void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException) {
+#ifdef CVC4_STATISTICS_ON
+ PrettyCheckArgument(d_stats.find(s) != d_stats.end(), s,
+ "Statistic `%s' was not registered with this registry.",
+ s->getName().c_str());
+ d_stats.erase(s);
+#endif /* CVC4_STATISTICS_ON */
+}/* StatisticsRegistry::unregisterStat_() */
+
+void StatisticsRegistry::flushStat(std::ostream &out) const {
+#ifdef CVC4_STATISTICS_ON
+ flushInformation(out);
+#endif /* CVC4_STATISTICS_ON */
+}
+
+void StatisticsRegistry::flushInformation(std::ostream &out) const {
+#ifdef CVC4_STATISTICS_ON
+ this->StatisticsBase::flushInformation(out);
+#endif /* CVC4_STATISTICS_ON */
+}
+
+void TimerStat::start() {
+ if(__CVC4_USE_STATISTICS) {
+ PrettyCheckArgument(!d_running, *this, "timer already running");
+ clock_gettime(CLOCK_MONOTONIC, &d_start);
+ d_running = true;
+ }
+}/* TimerStat::start() */
+
+void TimerStat::stop() {
+ if(__CVC4_USE_STATISTICS) {
+ PrettyCheckArgument(d_running, *this, "timer not running");
+ ::timespec end;
+ clock_gettime(CLOCK_MONOTONIC, &end);
+ d_data += end - d_start;
+ d_running = false;
+ }
+}/* TimerStat::stop() */
+
+bool TimerStat::running() const {
+ return d_running;
+}/* TimerStat::running() */
+
+timespec TimerStat::getData() const {
+ ::timespec data = d_data;
+ if(__CVC4_USE_STATISTICS && d_running) {
+ ::timespec end;
+ clock_gettime(CLOCK_MONOTONIC, &end);
+ data += end - d_start;
+ }
+ return data;
+}
+
+SExpr TimerStat::getValue() const {
+ ::timespec data = d_data;
+ if(__CVC4_USE_STATISTICS && d_running) {
+ ::timespec end;
+ clock_gettime(CLOCK_MONOTONIC, &end);
+ data += end - d_start;
+ }
+ std::stringstream ss;
+ ss << std::fixed << std::setprecision(8) << data;
+ return SExpr(Rational::fromDecimal(ss.str()));
+}/* TimerStat::getValue() */
+
+
+RegisterStatistic::RegisterStatistic(StatisticsRegistry* reg, Stat* stat)
+ : d_reg(reg),
+ d_stat(stat) {
+ CheckArgument(reg != NULL, reg,
+ "You need to specify a statistics registry"
+ "on which to set the statistic");
+ d_reg->registerStat(d_stat);
+}
+
+RegisterStatistic::~RegisterStatistic() {
+ d_reg->unregisterStat(d_stat);
+}
+
+}/* CVC4 namespace */
+
+#undef __CVC4_USE_STATISTICS
--- /dev/null
+/********************* */
+/*! \file statistics_registry.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: Tim King
+ ** Minor contributors (to current version): Kshitij Bansal
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Statistics utility classes
+ **
+ ** Statistics utility classes, including classes for holding (and referring
+ ** to) statistics, the statistics registry, and some other associated
+ ** classes.
+ **
+ ** This file is somewhat unique in that it is a "cvc4_private_library.h"
+ ** header. Because of this, most classes need to be marked as CVC4_PUBLIC.
+ ** This is because CVC4_PUBLIC is connected to the visibility of the linkage
+ ** in the object files for the class. It does not dictate what headers are
+ ** installed.
+ ** Because the StatisticsRegistry and associated classes are built into
+ ** libutil, which is used by libcvc4, and then later used by the libmain
+ ** without referring to libutil as well. Thus the without marking these as
+ ** CVC4_PUBLIC the symbols would be external in libutil, internal in libcvc4,
+ ** and not be visible to libmain and linking would fail.
+ ** You can debug this using "nm" on the .so and .o files in the builds/
+ ** directory. See
+ ** http://eli.thegreenplace.net/2013/07/09/library-order-in-static-linking
+ ** for a longer discussion on symbol visibility.
+ **/
+
+#include "cvc4_private_library.h"
+
+#ifndef __CVC4__STATISTICS_REGISTRY_H
+#define __CVC4__STATISTICS_REGISTRY_H
+
+#include <stdint.h>
+
+#include <cassert>
+#include <ctime>
+#include <iomanip>
+#include <map>
+#include <sstream>
+#include <vector>
+
+#include "base/exception.h"
+#include "lib/clock_gettime.h"
+#include "util/statistics.h"
+
+namespace CVC4 {
+
+/**
+ * Prints a timespec.
+ *
+ * This is used in the implementation of TimerStat. This needs to be available
+ * before Stat due to ordering constraints in clang for TimerStat.
+ */
+std::ostream& operator<<(std::ostream& os, const timespec& t) CVC4_PUBLIC;
+
+#ifdef CVC4_STATISTICS_ON
+# define __CVC4_USE_STATISTICS true
+#else
+# define __CVC4_USE_STATISTICS false
+#endif
+
+
+/**
+ * The base class for all statistics.
+ *
+ * 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 Stat {
+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
+ * statistic delimiter string.
+ */
+ Stat(const std::string& name) throw(CVC4::IllegalArgumentException) :
+ d_name(name) {
+ if(__CVC4_USE_STATISTICS) {
+ CheckArgument(d_name.find(", ") == std::string::npos, name,
+ "Statistics names cannot include a comma (',')");
+ }
+ }
+
+ /** Destruct a statistic. This base-class version does nothing. */
+ virtual ~Stat() {}
+
+ /**
+ * Flush the value of this statistic to an output stream. Should
+ * finish the output with an end-of-line character.
+ */
+ virtual void flushInformation(std::ostream& out) const = 0;
+
+ /**
+ * 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
+ */
+ virtual void flushStat(std::ostream& out) const {
+ if(__CVC4_USE_STATISTICS) {
+ out << d_name << ", ";
+ flushInformation(out);
+ }
+ }
+
+ /** Get the name of this statistic. */
+ const std::string& getName() const {
+ return d_name;
+ }
+
+ /** Get the value of this statistic as a string. */
+ virtual SExpr getValue() const {
+ std::stringstream ss;
+ flushInformation(ss);
+ return SExpr(ss.str());
+ }
+
+};/* class Stat */
+
+// A generic way of making a SExpr from templated stats code.
+// for example, the uint64_t version ensures that we create
+// Integer-SExprs for ReadOnlyDataStats (like those inside
+// Minisat) without having to specialize the entire
+// ReadOnlyDataStat class template.
+template <class T>
+inline SExpr mkSExpr(const T& x) {
+ std::stringstream ss;
+ ss << x;
+ return SExpr(ss.str());
+}
+
+template <>
+inline SExpr mkSExpr(const uint64_t& x) {
+ return SExpr(Integer(x));
+}
+
+template <>
+inline SExpr mkSExpr(const int64_t& x) {
+ return SExpr(Integer(x));
+}
+
+template <>
+inline SExpr mkSExpr(const int& x) {
+ return SExpr(Integer(x));
+}
+
+template <>
+inline SExpr mkSExpr(const Integer& x) {
+ return SExpr(x);
+}
+
+template <>
+inline SExpr mkSExpr(const double& x) {
+ // roundabout way to get a Rational from a double
+ std::stringstream ss;
+ ss << std::fixed << std::setprecision(8) << x;
+ return SExpr(Rational::fromDecimal(ss.str()));
+}
+
+template <>
+inline SExpr mkSExpr(const Rational& x) {
+ return SExpr(x);
+}
+
+/**
+ * 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, 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:
+ * std::ostream& operator<<(std::ostream&, const T&)
+ */
+template <class T>
+class ReadOnlyDataStat : public Stat {
+public:
+ /** The "payload" type of this data statistic (that is, T). */
+ typedef T payload_t;
+
+ /** Construct a read-only data statistic with the given name. */
+ ReadOnlyDataStat(const std::string& name) :
+ Stat(name) {
+ }
+
+ /** Get the value of the statistic. */
+ virtual T getData() const = 0;
+
+ /** Flush the value of the statistic to the given output stream. */
+ void flushInformation(std::ostream& out) const {
+ if(__CVC4_USE_STATISTICS) {
+ out << getData();
+ }
+ }
+
+ SExpr getValue() const {
+ return mkSExpr(getData());
+ }
+
+};/* class ReadOnlyDataStat<T> */
+
+
+/**
+ * A data statistic class. This class extends a read-only data statistic
+ * with assignment (the statistic can be set as well as read). This class
+ * adds to the read-only case a pure virtual function setData(), thus
+ * providing the basic interface for a data statistic: getData() to get the
+ * statistic value, and setData() to set it.
+ *
+ * As with the read-only data statistic class, template class T must have
+ * stream insertion operation defined:
+ * std::ostream& operator<<(std::ostream&, const T&)
+ */
+template <class T>
+class DataStat : public ReadOnlyDataStat<T> {
+public:
+
+ /** Construct a data statistic with the given name. */
+ DataStat(const std::string& name) :
+ ReadOnlyDataStat<T>(name) {
+ }
+
+ /** Set the data statistic. */
+ virtual void setData(const T&) = 0;
+
+};/* class DataStat<T> */
+
+
+/**
+ * A data statistic that references a data cell of type T,
+ * implementing getData() by referencing that memory cell, and
+ * setData() by reassigning the statistic to point to the new
+ * data cell. The referenced data cell is kept as a const
+ * reference, meaning the referenced data is never actually
+ * modified by this class (it must be externally modified for
+ * a reference statistic to make sense). A common use for
+ * this type of statistic is to output a statistic that is kept
+ * outside the statistics package (for example, one that's kept
+ * by a theory implementation for internal heuristic purposes,
+ * which is important to keep even if statistics are turned off).
+ *
+ * Template class T must have an assignment operator=().
+ */
+template <class T>
+class ReferenceStat : public DataStat<T> {
+private:
+ /** The referenced data cell */
+ const T* d_data;
+
+public:
+ /**
+ * Construct a reference stat with the given name and a reference
+ * to NULL.
+ */
+ ReferenceStat(const std::string& name) :
+ DataStat<T>(name),
+ d_data(NULL) {
+ }
+
+ /**
+ * Construct a reference stat with the given name and a reference to
+ * the given data.
+ */
+ ReferenceStat(const std::string& name, const T& data) :
+ DataStat<T>(name),
+ d_data(NULL) {
+ setData(data);
+ }
+
+ /** Set this reference statistic to refer to the given data cell. */
+ void setData(const T& t) {
+ if(__CVC4_USE_STATISTICS) {
+ d_data = &t;
+ }
+ }
+
+ /** Get the value of the referenced data cell. */
+ T getData() const {
+ return *d_data;
+ }
+
+};/* class ReferenceStat<T> */
+
+
+/**
+ * A data statistic that keeps a T and sets it with setData().
+ *
+ * Template class T must have an operator=() and a copy constructor.
+ */
+template <class T>
+class BackedStat : public DataStat<T> {
+protected:
+ /** The internally-kept statistic value */
+ T d_data;
+
+public:
+
+ /** Construct a backed statistic with the given name and initial value. */
+ BackedStat(const std::string& name, const T& init) :
+ DataStat<T>(name),
+ d_data(init) {
+ }
+
+ /** Set the underlying data value to the given value. */
+ void setData(const T& t) {
+ if(__CVC4_USE_STATISTICS) {
+ d_data = t;
+ }
+ }
+
+ /** Identical to setData(). */
+ BackedStat<T>& operator=(const T& t) {
+ if(__CVC4_USE_STATISTICS) {
+ d_data = t;
+ }
+ return *this;
+ }
+
+ /** Get the underlying data value. */
+ T getData() const {
+ return d_data;
+ }
+
+};/* class BackedStat<T> */
+
+
+/**
+ * A wrapper Stat for another Stat.
+ *
+ * This type of Stat is useful in cases where a module (like the
+ * CongruenceClosure module) might keep its own statistics, but might
+ * be instantiated in many contexts by many clients. This makes such
+ * a statistic inappopriate to register with the StatisticsRegistry
+ * directly, as all would be output with the same name (and may be
+ * unregistered too quickly anyway). A WrappedStat allows the calling
+ * client (say, TheoryUF) to wrap the Stat from the client module,
+ * giving it a globally unique name.
+ */
+template <class Stat>
+class WrappedStat : public ReadOnlyDataStat<typename Stat::payload_t> {
+ typedef typename Stat::payload_t T;
+
+ const ReadOnlyDataStat<T>& d_stat;
+
+ /** Private copy constructor undefined (no copy permitted). */
+ WrappedStat(const WrappedStat&) CVC4_UNDEFINED;
+ /** Private assignment operator undefined (no copy permitted). */
+ WrappedStat<T>& operator=(const WrappedStat&) CVC4_UNDEFINED;
+
+public:
+
+ /**
+ * Construct a wrapped statistic with the given name that wraps the
+ * given statistic.
+ */
+ WrappedStat(const std::string& name, const ReadOnlyDataStat<T>& stat) :
+ ReadOnlyDataStat<T>(name),
+ d_stat(stat) {
+ }
+
+ /** Get the data of the underlying (wrapped) statistic. */
+ T getData() const {
+ return d_stat.getData();
+ }
+
+ SExpr getValue() const {
+ return d_stat.getValue();
+ }
+
+};/* class WrappedStat<T> */
+
+/**
+ * A backed integer-valued (64-bit signed) statistic.
+ * This doesn't functionally differ from its base class BackedStat<int64_t>,
+ * except for adding convenience functions for dealing with integers.
+ */
+class IntStat : public BackedStat<int64_t> {
+public:
+
+ /**
+ * Construct an integer-valued statistic with the given name and
+ * initial value.
+ */
+ IntStat(const std::string& name, int64_t init) :
+ BackedStat<int64_t>(name, init) {
+ }
+
+ /** Increment the underlying integer statistic. */
+ IntStat& operator++() {
+ if(__CVC4_USE_STATISTICS) {
+ ++d_data;
+ }
+ return *this;
+ }
+
+ /** Increment the underlying integer statistic by the given amount. */
+ IntStat& operator+=(int64_t val) {
+ if(__CVC4_USE_STATISTICS) {
+ d_data += val;
+ }
+ return *this;
+ }
+
+ /** Keep the maximum of the current statistic value and the given one. */
+ void maxAssign(int64_t val) {
+ if(__CVC4_USE_STATISTICS) {
+ if(d_data < val) {
+ d_data = val;
+ }
+ }
+ }
+
+ /** Keep the minimum of the current statistic value and the given one. */
+ void minAssign(int64_t val) {
+ if(__CVC4_USE_STATISTICS) {
+ if(d_data > val) {
+ d_data = val;
+ }
+ }
+ }
+
+ SExpr getValue() const {
+ return SExpr(Integer(d_data));
+ }
+
+};/* class IntStat */
+
+template <class T>
+class SizeStat : public Stat {
+private:
+ const T& d_sized;
+public:
+ SizeStat(const std::string&name, const T& sized) :
+ Stat(name), d_sized(sized) {}
+ ~SizeStat() {}
+
+ void flushInformation(std::ostream& out) const {
+ out << d_sized.size();
+ }
+
+ SExpr getValue() const {
+ return SExpr(Integer(d_sized.size()));
+ }
+
+};/* class SizeStat */
+
+/**
+ * The value for an AverageStat is the running average of (e1, e_2, ..., e_n),
+ * (e1 + e_2 + ... + e_n)/n,
+ * where e_i is an entry added by an addEntry(e_i) call.
+ * The value is initially always 0.
+ * (This is to avoid making parsers confused.)
+ *
+ * A call to setData() will change the running average but not reset the
+ * running count, so should generally be avoided. Call addEntry() to add
+ * an entry to the average calculation.
+ */
+class AverageStat : public BackedStat<double> {
+private:
+ /**
+ * The number of accumulations of the running average that we
+ * 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), d_sum(0.0) {
+ }
+
+ /** Add an entry to the running-average calculation. */
+ void addEntry(double e) {
+ if(__CVC4_USE_STATISTICS) {
+ ++d_count;
+ d_sum += e;
+ setData(d_sum / d_count);
+ }
+ }
+
+ SExpr getValue() const {
+ std::stringstream ss;
+ ss << std::fixed << std::setprecision(8) << d_data;
+ return SExpr(Rational::fromDecimal(ss.str()));
+ }
+
+};/* class AverageStat */
+
+/** A statistic that contains a SExpr. */
+class SExprStat : public Stat {
+private:
+ SExpr d_data;
+
+public:
+
+ /**
+ * Construct a SExpr-valued statistic with the given name and
+ * initial value.
+ */
+ SExprStat(const std::string& name, const SExpr& init) :
+ Stat(name), d_data(init){}
+
+ virtual void flushInformation(std::ostream& out) const {
+ out << d_data << std::endl;
+ }
+
+ SExpr getValue() const {
+ return d_data;
+ }
+
+};/* class SExprStat */
+
+template <class T>
+class ListStat : public Stat {
+private:
+ typedef std::vector<T> List;
+ List d_list;
+public:
+
+ /**
+ * Construct an integer-valued statistic with the given name and
+ * initial value.
+ */
+ ListStat(const std::string& name) : Stat(name) {}
+ ~ListStat() {}
+
+ void flushInformation(std::ostream& out) const{
+ if(__CVC4_USE_STATISTICS) {
+ typename List::const_iterator i = d_list.begin(), end = d_list.end();
+ out << "[";
+ if(i != end){
+ out << *i;
+ ++i;
+ for(; i != end; ++i){
+ out << ", " << *i;
+ }
+ }
+ out << "]";
+ }
+ }
+
+ ListStat& operator<<(const T& val){
+ if(__CVC4_USE_STATISTICS) {
+ d_list.push_back(val);
+ }
+ return (*this);
+ }
+
+};/* class ListStat */
+
+template <class T>
+class HistogramStat : public Stat {
+private:
+ typedef std::map<T, unsigned int> Histogram;
+ Histogram d_hist;
+public:
+
+ /** Construct a histogram of a stream of entries. */
+ HistogramStat(const std::string& name) : Stat(name) {}
+ ~HistogramStat() {}
+
+ void flushInformation(std::ostream& out) const{
+ if(__CVC4_USE_STATISTICS) {
+ typename Histogram::const_iterator i = d_hist.begin();
+ typename Histogram::const_iterator end = d_hist.end();
+ out << "[";
+ while(i != end){
+ const T& key = (*i).first;
+ unsigned int count = (*i).second;
+ out << "("<<key<<" : "<<count<< ")";
+ ++i;
+ if(i != end){
+ out << ", ";
+ }
+ }
+ out << "]";
+ }
+ }
+
+ HistogramStat& operator<<(const T& val){
+ if(__CVC4_USE_STATISTICS) {
+ if(d_hist.find(val) == d_hist.end()){
+ d_hist.insert(std::make_pair(val,0));
+ }
+ d_hist[val]++;
+ }
+ return (*this);
+ }
+
+};/* class HistogramStat */
+
+/****************************************************************************/
+/* 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 StatisticsBase, public Stat {
+private:
+
+ /** Private copy constructor undefined (no copy permitted). */
+ StatisticsRegistry(const StatisticsRegistry&) CVC4_UNDEFINED;
+
+public:
+
+ /** Construct an nameless statistics registry */
+ StatisticsRegistry() {}
+
+ /** Construct a statistics registry */
+ StatisticsRegistry(const std::string& name)
+ throw(CVC4::IllegalArgumentException);
+
+ /**
+ * Set the name of this statistic registry, used as prefix during
+ * output. (This version overrides StatisticsBase::setPrefix().)
+ */
+ void setPrefix(const std::string& name) {
+ d_prefix = d_name = name;
+ }
+
+ /** Overridden to avoid the name being printed */
+ void flushStat(std::ostream &out) const;
+
+ virtual void flushInformation(std::ostream& out) const;
+
+ SExpr getValue() const {
+ std::vector<SExpr> v;
+ for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) {
+ std::vector<SExpr> w;
+ w.push_back(SExpr((*i)->getName()));
+ w.push_back((*i)->getValue());
+ v.push_back(SExpr(w));
+ }
+ return SExpr(v);
+ }
+
+ /** Register a new statistic */
+ void registerStat(Stat* s) throw(CVC4::IllegalArgumentException);
+
+ /** Unregister a new statistic */
+ void unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException);
+
+};/* class StatisticsRegistry */
+
+class CodeTimer;
+
+/**
+ * A timer statistic. The timer can be started and stopped
+ * arbitrarily, like a stopwatch; the value of the statistic at the
+ * end is the accumulated time over all (start,stop) pairs.
+ */
+class CVC4_PUBLIC TimerStat : public BackedStat<timespec> {
+
+ // strange: timespec isn't placed in 'std' namespace ?!
+ /** The last start time of this timer */
+ timespec d_start;
+
+ /** Whether this timer is currently running */
+ bool d_running;
+
+public:
+
+ typedef CVC4::CodeTimer CodeTimer;
+
+ /**
+ * Construct a timer statistic with the given name. Newly-constructed
+ * timers have a 0.0 value and are not running.
+ */
+ TimerStat(const std::string& name) :
+ BackedStat< timespec >(name, timespec()),
+ d_running(false) {
+ /* timespec is POD and so may not be initialized to zero;
+ * here, ensure it is */
+ d_data.tv_sec = d_data.tv_nsec = 0;
+ }
+
+ /** Start the timer. */
+ void start();
+
+ /**
+ * Stop the timer and update the statistic value with the
+ * accumulated time.
+ */
+ void stop();
+
+ /** If the timer is currently running */
+ bool running() const;
+
+ timespec getData() const;
+
+ SExpr getValue() const;
+
+};/* class TimerStat */
+
+/**
+ * Utility class to make it easier to call stop() at the end of a
+ * code block. When constructed, it starts the timer. When
+ * destructed, it stops the timer.
+ */
+class CodeTimer {
+ TimerStat& d_timer;
+ bool d_reentrant;
+
+ /** Private copy constructor undefined (no copy permitted). */
+ CodeTimer(const CodeTimer& timer) CVC4_UNDEFINED;
+ /** Private assignment operator undefined (no copy permitted). */
+ CodeTimer& operator=(const CodeTimer& timer) CVC4_UNDEFINED;
+
+public:
+ CodeTimer(TimerStat& timer, bool allow_reentrant = false) : d_timer(timer), d_reentrant(false) {
+ if(!allow_reentrant || !(d_reentrant = d_timer.running())) {
+ d_timer.start();
+ }
+ }
+ ~CodeTimer() {
+ if(!d_reentrant) {
+ d_timer.stop();
+ }
+ }
+};/* class CodeTimer */
+
+/**
+ * Resource-acquisition-is-initialization idiom for statistics
+ * registry. Useful for stack-based statistics (like in the driver).
+ * Generally, for statistics kept in a member field of class, it's
+ * better to use the above KEEP_STATISTIC(), which does declaration of
+ * the member, construction of the statistic, and
+ * registration/unregistration. This RAII class only does
+ * registration and unregistration.
+ */
+class CVC4_PUBLIC RegisterStatistic {
+public:
+ RegisterStatistic(StatisticsRegistry* reg, Stat* stat);
+ ~RegisterStatistic();
+
+private:
+ StatisticsRegistry* d_reg;
+ Stat* d_stat;
+
+};/* class RegisterStatistic */
+
+#undef __CVC4_USE_STATISTICS
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__STATISTICS_REGISTRY_H */
#include <sstream>
#include "expr/expr.h"
-#include "expr/statistics.h"
#include "smt/smt_engine.h"
#include "util/sexpr.h"
+#include "util/statistics.h"
using namespace CVC4;
using namespace std;
#include <string>
#include <ctime>
-#include "expr/statistics_registry.h"
+#include "lib/clock_gettime.h"
+#include "util/statistics_registry.h"
using namespace CVC4;
using namespace std;
+/**
+ * This is a duplicate of operator== in statistics_registry.h.
+ * This is duplicated here to try to avoid polluting top namepsace.
+ *
+ * If operator== is in the CVC4 namespace, there are some circumstances
+ * where clang does not find this operator.
+ */
+bool operator==(const timespec& a, const timespec& b) {
+ // assumes a.tv_nsec and b.tv_nsec are in range
+ return a.tv_sec == b.tv_sec && a.tv_nsec == b.tv_nsec;
+}
+
class StatsBlack : public CxxTest::TestSuite {
public:
projects / cvc5.git / commitdiff