1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Mathias Preiner, Aina Niemetz |
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 rewriter for the theory of (co)inductive datatypes. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/datatypes/sygus_datatype_utils.h" |
17 |
|
|
18 |
|
#include <sstream> |
19 |
|
|
20 |
|
#include "expr/dtype.h" |
21 |
|
#include "expr/dtype_cons.h" |
22 |
|
#include "expr/node_algorithm.h" |
23 |
|
#include "expr/sygus_datatype.h" |
24 |
|
#include "smt/env.h" |
25 |
|
#include "theory/evaluator.h" |
26 |
|
#include "theory/rewriter.h" |
27 |
|
|
28 |
|
using namespace cvc5; |
29 |
|
using namespace cvc5::kind; |
30 |
|
|
31 |
|
namespace cvc5 { |
32 |
|
namespace theory { |
33 |
|
namespace datatypes { |
34 |
|
namespace utils { |
35 |
|
|
36 |
89753 |
Node applySygusArgs(const DType& dt, |
37 |
|
Node op, |
38 |
|
Node n, |
39 |
|
const std::vector<Node>& args) |
40 |
|
{ |
41 |
|
// optimization: if n is just a sygus bound variable, return immediately |
42 |
|
// by replacing with the proper argument, or returning unchanged if it is |
43 |
|
// a bound variable not corresponding to a formal argument. |
44 |
89753 |
if (n.getKind() == BOUND_VARIABLE) |
45 |
|
{ |
46 |
1630 |
if (n.hasAttribute(SygusVarNumAttribute())) |
47 |
|
{ |
48 |
1518 |
int vn = n.getAttribute(SygusVarNumAttribute()); |
49 |
1518 |
Assert(dt.getSygusVarList()[vn] == n); |
50 |
1518 |
return args[vn]; |
51 |
|
} |
52 |
|
// it is a different bound variable, it is unchanged |
53 |
112 |
return n; |
54 |
|
} |
55 |
|
// n is an application of operator op. |
56 |
|
// We must compute the free variables in op to determine if there are |
57 |
|
// any substitutions we need to make to n. |
58 |
176246 |
TNode val; |
59 |
88123 |
if (!op.hasAttribute(SygusVarFreeAttribute())) |
60 |
|
{ |
61 |
1750 |
std::unordered_set<Node> fvs; |
62 |
875 |
if (expr::getFreeVariables(op, fvs)) |
63 |
|
{ |
64 |
22 |
if (fvs.size() == 1) |
65 |
|
{ |
66 |
24 |
for (const Node& v : fvs) |
67 |
|
{ |
68 |
12 |
val = v; |
69 |
|
} |
70 |
|
} |
71 |
|
else |
72 |
|
{ |
73 |
10 |
val = op; |
74 |
|
} |
75 |
|
} |
76 |
875 |
Trace("dt-sygus-fv") << "Free var in " << op << " : " << val << std::endl; |
77 |
875 |
op.setAttribute(SygusVarFreeAttribute(), val); |
78 |
|
} |
79 |
|
else |
80 |
|
{ |
81 |
87248 |
val = op.getAttribute(SygusVarFreeAttribute()); |
82 |
|
} |
83 |
88123 |
if (val.isNull()) |
84 |
|
{ |
85 |
87507 |
return n; |
86 |
|
} |
87 |
616 |
if (val.getKind() == BOUND_VARIABLE) |
88 |
|
{ |
89 |
|
// single substitution case |
90 |
324 |
int vn = val.getAttribute(SygusVarNumAttribute()); |
91 |
648 |
TNode sub = args[vn]; |
92 |
324 |
return n.substitute(val, sub); |
93 |
|
} |
94 |
|
// do the full substitution |
95 |
584 |
std::vector<Node> vars; |
96 |
584 |
Node bvl = dt.getSygusVarList(); |
97 |
984 |
for (unsigned i = 0, nvars = bvl.getNumChildren(); i < nvars; i++) |
98 |
|
{ |
99 |
692 |
vars.push_back(bvl[i]); |
100 |
|
} |
101 |
292 |
return n.substitute(vars.begin(), vars.end(), args.begin(), args.end()); |
102 |
|
} |
103 |
|
|
104 |
217 |
Kind getOperatorKindForSygusBuiltin(Node op) |
105 |
|
{ |
106 |
217 |
Assert(op.getKind() != BUILTIN); |
107 |
217 |
if (op.getKind() == LAMBDA) |
108 |
|
{ |
109 |
|
return APPLY_UF; |
110 |
|
} |
111 |
217 |
return NodeManager::getKindForFunction(op); |
112 |
|
} |
113 |
|
|
114 |
221644 |
Kind getEliminateKind(Kind ok) |
115 |
|
{ |
116 |
221644 |
Kind nk = ok; |
117 |
|
// We also must ensure that builtin operators which are eliminated |
118 |
|
// during expand definitions are replaced by the proper operator. |
119 |
221644 |
if (ok == DIVISION) |
120 |
|
{ |
121 |
105 |
nk = DIVISION_TOTAL; |
122 |
|
} |
123 |
221539 |
else if (ok == INTS_DIVISION) |
124 |
|
{ |
125 |
|
nk = INTS_DIVISION_TOTAL; |
126 |
|
} |
127 |
221539 |
else if (ok == INTS_MODULUS) |
128 |
|
{ |
129 |
|
nk = INTS_MODULUS_TOTAL; |
130 |
|
} |
131 |
221644 |
return nk; |
132 |
|
} |
133 |
|
|
134 |
762827 |
Node mkSygusTerm(const DType& dt, |
135 |
|
unsigned i, |
136 |
|
const std::vector<Node>& children, |
137 |
|
bool doBetaReduction, |
138 |
|
bool isExternal) |
139 |
|
{ |
140 |
1525654 |
Trace("dt-sygus-util") << "Make sygus term " << dt.getName() << "[" << i |
141 |
762827 |
<< "] with children: " << children << std::endl; |
142 |
762827 |
Assert(i < dt.getNumConstructors()); |
143 |
762827 |
Assert(dt.isSygus()); |
144 |
762827 |
Assert(!dt[i].getSygusOp().isNull()); |
145 |
1525654 |
Node op = dt[i].getSygusOp(); |
146 |
1525654 |
Node opn = op; |
147 |
762827 |
if (!isExternal) |
148 |
|
{ |
149 |
|
// Get the normalized version of the sygus operator. We do this by |
150 |
|
// expanding definitions, rewriting it, and eliminating partial operators. |
151 |
755059 |
if (op.isConst()) |
152 |
|
{ |
153 |
|
// If it is a builtin operator, convert to total version if necessary. |
154 |
|
// First, get the kind for the operator. |
155 |
221644 |
Kind ok = NodeManager::operatorToKind(op); |
156 |
443288 |
Trace("sygus-grammar-normalize-debug") |
157 |
221644 |
<< "...builtin kind is " << ok << std::endl; |
158 |
221644 |
Kind nk = getEliminateKind(ok); |
159 |
221644 |
if (nk != ok) |
160 |
|
{ |
161 |
210 |
Trace("sygus-grammar-normalize-debug") |
162 |
105 |
<< "...replace by builtin operator " << nk << std::endl; |
163 |
105 |
opn = NodeManager::currentNM()->operatorOf(nk); |
164 |
|
} |
165 |
|
} |
166 |
|
else |
167 |
|
{ |
168 |
|
// Get the expanded definition form, if it has been marked. This ensures |
169 |
|
// that user-defined functions have been eliminated from op. |
170 |
533415 |
opn = getExpandedDefinitionForm(op); |
171 |
|
} |
172 |
|
} |
173 |
1525654 |
return mkSygusTerm(opn, children, doBetaReduction); |
174 |
|
} |
175 |
|
|
176 |
762831 |
Node mkSygusTerm(Node op, |
177 |
|
const std::vector<Node>& children, |
178 |
|
bool doBetaReduction) |
179 |
|
{ |
180 |
762831 |
Trace("dt-sygus-util") << "Operator is " << op << std::endl; |
181 |
762831 |
if (children.empty()) |
182 |
|
{ |
183 |
|
// no children, return immediately |
184 |
168817 |
Trace("dt-sygus-util") << "...return direct op" << std::endl; |
185 |
168817 |
return op; |
186 |
|
} |
187 |
|
// if it is the any constant, we simply return the child |
188 |
594014 |
if (op.getAttribute(SygusAnyConstAttribute())) |
189 |
|
{ |
190 |
640 |
Assert(children.size() == 1); |
191 |
640 |
return children[0]; |
192 |
|
} |
193 |
1186748 |
std::vector<Node> schildren; |
194 |
|
// get the kind of the operator |
195 |
593374 |
Kind ok = op.getKind(); |
196 |
593374 |
if (ok != BUILTIN) |
197 |
|
{ |
198 |
530567 |
if (ok == LAMBDA && doBetaReduction) |
199 |
|
{ |
200 |
|
// Do immediate beta reduction. It suffices to use a normal substitution |
201 |
|
// since neither op nor children have quantifiers, since they are |
202 |
|
// generated by sygus grammars. |
203 |
1057326 |
std::vector<Node> vars{op[0].begin(), op[0].end()}; |
204 |
528663 |
Assert(vars.size() == children.size()); |
205 |
|
Node ret = op[1].substitute( |
206 |
1057326 |
vars.begin(), vars.end(), children.begin(), children.end()); |
207 |
528663 |
Trace("dt-sygus-util") << "...return (beta-reduce) " << ret << std::endl; |
208 |
528663 |
return ret; |
209 |
|
} |
210 |
|
else |
211 |
|
{ |
212 |
1904 |
schildren.push_back(op); |
213 |
|
} |
214 |
|
} |
215 |
64711 |
schildren.insert(schildren.end(), children.begin(), children.end()); |
216 |
129422 |
Node ret; |
217 |
64711 |
if (ok == BUILTIN) |
218 |
|
{ |
219 |
62807 |
ret = NodeManager::currentNM()->mkNode(op, schildren); |
220 |
62807 |
Trace("dt-sygus-util") << "...return (builtin) " << ret << std::endl; |
221 |
62807 |
return ret; |
222 |
|
} |
223 |
|
// get the kind used for applying op |
224 |
1904 |
Kind otk = NodeManager::operatorToKind(op); |
225 |
1904 |
Trace("dt-sygus-util") << "operator kind is " << otk << std::endl; |
226 |
1904 |
if (otk != UNDEFINED_KIND) |
227 |
|
{ |
228 |
|
// If it is an APPLY_UF operator, we should have at least an operator and |
229 |
|
// a child. |
230 |
1687 |
Assert(otk != APPLY_UF || schildren.size() != 1); |
231 |
1687 |
ret = NodeManager::currentNM()->mkNode(otk, schildren); |
232 |
1687 |
Trace("dt-sygus-util") << "...return (op) " << ret << std::endl; |
233 |
1687 |
return ret; |
234 |
|
} |
235 |
217 |
Kind tok = getOperatorKindForSygusBuiltin(op); |
236 |
217 |
if (schildren.size() == 1 && tok == UNDEFINED_KIND) |
237 |
|
{ |
238 |
|
ret = schildren[0]; |
239 |
|
} |
240 |
|
else |
241 |
|
{ |
242 |
217 |
ret = NodeManager::currentNM()->mkNode(tok, schildren); |
243 |
|
} |
244 |
217 |
Trace("dt-sygus-util") << "...return " << ret << std::endl; |
245 |
217 |
return ret; |
246 |
|
} |
247 |
|
|
248 |
|
struct SygusToBuiltinTermAttributeId |
249 |
|
{ |
250 |
|
}; |
251 |
|
typedef expr::Attribute<SygusToBuiltinTermAttributeId, Node> |
252 |
|
SygusToBuiltinTermAttribute; |
253 |
|
|
254 |
|
// A variant of the above attribute for cases where we introduce a fresh |
255 |
|
// variable. This is to support sygusToBuiltin on non-constant sygus terms, |
256 |
|
// where sygus variables should be mapped to canonical builtin variables. |
257 |
|
// It is important to cache this so that sygusToBuiltin is deterministic. |
258 |
|
struct SygusToBuiltinVarAttributeId |
259 |
|
{ |
260 |
|
}; |
261 |
|
typedef expr::Attribute<SygusToBuiltinVarAttributeId, Node> |
262 |
|
SygusToBuiltinVarAttribute; |
263 |
|
|
264 |
|
// A variant of the above attribute for cases where we introduce a fresh |
265 |
|
// variable. This is to support sygusToBuiltin on non-constant sygus terms, |
266 |
|
// where sygus variables should be mapped to canonical builtin variables. |
267 |
|
// It is important to cache this so that sygusToBuiltin is deterministic. |
268 |
|
struct BuiltinVarToSygusAttributeId |
269 |
|
{ |
270 |
|
}; |
271 |
|
typedef expr::Attribute<BuiltinVarToSygusAttributeId, Node> |
272 |
|
BuiltinVarToSygusAttribute; |
273 |
|
|
274 |
460352 |
Node sygusToBuiltin(Node n, bool isExternal) |
275 |
|
{ |
276 |
920704 |
std::unordered_map<TNode, Node> visited; |
277 |
460352 |
std::unordered_map<TNode, Node>::iterator it; |
278 |
920704 |
std::vector<TNode> visit; |
279 |
920704 |
TNode cur; |
280 |
|
unsigned index; |
281 |
460352 |
visit.push_back(n); |
282 |
270524 |
do |
283 |
|
{ |
284 |
730876 |
cur = visit.back(); |
285 |
730876 |
visit.pop_back(); |
286 |
730876 |
it = visited.find(cur); |
287 |
730876 |
if (it == visited.end()) |
288 |
|
{ |
289 |
|
// Notice this condition succeeds in roughly 99% of the executions of this |
290 |
|
// method (based on our coverage tests), hence the else if / else cases |
291 |
|
// below do not significantly impact performance. |
292 |
629968 |
if (cur.getKind() == APPLY_CONSTRUCTOR) |
293 |
|
{ |
294 |
620984 |
if (!isExternal && cur.hasAttribute(SygusToBuiltinTermAttribute())) |
295 |
|
{ |
296 |
525548 |
visited[cur] = cur.getAttribute(SygusToBuiltinTermAttribute()); |
297 |
|
} |
298 |
|
else |
299 |
|
{ |
300 |
95436 |
visited[cur] = Node::null(); |
301 |
95436 |
visit.push_back(cur); |
302 |
270524 |
for (const Node& cn : cur) |
303 |
|
{ |
304 |
175088 |
visit.push_back(cn); |
305 |
|
} |
306 |
|
} |
307 |
|
} |
308 |
8984 |
else if (cur.getType().isSygusDatatype()) |
309 |
|
{ |
310 |
8388 |
Assert (cur.isVar()); |
311 |
8388 |
if (cur.hasAttribute(SygusToBuiltinVarAttribute())) |
312 |
|
{ |
313 |
|
// use the previously constructed variable for it |
314 |
8263 |
visited[cur] = cur.getAttribute(SygusToBuiltinVarAttribute()); |
315 |
|
} |
316 |
|
else |
317 |
|
{ |
318 |
250 |
std::stringstream ss; |
319 |
125 |
ss << cur; |
320 |
125 |
const DType& dt = cur.getType().getDType(); |
321 |
|
// make a fresh variable |
322 |
125 |
NodeManager * nm = NodeManager::currentNM(); |
323 |
250 |
Node var = nm->mkBoundVar(ss.str(), dt.getSygusType()); |
324 |
|
SygusToBuiltinVarAttribute stbv; |
325 |
125 |
cur.setAttribute(stbv, var); |
326 |
125 |
visited[cur] = var; |
327 |
|
// create backwards mapping |
328 |
|
BuiltinVarToSygusAttribute bvtsa; |
329 |
125 |
var.setAttribute(bvtsa, cur); |
330 |
|
} |
331 |
|
} |
332 |
|
else |
333 |
|
{ |
334 |
|
// non-datatypes are themselves |
335 |
596 |
visited[cur] = cur; |
336 |
|
} |
337 |
|
} |
338 |
100908 |
else if (it->second.isNull()) |
339 |
|
{ |
340 |
190872 |
Node ret = cur; |
341 |
95436 |
Assert(cur.getKind() == APPLY_CONSTRUCTOR); |
342 |
95436 |
const DType& dt = cur.getType().getDType(); |
343 |
|
// Non sygus-datatype terms are also themselves. Notice we treat the |
344 |
|
// case of non-sygus datatypes this way since it avoids computing |
345 |
|
// the type / datatype of the node in the pre-traversal above. The |
346 |
|
// case of non-sygus datatypes is very rare, so the extra addition to |
347 |
|
// visited is justified performance-wise. |
348 |
95436 |
if (dt.isSygus()) |
349 |
|
{ |
350 |
190872 |
std::vector<Node> children; |
351 |
270524 |
for (const Node& cn : cur) |
352 |
|
{ |
353 |
175088 |
it = visited.find(cn); |
354 |
175088 |
Assert(it != visited.end()); |
355 |
175088 |
Assert(!it->second.isNull()); |
356 |
175088 |
children.push_back(it->second); |
357 |
|
} |
358 |
95436 |
index = indexOf(cur.getOperator()); |
359 |
95436 |
ret = mkSygusTerm(dt, index, children, true, isExternal); |
360 |
|
} |
361 |
95436 |
visited[cur] = ret; |
362 |
|
// cache |
363 |
95436 |
if (!isExternal) |
364 |
|
{ |
365 |
|
SygusToBuiltinTermAttribute stbt; |
366 |
87668 |
cur.setAttribute(stbt, ret); |
367 |
|
} |
368 |
|
} |
369 |
730876 |
} while (!visit.empty()); |
370 |
460352 |
Assert(visited.find(n) != visited.end()); |
371 |
460352 |
Assert(!visited.find(n)->second.isNull()); |
372 |
920704 |
return visited[n]; |
373 |
|
} |
374 |
|
|
375 |
237 |
Node builtinVarToSygus(Node v) |
376 |
|
{ |
377 |
|
BuiltinVarToSygusAttribute bvtsa; |
378 |
237 |
if (v.hasAttribute(bvtsa)) |
379 |
|
{ |
380 |
237 |
return v.getAttribute(bvtsa); |
381 |
|
} |
382 |
|
return Node::null(); |
383 |
|
} |
384 |
|
|
385 |
|
void getFreeSymbolsSygusType(TypeNode sdt, std::unordered_set<Node>& syms) |
386 |
|
{ |
387 |
|
// datatype types we need to process |
388 |
|
std::vector<TypeNode> typeToProcess; |
389 |
|
// datatype types we have processed |
390 |
|
std::map<TypeNode, TypeNode> typesProcessed; |
391 |
|
typeToProcess.push_back(sdt); |
392 |
|
while (!typeToProcess.empty()) |
393 |
|
{ |
394 |
|
std::vector<TypeNode> typeNextToProcess; |
395 |
|
for (const TypeNode& curr : typeToProcess) |
396 |
|
{ |
397 |
|
Assert(curr.isDatatype() && curr.getDType().isSygus()); |
398 |
|
const DType& dtc = curr.getDType(); |
399 |
|
for (unsigned j = 0, ncons = dtc.getNumConstructors(); j < ncons; j++) |
400 |
|
{ |
401 |
|
// collect the symbols from the operator |
402 |
|
Node op = dtc[j].getSygusOp(); |
403 |
|
expr::getSymbols(op, syms); |
404 |
|
// traverse the argument types |
405 |
|
for (unsigned k = 0, nargs = dtc[j].getNumArgs(); k < nargs; k++) |
406 |
|
{ |
407 |
|
TypeNode argt = dtc[j].getArgType(k); |
408 |
|
if (!argt.isDatatype() || !argt.getDType().isSygus()) |
409 |
|
{ |
410 |
|
// not a sygus datatype |
411 |
|
continue; |
412 |
|
} |
413 |
|
if (typesProcessed.find(argt) == typesProcessed.end()) |
414 |
|
{ |
415 |
|
typeNextToProcess.push_back(argt); |
416 |
|
} |
417 |
|
} |
418 |
|
} |
419 |
|
} |
420 |
|
typeToProcess.clear(); |
421 |
|
typeToProcess.insert(typeToProcess.end(), |
422 |
|
typeNextToProcess.begin(), |
423 |
|
typeNextToProcess.end()); |
424 |
|
} |
425 |
|
} |
426 |
|
|
427 |
11 |
TypeNode substituteAndGeneralizeSygusType(TypeNode sdt, |
428 |
|
const std::vector<Node>& syms, |
429 |
|
const std::vector<Node>& vars) |
430 |
|
{ |
431 |
11 |
NodeManager* nm = NodeManager::currentNM(); |
432 |
11 |
const DType& sdtd = sdt.getDType(); |
433 |
|
// compute the new formal argument list |
434 |
22 |
std::vector<Node> formalVars; |
435 |
22 |
Node prevVarList = sdtd.getSygusVarList(); |
436 |
11 |
if (!prevVarList.isNull()) |
437 |
|
{ |
438 |
|
for (const Node& v : prevVarList) |
439 |
|
{ |
440 |
|
// if it is not being replaced |
441 |
|
if (std::find(syms.begin(), syms.end(), v) != syms.end()) |
442 |
|
{ |
443 |
|
formalVars.push_back(v); |
444 |
|
} |
445 |
|
} |
446 |
|
} |
447 |
49 |
for (const Node& v : vars) |
448 |
|
{ |
449 |
38 |
if (v.getKind() == BOUND_VARIABLE) |
450 |
|
{ |
451 |
38 |
formalVars.push_back(v); |
452 |
|
} |
453 |
|
} |
454 |
|
// make the sygus variable list for the formal argument list |
455 |
22 |
Node abvl = nm->mkNode(BOUND_VAR_LIST, formalVars); |
456 |
11 |
Trace("sygus-abduct-debug") << "...finish" << std::endl; |
457 |
|
|
458 |
|
// must convert all constructors to version with variables in "vars" |
459 |
22 |
std::vector<SygusDatatype> sdts; |
460 |
22 |
std::set<TypeNode> unres; |
461 |
|
|
462 |
11 |
Trace("dtsygus-gen-debug") << "Process sygus type:" << std::endl; |
463 |
11 |
Trace("dtsygus-gen-debug") << sdtd.getName() << std::endl; |
464 |
|
|
465 |
|
// datatype types we need to process |
466 |
22 |
std::vector<TypeNode> dtToProcess; |
467 |
|
// datatype types we have processed |
468 |
22 |
std::map<TypeNode, TypeNode> dtProcessed; |
469 |
11 |
dtToProcess.push_back(sdt); |
470 |
22 |
std::stringstream ssutn0; |
471 |
11 |
ssutn0 << sdtd.getName() << "_s"; |
472 |
|
TypeNode abdTNew = |
473 |
22 |
nm->mkSort(ssutn0.str(), NodeManager::SORT_FLAG_PLACEHOLDER); |
474 |
11 |
unres.insert(abdTNew); |
475 |
11 |
dtProcessed[sdt] = abdTNew; |
476 |
|
|
477 |
|
// We must convert all symbols in the sygus datatype type sdt to |
478 |
|
// apply the substitution { syms -> vars }, where syms is the free |
479 |
|
// variables of the input problem, and vars is the formal argument list |
480 |
|
// of the function-to-synthesize. |
481 |
|
|
482 |
|
// We are traversing over the subfield types of the datatype to convert |
483 |
|
// them into the form described above. |
484 |
51 |
while (!dtToProcess.empty()) |
485 |
|
{ |
486 |
40 |
std::vector<TypeNode> dtNextToProcess; |
487 |
42 |
for (const TypeNode& curr : dtToProcess) |
488 |
|
{ |
489 |
22 |
Assert(curr.isDatatype() && curr.getDType().isSygus()); |
490 |
22 |
const DType& dtc = curr.getDType(); |
491 |
44 |
std::stringstream ssdtn; |
492 |
22 |
ssdtn << dtc.getName() << "_s"; |
493 |
22 |
sdts.push_back(SygusDatatype(ssdtn.str())); |
494 |
44 |
Trace("dtsygus-gen-debug") |
495 |
22 |
<< "Process datatype " << sdts.back().getName() << "..." << std::endl; |
496 |
76 |
for (unsigned j = 0, ncons = dtc.getNumConstructors(); j < ncons; j++) |
497 |
|
{ |
498 |
108 |
Node op = dtc[j].getSygusOp(); |
499 |
|
// apply the substitution to the argument |
500 |
|
Node ops = |
501 |
108 |
op.substitute(syms.begin(), syms.end(), vars.begin(), vars.end()); |
502 |
108 |
Trace("dtsygus-gen-debug") << " Process constructor " << op << " / " |
503 |
54 |
<< ops << "..." << std::endl; |
504 |
108 |
std::vector<TypeNode> cargs; |
505 |
92 |
for (unsigned k = 0, nargs = dtc[j].getNumArgs(); k < nargs; k++) |
506 |
|
{ |
507 |
76 |
TypeNode argt = dtc[j].getArgType(k); |
508 |
38 |
std::map<TypeNode, TypeNode>::iterator itdp = dtProcessed.find(argt); |
509 |
76 |
TypeNode argtNew; |
510 |
38 |
if (itdp == dtProcessed.end()) |
511 |
|
{ |
512 |
22 |
std::stringstream ssutn; |
513 |
11 |
ssutn << argt.getDType().getName() << "_s"; |
514 |
11 |
argtNew = |
515 |
22 |
nm->mkSort(ssutn.str(), NodeManager::SORT_FLAG_PLACEHOLDER); |
516 |
22 |
Trace("dtsygus-gen-debug") << " ...unresolved type " << argtNew |
517 |
11 |
<< " for " << argt << std::endl; |
518 |
11 |
unres.insert(argtNew); |
519 |
11 |
dtProcessed[argt] = argtNew; |
520 |
11 |
dtNextToProcess.push_back(argt); |
521 |
|
} |
522 |
|
else |
523 |
|
{ |
524 |
27 |
argtNew = itdp->second; |
525 |
|
} |
526 |
76 |
Trace("dtsygus-gen-debug") |
527 |
38 |
<< " Arg #" << k << ": " << argtNew << std::endl; |
528 |
38 |
cargs.push_back(argtNew); |
529 |
|
} |
530 |
108 |
std::stringstream ss; |
531 |
54 |
ss << ops.getKind(); |
532 |
54 |
Trace("dtsygus-gen-debug") << "Add constructor : " << ops << std::endl; |
533 |
54 |
sdts.back().addConstructor(ops, ss.str(), cargs); |
534 |
|
} |
535 |
44 |
Trace("dtsygus-gen-debug") |
536 |
22 |
<< "Set sygus : " << dtc.getSygusType() << " " << abvl << std::endl; |
537 |
44 |
TypeNode stn = dtc.getSygusType(); |
538 |
66 |
sdts.back().initializeDatatype( |
539 |
44 |
stn, abvl, dtc.getSygusAllowConst(), dtc.getSygusAllowAll()); |
540 |
|
} |
541 |
20 |
dtToProcess.clear(); |
542 |
20 |
dtToProcess.insert( |
543 |
40 |
dtToProcess.end(), dtNextToProcess.begin(), dtNextToProcess.end()); |
544 |
|
} |
545 |
22 |
Trace("dtsygus-gen-debug") |
546 |
11 |
<< "Make " << sdts.size() << " datatype types..." << std::endl; |
547 |
|
// extract the datatypes |
548 |
22 |
std::vector<DType> datatypes; |
549 |
33 |
for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++) |
550 |
|
{ |
551 |
22 |
datatypes.push_back(sdts[i].getDatatype()); |
552 |
|
} |
553 |
|
// make the datatype types |
554 |
|
std::vector<TypeNode> datatypeTypes = nm->mkMutualDatatypeTypes( |
555 |
22 |
datatypes, unres, NodeManager::DATATYPE_FLAG_PLACEHOLDER); |
556 |
11 |
TypeNode sdtS = datatypeTypes[0]; |
557 |
11 |
if (Trace.isOn("dtsygus-gen-debug")) |
558 |
|
{ |
559 |
|
Trace("dtsygus-gen-debug") << "Made datatype types:" << std::endl; |
560 |
|
for (unsigned j = 0, ndts = datatypeTypes.size(); j < ndts; j++) |
561 |
|
{ |
562 |
|
const DType& dtj = datatypeTypes[j].getDType(); |
563 |
|
Trace("dtsygus-gen-debug") << "#" << j << ": " << dtj << std::endl; |
564 |
|
for (unsigned k = 0, ncons = dtj.getNumConstructors(); k < ncons; k++) |
565 |
|
{ |
566 |
|
for (unsigned l = 0, nargs = dtj[k].getNumArgs(); l < nargs; l++) |
567 |
|
{ |
568 |
|
if (!dtj[k].getArgType(l).isDatatype()) |
569 |
|
{ |
570 |
|
Trace("dtsygus-gen-debug") |
571 |
|
<< "Argument " << l << " of " << dtj[k] |
572 |
|
<< " is not datatype : " << dtj[k].getArgType(l) << std::endl; |
573 |
|
AlwaysAssert(false); |
574 |
|
} |
575 |
|
} |
576 |
|
} |
577 |
|
} |
578 |
|
} |
579 |
22 |
return sdtS; |
580 |
|
} |
581 |
|
|
582 |
458045 |
unsigned getSygusTermSize(Node n) |
583 |
|
{ |
584 |
458045 |
if (n.getKind() != APPLY_CONSTRUCTOR) |
585 |
|
{ |
586 |
21915 |
return 0; |
587 |
|
} |
588 |
436130 |
unsigned sum = 0; |
589 |
724371 |
for (const Node& nc : n) |
590 |
|
{ |
591 |
288241 |
sum += getSygusTermSize(nc); |
592 |
|
} |
593 |
436130 |
const DType& dt = datatypeOf(n.getOperator()); |
594 |
436130 |
int cindex = indexOf(n.getOperator()); |
595 |
436130 |
Assert(cindex >= 0 && static_cast<size_t>(cindex) < dt.getNumConstructors()); |
596 |
436130 |
unsigned weight = dt[cindex].getWeight(); |
597 |
436130 |
return weight + sum; |
598 |
|
} |
599 |
|
|
600 |
|
/** |
601 |
|
* Map terms to the result of expand definitions calling smt::expandDefinitions |
602 |
|
* on it. |
603 |
|
*/ |
604 |
|
struct SygusExpDefFormAttributeId |
605 |
|
{ |
606 |
|
}; |
607 |
|
typedef expr::Attribute<SygusExpDefFormAttributeId, Node> |
608 |
|
SygusExpDefFormAttribute; |
609 |
|
|
610 |
4331 |
void setExpandedDefinitionForm(Node op, Node eop) |
611 |
|
{ |
612 |
4331 |
op.setAttribute(SygusExpDefFormAttribute(), eop); |
613 |
4331 |
} |
614 |
|
|
615 |
533415 |
Node getExpandedDefinitionForm(Node op) |
616 |
|
{ |
617 |
1066830 |
Node eop = op.getAttribute(SygusExpDefFormAttribute()); |
618 |
|
// if not set, assume original |
619 |
1066830 |
return eop.isNull() ? op : eop; |
620 |
|
} |
621 |
|
|
622 |
|
} // namespace utils |
623 |
|
} // namespace datatypes |
624 |
|
} // namespace theory |
625 |
31125 |
} // namespace cvc5 |