Generalize sygus-rr-verify for fast enumerator (#2829)

5 files changed, 77 insertions, 52 deletions

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index a8d9d93bc..cb2968bd5 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -1090,8 +1090,6 @@ Node SygusSymBreakNew::registerSearchValue(Node a,
       {
         if (bv != bvr)
         {
-          Trace("sygus-rr-verify")
-              << "Testing rewrite rule " << bv << " ---> " << bvr << std::endl;
           // add to the sampler database object
           std::map<TypeNode, quantifiers::SygusSampler>::iterator its =
               d_sampler[a].find(tn);
@@ -1101,55 +1099,8 @@ Node SygusSymBreakNew::registerSearchValue(Node a,
                 d_tds, nv, options::sygusSamples(), false);
             its = d_sampler[a].find(tn);
           }
-          // see if they evaluate to same thing on all sample points
-          bool ptDisequal = false;
-          unsigned pt_index = 0;
-          Node bve, bvre;
-          for (unsigned i = 0, npoints = its->second.getNumSamplePoints();
-               i < npoints;
-               i++)
-          {
-            bve = its->second.evaluate(bv, i);
-            bvre = its->second.evaluate(bvr, i);
-            if (bve != bvre)
-            {
-              ptDisequal = true;
-              pt_index = i;
-              break;
-            }
-          }
-          // bv and bvr should be equivalent under examples
-          if (ptDisequal)
-          {
-            // we have detected unsoundness in the rewriter
-            Options& nodeManagerOptions =
-                NodeManager::currentNM()->getOptions();
-            std::ostream* out = nodeManagerOptions.getOut();
-            (*out) << "(unsound-rewrite " << bv << " " << bvr << ")"
-                   << std::endl;
-            // debugging information
-            (*out) << "; unsound: are not equivalent for : " << std::endl;
-            std::vector<Node> vars;
-            its->second.getVariables(vars);
-            std::vector<Node> pt;
-            its->second.getSamplePoint(pt_index, pt);
-            Assert(vars.size() == pt.size());
-            for (unsigned i = 0, size = pt.size(); i < size; i++)
-            {
-              (*out) << "; unsound:    " << vars[i] << " -> " << pt[i]
-                     << std::endl;
-            }
-            Assert(bve != bvre);
-            (*out) << "; unsound: where they evaluate to " << bve << " and "
-                   << bvre << std::endl;
-
-            if (options::sygusRewVerifyAbort())
-            {
-              AlwaysAssert(
-                  false,
-                  "--sygus-rr-verify detected unsoundness in the rewriter!");
-            }
-          }
+          // check equivalent
+          its->second.checkEquivalent(bv, bvr);
         }
       }
 
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index d4b4dd0bf..9981b5141 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -145,7 +145,8 @@ SygusEnumerator::TermCache::TermCache()
       d_isSygusType(false),
       d_numConClasses(0),
       d_sizeEnum(0),
-      d_isComplete(false)
+      d_isComplete(false),
+      d_sampleRrVInit(false)
 {
 }
 void SygusEnumerator::TermCache::initialize(Node e,
@@ -311,6 +312,19 @@ bool SygusEnumerator::TermCache::addTerm(Node n)
   {
     Node bn = d_tds->sygusToBuiltin(n);
     Node bnr = d_tds->getExtRewriter()->extendedRewrite(bn);
+    if (options::sygusRewVerify())
+    {
+      if (bn != bnr)
+      {
+        if (!d_sampleRrVInit)
+        {
+          d_sampleRrVInit = true;
+          d_samplerRrV.initializeSygus(
+              d_tds, d_enum, options::sygusSamples(), false);
+        }
+        d_samplerRrV.checkEquivalent(bn, bnr);
+      }
+    }
     // must be unique up to rewriting
     if (d_bterms.find(bnr) != d_bterms.end())
     {
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h
index af6bb03f0..716a047d2 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.h
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.h
@@ -179,6 +179,10 @@ class SygusEnumerator : public EnumValGenerator
     unsigned d_sizeEnum;
     /** whether this term cache is complete */
     bool d_isComplete;
+    /** sampler (for --sygus-rr-verify) */
+    quantifiers::SygusSampler d_samplerRrV;
+    /** is the above sampler initialized? */
+    bool d_sampleRrVInit;
   };
   /** above cache for each sygus type */
   std::map<TypeNode, TermCache> d_tcache;
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 27ca270cc..9727149be 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -769,6 +769,56 @@ void SygusSampler::registerSygusType(TypeNode tn)
   }
 }
 
+void SygusSampler::checkEquivalent(Node bv, Node bvr)
+{
+  Trace("sygus-rr-verify") << "Testing rewrite rule " << bv << " ---> " << bvr
+                           << std::endl;
+
+  // see if they evaluate to same thing on all sample points
+  bool ptDisequal = false;
+  unsigned pt_index = 0;
+  Node bve, bvre;
+  for (unsigned i = 0, npoints = getNumSamplePoints(); i < npoints; i++)
+  {
+    bve = evaluate(bv, i);
+    bvre = evaluate(bvr, i);
+    if (bve != bvre)
+    {
+      ptDisequal = true;
+      pt_index = i;
+      break;
+    }
+  }
+  // bv and bvr should be equivalent under examples
+  if (ptDisequal)
+  {
+    // we have detected unsoundness in the rewriter
+    Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
+    std::ostream* out = nodeManagerOptions.getOut();
+    (*out) << "(unsound-rewrite " << bv << " " << bvr << ")" << std::endl;
+    // debugging information
+    (*out) << "; unsound: are not equivalent for : " << std::endl;
+    std::vector<Node> vars;
+    getVariables(vars);
+    std::vector<Node> pt;
+    getSamplePoint(pt_index, pt);
+    Assert(vars.size() == pt.size());
+    for (unsigned i = 0, size = pt.size(); i < size; i++)
+    {
+      (*out) << "; unsound:    " << vars[i] << " -> " << pt[i] << std::endl;
+    }
+    Assert(bve != bvre);
+    (*out) << "; unsound: where they evaluate to " << bve << " and " << bvre
+           << std::endl;
+
+    if (options::sygusRewVerifyAbort())
+    {
+      AlwaysAssert(false,
+                   "--sygus-rr-verify detected unsoundness in the rewriter!");
+    }
+  }
+}
+
 } /* CVC4::theory::quantifiers namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index 526a9e4b1..288563a04 100644
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -165,6 +165,12 @@ class SygusSampler : public LazyTrieEvaluator
    */
   bool containsFreeVariables(Node a, Node b, bool strict = false);
   //--------------------------end queries about terms
+  /** check equivalent
+   *
+   * Check whether bv and bvr are equivalent on all sample points, print
+   * an error if not. Used with --sygus-rr-verify.
+   */
+  void checkEquivalent(Node bv, Node bvr);
 
  protected:
   /** sygus term database of d_qe */