diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus_sampler.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus_sampler.h | 13 |
3 files changed, 8 insertions, 12 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 37ee01370..7319ba73e 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -526,9 +526,8 @@ bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates, Trace("cegis-sample-debug") << "...false for point #" << i << std::endl; // mark this as a CEGIS point (no longer sampled) d_cegis_sample_refine.insert(i); - std::vector<Node> vars; std::vector<Node> pt; - d_cegis_sampler.getSamplePoint(i, vars, pt); + d_cegis_sampler.getSamplePoint(i, pt); Assert(d_base_vars.size() == pt.size()); Node rlem = d_base_body.substitute( d_base_vars.begin(), d_base_vars.end(), pt.begin(), pt.end()); diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index 6808f2a6e..e30fda8f9 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -32,7 +32,7 @@ SygusSampler::SygusSampler() } void SygusSampler::initialize(TypeNode tn, - std::vector<Node>& vars, + const std::vector<Node>& vars, unsigned nsamples, bool unique_type_ids) { @@ -433,11 +433,9 @@ void SygusSampler::getVariables(std::vector<Node>& vars) const } void SygusSampler::getSamplePoint(unsigned index, - std::vector<Node>& vars, std::vector<Node>& pt) { Assert(index < d_samples.size()); - vars.insert(vars.end(), d_vars.begin(), d_vars.end()); std::vector<Node>& spt = d_samples[index]; pt.insert(pt.end(), spt.begin(), spt.end()); } diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index f90c6ebd0..64706264a 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -77,7 +77,7 @@ class SygusSampler : public LazyTrieEvaluator * type that is used to determine when a rewrite rule is redundant. */ virtual void initialize(TypeNode tn, - std::vector<Node>& vars, + const std::vector<Node>& vars, unsigned nsamples, bool unique_type_ids = false); /** initialize sygus @@ -110,13 +110,17 @@ class SygusSampler : public LazyTrieEvaluator * Appends sample point #index to the vector pt, d_vars to vars. */ 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; /** + * Compute the variables from the domain of d_var_index that occur in n, + * store these in the vector fvs. + */ + void computeFreeVariables(Node n, std::vector<Node>& fvs); + /** * Returns the index of a sample point such that the evaluation of a and b * diverge, or -1 if no such sample point exists. */ @@ -220,11 +224,6 @@ class SygusSampler : public LazyTrieEvaluator * of an argument to function f. */ bool d_is_valid; - /** - * Compute the variables from the domain of d_var_index that occur in n, - * store these in the vector fvs. - */ - void computeFreeVariables(Node n, std::vector<Node>& fvs); /** initialize samples * * Adds nsamples sample points to d_samples. |