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