1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Haniel Barbosa, Andrew Reynolds, Tim King |
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 |
|
* Implementation of class for for simplifying SyGuS grammars after they |
14 |
|
* are encoded into datatypes. |
15 |
|
*/ |
16 |
|
|
17 |
|
#include "theory/quantifiers/sygus/sygus_grammar_norm.h" |
18 |
|
|
19 |
|
#include <sstream> |
20 |
|
|
21 |
|
#include "expr/dtype_cons.h" |
22 |
|
#include "expr/node_manager_attributes.h" // for VarNameAttr |
23 |
|
#include "options/quantifiers_options.h" |
24 |
|
#include "theory/datatypes/theory_datatypes_utils.h" |
25 |
|
#include "theory/quantifiers/cegqi/ceg_instantiator.h" |
26 |
|
#include "theory/quantifiers/sygus/sygus_grammar_cons.h" |
27 |
|
#include "theory/quantifiers/sygus/sygus_grammar_red.h" |
28 |
|
#include "theory/quantifiers/sygus/term_database_sygus.h" |
29 |
|
#include "theory/quantifiers/term_util.h" |
30 |
|
|
31 |
|
#include <numeric> // for std::iota |
32 |
|
|
33 |
|
using namespace cvc5::kind; |
34 |
|
|
35 |
|
namespace cvc5 { |
36 |
|
namespace theory { |
37 |
|
namespace quantifiers { |
38 |
|
|
39 |
22688 |
bool OpPosTrie::getOrMakeType(TypeNode tn, |
40 |
|
TypeNode& unres_tn, |
41 |
|
const std::vector<unsigned>& op_pos, |
42 |
|
unsigned ind) |
43 |
|
{ |
44 |
22688 |
if (ind == op_pos.size()) |
45 |
|
{ |
46 |
|
/* Found type */ |
47 |
2377 |
if (!d_unres_tn.isNull()) |
48 |
|
{ |
49 |
3862 |
Trace("sygus-grammar-normalize-trie") |
50 |
1931 |
<< "\tFound type " << d_unres_tn << "\n"; |
51 |
1931 |
unres_tn = d_unres_tn; |
52 |
1931 |
return true; |
53 |
|
} |
54 |
|
/* Creating unresolved type */ |
55 |
892 |
std::stringstream ss; |
56 |
446 |
ss << tn << "_"; |
57 |
2605 |
for (unsigned i = 0, size = op_pos.size(); i < size; ++i) |
58 |
|
{ |
59 |
2159 |
ss << "_" << std::to_string(op_pos[i]); |
60 |
|
} |
61 |
1338 |
d_unres_tn = NodeManager::currentNM()->mkSort( |
62 |
1338 |
ss.str(), NodeManager::SORT_FLAG_PLACEHOLDER); |
63 |
892 |
Trace("sygus-grammar-normalize-trie") |
64 |
446 |
<< "\tCreating type " << d_unres_tn << "\n"; |
65 |
446 |
unres_tn = d_unres_tn; |
66 |
446 |
return false; |
67 |
|
} |
68 |
|
/* Go to next node */ |
69 |
20311 |
return d_children[op_pos[ind]].getOrMakeType(tn, unres_tn, op_pos, ind + 1); |
70 |
|
} |
71 |
|
|
72 |
202 |
SygusGrammarNorm::SygusGrammarNorm(TermDbSygus* tds) : d_tds(tds) {} |
73 |
|
|
74 |
446 |
SygusGrammarNorm::TypeObject::TypeObject(TypeNode src_tn, TypeNode unres_tn) |
75 |
|
: d_tn(src_tn), |
76 |
|
d_unres_tn(unres_tn), |
77 |
446 |
d_sdt(unres_tn.getAttribute(expr::VarNameAttr())) |
78 |
|
{ |
79 |
446 |
} |
80 |
|
|
81 |
2138 |
void SygusGrammarNorm::TypeObject::addConsInfo( |
82 |
|
SygusGrammarNorm* sygus_norm, |
83 |
|
const DTypeConstructor& cons) |
84 |
|
{ |
85 |
2138 |
Trace("sygus-grammar-normalize") << "...for " << cons.getName() << "\n"; |
86 |
|
/* Recover the sygus operator to not lose reference to the original |
87 |
|
* operator (NOT, ITE, etc) */ |
88 |
4276 |
Node sygus_op = cons.getSygusOp(); |
89 |
4276 |
Trace("sygus-grammar-normalize-debug") |
90 |
2138 |
<< ".....operator is " << sygus_op << std::endl; |
91 |
|
|
92 |
4276 |
std::vector<TypeNode> consTypes; |
93 |
2138 |
const std::vector<std::shared_ptr<DTypeSelector> >& args = cons.getArgs(); |
94 |
4313 |
for (const std::shared_ptr<DTypeSelector>& arg : args) |
95 |
|
{ |
96 |
|
// Collect unresolved type nodes corresponding to the typenode of the |
97 |
|
// arguments. |
98 |
4350 |
TypeNode atype = arg->getRangeType(); |
99 |
|
// normalize it recursively |
100 |
2175 |
atype = sygus_norm->normalizeSygusRec(atype); |
101 |
2175 |
consTypes.push_back(atype); |
102 |
|
} |
103 |
|
|
104 |
4276 |
d_sdt.addConstructor( |
105 |
2138 |
sygus_op, cons.getName(), consTypes, cons.getWeight()); |
106 |
2138 |
} |
107 |
|
|
108 |
446 |
void SygusGrammarNorm::TypeObject::initializeDatatype( |
109 |
|
SygusGrammarNorm* sygus_norm, const DType& dt) |
110 |
|
{ |
111 |
|
/* Use the sygus type to not lose reference to the original types (Bool, |
112 |
|
* Int, etc) */ |
113 |
892 |
TypeNode sygusType = dt.getSygusType(); |
114 |
1338 |
d_sdt.initializeDatatype(sygusType, |
115 |
|
sygus_norm->d_sygus_vars, |
116 |
446 |
dt.getSygusAllowConst(), |
117 |
446 |
dt.getSygusAllowAll()); |
118 |
892 |
Trace("sygus-grammar-normalize") |
119 |
446 |
<< "...built datatype " << d_sdt.getDatatype() << " "; |
120 |
|
/* Add to global accumulators */ |
121 |
446 |
sygus_norm->d_dt_all.push_back(d_sdt.getDatatype()); |
122 |
446 |
sygus_norm->d_unres_t_all.insert(d_unres_tn); |
123 |
446 |
Trace("sygus-grammar-normalize") << "---------------------------------\n"; |
124 |
446 |
} |
125 |
|
|
126 |
15 |
void SygusGrammarNorm::TransfDrop::buildType(SygusGrammarNorm* sygus_norm, |
127 |
|
TypeObject& to, |
128 |
|
const DType& dt, |
129 |
|
std::vector<unsigned>& op_pos) |
130 |
|
{ |
131 |
30 |
std::vector<unsigned> difference; |
132 |
15 |
std::set_difference(op_pos.begin(), |
133 |
|
op_pos.end(), |
134 |
|
d_drop_indices.begin(), |
135 |
|
d_drop_indices.end(), |
136 |
15 |
std::back_inserter(difference)); |
137 |
15 |
op_pos = difference; |
138 |
15 |
} |
139 |
|
|
140 |
|
/* TODO #1304: have more operators and types. Moreover, have more general ways |
141 |
|
of finding kind of operator, e.g. if op is (\lambda xy. x + y) this |
142 |
|
function should realize that it is chainable for integers */ |
143 |
|
bool SygusGrammarNorm::TransfChain::isChainable(TypeNode tn, Node op) |
144 |
|
{ |
145 |
|
/* Checks whether operator occurs chainable for its type */ |
146 |
|
if (tn.isInteger() && NodeManager::currentNM()->operatorToKind(op) == PLUS) |
147 |
|
{ |
148 |
|
return true; |
149 |
|
} |
150 |
|
return false; |
151 |
|
} |
152 |
|
|
153 |
|
/* TODO #1304: have more operators and types. Moreover, have more general ways |
154 |
|
of finding kind of operator, e.g. if op is (\lambda xy. x + y) this |
155 |
|
function should realize that it is chainable for integers */ |
156 |
|
bool SygusGrammarNorm::TransfChain::isId(TypeNode tn, Node op, Node n) |
157 |
|
{ |
158 |
|
if (tn.isInteger() && NodeManager::currentNM()->operatorToKind(op) == PLUS |
159 |
|
&& n == TermUtil::mkTypeValue(tn, 0)) |
160 |
|
{ |
161 |
|
return true; |
162 |
|
} |
163 |
|
return false; |
164 |
|
} |
165 |
|
|
166 |
|
void SygusGrammarNorm::TransfChain::buildType(SygusGrammarNorm* sygus_norm, |
167 |
|
TypeObject& to, |
168 |
|
const DType& dt, |
169 |
|
std::vector<unsigned>& op_pos) |
170 |
|
{ |
171 |
|
NodeManager* nm = NodeManager::currentNM(); |
172 |
|
std::vector<unsigned> claimed(d_elem_pos); |
173 |
|
claimed.push_back(d_chain_op_pos); |
174 |
|
unsigned nb_op_pos = op_pos.size(); |
175 |
|
/* TODO do this properly */ |
176 |
|
/* Remove from op_pos the positions claimed by the transformation */ |
177 |
|
std::sort(op_pos.begin(), op_pos.end()); |
178 |
|
std::sort(claimed.begin(), claimed.end()); |
179 |
|
std::vector<unsigned> difference; |
180 |
|
std::set_difference(op_pos.begin(), |
181 |
|
op_pos.end(), |
182 |
|
claimed.begin(), |
183 |
|
claimed.end(), |
184 |
|
std::back_inserter(difference)); |
185 |
|
op_pos = difference; |
186 |
|
if (Trace.isOn("sygus-grammar-normalize-chain")) |
187 |
|
{ |
188 |
|
Trace("sygus-grammar-normalize-chain") |
189 |
|
<< "OP at " << d_chain_op_pos << "\n" |
190 |
|
<< d_elem_pos.size() << " d_elem_pos: "; |
191 |
|
for (unsigned i = 0, size = d_elem_pos.size(); i < size; ++i) |
192 |
|
{ |
193 |
|
Trace("sygus-grammar-normalize-chain") << d_elem_pos[i] << " "; |
194 |
|
} |
195 |
|
Trace("sygus-grammar-normalize-chain") |
196 |
|
<< "\n" |
197 |
|
<< op_pos.size() << " remaining op_pos: "; |
198 |
|
for (unsigned i = 0, size = op_pos.size(); i < size; ++i) |
199 |
|
{ |
200 |
|
Trace("sygus-grammar-normalize-chain") << op_pos[i] << " "; |
201 |
|
} |
202 |
|
Trace("sygus-grammar-normalize-chain") << "\n"; |
203 |
|
} |
204 |
|
/* Build identity operator and empty callback */ |
205 |
|
Node iden_op = SygusGrammarNorm::getIdOp(dt.getSygusType()); |
206 |
|
/* If all operators are claimed, create a monomial */ |
207 |
|
if (nb_op_pos == d_elem_pos.size() + 1) |
208 |
|
{ |
209 |
|
Trace("sygus-grammar-normalize-chain") |
210 |
|
<< "\tCreating id type for " << d_elem_pos.back() << "\n"; |
211 |
|
/* creates type for element */ |
212 |
|
std::vector<unsigned> tmp; |
213 |
|
tmp.push_back(d_elem_pos.back()); |
214 |
|
TypeNode t = sygus_norm->normalizeSygusRec(to.d_tn, dt, tmp); |
215 |
|
/* consumes element */ |
216 |
|
d_elem_pos.pop_back(); |
217 |
|
/* adds to Root: "type" */ |
218 |
|
std::vector<TypeNode> ctypes; |
219 |
|
ctypes.push_back(t); |
220 |
|
to.d_sdt.addConstructor(iden_op, |
221 |
|
"id", |
222 |
|
ctypes, |
223 |
|
0); |
224 |
|
Trace("sygus-grammar-normalize-chain") |
225 |
|
<< "\tAdding " << t << " to " << to.d_unres_tn << "\n"; |
226 |
|
/* adds to Root: "type + Root" */ |
227 |
|
std::vector<TypeNode> ctypesp; |
228 |
|
ctypesp.push_back(t); |
229 |
|
ctypesp.push_back(to.d_unres_tn); |
230 |
|
to.d_sdt.addConstructor(nm->operatorOf(PLUS), kindToString(PLUS), ctypesp); |
231 |
|
Trace("sygus-grammar-normalize-chain") |
232 |
|
<< "\tAdding PLUS to " << to.d_unres_tn << " with arg types " |
233 |
|
<< to.d_unres_tn << " and " << t << "\n"; |
234 |
|
} |
235 |
|
/* In the initial case if not all operators claimed always creates a next */ |
236 |
|
Assert(nb_op_pos != d_elem_pos.size() + 1 || d_elem_pos.size() > 1); |
237 |
|
/* TODO #1304: consider case in which CHAIN op has different types than |
238 |
|
to.d_tn */ |
239 |
|
/* If no more elements to chain, finish */ |
240 |
|
if (d_elem_pos.size() == 0) |
241 |
|
{ |
242 |
|
return; |
243 |
|
} |
244 |
|
/* Creates a type do be added to root representing next step in the chain */ |
245 |
|
/* Add + to elems */ |
246 |
|
d_elem_pos.push_back(d_chain_op_pos); |
247 |
|
if (Trace.isOn("sygus-grammar-normalize-chain")) |
248 |
|
{ |
249 |
|
Trace("sygus-grammar-normalize-chain") |
250 |
|
<< "\tCreating type for next entry with sygus_ops "; |
251 |
|
for (unsigned i = 0, size = d_elem_pos.size(); i < size; ++i) |
252 |
|
{ |
253 |
|
Trace("sygus-grammar-normalize-chain") |
254 |
|
<< dt[d_elem_pos[i]].getSygusOp() << " "; |
255 |
|
} |
256 |
|
Trace("sygus-grammar-normalize-chain") << "\n"; |
257 |
|
} |
258 |
|
/* adds to Root: (\lambda x. x ) Next */ |
259 |
|
std::vector<TypeNode> ctypes; |
260 |
|
ctypes.push_back(sygus_norm->normalizeSygusRec(to.d_tn, dt, d_elem_pos)); |
261 |
|
to.d_sdt.addConstructor(iden_op, |
262 |
|
"id_next", |
263 |
|
ctypes, |
264 |
|
0); |
265 |
|
} |
266 |
|
|
267 |
7582 |
std::map<TypeNode, Node> SygusGrammarNorm::d_tn_to_id = {}; |
268 |
|
|
269 |
|
/* Traverse the constructors of dt according to the positions in op_pos. Collect |
270 |
|
* those that fit the kinds established by to_collect. Remove collected operator |
271 |
|
* positions from op_pos. Accumulate collected positions in collected |
272 |
|
* |
273 |
|
* returns true if collected anything |
274 |
|
*/ |
275 |
446 |
std::unique_ptr<SygusGrammarNorm::Transf> SygusGrammarNorm::inferTransf( |
276 |
|
TypeNode tn, const DType& dt, const std::vector<unsigned>& op_pos) |
277 |
|
{ |
278 |
446 |
NodeManager* nm = NodeManager::currentNM(); |
279 |
892 |
TypeNode sygus_tn = dt.getSygusType(); |
280 |
892 |
Trace("sygus-gnorm") << "Infer transf for " << dt.getName() << "..." |
281 |
446 |
<< std::endl; |
282 |
892 |
Trace("sygus-gnorm") << " #cons = " << op_pos.size() << " / " |
283 |
446 |
<< dt.getNumConstructors() << std::endl; |
284 |
|
// look for redundant constructors to drop |
285 |
446 |
if (options::sygusMinGrammar() && dt.getNumConstructors() == op_pos.size()) |
286 |
|
{ |
287 |
877 |
SygusRedundantCons src; |
288 |
446 |
src.initialize(d_tds, tn); |
289 |
877 |
std::vector<unsigned> rindices; |
290 |
446 |
src.getRedundant(rindices); |
291 |
446 |
if (!rindices.empty()) |
292 |
|
{ |
293 |
30 |
Trace("sygus-gnorm") << "...drop transf, " << rindices.size() << "/" |
294 |
15 |
<< op_pos.size() << " constructors." << std::endl; |
295 |
15 |
Assert(rindices.size() < op_pos.size()); |
296 |
15 |
return std::unique_ptr<Transf>(new TransfDrop(rindices)); |
297 |
|
} |
298 |
|
} |
299 |
|
|
300 |
|
// if normalization option is not enabled, we do not infer the transformations |
301 |
|
// below |
302 |
431 |
if (!options::sygusGrammarNorm()) |
303 |
|
{ |
304 |
431 |
return nullptr; |
305 |
|
} |
306 |
|
|
307 |
|
/* TODO #1304: step 1: look for singleton */ |
308 |
|
/* step 2: look for chain */ |
309 |
|
unsigned chain_op_pos = dt.getNumConstructors(); |
310 |
|
std::vector<unsigned> elem_pos; |
311 |
|
for (unsigned i = 0, size = op_pos.size(); i < size; ++i) |
312 |
|
{ |
313 |
|
Assert(op_pos[i] < dt.getNumConstructors()); |
314 |
|
Node sop = dt[op_pos[i]].getSygusOp(); |
315 |
|
/* Collects a chainable operator such as PLUS */ |
316 |
|
if (sop.getKind() == BUILTIN && TransfChain::isChainable(sygus_tn, sop)) |
317 |
|
{ |
318 |
|
Assert(nm->operatorToKind(sop) == PLUS); |
319 |
|
/* TODO #1304: be robust for this case */ |
320 |
|
/* For now only transforms applications whose arguments have the same type |
321 |
|
* as the root */ |
322 |
|
bool same_type_plus = true; |
323 |
|
const std::vector<std::shared_ptr<DTypeSelector> >& args = |
324 |
|
dt[op_pos[i]].getArgs(); |
325 |
|
for (const std::shared_ptr<DTypeSelector>& arg : args) |
326 |
|
{ |
327 |
|
if (arg->getRangeType() != tn) |
328 |
|
{ |
329 |
|
same_type_plus = false; |
330 |
|
break; |
331 |
|
} |
332 |
|
} |
333 |
|
if (!same_type_plus) |
334 |
|
{ |
335 |
|
Trace("sygus-grammar-normalize-infer") |
336 |
|
<< "\tFor OP " << PLUS << " did not collecting sop " << sop |
337 |
|
<< " in position " << op_pos[i] << "\n"; |
338 |
|
continue; |
339 |
|
} |
340 |
|
Assert(chain_op_pos == dt.getNumConstructors()); |
341 |
|
Trace("sygus-grammar-normalize-infer") |
342 |
|
<< "\tCollecting chainable OP " << sop << " in position " << op_pos[i] |
343 |
|
<< "\n"; |
344 |
|
chain_op_pos = op_pos[i]; |
345 |
|
continue; |
346 |
|
} |
347 |
|
/* TODO #1304: check this for each operator */ |
348 |
|
/* Collects elements that are not the identity (e.g. 0 is the id of PLUS) */ |
349 |
|
if (!TransfChain::isId(sygus_tn, nm->operatorOf(PLUS), sop)) |
350 |
|
{ |
351 |
|
Trace("sygus-grammar-normalize-infer") |
352 |
|
<< "\tCollecting for NON_ID_ELEMS the sop " << sop |
353 |
|
<< " in position " << op_pos[i] << "\n"; |
354 |
|
elem_pos.push_back(op_pos[i]); |
355 |
|
} |
356 |
|
} |
357 |
|
/* Typenode admits a chain transformation for normalization */ |
358 |
|
if (chain_op_pos != dt.getNumConstructors() && !elem_pos.empty()) |
359 |
|
{ |
360 |
|
Trace("sygus-gnorm") << "...chain transf." << std::endl; |
361 |
|
Trace("sygus-grammar-normalize-infer") |
362 |
|
<< "\tInfering chain transformation\n"; |
363 |
|
return std::unique_ptr<Transf>(new TransfChain(chain_op_pos, elem_pos)); |
364 |
|
} |
365 |
|
return nullptr; |
366 |
|
} |
367 |
|
|
368 |
2377 |
TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn, |
369 |
|
const DType& dt, |
370 |
|
std::vector<unsigned>& op_pos) |
371 |
|
{ |
372 |
2377 |
Assert(tn.isDatatype()); |
373 |
|
/* Corresponding type node to tn with the given operator positions. To be |
374 |
|
* retrieved (if cached) or defined (otherwise) */ |
375 |
2377 |
TypeNode unres_tn; |
376 |
2377 |
if (Trace.isOn("sygus-grammar-normalize-trie")) |
377 |
|
{ |
378 |
|
Trace("sygus-grammar-normalize-trie") |
379 |
|
<< "\tRecursing on " << tn << " with op_positions "; |
380 |
|
for (unsigned i = 0, size = op_pos.size(); i < size; ++i) |
381 |
|
{ |
382 |
|
Trace("sygus-grammar-normalize-trie") << op_pos[i] << " "; |
383 |
|
} |
384 |
|
Trace("sygus-grammar-normalize-trie") << "\n"; |
385 |
|
} |
386 |
|
/* Checks if unresolved type already created (and returns) or creates it |
387 |
|
* (and then proceeds to definition) */ |
388 |
2377 |
std::sort(op_pos.begin(), op_pos.end()); |
389 |
2377 |
if (d_tries[tn].getOrMakeType(tn, unres_tn, op_pos)) |
390 |
|
{ |
391 |
1931 |
if (Trace.isOn("sygus-grammar-normalize-trie")) |
392 |
|
{ |
393 |
|
Trace("sygus-grammar-normalize-trie") |
394 |
|
<< "\tTypenode " << tn << " has already been normalized with op_pos "; |
395 |
|
for (unsigned i = 0, size = op_pos.size(); i < size; ++i) |
396 |
|
{ |
397 |
|
Trace("sygus-grammar-normalize-trie") << op_pos[i] << " "; |
398 |
|
} |
399 |
|
Trace("sygus-grammar-normalize-trie") << " with tn " << unres_tn << "\n"; |
400 |
|
} |
401 |
1931 |
return unres_tn; |
402 |
|
} |
403 |
446 |
if (Trace.isOn("sygus-grammar-normalize-trie")) |
404 |
|
{ |
405 |
|
Trace("sygus-grammar-normalize-trie") |
406 |
|
<< "\tTypenode " << tn << " not yet normalized with op_pos "; |
407 |
|
for (unsigned i = 0, size = op_pos.size(); i < size; ++i) |
408 |
|
{ |
409 |
|
Trace("sygus-grammar-normalize-trie") << op_pos[i] << " "; |
410 |
|
} |
411 |
|
Trace("sygus-grammar-normalize-trie") << "\n"; |
412 |
|
} |
413 |
|
/* Creates type object for normalization */ |
414 |
892 |
TypeObject to(tn, unres_tn); |
415 |
|
|
416 |
446 |
if (dt.getSygusAllowConst()) |
417 |
|
{ |
418 |
84 |
TypeNode sygus_type = dt.getSygusType(); |
419 |
|
// must be handled by counterexample-guided instantiation |
420 |
|
// don't do it for Boolean (not worth the trouble, since it has only |
421 |
|
// minimal gain (1 any constant vs 2 constructors for true/false), and |
422 |
|
// we need to do a lot of special symmetry breaking, e.g. for ensuring |
423 |
|
// any constant constructors are not the 1st children of ITEs. |
424 |
126 |
if (CegInstantiator::isCbqiSort(sygus_type) >= CEG_HANDLED |
425 |
126 |
&& !sygus_type.isBoolean()) |
426 |
|
{ |
427 |
29 |
Trace("sygus-grammar-normalize") << "...add any constant constructor.\n"; |
428 |
58 |
TypeNode dtn = dt.getSygusType(); |
429 |
|
// we add this constructor first since we use left associative chains |
430 |
|
// and our symmetry breaking should group any constants together |
431 |
|
// beneath the same application |
432 |
|
// we set its weight to zero since it should be considered at the |
433 |
|
// same level as constants. |
434 |
29 |
to.d_sdt.addAnyConstantConstructor(dtn); |
435 |
|
} |
436 |
|
else |
437 |
|
{ |
438 |
|
// add default constant constructors |
439 |
26 |
std::vector<Node> ops; |
440 |
13 |
CegGrammarConstructor::mkSygusConstantsForType(sygus_type, ops); |
441 |
37 |
for (const Node& op : ops) |
442 |
|
{ |
443 |
48 |
std::stringstream ss; |
444 |
24 |
ss << op; |
445 |
48 |
std::vector<TypeNode> ctypes; |
446 |
24 |
to.d_sdt.addConstructor(op, ss.str(), ctypes); |
447 |
|
} |
448 |
|
} |
449 |
|
} |
450 |
|
|
451 |
|
/* Determine normalization transformation based on sygus type and given |
452 |
|
* operators */ |
453 |
892 |
std::unique_ptr<Transf> transformation = inferTransf(tn, dt, op_pos); |
454 |
|
/* If a transformation was selected, apply it */ |
455 |
446 |
if (transformation != nullptr) |
456 |
|
{ |
457 |
15 |
transformation->buildType(this, to, dt, op_pos); |
458 |
|
} |
459 |
|
|
460 |
|
// Remaining operators are rebuilt as they are. |
461 |
|
// Notice that we must extract the Datatype here to get the (Expr-layer) |
462 |
|
// sygus print callback. |
463 |
2584 |
for (unsigned i = 0, size = op_pos.size(); i < size; ++i) |
464 |
|
{ |
465 |
2138 |
unsigned oi = op_pos[i]; |
466 |
2138 |
Assert(oi < dt.getNumConstructors()); |
467 |
2138 |
to.addConsInfo(this, dt[oi]); |
468 |
|
} |
469 |
|
/* Build normalize datatype */ |
470 |
446 |
if (Trace.isOn("sygus-grammar-normalize")) |
471 |
|
{ |
472 |
|
Trace("sygus-grammar-normalize") << "\nFor positions "; |
473 |
|
for (unsigned i = 0, size = op_pos.size(); i < size; ++i) |
474 |
|
{ |
475 |
|
Trace("sygus-grammar-normalize") << op_pos[i] << " "; |
476 |
|
} |
477 |
|
Trace("sygus-grammar-normalize") << " and datatype " << dt << " \n"; |
478 |
|
} |
479 |
446 |
to.initializeDatatype(this, dt); |
480 |
446 |
return unres_tn; |
481 |
|
} |
482 |
|
|
483 |
2377 |
TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn) |
484 |
|
{ |
485 |
2377 |
if (!tn.isDatatype()) |
486 |
|
{ |
487 |
|
// Might not be a sygus datatype, e.g. if the input grammar had the |
488 |
|
// any constant constructor. |
489 |
|
return tn; |
490 |
|
} |
491 |
|
/* Collect all operators for normalization */ |
492 |
2377 |
const DType& dt = tn.getDType(); |
493 |
2377 |
if (!dt.isSygus()) |
494 |
|
{ |
495 |
|
// datatype but not sygus datatype case |
496 |
|
return tn; |
497 |
|
} |
498 |
4754 |
std::vector<unsigned> op_pos(dt.getNumConstructors()); |
499 |
2377 |
std::iota(op_pos.begin(), op_pos.end(), 0); |
500 |
2377 |
return normalizeSygusRec(tn, dt, op_pos); |
501 |
|
} |
502 |
|
|
503 |
202 |
TypeNode SygusGrammarNorm::normalizeSygusType(TypeNode tn, Node sygus_vars) |
504 |
|
{ |
505 |
|
/* Normalize all types in tn */ |
506 |
202 |
d_sygus_vars = sygus_vars; |
507 |
202 |
normalizeSygusRec(tn); |
508 |
|
/* Resolve created types */ |
509 |
202 |
Assert(!d_dt_all.empty() && !d_unres_t_all.empty()); |
510 |
202 |
if (Trace.isOn("sygus-grammar-normalize-build")) |
511 |
|
{ |
512 |
|
Trace("sygus-grammar-normalize-build") |
513 |
|
<< "making mutual datatyes with datatypes \n"; |
514 |
|
for (unsigned i = 0, size = d_dt_all.size(); i < size; ++i) |
515 |
|
{ |
516 |
|
Trace("sygus-grammar-normalize-build") << d_dt_all[i]; |
517 |
|
} |
518 |
|
Trace("sygus-grammar-normalize-build") << " and unresolved types\n"; |
519 |
|
for (const TypeNode& unres_t : d_unres_t_all) |
520 |
|
{ |
521 |
|
Trace("sygus-grammar-normalize-build") << unres_t << " "; |
522 |
|
} |
523 |
|
Trace("sygus-grammar-normalize-build") << "\n"; |
524 |
|
} |
525 |
202 |
Assert(d_dt_all.size() == d_unres_t_all.size()); |
526 |
|
std::vector<TypeNode> types = NodeManager::currentNM()->mkMutualDatatypeTypes( |
527 |
404 |
d_dt_all, d_unres_t_all, NodeManager::DATATYPE_FLAG_PLACEHOLDER); |
528 |
202 |
Assert(types.size() == d_dt_all.size()); |
529 |
|
/* Clear accumulators */ |
530 |
202 |
d_dt_all.clear(); |
531 |
202 |
d_unres_t_all.clear(); |
532 |
|
/* By construction the normalized type node will be the last one considered */ |
533 |
404 |
return types.back(); |
534 |
|
} |
535 |
|
|
536 |
|
} // namespace quantifiers |
537 |
|
} // namespace theory |
538 |
22746 |
} // namespace cvc5 |