GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_grammar_norm.h Lines: 8 20 40.0 %
Date: 2021-03-23 Branches: 1 38 2.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_grammar_norm.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Haniel Barbosa, Andrew Reynolds, Tim King
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 simplifying SyGuS grammars after they are encoded into
13
 ** datatypes.
14
 **/
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H
18
#define CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H
19
20
#include <map>
21
#include <memory>
22
#include <vector>
23
24
#include "expr/node.h"
25
#include "expr/sygus_datatype.h"
26
#include "expr/type_node.h"
27
28
namespace CVC4 {
29
namespace theory {
30
namespace quantifiers {
31
32
class SygusGrammarNorm;
33
class TermDbSygus;
34
35
/** Operator position trie class
36
 *
37
 * This data structure stores an unresolved type corresponding to the
38
 * normalization of a type. This unresolved type is indexed by the positions of
39
 * the construtors of the datatype associated with the original type. The list
40
 * of positions represent the operators, associated with the respective
41
 * considered constructors, that were used for building the unresolved type.
42
 *
43
 * Example:
44
 *
45
 * Let A be a type defined by the grammar "A -> x | 0 | 1 | A + A". In its
46
 * datatype representation the operator for "x" is in position 0, for "0" in
47
 * position "1" and so on. Consider entries (T, [op_1, ..., op_n]) -> T' to
48
 * represent that a type T is normalized with operators [op_1, ..., op_n] into
49
 * the type T'. For entries
50
 *
51
 * (A, [x, 0, 1, +]) -> A1
52
 * (A, [x, 1, +]) -> A2
53
 * (A, [1, +]) -> A3
54
 * (A, [0]) -> AZ
55
 * (A, [x]) -> AX
56
 * (A, [1]) -> AO
57
 *
58
 * the OpPosTrie T we build for this type is :
59
 *
60
 * T[A] :
61
 *      T[A].d_children[0] : AX
62
 *        T[A].d_children[0].d_children[1] :
63
 *          T[A].d_children[0].d_children[1].d_children[2] :
64
 *            T[A].d_children[0].d_children[1].d_children[2].d_children[3] : A1
65
 *        T[A].d_children[0].d_children[2] :
66
 *          T[A].d_children[0].d_children[2].d_children[3] : A2
67
 *      T[A].d_children[1] : AZ
68
 *      T[A].d_children[2] : AO
69
 *        T[A].d_children[2].d_children[4] : A3
70
 *
71
 * Nodes store the types built for the path of positions up to that point, if
72
 * any.
73
 */
74
8316
class OpPosTrie
75
{
76
 public:
77
  /** type retrieval/addition
78
   *
79
   * if type indexed by the given operator positions is already in the trie then
80
   * unres_t becomes the indexed type and true is returned. Otherwise a new type
81
   * is created, indexed by the given positions, and assigned to unres_t, with
82
   * false being returned.
83
   */
84
  bool getOrMakeType(TypeNode tn,
85
                     TypeNode& unres_tn,
86
                     const std::vector<unsigned>& op_pos,
87
                     unsigned ind = 0);
88
  /** clear all data from this trie */
89
  void clear() { d_children.clear(); }
90
91
 private:
92
  /** the data (only set for the final node of an inserted path) */
93
  TypeNode d_unres_tn;
94
  /* the children of the trie node */
95
  std::map<unsigned, OpPosTrie> d_children;
96
}; /* class OpPosTrie */
97
98
/** Utility for normalizing SyGuS grammars to avoid spurious enumerations
99
 *
100
 * Uses the datatype representation of a SyGuS grammar to identify entries that
101
 * can normalized in order to have less possible enumerations. An example is
102
 * with integer types, e.g.:
103
 *
104
 * Int -> x | y | Int + Int | 0 | 1 | ite(Bool, Int, Int)
105
 *
106
 * becomes
107
 *
108
 * Int0 -> IntZ | Int1
109
 * IntZ -> 0
110
 * Int1 -> IntX | IntX + Int1 | Int2
111
 * IntX -> x
112
 * Int2 -> IntY | IntY + Int2 | Int3
113
 * IntY -> y
114
 * Int3 -> IntO | IntO + Int3 | Int4
115
 * IntO -> 1
116
 * Int4 -> IntITE | IntITE + Int4
117
 * IntITE -> ite(Bool, Int0, Int0)
118
 *
119
 * TODO: #1304 normalize more complex grammars
120
 *
121
 * This class also performs more straightforward normalizations, such as
122
 * expanding definitions of functions declared with a "define-fun" command.
123
 * These lighweight transformations are always applied, independently of the
124
 * normalization option being enabled.
125
 */
126
class SygusGrammarNorm
127
{
128
 public:
129
  SygusGrammarNorm(TermDbSygus* tds);
130
329
  ~SygusGrammarNorm() {}
131
  /** creates a normalized typenode from a given one.
132
   *
133
   * In a normalized typenode all typenodes it contains are normalized.
134
   * Normalized typenodes can be structurally identicial to their original
135
   * counterparts.
136
   *
137
   * sygus_vars are the input variables for the function to be synthesized,
138
   * which are used as input for the built datatypes.
139
   *
140
   * This is the function that will resolve all types and datatypes built during
141
   * normalization. This operation can only be performed after all types
142
   * contained in "tn" have been normalized, since the resolution of datatypes
143
   * depends on all types involved being defined.
144
   */
145
  TypeNode normalizeSygusType(TypeNode tn, Node sygus_vars);
146
147
  /* Retrives, or, if none, creates, stores and returns, the node for the
148
   * identity operator (\lambda x. x) for the given type node */
149
  static inline Node getIdOp(TypeNode tn)
150
  {
151
    auto it = d_tn_to_id.find(tn);
152
    if (it == d_tn_to_id.end())
153
    {
154
      std::vector<Node> vars = {NodeManager::currentNM()->mkBoundVar(tn)};
155
      Node n = NodeManager::currentNM()->mkNode(
156
          kind::LAMBDA,
157
          NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars),
158
          vars.back());
159
      d_tn_to_id[tn] = n;
160
      return n;
161
    }
162
    return it->second;
163
  }
164
165
 private:
166
  /** Keeps the necessary information for bulding a normalized type:
167
   *
168
   * the original typenode, from which the datatype representation can be
169
   * extracted
170
   *
171
   * the operators, names, print callbacks and list of argument types for each
172
   * constructor
173
   *
174
   * the unresolved type node used as placeholder for references of the yet to
175
   * be built normalized type
176
   *
177
   * A (SyGuS) datatype to represent the structure of the type node for the
178
   * normalized type.
179
   */
180
  class TypeObject
181
  {
182
   public:
183
    /* Stores the original type node and the unresolved placeholder. The
184
     * datatype for the latter is created with the respective name. */
185
    TypeObject(TypeNode src_tn, TypeNode unres_tn);
186
729
    ~TypeObject() {}
187
188
    /** adds information in "cons" (operator, name, print callback, argument
189
     * types) as it is into "to"
190
     *
191
     * A side effect of this procedure is to expand the definitions in the sygus
192
     * operator of "cons"
193
     *
194
     * The types of the arguments of "cons" are recursively normalized
195
     */
196
    void addConsInfo(SygusGrammarNorm* sygus_norm,
197
                     const DTypeConstructor& cons);
198
199
    /** initializes a datatype with the information in the type object
200
     *
201
     * "dt" is the datatype of the original typenode. It is necessary for
202
     * retrieving ancillary information during the datatype building, such as
203
     * its sygus type (e.g. Int)
204
     *
205
     * The initialized datatype and its unresolved type are saved in the global
206
     * accumulators of "sygus_norm"
207
     */
208
    void initializeDatatype(SygusGrammarNorm* sygus_norm, const DType& dt);
209
210
    //---------- information stored from original type node
211
212
    /* The original typenode this TypeObject is built from */
213
    TypeNode d_tn;
214
215
    //---------- information to build normalized type node
216
217
    /* Unresolved type node placeholder */
218
    TypeNode d_unres_tn;
219
    /** A sygus datatype */
220
    SygusDatatype d_sdt;
221
  }; /* class TypeObject */
222
223
  /** Transformation abstract class
224
   *
225
   * Classes extending this one will define specif transformationst for building
226
   * normalized types based on applications of specific operators
227
   */
228
27
  class Transf
229
  {
230
   public:
231
27
    virtual ~Transf() {}
232
233
    /** abstract function for building normalized types
234
     *
235
     * Builds normalized types for the operators specifed by the positions in
236
     * op_pos of constructors from dt. The built types are associated with the
237
     * given type object and accumulated in the sygus_norm object, whose
238
     * utilities for any extra necessary normalization.
239
     */
240
    virtual void buildType(SygusGrammarNorm* sygus_norm,
241
                           TypeObject& to,
242
                           const DType& dt,
243
                           std::vector<unsigned>& op_pos) = 0;
244
  }; /* class Transf */
245
246
  /** Drop transformation class
247
   *
248
   * This class builds a type by dropping a set of redundant constructors,
249
   * whose indices are given as input to the constructor of this class.
250
   */
251
54
  class TransfDrop : public Transf
252
  {
253
   public:
254
27
    TransfDrop(const std::vector<unsigned>& indices) : d_drop_indices(indices)
255
    {
256
27
    }
257
    /** build type */
258
    void buildType(SygusGrammarNorm* sygus_norm,
259
                   TypeObject& to,
260
                   const DType& dt,
261
                   std::vector<unsigned>& op_pos) override;
262
263
   private:
264
    std::vector<unsigned> d_drop_indices;
265
  };
266
267
  /** Chain transformation class
268
   *
269
   * Determines how to build normalized types by chaining the application of one
270
   * of its operators. The resulting type should admit the same terms as the
271
   * previous one modulo commutativity, associativity and identity of the
272
   * neutral element.
273
   *
274
   * TODO: #1304:
275
   * - define this transformation for more than just PLUS for Int.
276
   * - improve the building such that elements that should not be entitled a
277
   * "link in the chain" (such as 5 in opposition to variables and 1) do not get
278
   * one
279
   * - consider the case when operator is applied to different types, e.g.:
280
   *   A -> B + B | x; B -> 0 | 1
281
   * - consider the case in which in which the operator occurs nested in an
282
   *   argument type of itself, e.g.:
283
   *   A -> (B + B) + B | x; B -> 0 | 1
284
   */
285
  class TransfChain : public Transf
286
  {
287
   public:
288
    TransfChain(unsigned chain_op_pos, const std::vector<unsigned>& elem_pos)
289
        : d_chain_op_pos(chain_op_pos), d_elem_pos(elem_pos){};
290
291
    /** builds types encoding a chain in which each link contains a repetition
292
     * of the application of the chain operator over a non-identity element
293
     *
294
     * Example: when considering, over the integers, the operator "+" and the
295
     * elemenst "1", "x" and "y", the built chain is e.g.
296
     *
297
     * x + ... + x + y + ... + y + 1 + ...+ 1
298
     *
299
     * whose encoding in types would be e.g.
300
     *
301
     * A  -> AX | AX + A | B
302
     * AX -> x
303
     * B  -> BY | BY + B | C
304
     * BY -> y
305
     * C  -> C1 | C1 + C
306
     * C1 -> 1
307
     *
308
     * ++++++++
309
     *
310
     * The types composing links in the chain are built recursively by invoking
311
     * sygus_norm, which caches results and handles the global normalization, on
312
     * the operators not used in a given link, which will lead to recalling this
313
     * transformation and so on until all operators originally given are
314
     * considered.
315
     */
316
    void buildType(SygusGrammarNorm* sygus_norm,
317
                   TypeObject& to,
318
                   const DType& dt,
319
                   std::vector<unsigned>& op_pos) override;
320
321
    /** Whether operator is chainable for the type (e.g. PLUS for Int)
322
     *
323
     *  Since the map this function depends on cannot be built statically, this
324
     *  function first build maps the first time a type is checked. As a
325
     *  consequence the list of chainabel operators is hardcoded in the map
326
     *  building.
327
     *
328
     * TODO: #1304: Cover more types and operators, make this robust to more
329
     * complex grammars
330
     */
331
    static bool isChainable(TypeNode tn, Node op);
332
    /* Whether n is the identity for the chain operator of the type (e.g. 1 is
333
     * not the identity 0 for PLUS for Int)
334
     *
335
     * TODO: #1304: Cover more types, make this robust to more complex grammars
336
     */
337
    static bool isId(TypeNode tn, Node op, Node n);
338
339
   private:
340
    /* TODO #1304: this should admit more than one, as well as which elements
341
     * are associated with which operator */
342
    /* Position of chain operator */
343
    unsigned d_chain_op_pos;
344
    /* Positions (of constructors in the datatype whose type is being
345
     * normalized) of elements the chain operator is applied to */
346
    std::vector<unsigned> d_elem_pos;
347
    /** Specifies for each type node which are its chainable operators
348
     *
349
     * For example, for Int the map is {OP -> [+]}
350
     *
351
     * TODO #1304: consider more operators
352
     */
353
    static std::map<TypeNode, std::vector<Kind>> d_chain_ops;
354
    /** Specifies for each type node and chainable operator its identity
355
     *
356
     * For example, for Int and PLUS the map is {Int -> {+ -> 0}}
357
     *
358
     * TODO #1304: consider more operators
359
     */
360
    static std::map<TypeNode, std::map<Kind, Node>> d_chain_op_id;
361
362
  }; /* class TransfChain */
363
364
  /** sygus term database associated with this utility */
365
  TermDbSygus* d_tds;
366
  /** List of variable inputs of function-to-synthesize.
367
   *
368
   * This information is needed in the construction of each datatype
369
   * representation of type nodes contained in the type node being normalized
370
   */
371
  TNode d_sygus_vars;
372
  /* Datatypes to be resolved */
373
  std::vector<DType> d_dt_all;
374
  /* Types to be resolved */
375
  std::set<TypeNode> d_unres_t_all;
376
  /* Associates type nodes with OpPosTries */
377
  std::map<TypeNode, OpPosTrie> d_tries;
378
  /* Map of type nodes into their identity operators (\lambda x. x) */
379
  static std::map<TypeNode, Node> d_tn_to_id;
380
381
  /** recursively traverses a typenode normalizing all of its elements
382
   *
383
   * "tn" is the typenode to be normalized
384
   * "dt" is its datatype representation
385
   * "op_pos" is the list of positions of construtors of dt that are being
386
   * considered for the normalization
387
   *
388
   * The result of normalizing tn with the respective constructors is cached
389
   * with an OpPosTrie. New types and datatypes created during normalization are
390
   * accumulated grobally to be later resolved.
391
   *
392
   * The normalization occurs following some inferred transformation based on
393
   * the sygus type (e.g. Int) of tn, and the operators being considered.
394
   *
395
   * Example: Let A be the type node encoding the grammar
396
   *
397
   * Int -> x | y | Int + Int | 0 | 1 | ite(Bool, Int, Int)
398
   *
399
   * and assume all its datatype constructors are being used for
400
   * normalization. The inferred normalization transformation will consider the
401
   * non-zero elements {x, y, 1, ite(...)} and the operator {+} to build a chain
402
   * of monomials, as seen above. The operator for "0" is rebuilt as is (the
403
   * default behaviour of operators not selected for transformations).
404
   *
405
   * recursion depth is limited by the height of the types, which is small
406
   */
407
  TypeNode normalizeSygusRec(TypeNode tn,
408
                             const DType& dt,
409
                             std::vector<unsigned>& op_pos);
410
411
  /** wrapper for the above function
412
   *
413
   * invoked when all operators of "tn" are to be considered for normalization
414
   */
415
  TypeNode normalizeSygusRec(TypeNode tn);
416
417
  /** infers a transformation for normalizing dt when allowed to use the
418
   * operators in the positions op_pos.
419
   *
420
   * TODO: #1304: Infer more complex transformations
421
   */
422
  std::unique_ptr<Transf> inferTransf(TypeNode tn,
423
                                      const DType& dt,
424
                                      const std::vector<unsigned>& op_pos);
425
}; /* class SygusGrammarNorm */
426
427
}  // namespace quantifiers
428
}  // namespace theory
429
}  // namespace CVC4
430
431
#endif