Generalize sygus rr verify feature.

5 files changed, 81 insertions, 53 deletions

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index a8d9d93bc..d35c349bc 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..ff667a107 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 8834fe751..a2f05223a 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -769,6 +769,62 @@ 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 98f52992b..d2092d531 100644
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -165,7 +165,10 @@ class SygusSampler : public LazyTrieEvaluator
    */
   bool containsFreeVariables(Node a, Node b, bool strict = false);
   //--------------------------end queries about terms
-
+  /** check equivalent 
+   * 
+   */
+  void checkEquivalent( Node bv, Node bvr );
  protected:
   /** sygus term database of d_qe */
   TermDbSygus* d_tds;