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) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel 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 "definefun" 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 nonidentity 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 functiontosynthesize. 
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 

* nonzero 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 