Minor improvements to the interface for sygus sampler (#2326)

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index aea449fd155fa73f09ed67371886a0c18e8bb374..7b01d6cb92629faa954d8538eb52962d2dc0cd11 100644 (file)
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -887,33 +887,30 @@ Node SygusSymBreakNew::registerSearchValue(
           std::ostream* out = nodeManagerOptions.getOut();
           (*out) << "(unsound-rewrite " << bv << " " << bvr << ")" << std::endl;
           // debugging information
-          if (Trace.isOn("sygus-rr-debug"))
+          int pt_index = its->second.getDiffSamplePointIndex(bv, bvr);
+          if (pt_index >= 0)
           {
-            int pt_index = its->second.getDiffSamplePointIndex(bv, bvr);
-            if (pt_index >= 0)
+            (*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++)
             {
-              Trace("sygus-rr-debug")
-                  << "; unsound: are not equivalent for : " << std::endl;
-              std::vector<Node> vars;
-              std::vector<Node> pt;
-              its->second.getSamplePoint(pt_index, vars, pt);
-              Assert(vars.size() == pt.size());
-              for (unsigned i = 0, size = pt.size(); i < size; i++)
-              {
-                Trace("sygus-rr-debug") << "; unsound:    " << vars[i] << " -> "
-                                        << pt[i] << std::endl;
-              }
-              Node bv_e = its->second.evaluate(bv, pt_index);
-              Node pbv_e = its->second.evaluate(bvr, pt_index);
-              Assert(bv_e != pbv_e);
-              Trace("sygus-rr-debug") << "; unsound: where they evaluate to "
-                                      << bv_e << " and " << pbv_e << std::endl;
-            }
-            else
-            {
-              // no witness point found?
-              Assert(false);
+              (*out) << "; unsound:    " << vars[i] << " -> " << pt[i]
+                     << std::endl;
             }
+            Node bv_e = its->second.evaluate(bv, pt_index);
+            Node pbv_e = its->second.evaluate(bvr, pt_index);
+            Assert(bv_e != pbv_e);
+            (*out) << "; unsound: where they evaluate to " << bv_e << " and "
+                   << pbv_e << std::endl;
+          }
+          else
+          {
+            // no witness point found?
+            Assert(false);
           }
           if (options::sygusRewVerifyAbort())
           {

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 37ee013703c61ec6d33da24a10fd968af60fea51..7319ba73e1da3a1b55043c798df5188534d15f51 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -526,9 +526,8 @@ bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates,
         Trace("cegis-sample-debug") << "...false for point #" << i << std::endl;
         // mark this as a CEGIS point (no longer sampled)
         d_cegis_sample_refine.insert(i);
-        std::vector<Node> vars;
         std::vector<Node> pt;
-        d_cegis_sampler.getSamplePoint(i, vars, pt);
+        d_cegis_sampler.getSamplePoint(i, pt);
         Assert(d_base_vars.size() == pt.size());
         Node rlem = d_base_body.substitute(
             d_base_vars.begin(), d_base_vars.end(), pt.begin(), pt.end());

diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 6808f2a6e13cf4e20821871ab7e436b58cf32fc7..e30fda8f9f4b998894ec7efe844de0f23d1710bc 100644 (file)
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -32,7 +32,7 @@ SygusSampler::SygusSampler()
 }
 
 void SygusSampler::initialize(TypeNode tn,
-                              std::vector<Node>& vars,
+                              const std::vector<Node>& vars,
                               unsigned nsamples,
                               bool unique_type_ids)
 {
@@ -433,11 +433,9 @@ void SygusSampler::getVariables(std::vector<Node>& vars) const
 }
 
 void SygusSampler::getSamplePoint(unsigned index,
-                                  std::vector<Node>& vars,
                                   std::vector<Node>& pt)
 {
   Assert(index < d_samples.size());
-  vars.insert(vars.end(), d_vars.begin(), d_vars.end());
   std::vector<Node>& spt = d_samples[index];
   pt.insert(pt.end(), spt.begin(), spt.end());
 }

diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index f90c6ebd0a534be5e48469853cf7ddc22374efac..64706264ad4953b9ba8ad4ab1bde543cd4550766 100644 (file)
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -77,7 +77,7 @@ class SygusSampler : public LazyTrieEvaluator
    * type that is used to determine when a rewrite rule is redundant.
    */
   virtual void initialize(TypeNode tn,
-                          std::vector<Node>& vars,
+                          const std::vector<Node>& vars,
                           unsigned nsamples,
                           bool unique_type_ids = false);
   /** initialize sygus
@@ -110,12 +110,16 @@ class SygusSampler : public LazyTrieEvaluator
    * Appends sample point #index to the vector pt, d_vars to vars.
    */
   void getSamplePoint(unsigned index,
-                      std::vector<Node>& vars,
                       std::vector<Node>& pt);
   /** Add pt to the set of sample points considered by this sampler */
   void addSamplePoint(std::vector<Node>& pt);
   /** evaluate n on sample point index */
   Node evaluate(Node n, unsigned index) override;
+  /**
+   * Compute the variables from the domain of d_var_index that occur in n,
+   * store these in the vector fvs.
+   */
+  void computeFreeVariables(Node n, std::vector<Node>& fvs);
   /**
    * Returns the index of a sample point such that the evaluation of a and b
    * diverge, or -1 if no such sample point exists.
@@ -220,11 +224,6 @@ class SygusSampler : public LazyTrieEvaluator
    * of an argument to function f.
    */
   bool d_is_valid;
-  /**
-   * Compute the variables from the domain of d_var_index that occur in n,
-   * store these in the vector fvs.
-   */
-  void computeFreeVariables(Node n, std::vector<Node>& fvs);
   /** initialize samples
    *
    * Adds nsamples sample points to d_samples.