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