diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-10 20:13:29 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-02-10 20:13:29 -0600 |
commit | 544cf41c1a5c1a3c8514c21d426ad66e578e67b0 (patch) | |
tree | 663bd3f617bf64df2ddb4314442c0d04fad985ed /src/theory/quantifiers/ce_guided_instantiation.cpp | |
parent | 2ff61502c2df1db8fbdba3b2487fb72aa1e6d509 (diff) |
More minor improvements to synth-rr (#1597)
Diffstat (limited to 'src/theory/quantifiers/ce_guided_instantiation.cpp')
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 38cfb9ba7..fbafb8b8c 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -357,20 +357,27 @@ void CegInstantiation::preregisterAssertion( Node n ) { } } -CegInstantiation::Statistics::Statistics(): - d_cegqi_lemmas_ce("CegInstantiation::cegqi_lemmas_ce", 0), - d_cegqi_lemmas_refine("CegInstantiation::cegqi_lemmas_refine", 0), - d_cegqi_si_lemmas("CegInstantiation::cegqi_lemmas_si", 0) +CegInstantiation::Statistics::Statistics() + : d_cegqi_lemmas_ce("CegInstantiation::cegqi_lemmas_ce", 0), + d_cegqi_lemmas_refine("CegInstantiation::cegqi_lemmas_refine", 0), + d_cegqi_si_lemmas("CegInstantiation::cegqi_lemmas_si", 0), + d_solutions("CegConjecture::solutions", 0), + d_candidate_rewrites("CegConjecture::candidate_rewrites", 0) + { smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_ce); smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_refine); smtStatisticsRegistry()->registerStat(&d_cegqi_si_lemmas); + smtStatisticsRegistry()->registerStat(&d_solutions); + smtStatisticsRegistry()->registerStat(&d_candidate_rewrites); } CegInstantiation::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_ce); smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_refine); smtStatisticsRegistry()->unregisterStat(&d_cegqi_si_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_solutions); + smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites); } }/* namespace CVC4::theory::quantifiers */ |