From d6c7967cfc7a9f8530f0de50f12f99bfc5f93da7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 27 Jun 2018 14:12:17 -0500 Subject: Synthesize candidate-rewrites from standard inputs (#1918) --- .../quantifiers/candidate_rewrite_database.h | 91 ++++++++++++++++++++-- 1 file changed, 85 insertions(+), 6 deletions(-) (limited to 'src/theory/quantifiers/candidate_rewrite_database.h') diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index 9ca946d26..a2a6c5745 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -18,6 +18,9 @@ #define __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H #include +#include +#include +#include #include "theory/quantifiers/sygus_sampler.h" namespace CVC4 { @@ -43,7 +46,32 @@ class CandidateRewriteDatabase ~CandidateRewriteDatabase() {} /** Initialize this class * - * qe : pointer to quantifiers engine, + * er : pointer to the extended rewriter (if any) we are using to compute + * candidate rewrites, + * 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 each variable is treated + * as unique. This affects whether or not a rewrite rule is considered + * redundant or not. For example the rewrite f(y)=y is redundant if + * f(x)=x has also been printed as a rewrite and x and y have the same type + * id (see SygusSampler for details). On the other hand, when a candidate + * rewrite database is initialized with sygus below, the type ids of the + * (sygus formal argument list) variables are always computed and used. + */ + void initialize(ExtendedRewriter* er, + TypeNode tn, + std::vector& vars, + unsigned nsamples, + bool unique_type_ids = false); + /** Initialize this class + * + * Serves the same purpose as the above function, but we will be using + * sygus to enumerate terms and generate samples. + * + * qe : pointer to quantifiers engine. We use the sygus term database of this + * quantifiers engine, and the extended rewriter of the corresponding term + * database when computing candidate rewrites, * f : a term of some SyGuS datatype type whose values we will be * testing under the free variables in the grammar of f. This is the * "candidate variable" CegConjecture::d_candidates, @@ -55,28 +83,44 @@ class CandidateRewriteDatabase * * These arguments are used to initialize the sygus sampler class. */ - void initialize(QuantifiersEngine* qe, - Node f, - unsigned nsamples, - bool useSygusType); + void initializeSygus(QuantifiersEngine* qe, + Node f, + unsigned nsamples, + bool useSygusType); /** add term * * Notifies this class that the solution sol was enumerated. This may * cause a candidate-rewrite to be printed on the output stream out. + * We return true if the term sol is distinct (up to equivalence) with + * all previous terms added to this class. The argument rew_print is set to + * true if this class printed a rewrite. */ + bool addTerm(Node sol, std::ostream& out, bool& rew_print); bool addTerm(Node sol, std::ostream& out); private: /** reference to quantifier engine */ QuantifiersEngine* d_qe; - /** the function-to-synthesize we are testing */ + /** pointer to the sygus term database of d_qe */ + TermDbSygus* d_tds; + /** pointer to the extended rewriter object we are using */ + ExtendedRewriter* d_ext_rewrite; + /** the (sygus or builtin) type of terms we are testing */ + TypeNode d_type; + /** the function-to-synthesize we are testing (if sygus) */ Node d_candidate; + /** whether we are using sygus */ + bool d_using_sygus; /** sygus sampler objects for each program variable * * This is used for the sygusRewSynth() option to synthesize new candidate * rewrite rules. */ SygusSamplerExt d_sampler; + /** a (dummy) user context, used for d_drewrite */ + context::UserContext d_fake_context; + /** dynamic rewriter class */ + std::unique_ptr d_drewrite; /** * Cache of skolems for each free variable that appears in a synthesis check * (for --sygus-rr-synth-check). @@ -84,6 +128,41 @@ class CandidateRewriteDatabase std::map d_fv_to_skolem; }; +/** + * This class generates and stores candidate rewrite databases for multiple + * types as needed. + */ +class CandidateRewriteDatabaseGen +{ + public: + /** constructor + * + * vars : the variables we are testing substitutions for, for all types, + * nsamples : number of sample points this class will test for all types. + */ + CandidateRewriteDatabaseGen(std::vector& vars, unsigned nsamples); + /** add term + * + * This registers term n with this class. We generate the candidate rewrite + * database of the appropriate type (if not allocated already), and register + * n with this database. This may result in "candidate-rewrite" being + * printed on the output stream out. + */ + bool addTerm(Node n, std::ostream& out); + + private: + /** reference to quantifier engine */ + QuantifiersEngine* d_qe; + /** the variables */ + std::vector d_vars; + /** the number of samples */ + unsigned d_nsamples; + /** candidate rewrite databases for each type */ + std::map d_cdbs; + /** an extended rewriter object */ + ExtendedRewriter d_ext_rewrite; +}; + } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ -- cgit v1.2.3