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 | |
| parent | f76e985c8948334f6e65679491be4f003157f460 (diff) | |
Minor fix and addition to sygus sampler (#1678)
| -rw-r--r-- | src/theory/quantifiers/sygus_sampler.cpp | 14 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus_sampler.h | 4 |
2 files changed, 17 insertions, 1 deletions
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; /** |