diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-06-27 14:12:17 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-06-27 14:12:17 -0500 |
commit | d6c7967cfc7a9f8530f0de50f12f99bfc5f93da7 (patch) | |
tree | 2741c23c2cc42c065dc2aa573e0983e8f10823c1 /src/theory/quantifiers/sygus_sampler.h | |
parent | a236ade3242599d4916fd9ee676c2c68c7c004b1 (diff) |
Synthesize candidate-rewrites from standard inputs (#1918)
Diffstat (limited to 'src/theory/quantifiers/sygus_sampler.h')
-rw-r--r-- | src/theory/quantifiers/sygus_sampler.h | 50 |
1 files changed, 33 insertions, 17 deletions
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index fcd35613b..d323b36bd 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -21,6 +21,7 @@ #include "theory/quantifiers/dynamic_rewrite.h" #include "theory/quantifiers/lazy_trie.h" #include "theory/quantifiers/sygus/term_database_sygus.h" +#include "theory/quantifiers/term_enumeration.h" namespace CVC4 { namespace theory { @@ -69,14 +70,20 @@ class SygusSampler : public LazyTrieEvaluator /** initialize * - * tn : the return type of terms we will be testing with this class - * vars : the variables we are testing substitutions for - * nsamples : number of sample points this class will test. + * tn : the return type of terms we will be testing with this class, + * vars : the variables we are testing substitutions for, + * nsamples : number of sample points this class will test, + * unique_type_ids : if this is set to true, then we consider each variable + * in vars to have a unique "type id". A type id is a finer-grained notion of + * type that is used to determine when a rewrite rule is redundant. */ - void initialize(TypeNode tn, std::vector<Node>& vars, unsigned nsamples); + virtual void initialize(TypeNode tn, + std::vector<Node>& vars, + unsigned nsamples, + bool unique_type_ids = false); /** initialize sygus * - * tds : pointer to sygus database, + * qe : pointer to quantifiers engine, * 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, @@ -85,10 +92,10 @@ class SygusSampler : public LazyTrieEvaluator * 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, - bool useSygusType); + virtual 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 @@ -145,6 +152,8 @@ class SygusSampler : public LazyTrieEvaluator protected: /** sygus term database of d_qe */ TermDbSygus* d_tds; + /** term enumerator object (used for random sampling) */ + TermEnumeration d_tenum; /** samples */ std::vector<std::vector<Node> > d_samples; /** data structure to check duplication of sample points */ @@ -330,11 +339,19 @@ class SygusSamplerExt : public SygusSampler { public: SygusSamplerExt(); - /** initialize extended */ - void initializeSygusExt(QuantifiersEngine* qe, - Node f, - unsigned nsamples, - bool useSygusType); + /** initialize */ + void initializeSygus(TermDbSygus* tds, + Node f, + unsigned nsamples, + bool useSygusType) override; + /** set dynamic rewriter + * + * This tells this class to use the dynamic rewriter object dr. This utility + * is used to query whether pairs of terms are already entailed to be + * equal based on previous rewrite rules. + */ + void setDynamicRewriter(DynamicRewriter* dr); + /** register term n with this sampler database * * For each call to registerTerm( t, ... ) that returns s, we say that @@ -366,7 +383,6 @@ class SygusSamplerExt : public SygusSampler * d_drewrite utility, or is an instance of a previous pair */ Node registerTerm(Node n, bool forceKeep = false) override; - /** register relevant pair * * This should be called after registerTerm( n ) returns eq_n. @@ -375,8 +391,8 @@ class SygusSamplerExt : public SygusSampler void registerRelevantPair(Node n, Node eq_n); private: - /** dynamic rewriter class */ - std::unique_ptr<DynamicRewriter> d_drewrite; + /** pointer to the dynamic rewriter class */ + DynamicRewriter* d_drewrite; //----------------------------match filtering /** |