GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/type_info.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file type_info.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
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 Sygus type info data structure
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H
18
#define CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H
19
20
#include <map>
21
22
#include "expr/node.h"
23
24
namespace CVC4 {
25
namespace theory {
26
namespace quantifiers {
27
28
class TermDbSygus;
29
30
/**
31
 * This data structure stores statically computed information regarding a sygus
32
 * datatype type.
33
 *
34
 * To use an instance of this class x, call x.initialize(tn); where tn is a
35
 * sygus datatype type. Then, most of the query methods on x can be called.
36
 * As an exception, the variable subclass queries require that additionally
37
 * x.initializeVarSubclasses() is called.
38
 *
39
 */
40
2682
class SygusTypeInfo
41
{
42
 public:
43
  SygusTypeInfo();
44
  //-------------------------------------------- initialize
45
  /** initialize this information for sygus datatype type tn */
46
  void initialize(TermDbSygus* tds, TypeNode tn);
47
  /**
48
   * Initialize the variable subclass information for this class. Must have
49
   * called initialize(...) prior to calling this method.
50
   */
51
  void initializeVarSubclasses();
52
  //-------------------------------------------- end initialize
53
  /** Get the builtin type that this sygus type encodes */
54
  TypeNode getBuiltinType() const;
55
  /** Get the variable list (formal argument list) for the sygus type */
56
  const std::vector<Node>& getVarList() const;
57
  /**
58
   * Return the index of the constructor of this sygus type that encodes
59
   * application of the builtin Kind k, or -1 if one does not exist.
60
   */
61
  int getKindConsNum(Kind k) const;
62
  /**
63
   * Return the index of the constructor of this sygus type that encodes
64
   * constant c, or -1 if one does not exist.
65
   */
66
  int getConstConsNum(Node c) const;
67
  /**
68
   * Return the index of the constructor of this sygus type whose builtin
69
   * operator is n, or -1 if one does not exist.
70
   */
71
  int getOpConsNum(Node n) const;
72
  /** Is there a constructor that encodes application of builtin Kind k? */
73
  bool hasKind(Kind k) const;
74
  /** Is there a constructor that encodes constant c? */
75
  bool hasConst(Node c) const;
76
  /** Is there a constructor whose builtin operator is n? */
77
  bool hasOp(Node n) const;
78
  /**
79
   * Returns true if this sygus type has a constructor whose sygus operator is
80
   * ITE, or is a lambda whose body is ITE.
81
   */
82
  bool hasIte() const;
83
  /**
84
   * Get the builtin kind for the i^th constructor of this sygus type. If the
85
   * i^th constructor does not encode an application of a builtin kind, this
86
   * method returns UNDEFINED_KIND.
87
   */
88
  Kind getConsNumKind(unsigned i) const;
89
  /**
90
   * Get the construct for the i^th constructor of this sygus type. If the
91
   * i^th constructor does not encode a builtin constant, this method returns
92
   * the null node.
93
   */
94
  Node getConsNumConst(unsigned i) const;
95
  /** Get the builtin operator of the i^th constructor of this sygus type */
96
  Node getConsNumOp(unsigned i) const;
97
  /**
98
   * Returns true if the i^th constructor encodes application of a builtin Kind.
99
   */
100
  bool isKindArg(unsigned i) const;
101
  /**
102
   * Returns true if the i^th constructor encodes a builtin constant.
103
   */
104
  bool isConstArg(unsigned i) const;
105
  /**
106
   * Get the index of the "any constant" constructor of type tn if it has one,
107
   * or returns -1 otherwise.
108
   */
109
  int getAnyConstantConsNum() const;
110
  /** has subterm symbolic constructor
111
   *
112
   * Returns true if any subterm of type tn can be a symbolic constructor.
113
   */
114
  bool hasSubtermSymbolicCons() const;
115
  /** get subfield types
116
   *
117
   * This adds all "subfield types" of tn to sf_types. A type tnc is a subfield
118
   * type of tn if there exists a selector chain S1( ... Sn( x )...) that has
119
   * type tnc, where x has type tn. In other words, tnc is the type of some
120
   * subfield of terms of type tn, at any depth.
121
   */
122
  void getSubfieldTypes(std::vector<TypeNode>& sf_types) const;
123
  //--------------------------------- variable subclasses
124
  /** Get subclass id for variable
125
   *
126
   * This returns the "subclass" identifier for variable v in sygus
127
   * type tn. A subclass identifier groups variables based on the sygus
128
   * types they occur in:
129
   *   A -> A + B | C + C | x | y | z | w | u
130
   *   B -> y | z
131
   *   C -> u
132
   * The variables in this grammar can be grouped according to the sygus types
133
   * they appear in:
134
   *   { x,w } occur in A
135
   *   { y,z } occur in A,B
136
   *   { u } occurs in A,C
137
   * We say that e.g. x, w are in the same subclass.
138
   *
139
   * If this method returns 0, then v is not a variable in sygus type tn.
140
   * Otherwise, this method returns a positive value n, such that
141
   * getSubclassIdForVar[v1] = getSubclassIdForVar[v2] iff v1 and v2 are in the
142
   * same subclass.
143
   *
144
   * The type tn should be the type of an enumerator registered to this
145
   * database, where notice that we do not compute this information for the
146
   * subfield types of the enumerator.
147
   */
148
  unsigned getSubclassForVar(Node v) const;
149
  /**
150
   * Get the number of variable in the subclass with identifier sc for type tn.
151
   */
152
  unsigned getNumSubclassVars(unsigned sc) const;
153
  /** Get the i^th variable in the subclass with identifier sc for type tn */
154
  Node getVarSubclassIndex(unsigned sc, unsigned i) const;
155
  /**
156
   * Get the a variable's index in its subclass list. This method returns true
157
   * iff variable v has been assigned a subclass in tn. It updates index to
158
   * be v's index iff the method returns true.
159
   */
160
  bool getIndexInSubclassForVar(Node v, unsigned& index) const;
161
  /**
162
   * Are the variable subclasses a trivial partition (each variable subclass
163
   * has a single variable)?
164
   */
165
  bool isSubclassVarTrivial() const;
166
  //--------------------------------- end variable subclasses
167
  /**
168
   * Get the minimum depth of type in this grammar
169
   *
170
   */
171
  unsigned getMinTypeDepth(TypeNode tn) const;
172
  /** Get the minimum size for a term of this sygus type */
173
  unsigned getMinTermSize() const;
174
  /**
175
   * Get the minimum size for a term that is an application of a constructor of
176
   * this type.
177
   */
178
  unsigned getMinConsTermSize(unsigned cindex);
179
180
 private:
181
  /** The sygus type that this class is for */
182
  TypeNode d_this;
183
  /** The builtin type that this sygus type encodes */
184
  TypeNode d_btype;
185
  /** The variable list of the sygus type */
186
  std::vector<Node> d_var_list;
187
  /**
188
   * Maps constructor indices to the (builtin) Kind that they encode, if any.
189
   */
190
  std::map<unsigned, Kind> d_arg_kind;
191
  /** Reverse of the above map */
192
  std::map<Kind, unsigned> d_kinds;
193
  /**
194
   * Whether this sygus type has a constructors whose sygus operator is ITE,
195
   * or is a lambda whose body is ITE.
196
   */
197
  bool d_hasIte;
198
  /**
199
   * Maps constructor indices to the constant that they encode, if any.
200
   */
201
  std::map<unsigned, Node> d_arg_const;
202
  /** Reverse of the above map */
203
  std::map<Node, unsigned> d_consts;
204
  /**
205
   * Maps constructor indices to the operator they encode.
206
   */
207
  std::map<unsigned, Node> d_arg_ops;
208
  /** Reverse of the above map */
209
  std::map<Node, unsigned> d_ops;
210
  /**
211
   * This maps the subfield datatype types T to the smallest size of a term of
212
   * this sygus type that includes T as a subterm. For example, for type A with
213
   * grammar:
214
   *   A -> B+B | 0 | B-D
215
   *   B -> C+C
216
   *   ...
217
   * we have that d_min_type_depth = { A -> 0, B -> 1, C -> 2, D -> 1 }.
218
   */
219
  std::map<TypeNode, unsigned> d_min_type_depth;
220
  /** The minimimum size term of this type */
221
  unsigned d_min_term_size;
222
  /**
223
   * Maps constructors to the minimum size term that is an application of that
224
   * constructor.
225
   */
226
  std::map<unsigned, unsigned> d_min_cons_term_size;
227
  /** a cache for getSelectorWeight */
228
  std::map<Node, unsigned> d_sel_weight;
229
  /**
230
   * For each sygus type, the index of the "any constant" constructor, if it
231
   * has one, or -1 otherwise.
232
   */
233
  int d_sym_cons_any_constant;
234
  /**
235
   * Whether any subterm of this type contains a symbolic constructor. This
236
   * corresponds to whether sygus repair techniques will ever have any effect
237
   * for this type.
238
   */
239
  bool d_has_subterm_sym_cons;
240
  /**
241
   * Map from sygus types and bound variables to their type subclass id. Note
242
   * type class identifiers are computed for each type of registered sygus
243
   * enumerators, but not all sygus types. For details, see getSubclassIdForVar.
244
   */
245
  std::map<Node, unsigned> d_var_subclass_id;
246
  /** the list of variables with given subclass */
247
  std::map<unsigned, std::vector<Node> > d_var_subclass_list;
248
  /** the index of each variable in the above list */
249
  std::map<Node, unsigned> d_var_subclass_list_index;
250
  /** computes the map d_min_type_depth */
251
  void computeMinTypeDepthInternal(TypeNode root_tn, unsigned type_depth);
252
};
253
254
}  // namespace quantifiers
255
}  // namespace theory
256
}  // namespace CVC4
257
258
#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H */