diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-07 10:41:09 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-07 10:41:09 -0600 |
| commit | bcbddbc8264c095da435c51b9bff3306b565aee7 (patch) | |
| tree | 25c45a5d58c0e430bc10f6e22e602fd92364e441 /src/theory/quantifiers/sygus/sygus_stats.cpp | |
| parent | 841ef93ea04d4e5434d62ecf18adb85e8255c4ed (diff) | |
Statistics for fast enumerator (#3699)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_stats.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_stats.cpp | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_stats.cpp b/src/theory/quantifiers/sygus/sygus_stats.cpp index bee2e1d56..e8e7c0357 100644 --- a/src/theory/quantifiers/sygus/sygus_stats.cpp +++ b/src/theory/quantifiers/sygus/sygus_stats.cpp @@ -27,7 +27,11 @@ SygusStatistics::SygusStatistics() d_cegqi_si_lemmas("SynthEngine::cegqi_lemmas_si", 0), d_solutions("SynthConjecture::solutions", 0), d_filtered_solutions("SynthConjecture::filtered_solutions", 0), - d_candidate_rewrites_print("SynthConjecture::candidate_rewrites_print", 0) + d_candidate_rewrites_print("SynthConjecture::candidate_rewrites_print", + 0), + d_enumTermsRewrite("SygusEnumerator::enumTermsRewrite", 0), + d_enumTermsExampleEval("SygusEnumerator::enumTermsEvalExamples", 0), + d_enumTerms("SygusEnumerator::enumTerms", 0) { smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_ce); @@ -36,6 +40,9 @@ SygusStatistics::SygusStatistics() smtStatisticsRegistry()->registerStat(&d_solutions); smtStatisticsRegistry()->registerStat(&d_filtered_solutions); smtStatisticsRegistry()->registerStat(&d_candidate_rewrites_print); + smtStatisticsRegistry()->registerStat(&d_enumTermsRewrite); + smtStatisticsRegistry()->registerStat(&d_enumTermsExampleEval); + smtStatisticsRegistry()->registerStat(&d_enumTerms); } SygusStatistics::~SygusStatistics() @@ -46,6 +53,9 @@ SygusStatistics::~SygusStatistics() smtStatisticsRegistry()->unregisterStat(&d_solutions); smtStatisticsRegistry()->unregisterStat(&d_filtered_solutions); smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites_print); + smtStatisticsRegistry()->unregisterStat(&d_enumTermsRewrite); + smtStatisticsRegistry()->unregisterStat(&d_enumTermsExampleEval); + smtStatisticsRegistry()->unregisterStat(&d_enumTerms); } } // namespace quantifiers |