diff options
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/cardinality_extension.cpp | 25 | ||||
-rw-r--r-- | src/theory/uf/cardinality_extension.h | 3 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 27 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.h | 6 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.cpp | 68 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.h | 6 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 2 |
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 ); |