diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-03-20 12:13:13 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-03-20 12:13:13 -0500 |
| commit | 425369ce6f2e355961954c399dfabe917320da52 (patch) | |
| tree | 0fed1f9e299510fd88272a6b8be02bbf71921f31 /src/theory/quantifiers/sygus_sampler.h | |
| parent | f76e985c8948334f6e65679491be4f003157f460 (diff) | |
Minor fix and addition to sygus sampler (#1678)
Diffstat (limited to 'src/theory/quantifiers/sygus_sampler.h')
| -rw-r--r-- | src/theory/quantifiers/sygus_sampler.h | 4 |
1 files changed, 4 insertions, 0 deletions
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; /** |