From 425369ce6f2e355961954c399dfabe917320da52 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 20 Mar 2018 12:13:13 -0500 Subject: [PATCH] Minor fix and addition to sygus sampler (#1678) --- src/theory/quantifiers/sygus_sampler.cpp | 14 +++++++++++++- src/theory/quantifiers/sygus_sampler.h | 4 ++++ 2 files changed, 17 insertions(+), 1 deletion(-) 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& vars) const +{ + vars.insert(vars.end(), d_vars.begin(), d_vars.end()); +} + void SygusSampler::getSamplePoint(unsigned index, std::vector& vars, std::vector& pt) @@ -449,6 +455,12 @@ void SygusSampler::getSamplePoint(unsigned index, pt.insert(pt.end(), spt.begin(), spt.end()); } +void SygusSampler::addSamplePoint(std::vector& 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& 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& vars, std::vector& pt); + /** Add pt to the set of sample points considered by this sampler */ + void addSamplePoint(std::vector& pt); /** evaluate n on sample point index */ Node evaluate(Node n, unsigned index) override; /** -- 2.30.2