From bcbddbc8264c095da435c51b9bff3306b565aee7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 7 Feb 2020 10:41:09 -0600 Subject: [PATCH] Statistics for fast enumerator (#3699) --- .../quantifiers/sygus/sygus_enumerator.cpp | 18 +++++++++++------- .../quantifiers/sygus/sygus_enumerator.h | 13 +++++++++---- src/theory/quantifiers/sygus/sygus_stats.cpp | 12 +++++++++++- src/theory/quantifiers/sygus/sygus_stats.h | 6 ++++++ .../quantifiers/sygus/synth_conjecture.cpp | 2 +- 5 files changed, 38 insertions(+), 13 deletions(-) diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index ea539cc16..99f8eee2c 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -24,8 +24,10 @@ namespace CVC4 { namespace theory { namespace quantifiers { -SygusEnumerator::SygusEnumerator(TermDbSygus* tds, SynthConjecture* p) - : d_tds(tds), d_parent(p), d_tlEnum(nullptr), d_abortSize(-1) +SygusEnumerator::SygusEnumerator(TermDbSygus* tds, + SynthConjecture* p, + SygusStatistics& s) + : d_tds(tds), d_parent(p), d_stats(s), d_tlEnum(nullptr), d_abortSize(-1) { } @@ -149,12 +151,11 @@ SygusEnumerator::TermCache::TermCache() d_sampleRrVInit(false) { } -void SygusEnumerator::TermCache::initialize(Node e, - TypeNode tn, - TermDbSygus* tds, - SygusPbe* pbe) +void SygusEnumerator::TermCache::initialize( + SygusStatistics* s, Node e, TypeNode tn, TermDbSygus* tds, SygusPbe* pbe) { Trace("sygus-enum-debug") << "Init term cache " << tn << "..." << std::endl; + d_stats = s; d_enum = e; d_tn = tn; d_tds = tds; @@ -312,6 +313,7 @@ bool SygusEnumerator::TermCache::addTerm(Node n) { Node bn = d_tds->sygusToBuiltin(n); Node bnr = d_tds->getExtRewriter()->extendedRewrite(bn); + ++(d_stats->d_enumTermsRewrite); if (options::sygusRewVerify()) { if (bn != bnr) @@ -334,6 +336,7 @@ bool SygusEnumerator::TermCache::addTerm(Node n) // if we are doing PBE symmetry breaking if (d_pbe != nullptr) { + ++(d_stats->d_enumTermsExampleEval); // Is it equivalent under examples? Node bne = d_pbe->addSearchVal(d_tn, d_enum, bnr); if (!bne.isNull()) @@ -350,6 +353,7 @@ bool SygusEnumerator::TermCache::addTerm(Node n) Trace("sygus-enum-terms") << "tc(" << d_tn << "): term " << bn << std::endl; d_bterms.insert(bnr); } + ++(d_stats->d_enumTerms); d_terms.push_back(n); return true; } @@ -539,7 +543,7 @@ void SygusEnumerator::initializeTermCache(TypeNode tn) pbe = nullptr; } } - d_tcache[tn].initialize(d_enum, tn, d_tds, pbe); + d_tcache[tn].initialize(&d_stats, d_enum, tn, d_tds, pbe); } SygusEnumerator::TermEnum* SygusEnumerator::getMasterEnumForType(TypeNode tn) diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h index 3f4490b15..7e5add299 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator.h @@ -44,7 +44,7 @@ class SygusPbe; class SygusEnumerator : public EnumValGenerator { public: - SygusEnumerator(TermDbSygus* tds, SynthConjecture* p); + SygusEnumerator(TermDbSygus* tds, SynthConjecture* p, SygusStatistics& s); ~SygusEnumerator() {} /** initialize this class with enumerator e */ void initialize(Node e) override; @@ -60,6 +60,8 @@ class SygusEnumerator : public EnumValGenerator TermDbSygus* d_tds; /** pointer to the synth conjecture that owns this enumerator */ SynthConjecture* d_parent; + /** reference to the statistics of parent */ + SygusStatistics& d_stats; /** Term cache * * This stores a list of terms for a given sygus type. The key features of @@ -68,8 +70,8 @@ class SygusEnumerator : public EnumValGenerator * natural number n, and redundancy criteria are used for discarding terms * that are not relevant. This includes discarding terms whose builtin version * is the same up to T-rewriting with another, or is equivalent under - * examples, if the conjecture in question is in PBE form and sygusSymBreakPbe - * is enabled. + * examples, if the conjecture in question is in examples form and + * sygusSymBreakPbe is enabled. * * This class also computes static information about sygus types that is * relevant for enumeration. Primarily, this includes mapping constructors @@ -97,7 +99,8 @@ class SygusEnumerator : public EnumValGenerator public: TermCache(); /** initialize this cache */ - void initialize(Node e, + void initialize(SygusStatistics* s, + Node e, TypeNode tn, TermDbSygus* tds, SygusPbe* pbe = nullptr); @@ -141,6 +144,8 @@ class SygusEnumerator : public EnumValGenerator void setComplete(); private: + /** reference to the statistics of parent */ + SygusStatistics* d_stats; /** the enumerator this cache is for */ Node d_enum; /** the sygus type of terms in this cache */ 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 diff --git a/src/theory/quantifiers/sygus/sygus_stats.h b/src/theory/quantifiers/sygus/sygus_stats.h index c4c7ba060..80499f7a4 100644 --- a/src/theory/quantifiers/sygus/sygus_stats.h +++ b/src/theory/quantifiers/sygus/sygus_stats.h @@ -43,6 +43,12 @@ class SygusStatistics IntStat d_filtered_solutions; /** Number of candidate rewrites printed (for --sygus-rr) */ IntStat d_candidate_rewrites_print; + /** Number of terms checked for rewrite-based symmetry in fast enumerators */ + IntStat d_enumTermsRewrite; + /** Number of terms checked for example-based symmetry in fast enumerators */ + IntStat d_enumTermsExampleEval; + /** Number of non-redundant terms generated by fast enumerators */ + IntStat d_enumTerms; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 73fc53d86..b7c3851af 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -813,7 +813,7 @@ Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete) == options::SygusActiveGenMode::ENUM || options::sygusActiveGenMode() == options::SygusActiveGenMode::AUTO); - d_evg[e].reset(new SygusEnumerator(d_tds, this)); + d_evg[e].reset(new SygusEnumerator(d_tds, this, d_stats)); } } Trace("sygus-active-gen") -- 2.30.2