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 65883502fcccd3047f4b3dc0b8a77fc8ae66a81c..afbdc42e18cfa12973fa637b4878921077b6d17c 100644 (file)
--- 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 eba1a87b105c61a0e50383ed4e63d17a02f8c292..4bc10075dea0e8475f09b887f2fd1dbe67cf181f 100644 (file)
--- 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;
   /**