summaryrefslogtreecommitdiff
path: root/src/prop/theory_proxy.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/theory_proxy.cpp')
-rw-r--r--src/prop/theory_proxy.cpp11
1 files changed, 8 insertions, 3 deletions
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index d0830b9a5..e87046ad5 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -19,14 +19,15 @@
#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 {
@@ -42,11 +43,15 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine,
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. */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback