diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-08 14:01:17 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-02-08 14:01:17 -0600 |
commit | 8a64433caffd3bedd99c0e73dac0941b87060778 (patch) | |
tree | 9c3f9502aaf8f750a3c75820e8dc6836239dabb3 /src/theory/quantifiers/sygus_sampler.h | |
parent | 9b3d7b040def03d1b5764ddfafc24ac24b40d0ef (diff) |
Minor improvements to sygus sampling. (#1577)
Diffstat (limited to 'src/theory/quantifiers/sygus_sampler.h')
-rw-r--r-- | src/theory/quantifiers/sygus_sampler.h | 78 |
1 files changed, 58 insertions, 20 deletions
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index 02b60d155..d8f2244c7 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -155,22 +155,40 @@ class SygusSampler : public LazyTrieEvaluator * forceKeep is whether we wish to force that n is chosen as a representative * value in the trie. */ - Node registerTerm(Node n, bool forceKeep = false); + virtual Node registerTerm(Node n, bool forceKeep = false); + /** get number of sample points */ + unsigned getNumSamplePoints() const { return d_samples.size(); } + /** get sample point + * + * Appends sample point #index to the vector pt, d_vars to vars. + */ + void getSamplePoint(unsigned index, + std::vector<Node>& vars, + std::vector<Node>& pt); + /** evaluate n on sample point index */ + Node evaluate(Node n, unsigned index); + /** + * Returns the index of a sample point such that the evaluation of a and b + * diverge, or -1 if no such sample point exists. + */ + int getDiffSamplePointIndex(Node a, Node b); + + protected: /** is contiguous * * This returns whether n's free variables (terms occurring in the range of * d_type_vars) are a prefix of the list of variables in d_type_vars for each - * type. For instance, if d_type_vars[Int] = { x, y }, then 0, x, x+y, y+x are - * contiguous but y is not. This is useful for excluding terms from - * consideration that are alpha-equivalent to others. + * type id. For instance, if d_type_vars[id] = { x, y } for some id, then + * 0, x, x+y, y+x are contiguous but y is not. This is useful for excluding + * terms from consideration that are alpha-equivalent to others. */ bool isContiguous(Node n); /** is ordered * * This returns whether n's free variables are in order with respect to * variables in d_type_vars for each type. For instance, if - * d_type_vars[Int] = { x, y }, then 0, x, x+y are ordered but y and y+x - * are not. + * d_type_vars[id] = { x, y } for some id, then 0, x, x+y are ordered but + * y and y+x are not. */ bool isOrdered(Node n); /** contains free variables @@ -179,16 +197,6 @@ class SygusSampler : public LazyTrieEvaluator * are those that occur in the range d_type_vars. */ bool containsFreeVariables(Node a, Node b); - /** get number of sample points */ - unsigned getNumSamplePoints() const { return d_samples.size(); } - /** get sample point - * - * Appends sample point #index to the vector pt. - */ - void getSamplePoint(unsigned index, std::vector<Node>& pt); - /** evaluate n on sample point index */ - Node evaluate(Node n, unsigned index); - private: /** sygus term database of d_qe */ TermDbSygus* d_tds; @@ -211,20 +219,33 @@ class SygusSampler : public LazyTrieEvaluator TypeNode d_tn; /** the sygus type for this sampler (if applicable). */ TypeNode d_ftn; - /** all variables */ + /** all variables we are sampling values for */ std::vector<Node> d_vars; /** type variables * - * For each type, a list of variables in the grammar we are considering, for - * that type. These typically correspond to the arguments of the + * We group variables according to "type ids". Two variables have the same + * type id if they have indistinguishable status according to this sampler. + * This is a finer-grained grouping than types. For example, two variables + * of the same type may have different type ids if they occur as constructors + * of a different set of sygus types in the grammar we are considering. + * For instance, we assign x and y different type ids in this grammar: + * A -> B + C + * B -> x | 0 | 1 + * C -> y + * Type ids are computed for each variable in d_vars during initialize(...). + * + * For each type id, a list of variables in the grammar we are considering, + * for that type. These typically correspond to the arguments of the * function-to-synthesize whose grammar we are considering. */ - std::map<TypeNode, std::vector<Node> > d_type_vars; + std::map<unsigned, std::vector<Node> > d_type_vars; /** * A map all variables in the grammar we are considering to their index in * d_type_vars. */ std::map<Node, unsigned> d_var_index; + /** Map from variables to the id (the domain of d_type_vars). */ + std::map<Node, unsigned> d_type_ids; /** constants * * For each type, a list of constants in the grammar we are considering, for @@ -300,6 +321,23 @@ class SygusSampler : public LazyTrieEvaluator void registerSygusType(TypeNode tn); }; +/** Version of the above class with some additional features */ +class SygusSamplerExt : public SygusSampler +{ + public: + /** register term n with this sampler database + * + * This returns a term ret with the same guarantees as + * SygusSampler::registerTerm, with the additional guarantee + * that for all ret' returned by a previous call to registerTerm( n' ), + * we have that ret = n is not alpha-equivalent to ret' = n, + * modulo symmetry of equality. For example, + * (t+0), t and (s+0), s + * will not be input/output pairs of this function. + */ + virtual Node registerTerm(Node n, bool forceKeep = false) override; +}; + } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ |