Format

4 files changed, 21 insertions, 26 deletions

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index d35c349bc..cb2968bd5 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -1100,7 +1100,7 @@ Node SygusSymBreakNew::registerSearchValue(Node a,
             its = d_sampler[a].find(tn);
           }
           // check equivalent
-          its->second.checkEquivalent(bv,bvr);
+          its->second.checkEquivalent(bv, bvr);
         }
       }
 
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index ff667a107..9981b5141 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -314,15 +314,15 @@ bool SygusEnumerator::TermCache::addTerm(Node n)
     Node bnr = d_tds->getExtRewriter()->extendedRewrite(bn);
     if (options::sygusRewVerify())
     {
-      if( bn!=bnr )
+      if (bn != bnr)
       {
-        if( !d_sampleRrVInit )
+        if (!d_sampleRrVInit)
         {
           d_sampleRrVInit = true;
           d_samplerRrV.initializeSygus(
-                d_tds, d_enum, options::sygusSamples(), false);
+              d_tds, d_enum, options::sygusSamples(), false);
         }
-        d_samplerRrV.checkEquivalent(bn,bnr);
+        d_samplerRrV.checkEquivalent(bn, bnr);
       }
     }
     // must be unique up to rewriting
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index a2f05223a..f1908fc19 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -769,18 +769,16 @@ void SygusSampler::registerSygusType(TypeNode tn)
   }
 }
 
-void SygusSampler::checkEquivalent( Node bv, Node bvr )
+void SygusSampler::checkEquivalent(Node bv, Node bvr)
 {
-  Trace("sygus-rr-verify")
-      << "Testing rewrite rule " << bv << " ---> " << bvr << std::endl;
-              
+  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++)
+  for (unsigned i = 0, npoints = getNumSamplePoints(); i < npoints; i++)
   {
     bve = evaluate(bv, i);
     bvre = evaluate(bvr, i);
@@ -795,11 +793,9 @@ void SygusSampler::checkEquivalent( Node bv, Node bvr )
   if (ptDisequal)
   {
     // we have detected unsoundness in the rewriter
-    Options& nodeManagerOptions =
-        NodeManager::currentNM()->getOptions();
+    Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
     std::ostream* out = nodeManagerOptions.getOut();
-    (*out) << "(unsound-rewrite " << bv << " " << bvr << ")"
-            << std::endl;
+    (*out) << "(unsound-rewrite " << bv << " " << bvr << ")" << std::endl;
     // debugging information
     (*out) << "; unsound: are not equivalent for : " << std::endl;
     std::vector<Node> vars;
@@ -809,18 +805,16 @@ void SygusSampler::checkEquivalent( Node bv, Node bvr )
     Assert(vars.size() == pt.size());
     for (unsigned i = 0, size = pt.size(); i < size; i++)
     {
-      (*out) << "; unsound:    " << vars[i] << " -> " << pt[i]
-              << std::endl;
+      (*out) << "; unsound:    " << vars[i] << " -> " << pt[i] << std::endl;
     }
     Assert(bve != bvre);
-    (*out) << "; unsound: where they evaluate to " << bve << " and "
-            << bvre << std::endl;
+    (*out) << "; unsound: where they evaluate to " << bve << " and " << bvre
+           << std::endl;
 
     if (options::sygusRewVerifyAbort())
     {
-      AlwaysAssert(
-          false,
-          "--sygus-rr-verify detected unsoundness in the rewriter!");
+      AlwaysAssert(false,
+                   "--sygus-rr-verify detected unsoundness in the rewriter!");
     }
   }
 }
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index d864a9d2b..28f715b34 100644
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -165,12 +165,13 @@ class SygusSampler : public LazyTrieEvaluator
    */
   bool containsFreeVariables(Node a, Node b, bool strict = false);
   //--------------------------end queries about terms
-  /** check equivalent 
-   * 
+  /** 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 );
+  void checkEquivalent(Node bv, Node bvr);
+
  protected:
   /** sygus term database of d_qe */
   TermDbSygus* d_tds;