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

3 files changed, 8 insertions, 12 deletions

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 37ee01370..7319ba73e 100644
--- 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 6808f2a6e..e30fda8f9 100644
--- 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 f90c6ebd0..64706264a 100644
--- 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,13 +110,17 @@ 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.