From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 20 Mar 2018 17:13:13 +0000 (-0500)
Subject: Minor fix and addition to sygus sampler (#1678)
X-Git-Tag: cvc5-1.0.0~5232
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=425369ce6f2e355961954c399dfabe917320da52;p=cvc5.git

Minor fix and addition to sygus sampler (#1678)
---

diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 65883502f..afbdc42e1 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -296,7 +296,8 @@ Node SygusSampler::registerTerm(Node n, bool forceKeep)
     {
       Assert(!d_ftn.isNull());
       bn = d_tds->sygusToBuiltin(n);
-      bn = Rewriter::rewrite(bn);
+      Assert(d_builtin_to_sygus.find(bn) == d_builtin_to_sygus.end()
+             || d_builtin_to_sygus[bn] == n);
       d_builtin_to_sygus[bn] = n;
     }
     Assert(bn.getType() == d_tn);
@@ -439,6 +440,11 @@ bool SygusSampler::containsFreeVariables(Node a, Node b)
   return true;
 }
 
+void SygusSampler::getVariables(std::vector<Node>& vars) const
+{
+  vars.insert(vars.end(), d_vars.begin(), d_vars.end());
+}
+
 void SygusSampler::getSamplePoint(unsigned index,
                                   std::vector<Node>& vars,
                                   std::vector<Node>& pt)
@@ -449,6 +455,12 @@ void SygusSampler::getSamplePoint(unsigned index,
   pt.insert(pt.end(), spt.begin(), spt.end());
 }
 
+void SygusSampler::addSamplePoint(std::vector<Node>& pt)
+{
+  Assert(pt.size() == d_vars.size());
+  d_samples.push_back(pt);
+}
+
 Node SygusSampler::evaluate(Node n, unsigned index)
 {
   Assert(index < d_samples.size());
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index eba1a87b1..4bc10075d 100644
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -168,6 +168,8 @@ class SygusSampler : public LazyTrieEvaluator
   virtual Node registerTerm(Node n, bool forceKeep = false);
   /** get number of sample points */
   unsigned getNumSamplePoints() const { return d_samples.size(); }
+  /** get variables, adds d_vars to vars */
+  void getVariables(std::vector<Node>& vars) const;
   /** get sample point
    *
    * Appends sample point #index to the vector pt, d_vars to vars.
@@ -175,6 +177,8 @@ class SygusSampler : public LazyTrieEvaluator
   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;
   /**