From 448ee080458373fbd3aabe97396101d98d68f0c0 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 14 Jan 2019 19:12:59 -0600
Subject: [PATCH]  Only check disequal terms with sygus-rr-verify (#2793)

---
 src/theory/datatypes/datatypes_sygus.cpp | 103 ++++++++++++-----------
 1 file changed, 55 insertions(+), 48 deletions(-)

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 526ca2d4a..a8d9d93bc 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -1088,60 +1088,67 @@ Node SygusSymBreakNew::registerSearchValue(Node a,
 
       if (options::sygusRewVerify())
       {
-        // add to the sampler database object
-        std::map<TypeNode, quantifiers::SygusSampler>::iterator its =
-            d_sampler[a].find(tn);
-        if (its == d_sampler[a].end())
+        if (bv != bvr)
         {
-          d_sampler[a][tn].initializeSygus(
-              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)
+          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);
+          if (its == d_sampler[a].end())
           {
-            ptDisequal = true;
-            pt_index = i;
-            break;
+            d_sampler[a][tn].initializeSygus(
+                d_tds, nv, options::sygusSamples(), false);
+            its = d_sampler[a].find(tn);
           }
-        }
-        // 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++)
+          // 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++)
           {
-            (*out) << "; unsound:    " << vars[i] << " -> " << pt[i]
-                   << std::endl;
+            bve = its->second.evaluate(bv, i);
+            bvre = its->second.evaluate(bvr, i);
+            if (bve != bvre)
+            {
+              ptDisequal = true;
+              pt_index = i;
+              break;
+            }
           }
-          Assert(bve != bvre);
-          (*out) << "; unsound: where they evaluate to " << bve << " and "
-                 << bvre << std::endl;
-
-          if (options::sygusRewVerifyAbort())
+          // bv and bvr should be equivalent under examples
+          if (ptDisequal)
           {
-            AlwaysAssert(
-                false,
-                "--sygus-rr-verify detected unsoundness in the rewriter!");
+            // 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!");
+            }
           }
         }
       }
-- 
2.30.2