diff options
Diffstat (limited to 'src/theory/quantifiers/sygus_sampler.h')
| -rw-r--r-- | src/theory/quantifiers/sygus_sampler.h | 29 |
1 files changed, 22 insertions, 7 deletions
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index abc9232af..eba1a87b1 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 @@ -169,7 +176,7 @@ class SygusSampler : public LazyTrieEvaluator std::vector<Node>& vars, std::vector<Node>& pt); /** evaluate n on sample point index */ - Node evaluate(Node n, unsigned index); + Node evaluate(Node n, unsigned index) override; /** * Returns the index of a sample point such that the evaluation of a and b * diverge, or -1 if no such sample point exists. @@ -200,7 +207,8 @@ class SygusSampler : public LazyTrieEvaluator * are those that occur in the range d_type_vars. */ bool containsFreeVariables(Node a, Node b); - private: + + protected: /** sygus term database of d_qe */ TermDbSygus* d_tds; /** samples */ @@ -222,6 +230,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 +341,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 @@ -352,7 +367,7 @@ class SygusSamplerExt : public SygusSampler * from the set of all previous input/output pairs based on the * d_drewrite utility. */ - virtual Node registerTerm(Node n, bool forceKeep = false) override; + Node registerTerm(Node n, bool forceKeep = false) override; private: /** dynamic rewriter class */ |