summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/main/main.cpp6
-rw-r--r--src/prop/prop_engine.h3
-rw-r--r--src/prop/sat.h53
-rw-r--r--src/theory/arith/theory_arith.cpp29
-rw-r--r--src/theory/arith/theory_arith.h18
-rw-r--r--src/theory/theory_engine.h33
-rw-r--r--src/util/Makefile.am4
-rw-r--r--src/util/bitvector.cpp2
-rw-r--r--src/util/bitvector.h2
-rw-r--r--src/util/gmp_util.h2
-rw-r--r--src/util/hash.h2
-rw-r--r--src/util/integer.h4
-rw-r--r--src/util/rational.h4
-rw-r--r--src/util/sexpr.h2
-rw-r--r--src/util/stats.cpp39
-rw-r--r--src/util/stats.h214
16 files changed, 394 insertions, 23 deletions
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<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() :
+ 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<Node>::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 <vector>
#include <queue>
@@ -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 <string>
+#include <ostream>
+#include <set>
+#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 T>
+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 T>
+class ReferenceStat: public DataStat<T>{
+private:
+ const T* d_data;
+
+public:
+ ReferenceStat(const std::string& s): DataStat<T>(s), d_data(NULL){}
+
+ ReferenceStat(const std::string& s, const T& data):ReferenceStat<T>(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 T>
+class BackedStat: public DataStat<T>{
+protected:
+ T d_data;
+
+public:
+
+ BackedStat(const std::string& s, const T& init): DataStat<T>(s), d_data(init)
+ {}
+
+ void setData(const T& t) {
+ if(USE_STATISTICS){
+ d_data = t;
+ }
+ }
+
+ BackedStat<T>& 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<int64_t>{
+public:
+
+ IntStat(const std::string& s, int64_t init): BackedStat<int64_t>(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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback