1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
|
/********************* */
/*! \file sygus_grammar_cons.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Haniel Barbosa
** This file is part of the CVC4 project.
** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief class for constructing inductive datatypes that correspond to
** grammars that encode syntactic restrictions for SyGuS.
**/
#include "cvc4_private.h"
#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
#define CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
#include "theory/quantifiers_engine.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
class SynthConjecture;
/** utility for constructing datatypes that correspond to syntactic restrictions,
* and applying the deep embedding from Section 4 of Reynolds et al CAV 2015.
*/
class CegGrammarConstructor
{
public:
CegGrammarConstructor(QuantifiersEngine* qe, SynthConjecture* p);
~CegGrammarConstructor() {}
/** process
*
* This converts node q based on its deep embedding
* (Section 4 of Reynolds et al CAV 2015).
* The syntactic restrictions are associated with
* the functions-to-synthesize using the attribute
* SygusSynthGrammarAttribute.
* The arguments templates and template_args
* indicate templates for the function to synthesize,
* in particular the solution for the i^th function
* to synthesis must be of the form
* templates[i]{ templates_arg[i] -> t }
* for some t if !templates[i].isNull().
*/
Node process(Node q,
const std::map<Node, Node>& templates,
const std::map<Node, Node>& templates_arg);
/**
* Same as above, but we have already determined that the set of first-order
* datatype variables that will quantify the deep embedding conjecture are
* the vector ebvl.
*/
Node process(Node q,
const std::map<Node, Node>& templates,
const std::map<Node, Node>& templates_arg,
const std::vector<Node>& ebvl);
/** is the syntax restricted? */
bool isSyntaxRestricted() { return d_is_syntax_restricted; }
/** make the default sygus datatype type corresponding to builtin type range
* bvl is the set of free variables to include in the grammar
* fun is for naming
* extra_cons is a set of extra constant symbols to include in the grammar,
* exclude_cons is used to exclude operators from the grammar,
* term_irrelevant is a set of terms that should not be included in the
* grammar.
*/
static TypeNode mkSygusDefaultType(
TypeNode range,
Node bvl,
const std::string& fun,
std::map<TypeNode, std::vector<Node> >& extra_cons,
std::map<TypeNode, std::vector<Node> >& exclude_cons,
std::unordered_set<Node, NodeHashFunction>& term_irrelevant);
/** make the default sygus datatype type corresponding to builtin type range */
static TypeNode mkSygusDefaultType(TypeNode range,
Node bvl,
const std::string& fun)
{
std::map<TypeNode, std::vector<Node> > extra_cons;
std::map<TypeNode, std::vector<Node> > exclude_cons;
std::unordered_set<Node, NodeHashFunction> term_irrelevant;
return mkSygusDefaultType(
range, bvl, fun, extra_cons, exclude_cons, term_irrelevant);
}
/** make the sygus datatype type that encodes the solution space (lambda
* templ_arg. templ[templ_arg]) where templ_arg
* has syntactic restrictions encoded by sygus type templ_arg_sygus_type
* bvl is the set of free variables to include in the grammar
* fun is for naming
*/
static TypeNode mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, const std::string& fun );
/**
* Returns the sygus variable list for function-to-synthesize variable f.
* These are the names of the arguments of f, which should be included in the
* grammar for f. This returns either the variable list set explicitly via the
* attribute SygusSynthFunVarListAttribute, or a fresh variable list of the
* proper type otherwise. It will return null if f is not a function.
*/
static Node getSygusVarList(Node f);
/**
* Returns true iff there are syntax restrictions on the
* functions-to-synthesize of sygus conjecture q.
*/
static bool hasSyntaxRestrictions(Node q);
/**
* Make the builtin constants for type "type" that should be included in a
* sygus grammar, add them to vector ops.
*/
static void mkSygusConstantsForType(TypeNode type, std::vector<Node>& ops);
/**
* Convert node n based on deep embedding, see Section 4 of Reynolds et al
* CAV 2015.
*
* This returns the result of converting n to its deep embedding based on
* the mapping from functions to datatype variables, stored in
* d_synth_fun_vars. This method should be called only after calling process
* above.
*/
Node convertToEmbedding(Node n);
private:
/** reference to quantifier engine */
QuantifiersEngine * d_qe;
/** parent conjecture
* This contains global information about the synthesis conjecture.
*/
SynthConjecture* d_parent;
/**
* Maps each synthesis function to its corresponding (first-order) sygus
* datatype variable. This map is initialized by the process methods.
*/
std::map<Node, Node> d_synth_fun_vars;
/** is the syntax restricted? */
bool d_is_syntax_restricted;
/** collect terms */
void collectTerms( Node n, std::map< TypeNode, std::vector< Node > >& consts );
//---------------- grammar construction
// helper for mkSygusDefaultGrammar (makes unresolved type for mutually recursive datatype construction)
static TypeNode mkUnresolvedType(const std::string& name, std::set<Type>& unres);
// collect the list of types that depend on type range
static void collectSygusGrammarTypesFor(TypeNode range,
std::vector<TypeNode>& types);
/** helper function for function mkSygusDefaultType
* Collects a set of mutually recursive datatypes "datatypes" corresponding to
* encoding type "range" to SyGuS.
* unres is used for the resulting call to mkMutualDatatypeTypes
*/
static void mkSygusDefaultGrammar(
TypeNode range,
Node bvl,
const std::string& fun,
std::map<TypeNode, std::vector<Node> >& extra_cons,
std::map<TypeNode, std::vector<Node> >& exclude_cons,
std::unordered_set<Node, NodeHashFunction>& term_irrelevant,
std::vector<CVC4::Datatype>& datatypes,
std::set<Type>& unres);
// helper function for mkSygusTemplateType
static TypeNode mkSygusTemplateTypeRec( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl,
const std::string& fun, unsigned& tcount );
//---------------- end grammar construction
};
} /* namespace CVC4::theory::quantifiers */
} /* namespace CVC4::theory */
} /* namespace CVC4 */
#endif
|
