Statistics for fast enumerator (#3699)

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")