diff options
Diffstat (limited to 'src/theory/uf/symmetry_breaker.cpp')
-rw-r--r-- | src/theory/uf/symmetry_breaker.cpp | 51 |
1 files changed, 42 insertions, 9 deletions
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index d5e18ed14..4f7a2667c 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -167,7 +167,8 @@ void SymmetryBreaker::Template::reset() { d_reps.clear(); } -SymmetryBreaker::SymmetryBreaker(context::Context* context) : +SymmetryBreaker::SymmetryBreaker(context::Context* context, + std::string name) : ContextNotifyObj(context), d_assertionsToRerun(context), d_rerunningAssertions(false), @@ -178,7 +179,10 @@ SymmetryBreaker::SymmetryBreaker(context::Context* context) : d_template(), d_normalizationCache(), d_termEqs(), - d_termEqsOnly() { + d_termEqsOnly(), + d_name(name), + d_stats(d_name) +{ } class SBGuard { @@ -461,7 +465,7 @@ void SymmetryBreaker::apply(std::vector<Node>& newClauses) { Debug("ufsymm") << "UFSYMM =====================================================" << endl << "UFSYMM have " << d_permutations.size() << " permutation sets" << endl; if(!d_permutations.empty()) { - { TimerStat::CodeTimer codeTimer(d_initNormalizationTimer); + { TimerStat::CodeTimer codeTimer(d_stats.d_initNormalizationTimer); // normalize d_phi for(vector<Node>::iterator i = d_phi.begin(); i != d_phi.end(); ++i) { @@ -476,12 +480,12 @@ void SymmetryBreaker::apply(std::vector<Node>& newClauses) { for(Permutations::iterator i = d_permutations.begin(); i != d_permutations.end(); ++i) { - ++d_permutationSetsConsidered; + ++(d_stats.d_permutationSetsConsidered); const Permutation& p = *i; Debug("ufsymm") << "UFSYMM looking at permutation: " << p << endl; size_t n = p.size() - 1; if(invariantByPermutations(p)) { - ++d_permutationSetsInvariant; + ++(d_stats.d_permutationSetsInvariant); selectTerms(p); set<Node> cts; while(!d_terms.empty() && cts.size() <= n) { @@ -539,11 +543,11 @@ void SymmetryBreaker::apply(std::vector<Node>& newClauses) { Node d; if(disj.getNumChildren() > 1) { d = disj; - ++d_clauses; + ++(d_stats.d_clauses); } else { d = disj[0]; disj.clear(); - ++d_units; + ++(d_stats.d_units); } if(Debug.isOn("ufsymm")) { Debug("ufsymm") << "UFSYMM symmetry-breaking clause: " << d << endl; @@ -569,7 +573,7 @@ void SymmetryBreaker::guessPermutations() { } bool SymmetryBreaker::invariantByPermutations(const Permutation& p) { - TimerStat::CodeTimer codeTimer(d_invariantByPermutationsTimer); + TimerStat::CodeTimer codeTimer(d_stats.d_invariantByPermutationsTimer); // use d_phi Debug("ufsymm") << "UFSYMM invariantByPermutations()? " << p << endl; @@ -681,7 +685,7 @@ static bool isSubset(const T1& s, const T2& t) { } void SymmetryBreaker::selectTerms(const Permutation& p) { - TimerStat::CodeTimer codeTimer(d_selectTermsTimer); + TimerStat::CodeTimer codeTimer(d_stats.d_selectTermsTimer); // use d_phi, put into d_terms Debug("ufsymm") << "UFSYMM selectTerms(): " << p << endl; @@ -733,6 +737,35 @@ 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() +{ + 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 SymmetryBreaker::selectMostPromisingTerm(Terms& terms) { // use d_phi |