diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-03-02 11:59:42 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-03-02 11:59:42 -0600 |
| commit | 30398e8552bd372264d99743d39b826e1a2b53be (patch) | |
| tree | 7b28268ef8f04c5b89e579fb4862a59aae2f3c5b /src/theory/quantifiers/sygus_sampler.h | |
| parent | 5eafdb88526da64b60009e30bb45b7e0e47d360b (diff) | |
Print candidate rewrites in terms of original grammar (#1635)
Diffstat (limited to 'src/theory/quantifiers/sygus_sampler.h')
| -rw-r--r-- | src/theory/quantifiers/sygus_sampler.h | 22 |
1 files changed, 18 insertions, 4 deletions
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index abc9232af..5fcfc1c93 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -148,11 +148,18 @@ class SygusSampler : public LazyTrieEvaluator /** initialize sygus * * tds : pointer to sygus database, - * f : a term of some SyGuS datatype type whose (builtin) values we will be + * f : a term of some SyGuS datatype type whose values we will be * testing under the free variables in the grammar of f, - * nsamples : number of sample points this class will test. + * nsamples : number of sample points this class will test, + * useSygusType : whether we will register terms with this sampler that have + * the same type as f. If this flag is false, then we will be registering + * terms of the analog of the type of f, that is, the builtin type that + * f's type encodes in the deep embedding. */ - void initializeSygus(TermDbSygus* tds, Node f, unsigned nsamples); + void initializeSygus(TermDbSygus* tds, + Node f, + unsigned nsamples, + bool useSygusType); /** register term n with this sampler database * * forceKeep is whether we wish to force that n is chosen as a representative @@ -222,6 +229,10 @@ class SygusSampler : public LazyTrieEvaluator TypeNode d_tn; /** the sygus type for this sampler (if applicable). */ TypeNode d_ftn; + /** whether we are registering terms of type d_ftn */ + bool d_use_sygus_type; + /** map from builtin terms to the sygus term they correspond to */ + std::map<Node, Node> d_builtin_to_sygus; /** all variables we are sampling values for */ std::vector<Node> d_vars; /** type variables @@ -329,7 +340,10 @@ class SygusSamplerExt : public SygusSampler { public: /** initialize extended */ - void initializeSygusExt(QuantifiersEngine* qe, Node f, unsigned nsamples); + void initializeSygusExt(QuantifiersEngine* qe, + Node f, + unsigned nsamples, + bool useSygusType); /** register term n with this sampler database * * This returns either null, or a term ret with the same guarantees as |