4 files changed, 32 insertions, 8 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index bd85ea496..736fdebee 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -25,8 +25,13 @@ namespace theory {
 namespace quantifiers {
 
 SygusEnumerator::SygusEnumerator(TermDbSygus* tds, SynthConjecture* p)
-    : d_tds(tds), d_parent(p), d_tlEnum(nullptr), d_abortSize(-1)
+    : d_tds(tds),
+      d_parent(p),
+      d_tlEnum(nullptr),
+      d_abortSize(-1),
+      d_rewriteChecks("sygus-rr-verify-rewrite-checks", 0)
 {
+  smtStatisticsRegistry()->registerStat(&d_rewriteChecks);
 }
 
 void SygusEnumerator::initialize(Node e)
@@ -152,7 +157,8 @@ SygusEnumerator::TermCache::TermCache()
 void SygusEnumerator::TermCache::initialize(Node e,
                                             TypeNode tn,
                                             TermDbSygus* tds,
-                                            SygusPbe* pbe)
+                                            SygusPbe* pbe,
+                                            IntStat* rewriteChecks)
 {
   Trace("sygus-enum-debug") << "Init term cache " << tn << "..." << std::endl;
   d_enum = e;
@@ -161,6 +167,7 @@ void SygusEnumerator::TermCache::initialize(Node e,
   d_pbe = pbe;
   d_sizeStartIndex[0] = 0;
   d_isSygusType = false;
+  d_rewriteChecks = rewriteChecks;
 
   // compute static information about tn
   if (!d_tn.isDatatype())
@@ -320,7 +327,7 @@ bool SygusEnumerator::TermCache::addTerm(Node n)
         {
           d_sampleRrVInit = true;
           d_samplerRrV.initializeSygus(
-              d_tds, d_enum, options::sygusSamples(), false);
+              d_tds, d_enum, options::sygusSamples(), false, d_rewriteChecks);
         }
         d_samplerRrV.checkEquivalent(bn, bnr);
       }
@@ -539,7 +546,7 @@ void SygusEnumerator::initializeTermCache(TypeNode tn)
       pbe = nullptr;
     }
   }
-  d_tcache[tn].initialize(d_enum, tn, d_tds, pbe);
+  d_tcache[tn].initialize(d_enum, tn, d_tds, pbe, &d_rewriteChecks);
 }
 
 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 d4c466b03..0f5c581f4 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.h
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.h
@@ -45,7 +45,10 @@ class SygusEnumerator : public EnumValGenerator
 {
  public:
   SygusEnumerator(TermDbSygus* tds, SynthConjecture* p);
-  ~SygusEnumerator() {}
+  ~SygusEnumerator()
+  {
+    smtStatisticsRegistry()->unregisterStat(&d_rewriteChecks);
+  }
   /** initialize this class with enumerator e */
   void initialize(Node e) override;
   /** Inform this generator that abstract value v was enumerated. */
@@ -100,7 +103,8 @@ class SygusEnumerator : public EnumValGenerator
     void initialize(Node e,
                     TypeNode tn,
                     TermDbSygus* tds,
-                    SygusPbe* pbe = nullptr);
+                    SygusPbe* pbe = nullptr,
+                    IntStat* rewriteChecks = nullptr);
     /** get last constructor class index for weight
      *
      * This returns a minimal index n such that all constructor classes at
@@ -183,6 +187,8 @@ class SygusEnumerator : public EnumValGenerator
     quantifiers::SygusSampler d_samplerRrV;
     /** is the above sampler initialized? */
     bool d_sampleRrVInit;
+
+    IntStat* d_rewriteChecks;
   };
   /** above cache for each sygus type */
   std::map<TypeNode, TermCache> d_tcache;
@@ -448,6 +454,8 @@ class SygusEnumerator : public EnumValGenerator
    */
   std::unordered_set<Node, NodeHashFunction> d_sbExcTlCons;
   //-------------------------------- end externally specified symmetry breaking
+
+  IntStat d_rewriteChecks;
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 10d7ef6ab..752bb018b 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -85,12 +85,14 @@ void SygusSampler::initialize(TypeNode tn,
 void SygusSampler::initializeSygus(TermDbSygus* tds,
                                    Node f,
                                    unsigned nsamples,
-                                   bool useSygusType)
+                                   bool useSygusType,
+                                   IntStat* rewriteChecks)
 {
   d_tds = tds;
   d_use_sygus_type = useSygusType;
   d_is_valid = true;
   d_ftn = f.getType();
+  d_rewriteChecks = rewriteChecks;
   Assert(d_ftn.isDatatype());
   const Datatype& dt = static_cast<DatatypeType>(d_ftn.toType()).getDatatype();
   Assert(dt.isSygus());
@@ -774,6 +776,8 @@ void SygusSampler::checkEquivalent(Node bv, Node bvr)
   Trace("sygus-rr-verify") << "Testing rewrite rule " << bv << " ---> " << bvr
                            << std::endl;
 
+  (*d_rewriteChecks) += 1;
+
   // see if they evaluate to same thing on all sample points
   bool ptDisequal = false;
   unsigned pt_index = 0;
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index 429b6f511..a6b8b8079 100644
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -18,6 +18,7 @@
 #define CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
 
 #include <map>
+#include "smt/smt_statistics_registry.h"
 #include "theory/evaluator.h"
 #include "theory/quantifiers/lazy_trie.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
@@ -65,6 +66,7 @@ class SygusSampler : public LazyTrieEvaluator
 {
  public:
   SygusSampler();
+
   ~SygusSampler() override {}
 
   /** initialize
@@ -94,7 +96,8 @@ class SygusSampler : public LazyTrieEvaluator
   virtual void initializeSygus(TermDbSygus* tds,
                                Node f,
                                unsigned nsamples,
-                               bool useSygusType);
+                               bool useSygusType,
+                               IntStat* rewriteChecks = nullptr);
   /** register term n with this sampler database
    *
    * forceKeep is whether we wish to force that n is chosen as a representative
@@ -316,6 +319,8 @@ class SygusSampler : public LazyTrieEvaluator
   std::map<Node, std::vector<TypeNode> > d_const_sygus_types;
   /** register sygus type, initializes the above two data structures */
   void registerSygusType(TypeNode tn);
+
+  IntStat* d_rewriteChecks;
 };
 
 } /* CVC4::theory::quantifiers namespace */