From: Tim King Date: Fri, 18 Jun 2010 22:24:59 +0000 (+0000) Subject: Merging the statistics branch into the main trunk. I'll go over how to use this Tuesd... X-Git-Tag: cvc5-1.0.0~8980 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fd6af9181e763cd9564245114cfa47f3952484db;p=cvc5.git Merging the statistics branch into the main trunk. I'll go over how to use this Tuesday during the meeting. You'll need to run autogen and receonfigure after updating. --- diff --git a/configure.ac b/configure.ac index f805c445c..28a5cca7a 100644 --- a/configure.ac +++ b/configure.ac @@ -71,7 +71,7 @@ AC_ARG_WITH([build], if test -z "${with_build+set}" -o "$with_build" = default; then with_build=default fi -if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}"; then +if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}"; then custom_build_profile=no else custom_build_profile=yes @@ -126,6 +126,13 @@ if test -n "${enable_profiling+set}"; then btargs="$btargs noprofiling" fi fi +if test -n "${enable_statistics+set}"; then + if test "$enable_statistics" = yes; then + btargs="$btargs statistics" + else + btargs="$btargs nostatistics" + fi +fi AC_MSG_RESULT([$with_build]) AC_MSG_CHECKING([for appropriate build string]) @@ -199,6 +206,7 @@ case "$with_build" in if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=3 ; fi if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi + if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi @@ -213,6 +221,7 @@ case "$with_build" in if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi + if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi ;; default) # moderately optimized, assertions, tracing @@ -225,6 +234,7 @@ case "$with_build" in if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi + if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi ;; @@ -238,6 +248,7 @@ case "$with_build" in if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no ; fi if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi + if test -z "${enable_statistics+set}" ; then enable_statistics=no ; fi if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi if test -z "${enable_muzzle+set}" ; then enable_muzzle=yes ; fi ;; @@ -302,6 +313,23 @@ if test "$enable_debug_symbols" = yes; then CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-ggdb3" fi +AC_MSG_CHECKING([whether to include statistics are turned on in libcvc4]) + +AC_ARG_ENABLE([statistics], + [AS_HELP_STRING([--disable-statistics], + [do not include statistics in libcvc4])]) + +if test -z "${enable_statistics+set}"; then + enable_statistics=yes +fi + +AC_MSG_RESULT([$enable_statistics]) + +if test "$enable_statistics" = yes; then + CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-DCVC4_STATISTICS_ON" + CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-DCVC4_STATISTICS_ON" +fi + AC_MSG_CHECKING([whether to include assertions in build]) AC_ARG_ENABLE([assertions], @@ -603,6 +631,7 @@ Muzzle : $enable_muzzle gcov support : $enable_coverage gprof support: $enable_profiling unit tests : $support_unit_tests +statistics : $enable_statistics static libs : $enable_static shared libs : $enable_shared diff --git a/src/main/main.cpp b/src/main/main.cpp index 7fb0d92c9..5c19a995d 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -35,6 +35,7 @@ #include "util/output.h" #include "util/options.h" #include "util/result.h" +#include "util/stats.h" using namespace std; using namespace CVC4; @@ -85,6 +86,7 @@ int main(int argc, char* argv[]) { } } + int runCvc4(int argc, char* argv[]) { // Initialize the signal handlers @@ -183,6 +185,10 @@ int runCvc4(int argc, char* argv[]) { // Remove the parser delete parser; + if(options.statistics){ + StatisticsRegistry::flushStatistics(cerr); + } + switch(lastResult.asSatisfiabilityResult().isSAT()) { case Result::SAT: diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 4adaa1434..c33982ddc 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -90,8 +90,7 @@ public: * PropEngine and Theory). For now, there's nothing to do here in * the PropEngine. */ - void shutdown() { - } + void shutdown() { } /** * Converts the given formula to CNF and assert the CNF to the sat solver. diff --git a/src/prop/sat.h b/src/prop/sat.h index e023410c7..f64697d7b 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -26,6 +26,7 @@ #define __CVC4_USE_MINISAT #include "util/options.h" +#include "util/stats.h" #ifdef __CVC4_USE_MINISAT @@ -132,6 +133,49 @@ class SatSolver : public SatInputInterface { /** Minisat solver */ minisat::SimpSolver* d_minisat; + class Statistics { + private: + ReferenceStat d_statStarts, d_statDecisions; + ReferenceStat d_statRndDecisions, d_statPropagations; + ReferenceStat d_statConflicts, d_statClausesLiterals; + ReferenceStat d_statLearntsLiterals, d_statMaxLiterals; + ReferenceStat d_statTotLiterals; + public: + 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") + { + 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); + } + void init(minisat::SimpSolver* d_minisat){ + d_statStarts.setData(d_minisat->starts); + d_statDecisions.setData(d_minisat->decisions); + d_statRndDecisions.setData(d_minisat->rnd_decisions); + d_statPropagations.setData(d_minisat->propagations); + d_statConflicts.setData(d_minisat->conflicts); + d_statClausesLiterals.setData(d_minisat->clauses_literals); + d_statLearntsLiterals.setData(d_minisat->learnts_literals); + d_statMaxLiterals.setData(d_minisat->max_literals); + d_statTotLiterals.setData(d_minisat->tot_literals); + } + }; + Statistics d_statistics; + #endif /* __CVC4_USE_MINISAT */ protected: @@ -150,7 +194,7 @@ public: ~SatSolver(); bool solve(); - + void addClause(SatClause& clause, bool lemma); SatVariable newVar(bool theoryAtom = false); @@ -158,7 +202,7 @@ public: void theoryCheck(SatClause& conflict); void enqueueTheoryLiteral(const SatLiteral& l); - + void setCnfStream(CnfStream* cnfStream); SatLiteralValue value(SatLiteral l); @@ -173,7 +217,8 @@ inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, d_propEngine(propEngine), d_cnfStream(NULL), d_theoryEngine(theoryEngine), - d_context(context) + d_context(context), + d_statistics() { // Create the solver d_minisat = new minisat::SimpSolver(this, d_context); @@ -183,6 +228,8 @@ inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, d_minisat->remove_satisfied = false; // Make minisat reuse the literal values d_minisat->polarity_mode = minisat::SimpSolver::polarity_user; + + d_statistics.init(d_minisat); } inline SatSolver::~SatSolver() { diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 18bea2b8d..c16d8f183 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -54,11 +54,11 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) : d_constants(NodeManager::currentNM()), d_partialModel(c), d_diseq(c), - d_rewriter(&d_constants) + d_rewriter(&d_constants), + d_statistics() { uint64_t ass_id = partial_model::Assignment::getId(); Debug("arithsetup") << "Assignment: " << ass_id << std::endl; - } TheoryArith::~TheoryArith(){ for(vector::iterator i=d_variables.begin(); i!= d_variables.end(); ++i){ @@ -67,6 +67,20 @@ TheoryArith::~TheoryArith(){ } } +TheoryArith::Statistics::Statistics(): + d_statPivots("theory::arith::pivots",0), + d_statUpdates("theory::arith::updates",0), + d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0), + d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0), + d_statUpdateConflicts("theory::arith::UpdateConflicts", 0) +{ + StatisticsRegistry::registerStat(&d_statPivots); + StatisticsRegistry::registerStat(&d_statUpdates); + StatisticsRegistry::registerStat(&d_statAssertUpperConflicts); + StatisticsRegistry::registerStat(&d_statAssertLowerConflicts); + StatisticsRegistry::registerStat(&d_statUpdateConflicts); +} + bool isBasicSum(TNode n){ if(n.getKind() != kind::PLUS) return false; @@ -260,6 +274,7 @@ bool TheoryArith::AssertUpper(TNode n, TNode original){ Node lbc = d_partialModel.getLowerConstraint(x_i); Node conflict = NodeManager::currentNM()->mkNode(AND, lbc, original); Debug("arith") << "AssertUpper conflict " << conflict << endl; + ++(d_statistics.d_statAssertUpperConflicts); d_out->conflict(conflict); return true; } @@ -294,6 +309,7 @@ bool TheoryArith::AssertLower(TNode n, TNode original){ Node conflict = NodeManager::currentNM()->mkNode(AND, ubc, original); d_out->conflict(conflict); Debug("arith") << "AssertLower conflict " << conflict << endl; + ++(d_statistics.d_statAssertLowerConflicts); return true; } @@ -362,6 +378,7 @@ bool TheoryArith::AssertEquality(TNode n, TNode original){ void TheoryArith::update(TNode x_i, DeltaRational& v){ Assert(!isBasic(x_i)); DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i); + ++(d_statistics.d_statUpdates); Debug("arith") <<"update " << x_i << ": " << assignment_x_i << "|-> " << v << endl; @@ -422,6 +439,7 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){ } } + ++(d_statistics.d_statPivots); d_tableau.pivot(x_i, x_j); checkBasicVariable(x_j); @@ -507,6 +525,7 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06 DeltaRational l_i = d_partialModel.getLowerBound(x_i); TNode x_j = selectSlackBelow(x_i); if(x_j == TNode::null() ){ + ++(d_statistics.d_statUpdateConflicts); return generateConflictBelow(x_i); //unsat } pivotAndUpdate(x_i, x_j, l_i); @@ -515,6 +534,7 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06 DeltaRational u_i = d_partialModel.getUpperBound(x_i); TNode x_j = selectSlackAbove(x_i); if(x_j == TNode::null() ){ + ++(d_statistics.d_statUpdateConflicts); return generateConflictAbove(x_i); //unsat } pivotAndUpdate(x_i, x_j, u_i); @@ -630,11 +650,6 @@ bool TheoryArith::assertionCases(TNode original, TNode assertion){ return AssertLower(assertion, original); case EQUAL: return AssertEquality(assertion,original); -// if(AssertUpper(assertion, original)){ -// return true; -// }else{ -// return AssertLower(assertion, original); -// } case NOT: { TNode atom = assertion[0]; diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index cb0705f4c..aff60f651 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -31,6 +31,8 @@ #include "theory/arith/arith_rewriter.h" #include "theory/arith/partial_model.h" +#include "util/stats.h" + #include #include @@ -94,6 +96,7 @@ private: */ ArithRewriter d_rewriter; + public: TheoryArith(context::Context* c, OutputChannel& out); ~TheoryArith(); @@ -115,6 +118,9 @@ public: void propagate(Effort e) { Unimplemented(); } void explain(TNode n, Effort e) { Unimplemented(); } + void shutdown(){ } + + private: /** * Assert*(n, orig) takes an bound n that is implied by orig. @@ -228,6 +234,18 @@ private: //TODO get rid of this! Node simulatePreprocessing(TNode n); + + /** These fields are designed to be accessable to TheoryArith methods. */ + class Statistics { + public: + IntStat d_statPivots, d_statUpdates, d_statAssertUpperConflicts; + IntStat d_statAssertLowerConflicts, d_statUpdateConflicts; + + Statistics(); + }; + + Statistics d_statistics; + }; }/* CVC4::theory::arith namespace */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 1912cb026..bf4d8d10c 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -32,6 +32,8 @@ #include "theory/arrays/theory_arrays.h" #include "theory/bv/theory_bv.h" +#include "util/stats.h" + namespace CVC4 { // In terms of abstraction, this is below (and provides services to) @@ -74,24 +76,31 @@ class TheoryEngine { void conflict(TNode conflictNode, bool safe) throw(theory::Interrupted, AssertionException) { Debug("theory") << "EngineOutputChannel::conflict(" << conflictNode << ")" << std::endl; d_conflictNode = conflictNode; + ++(d_engine->d_statistics.d_statConflicts); if(safe) { throw theory::Interrupted(); } } void propagate(TNode, bool) throw(theory::Interrupted, AssertionException) { + ++(d_engine->d_statistics.d_statPropagate); } void lemma(TNode node, bool) throw(theory::Interrupted, AssertionException) { + ++(d_engine->d_statistics.d_statLemma); d_engine->newLemma(node); } void augmentingLemma(TNode node, bool) throw(theory::Interrupted, AssertionException) { + ++(d_engine->d_statistics.d_statAugLemma); d_engine->newAugmentingLemma(node); } void explanation(TNode, bool) throw(theory::Interrupted, AssertionException) { + ++(d_engine->d_statistics.d_statExplanatation); } }; + + EngineOutputChannel d_theoryOut; theory::booleans::TheoryBool d_bool; @@ -100,6 +109,7 @@ class TheoryEngine { theory::arrays::TheoryArrays d_arrays; theory::bv::TheoryBV d_bv; + /** * Check whether a node is in the rewrite cache or not. */ @@ -190,7 +200,8 @@ public: d_uf(ctxt, d_theoryOut), d_arith(ctxt, d_theoryOut), d_arrays(ctxt, d_theoryOut), - d_bv(ctxt, d_theoryOut) { + d_bv(ctxt, d_theoryOut), + d_statistics() { d_theoryOfTable.registerTheory(&d_bool); d_theoryOfTable.registerTheory(&d_uf); @@ -319,6 +330,26 @@ public: return d_theoryOut.d_conflictNode; } +private: + class Statistics { + public: + IntStat d_statConflicts, d_statPropagate, d_statLemma, d_statAugLemma, d_statExplanatation; + Statistics(): + d_statConflicts("theory::conlficts",0), + d_statPropagate("theory::propagate",0), + d_statLemma("theory::lemma",0), + d_statAugLemma("theory::aug_lemma", 0), + d_statExplanatation("theory::explanation", 0) + { + StatisticsRegistry::registerStat(&d_statConflicts); + StatisticsRegistry::registerStat(&d_statPropagate); + StatisticsRegistry::registerStat(&d_statLemma); + StatisticsRegistry::registerStat(&d_statAugLemma); + StatisticsRegistry::registerStat(&d_statExplanatation); + } + }; + Statistics d_statistics; + };/* class TheoryEngine */ }/* CVC4 namespace */ diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 88d4fc56e..0f6fb5929 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -30,4 +30,6 @@ libutil_la_SOURCES = \ bitvector.h \ bitvector.cpp \ gmp_util.h \ - sexpr.h + sexpr.h \ + stats.h \ + stats.cpp diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp index f789313b8..9440b6df3 100644 --- a/src/util/bitvector.cpp +++ b/src/util/bitvector.cpp @@ -2,7 +2,7 @@ /*! \file bitvector.cpp ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/util/bitvector.h b/src/util/bitvector.h index e3ba969ec..746d9aaaf 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: dejan ** Major contributors: cconway - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h index de237b793..692d3d742 100644 --- a/src/util/gmp_util.h +++ b/src/util/gmp_util.h @@ -2,7 +2,7 @@ /*! \file gmp_util.h ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/util/hash.h b/src/util/hash.h index 708628c24..6a6130886 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -2,7 +2,7 @@ /*! \file hash.h ** \verbatim ** Original author: cconway - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/util/integer.h b/src/util/integer.h index d1921f597..f3431334d 100644 --- a/src/util/integer.h +++ b/src/util/integer.h @@ -2,8 +2,8 @@ /*! \file integer.h ** \verbatim ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): dejan, cconway, mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): dejan, cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/util/rational.h b/src/util/rational.h index 81e0f7fbd..feca66da1 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -2,8 +2,8 @@ /*! \file rational.h ** \verbatim ** Original author: taking - ** Major contributors: cconway - ** Minor contributors (to current version): dejan, mdeters + ** Major contributors: none + ** Minor contributors (to current version): dejan, mdeters, cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/util/sexpr.h b/src/util/sexpr.h index f00343729..607075658 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/util/stats.cpp b/src/util/stats.cpp new file mode 100644 index 000000000..cf7b3ad51 --- /dev/null +++ b/src/util/stats.cpp @@ -0,0 +1,39 @@ +/********************* */ +/*! \file stats.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** rief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "util/stats.h" + +using namespace CVC4; + +StatisticsRegistry::StatSet StatisticsRegistry::d_registeredStats; + +std::string Stat::s_delim(","); + + + + +void StatisticsRegistry::flushStatistics(std::ostream& out){ +#ifdef CVC4_STATISTICS_ON + for(StatSet::iterator i=d_registeredStats.begin();i != d_registeredStats.end();++i){ + Stat* s = *i; + s->flushStat(out); + out << std::endl; + } +#endif +} diff --git a/src/util/stats.h b/src/util/stats.h new file mode 100644 index 000000000..b9f0fdf61 --- /dev/null +++ b/src/util/stats.h @@ -0,0 +1,214 @@ +/********************* */ +/*! \file stats.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** rief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__STATS_H +#define __CVC4__STATS_H + +#include +#include +#include +#include "util/Assert.h" + +namespace CVC4 { + + +#ifdef CVC4_STATISTICS_ON +#define USE_STATISTICS true +#else +#define USE_STATISTICS false +#endif + +class CVC4_PUBLIC Stat; + +class CVC4_PUBLIC StatisticsRegistry { +private: + struct StatCmp; + + typedef std::set< Stat*, StatCmp > StatSet; + static StatSet d_registeredStats; + +public: + static void flushStatistics(std::ostream& out); + + static inline void registerStat(Stat* s) throw (AssertionException); +}; /* class StatisticsRegistry */ + + +class CVC4_PUBLIC Stat { +private: + std::string d_name; + + static std::string s_delim; + +public: + + Stat(const std::string& s) throw (CVC4::AssertionException) : d_name(s) + { + if(USE_STATISTICS){ + AlwaysAssert(d_name.find(s_delim) == std::string::npos); + } + } + + virtual void flushInformation(std::ostream& out) const = 0; + + void flushStat(std::ostream& out) const{ + if(USE_STATISTICS){ + out << d_name << s_delim; + flushInformation(out); + } + } + + const std::string& getName() const { + return d_name; + } +}; + +struct StatisticsRegistry::StatCmp { + bool operator()(const Stat* s1, const Stat* s2) const + { + return (s1->getName()) < (s2->getName()); + } +}; + +inline void StatisticsRegistry::registerStat(Stat* s) throw (AssertionException){ + if(USE_STATISTICS){ + AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end()); + d_registeredStats.insert(s); + } +} + + +template +class DataStat : public Stat{ +public: + DataStat(const std::string& s) : Stat(s) {} + + virtual const T& getData() const = 0; + virtual void setData(const T&) = 0; + + void flushInformation(std::ostream& out) const{ + if(USE_STATISTICS){ + out << getData(); + } + } +}; + +template +class ReferenceStat: public DataStat{ +private: + const T* d_data; + +public: + ReferenceStat(const std::string& s): DataStat(s), d_data(NULL){} + + ReferenceStat(const std::string& s, const T& data):ReferenceStat(s){ + setData(data); + } + + void setData(const T& t){ + if(USE_STATISTICS){ + d_data = &t; + } + } + const T& getData() const{ + if(USE_STATISTICS){ + return *d_data; + }else{ + Unreachable(); + } + } +}; + +/** T must have an operator=() and a copy constructor. */ +template +class BackedStat: public DataStat{ +protected: + T d_data; + +public: + + BackedStat(const std::string& s, const T& init): DataStat(s), d_data(init) + {} + + void setData(const T& t) { + if(USE_STATISTICS){ + d_data = t; + } + } + + BackedStat& operator=(const T& t){ + if(USE_STATISTICS){ + d_data = t; + } + return *this; + } + + const T& getData() const{ + if(USE_STATISTICS){ + return d_data; + }else{ + Unreachable(); + } + } +}; + +class IntStat : public BackedStat{ +public: + + IntStat(const std::string& s, int64_t init): BackedStat(s, init) + {} + + IntStat& operator++(){ + if(USE_STATISTICS){ + ++d_data; + } + return *this; + } + + IntStat& operator+=(int64_t val){ + if(USE_STATISTICS){ + d_data+= val; + } + return *this; + } + + void maxAssign(int64_t val){ + if(USE_STATISTICS){ + if(d_data < val){ + d_data = val; + } + } + } + + void minAssign(int64_t val){ + if(USE_STATISTICS){ + if(d_data > val){ + d_data = val; + } + } + } +}; + +#undef USE_STATISTICS + +}/* CVC4 namespace */ + +#endif /* __CVC4__STATS_H */