From 26977381d8e026718a056adee0fa6dea1a76555d Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 14 Mar 2019 07:46:52 -0500
Subject: Generalize sygus-rr-verify for fast enumerator (#2829)

---
 src/theory/quantifiers/sygus_sampler.cpp | 50 ++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)

(limited to 'src/theory/quantifiers/sygus_sampler.cpp')

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 */
-- 
cgit v1.2.3