summaryrefslogtreecommitdiff
path: root/src/theory/arith/constraint.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/constraint.cpp')
-rw-r--r--src/theory/arith/constraint.cpp12
1 files changed, 7 insertions, 5 deletions
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index f13565a7f..5dc0ba1ac 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -14,14 +14,15 @@
** [[ 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"
@@ -893,13 +894,14 @@ ConstraintDatabase::Statistics::Statistics():
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){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback