diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-20 16:29:30 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-08-20 16:29:30 -0500 |
| commit | 34a4f78458773e9816d90c84fd2047b74a699527 (patch) | |
| tree | 90b08ad7885d72f176dc3a9aaa4c9fea71729fe8 /src/theory/quantifiers/sygus_sampler.h | |
| parent | 991af9a7a73adaa84712e93af72980ba977b1155 (diff) | |
Minor improvements to the interface for sygus sampler (#2326)
Diffstat (limited to 'src/theory/quantifiers/sygus_sampler.h')
| -rw-r--r-- | src/theory/quantifiers/sygus_sampler.h | 13 |
1 files changed, 6 insertions, 7 deletions
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. |