summaryrefslogtreecommitdiff
path: root/src/theory/uf
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/uf')
-rw-r--r--src/theory/uf/cardinality_extension.cpp25
-rw-r--r--src/theory/uf/cardinality_extension.h3
-rw-r--r--src/theory/uf/equality_engine.cpp27
-rw-r--r--src/theory/uf/equality_engine.h6
-rw-r--r--src/theory/uf/symmetry_breaker.cpp68
-rw-r--r--src/theory/uf/symmetry_breaker.h6
-rw-r--r--src/theory/uf/theory_uf.cpp2
7 files changed, 51 insertions, 86 deletions
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index b45ccbac3..25f87de2c 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -1748,23 +1748,16 @@ void CardinalityExtension::checkCombinedCardinality()
}
CardinalityExtension::Statistics::Statistics()
- : d_clique_conflicts("CardinalityExtension::Clique_Conflicts", 0),
- d_clique_lemmas("CardinalityExtension::Clique_Lemmas", 0),
- d_split_lemmas("CardinalityExtension::Split_Lemmas", 0),
- d_max_model_size("CardinalityExtension::Max_Model_Size", 1)
+ : d_clique_conflicts(smtStatisticsRegistry().registerInt(
+ "CardinalityExtension::Clique_Conflicts")),
+ d_clique_lemmas(smtStatisticsRegistry().registerInt(
+ "CardinalityExtension::Clique_Lemmas")),
+ d_split_lemmas(smtStatisticsRegistry().registerInt(
+ "CardinalityExtension::Split_Lemmas")),
+ d_max_model_size(smtStatisticsRegistry().registerInt(
+ "CardinalityExtension::Max_Model_Size"))
{
- smtStatisticsRegistry()->registerStat(&d_clique_conflicts);
- smtStatisticsRegistry()->registerStat(&d_clique_lemmas);
- smtStatisticsRegistry()->registerStat(&d_split_lemmas);
- smtStatisticsRegistry()->registerStat(&d_max_model_size);
-}
-
-CardinalityExtension::Statistics::~Statistics()
-{
- smtStatisticsRegistry()->unregisterStat(&d_clique_conflicts);
- smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas);
- smtStatisticsRegistry()->unregisterStat(&d_split_lemmas);
- smtStatisticsRegistry()->unregisterStat(&d_max_model_size);
+ d_max_model_size.maxAssign(1);
}
} // namespace uf
diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h
index 53c850897..70db9257f 100644
--- a/src/theory/uf/cardinality_extension.h
+++ b/src/theory/uf/cardinality_extension.h
@@ -22,7 +22,7 @@
#include "context/context.h"
#include "theory/decision_strategy.h"
#include "theory/theory.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
@@ -397,7 +397,6 @@ class CardinalityExtension
IntStat d_split_lemmas;
IntStat d_max_model_size;
Statistics();
- ~Statistics();
};
/** statistics class */
Statistics d_statistics;
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index fe7b0ab84..7124a8890 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -29,23 +29,14 @@ namespace cvc5 {
namespace theory {
namespace eq {
-EqualityEngine::Statistics::Statistics(std::string name)
- : d_mergesCount(name + "::mergesCount", 0),
- d_termsCount(name + "::termsCount", 0),
- d_functionTermsCount(name + "::functionTermsCount", 0),
- d_constantTermsCount(name + "::constantTermsCount", 0)
+EqualityEngine::Statistics::Statistics(const std::string& name)
+ : d_mergesCount(smtStatisticsRegistry().registerInt(name + "mergesCount")),
+ d_termsCount(smtStatisticsRegistry().registerInt(name + "termsCount")),
+ d_functionTermsCount(
+ smtStatisticsRegistry().registerInt(name + "functionTermsCount")),
+ d_constantTermsCount(
+ smtStatisticsRegistry().registerInt(name + "constantTermsCount"))
{
- smtStatisticsRegistry()->registerStat(&d_mergesCount);
- smtStatisticsRegistry()->registerStat(&d_termsCount);
- smtStatisticsRegistry()->registerStat(&d_functionTermsCount);
- smtStatisticsRegistry()->registerStat(&d_constantTermsCount);
-}
-
-EqualityEngine::Statistics::~Statistics() {
- smtStatisticsRegistry()->unregisterStat(&d_mergesCount);
- smtStatisticsRegistry()->unregisterStat(&d_termsCount);
- smtStatisticsRegistry()->unregisterStat(&d_functionTermsCount);
- smtStatisticsRegistry()->unregisterStat(&d_constantTermsCount);
}
/**
@@ -128,7 +119,7 @@ EqualityEngine::EqualityEngine(context::Context* context,
d_assertedEqualitiesCount(context, 0),
d_equalityTriggersCount(context, 0),
d_subtermEvaluatesSize(context, 0),
- d_stats(name),
+ d_stats(name + "::"),
d_inPropagate(false),
d_constantsAreTriggers(constantsAreTriggers),
d_anyTermsAreTriggers(anyTermTriggers),
@@ -158,7 +149,7 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify,
d_assertedEqualitiesCount(context, 0),
d_equalityTriggersCount(context, 0),
d_subtermEvaluatesSize(context, 0),
- d_stats(name),
+ d_stats(name + "::"),
d_inPropagate(false),
d_constantsAreTriggers(constantsAreTriggers),
d_anyTermsAreTriggers(anyTermTriggers),
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index d8a8f3916..8676e446e 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -34,7 +34,7 @@
#include "theory/uf/equality_engine_iterator.h"
#include "theory/uf/equality_engine_notify.h"
#include "theory/uf/equality_engine_types.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
@@ -109,9 +109,7 @@ class EqualityEngine : public context::ContextNotifyObj {
/** Number of constant terms managed by the system */
IntStat d_constantTermsCount;
- Statistics(std::string name);
-
- ~Statistics();
+ Statistics(const std::string& name);
};/* struct EqualityEngine::statistics */
private:
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index 49b056f5a..65ed4d542 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -164,21 +164,20 @@ void SymmetryBreaker::Template::reset() {
d_reps.clear();
}
-SymmetryBreaker::SymmetryBreaker(context::Context* context,
- std::string name) :
- ContextNotifyObj(context),
- d_assertionsToRerun(context),
- d_rerunningAssertions(false),
- d_phi(),
- d_phiSet(),
- d_permutations(),
- d_terms(),
- d_template(),
- d_normalizationCache(),
- d_termEqs(),
- d_termEqsOnly(),
- d_name(name),
- d_stats(d_name)
+SymmetryBreaker::SymmetryBreaker(context::Context* context, std::string name)
+ : ContextNotifyObj(context),
+ d_assertionsToRerun(context),
+ d_rerunningAssertions(false),
+ d_phi(),
+ d_phiSet(),
+ d_permutations(),
+ d_terms(),
+ d_template(),
+ d_normalizationCache(),
+ d_termEqs(),
+ d_termEqsOnly(),
+ d_name(name),
+ d_stats(d_name + "theory::uf::symmetry_breaker::")
{
}
@@ -750,33 +749,20 @@ void SymmetryBreaker::selectTerms(const Permutation& p) {
}
}
-SymmetryBreaker::Statistics::Statistics(std::string name)
- : d_clauses(name + "theory::uf::symmetry_breaker::clauses", 0)
- , d_units(name + "theory::uf::symmetry_breaker::units", 0)
- , d_permutationSetsConsidered(name + "theory::uf::symmetry_breaker::permutationSetsConsidered", 0)
- , d_permutationSetsInvariant(name + "theory::uf::symmetry_breaker::permutationSetsInvariant", 0)
- , d_invariantByPermutationsTimer(name + "theory::uf::symmetry_breaker::timers::invariantByPermutations")
- , d_selectTermsTimer(name + "theory::uf::symmetry_breaker::timers::selectTerms")
- , d_initNormalizationTimer(name + "theory::uf::symmetry_breaker::timers::initNormalization")
-{
- smtStatisticsRegistry()->registerStat(&d_clauses);
- smtStatisticsRegistry()->registerStat(&d_units);
- smtStatisticsRegistry()->registerStat(&d_permutationSetsConsidered);
- smtStatisticsRegistry()->registerStat(&d_permutationSetsInvariant);
- smtStatisticsRegistry()->registerStat(&d_invariantByPermutationsTimer);
- smtStatisticsRegistry()->registerStat(&d_selectTermsTimer);
- smtStatisticsRegistry()->registerStat(&d_initNormalizationTimer);
-}
-
-SymmetryBreaker::Statistics::~Statistics()
+SymmetryBreaker::Statistics::Statistics(const std::string& name)
+ : d_clauses(smtStatisticsRegistry().registerInt(name + "clauses")),
+ d_units(smtStatisticsRegistry().registerInt(name + "units")),
+ d_permutationSetsConsidered(smtStatisticsRegistry().registerInt(
+ name + "permutationSetsConsidered")),
+ d_permutationSetsInvariant(smtStatisticsRegistry().registerInt(
+ name + "permutationSetsInvariant")),
+ d_invariantByPermutationsTimer(smtStatisticsRegistry().registerTimer(
+ name + "timers::invariantByPermutations")),
+ d_selectTermsTimer(
+ smtStatisticsRegistry().registerTimer(name + "timers::selectTerms")),
+ d_initNormalizationTimer(smtStatisticsRegistry().registerTimer(
+ name + "timers::initNormalization"))
{
- smtStatisticsRegistry()->unregisterStat(&d_clauses);
- smtStatisticsRegistry()->unregisterStat(&d_units);
- smtStatisticsRegistry()->unregisterStat(&d_permutationSetsConsidered);
- smtStatisticsRegistry()->unregisterStat(&d_permutationSetsInvariant);
- smtStatisticsRegistry()->unregisterStat(&d_invariantByPermutationsTimer);
- smtStatisticsRegistry()->unregisterStat(&d_selectTermsTimer);
- smtStatisticsRegistry()->unregisterStat(&d_initNormalizationTimer);
}
SymmetryBreaker::Terms::iterator
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index eb78f9101..b5d0fbdf9 100644
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -52,8 +52,7 @@
#include "expr/node.h"
#include "expr/node_builder.h"
#include "smt/smt_statistics_registry.h"
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
@@ -147,8 +146,7 @@ private:
/** time spent in initial round of normalization */
TimerStat d_initNormalizationTimer;
- Statistics(std::string name);
- ~Statistics();
+ Statistics(const std::string& name);
};
Statistics d_stats;
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 9fa86f402..5d91faa87 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -53,7 +53,7 @@ TheoryUF::TheoryUF(context::Context* c,
d_functionsTerms(c),
d_symb(u, instanceName),
d_state(c, u, valuation),
- d_im(*this, d_state, pnm, "theory::uf", false),
+ d_im(*this, d_state, pnm, "theory::uf::" + instanceName, false),
d_notify(d_im, *this)
{
d_true = NodeManager::currentNM()->mkConst( true );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback