GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_grammar_cons.h Lines: 4 4 100.0 %
Date: 2021-03-23 Branches: 2 4 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_grammar_cons.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Yoni Zohar, Haniel Barbosa
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief class for constructing inductive datatypes that correspond to
13
 ** grammars that encode syntactic restrictions for SyGuS.
14
 **/
15
16
#include "cvc4_private.h"
17
18
#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
19
#define CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
20
21
#include <map>
22
#include <vector>
23
24
#include "expr/attribute.h"
25
#include "expr/node.h"
26
#include "expr/sygus_datatype.h"
27
28
namespace CVC4 {
29
namespace theory {
30
31
/**
32
 * Attribute for associating a function-to-synthesize with a first order
33
 * variable whose type is a sygus datatype type that encodes its grammar.
34
 */
35
struct SygusSynthGrammarAttributeId
36
{
37
};
38
typedef expr::Attribute<SygusSynthGrammarAttributeId, Node>
39
    SygusSynthGrammarAttribute;
40
41
/**
42
 * Attribute for associating a function-to-synthesize with its formal argument
43
 * list.
44
 */
45
struct SygusSynthFunVarListAttributeId
46
{
47
};
48
typedef expr::Attribute<SygusSynthFunVarListAttributeId, Node>
49
    SygusSynthFunVarListAttribute;
50
51
namespace quantifiers {
52
53
class SynthConjecture;
54
class TermDbSygus;
55
56
/**
57
 * Utility for constructing datatypes that correspond to syntactic restrictions,
58
 * and applying the deep embedding from Section 4 of Reynolds et al CAV 2015.
59
 */
60
class CegGrammarConstructor
61
{
62
public:
63
 CegGrammarConstructor(TermDbSygus* tds, SynthConjecture* p);
64
2188
 ~CegGrammarConstructor() {}
65
 /** process
66
  *
67
  * This converts node q based on its deep embedding
68
  * (Section 4 of Reynolds et al CAV 2015).
69
  * The syntactic restrictions are associated with
70
  * the functions-to-synthesize using the attribute
71
  * SygusSynthGrammarAttribute.
72
  * The arguments templates and template_args
73
  * indicate templates for the function to synthesize,
74
  * in particular the solution for the i^th function
75
  * to synthesis must be of the form
76
  *   templates[i]{ templates_arg[i] -> t }
77
  * for some t if !templates[i].isNull().
78
  */
79
 Node process(Node q,
80
              const std::map<Node, Node>& templates,
81
              const std::map<Node, Node>& templates_arg);
82
 /**
83
  * Same as above, but we have already determined that the set of first-order
84
  * datatype variables that will quantify the deep embedding conjecture are
85
  * the vector ebvl.
86
  */
87
 Node process(Node q,
88
              const std::map<Node, Node>& templates,
89
              const std::map<Node, Node>& templates_arg,
90
              const std::vector<Node>& ebvl);
91
92
 /** Is the syntax restricted? */
93
506
 bool isSyntaxRestricted() { return d_is_syntax_restricted; }
94
95
 /**
96
  * Make the default sygus datatype type corresponding to builtin type range
97
  * arguments:
98
  *   - bvl: the set of free variables to include in the grammar
99
  *   - fun: used for naming
100
  *   - extra_cons: a set of extra constant symbols to include in the grammar,
101
  *     regardless of their inclusion in the default grammar.
102
  *   - exclude_cons: used to exclude operators from the grammar,
103
  *   - term_irrelevant: a set of terms that should not be included in the
104
  *      grammar.
105
  *   - include_cons: a set of operators such that if this set is not empty,
106
  *     its elements that are in the default grammar (and only them)
107
  *     will be included.
108
  */
109
 static TypeNode mkSygusDefaultType(
110
     TypeNode range,
111
     Node bvl,
112
     const std::string& fun,
113
     std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& extra_cons,
114
     std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>&
115
         exclude_cons,
116
     std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>&
117
         include_cons,
118
     std::unordered_set<Node, NodeHashFunction>& term_irrelevant);
119
120
 /**
121
  * Make the default sygus datatype type corresponding to builtin type range.
122
  */
123
 static TypeNode mkSygusDefaultType(TypeNode range,
124
                                    Node bvl,
125
                                    const std::string& fun)
126
 {
127
   std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> extra_cons;
128
   std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> exclude_cons;
129
   std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> include_cons;
130
   std::unordered_set<Node, NodeHashFunction> term_irrelevant;
131
   return mkSygusDefaultType(range,
132
                             bvl,
133
                             fun,
134
                             extra_cons,
135
                             exclude_cons,
136
                             include_cons,
137
                             term_irrelevant);
138
  }
139
140
  /** make the sygus datatype type that encodes the solution space (lambda
141
  * templ_arg. templ[templ_arg]) where templ_arg
142
  * has syntactic restrictions encoded by sygus type templ_arg_sygus_type
143
  *   bvl is the set of free variables to include in the grammar
144
  *   fun is for naming
145
  */
146
  static TypeNode mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, const std::string& fun );
147
  /**
148
   * Returns true iff there are syntax restrictions on the
149
   * functions-to-synthesize of sygus conjecture q.
150
   */
151
  static bool hasSyntaxRestrictions(Node q);
152
  /**
153
   * Make the builtin constants for type "type" that should be included in a
154
   * sygus grammar, add them to vector ops.
155
   */
156
  static void mkSygusConstantsForType(TypeNode type, std::vector<Node>& ops);
157
  /** Is it possible to construct a default grammar for type t? */
158
  static bool isHandledType(TypeNode t);
159
  /**
160
   * Convert node n based on deep embedding, see Section 4 of Reynolds et al
161
   * CAV 2015.
162
   *
163
   * This returns the result of converting n to its deep embedding based on
164
   * the mapping from functions to datatype variables, stored in
165
   * d_synth_fun_vars. This method should be called only after calling process
166
   * above.
167
   */
168
  Node convertToEmbedding(Node n);
169
170
 private:
171
  /** The sygus term database we are using */
172
  TermDbSygus* d_tds;
173
  /** parent conjecture
174
  * This contains global information about the synthesis conjecture.
175
  */
176
  SynthConjecture* d_parent;
177
  /**
178
   * Maps each synthesis function to its corresponding (first-order) sygus
179
   * datatype variable. This map is initialized by the process methods.
180
   */
181
  std::map<Node, Node> d_synth_fun_vars;
182
  /** is the syntax restricted? */
183
  bool d_is_syntax_restricted;
184
  /** collect terms */
185
  void collectTerms(
186
      Node n,
187
      std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& consts);
188
  //---------------- grammar construction
189
  /** A class for generating sygus datatypes */
190
2394
  class SygusDatatypeGenerator
191
  {
192
   public:
193
    SygusDatatypeGenerator(const std::string& name);
194
3412
    ~SygusDatatypeGenerator() {}
195
    /**
196
     * Possibly add a constructor to d_sdt, based on the criteria mentioned
197
     * in this class below. For details see expr/sygus_datatype.h.
198
     */
199
    void addConstructor(Node op,
200
                        const std::string& name,
201
                        const std::vector<TypeNode>& consTypes,
202
                        int weight = -1);
203
    /**
204
     * Possibly add a constructor to d_sdt, based on the criteria mentioned
205
     * in this class below.
206
     */
207
    void addConstructor(Kind k,
208
                        const std::vector<TypeNode>& consTypes,
209
                        int weight = -1);
210
    /** Should we include constructor with operator op? */
211
    bool shouldInclude(Node op) const;
212
    /** The constructors that should be excluded. */
213
    std::unordered_set<Node, NodeHashFunction> d_exclude_cons;
214
    /**
215
     * If this set is non-empty, then only include variables and constructors
216
     * from it.
217
     */
218
    std::unordered_set<Node, NodeHashFunction> d_include_cons;
219
    /** The sygus datatype we are generating. */
220
    SygusDatatype d_sdt;
221
  };
222
223
  // helper for mkSygusDefaultGrammar (makes unresolved type for mutually recursive datatype construction)
224
  static TypeNode mkUnresolvedType(const std::string& name,
225
                                   std::set<TypeNode>& unres);
226
  // collect the list of types that depend on type range
227
  static void collectSygusGrammarTypesFor(TypeNode range,
228
                                          std::vector<TypeNode>& types);
229
  /** helper function for function mkSygusDefaultType
230
  * Collects a set of mutually recursive datatypes "datatypes" corresponding to
231
  * encoding type "range" to SyGuS.
232
  *   unres is used for the resulting call to mkMutualDatatypeTypes
233
  */
234
  static void mkSygusDefaultGrammar(
235
      TypeNode range,
236
      Node bvl,
237
      const std::string& fun,
238
      std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>&
239
          extra_cons,
240
      std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>&
241
          exclude_cons,
242
      const std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>&
243
          include_cons,
244
      std::unordered_set<Node, NodeHashFunction>& term_irrelevant,
245
      std::vector<SygusDatatypeGenerator>& sdts,
246
      std::set<TypeNode>& unres);
247
248
  // helper function for mkSygusTemplateType
249
  static TypeNode mkSygusTemplateTypeRec(Node templ,
250
                                         Node templ_arg,
251
                                         TypeNode templ_arg_sygus_type,
252
                                         Node bvl,
253
                                         const std::string& fun,
254
                                         unsigned& tcount);
255
256
  /**
257
   * Given a kind k, create a lambda operator with the given builtin input type
258
   * and an extra zero argument of that same type.  For example, for k = LEQ and
259
   * bArgType = Int, the operator will be lambda x : Int. x + 0.  Currently the
260
   * supported input types are Real (thus also Int) and BitVector.
261
   */
262
  static Node createLambdaWithZeroArg(Kind k,
263
                                      TypeNode bArgType);
264
  //---------------- end grammar construction
265
};
266
267
} /* namespace CVC4::theory::quantifiers */
268
} /* namespace CVC4::theory */
269
} /* namespace CVC4 */
270
271
#endif