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 |
29891 |
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 |
29891 |
if (n.getKind() == BOUND_VARIABLE) |
45 |
|
{ |
46 |
917 |
if (n.hasAttribute(SygusVarNumAttribute())) |
47 |
|
{ |
48 |
820 |
int vn = n.getAttribute(SygusVarNumAttribute()); |
49 |
820 |
Assert(dt.getSygusVarList()[vn] == n); |
50 |
820 |
return args[vn]; |
51 |
|
} |
52 |
|
// it is a different bound variable, it is unchanged |
53 |
97 |
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 |
57948 |
TNode val; |
59 |
28974 |
if (!op.hasAttribute(SygusVarFreeAttribute())) |
60 |
|
{ |
61 |
916 |
std::unordered_set<Node> fvs; |
62 |
458 |
if (expr::getFreeVariables(op, fvs)) |
63 |
|
{ |
64 |
11 |
if (fvs.size() == 1) |
65 |
|
{ |
66 |
12 |
for (const Node& v : fvs) |
67 |
|
{ |
68 |
6 |
val = v; |
69 |
|
} |
70 |
|
} |
71 |
|
else |
72 |
|
{ |
73 |
5 |
val = op; |
74 |
|
} |
75 |
|
} |
76 |
458 |
Trace("dt-sygus-fv") << "Free var in " << op << " : " << val << std::endl; |
77 |
458 |
op.setAttribute(SygusVarFreeAttribute(), val); |
78 |
|
} |
79 |
|
else |
80 |
|
{ |
81 |
28516 |
val = op.getAttribute(SygusVarFreeAttribute()); |
82 |
|
} |
83 |
28974 |
if (val.isNull()) |
84 |
|
{ |
85 |
28609 |
return n; |
86 |
|
} |
87 |
365 |
if (val.getKind() == BOUND_VARIABLE) |
88 |
|
{ |
89 |
|
// single substitution case |
90 |
201 |
int vn = val.getAttribute(SygusVarNumAttribute()); |
91 |
402 |
TNode sub = args[vn]; |
92 |
201 |
return n.substitute(val, sub); |
93 |
|
} |
94 |
|
// do the full substitution |
95 |
328 |
std::vector<Node> vars; |
96 |
328 |
Node bvl = dt.getSygusVarList(); |
97 |
564 |
for (unsigned i = 0, nvars = bvl.getNumChildren(); i < nvars; i++) |
98 |
|
{ |
99 |
400 |
vars.push_back(bvl[i]); |
100 |
|
} |
101 |
164 |
return n.substitute(vars.begin(), vars.end(), args.begin(), args.end()); |
102 |
|
} |
103 |
|
|
104 |
131 |
Kind getOperatorKindForSygusBuiltin(Node op) |
105 |
|
{ |
106 |
131 |
Assert(op.getKind() != BUILTIN); |
107 |
131 |
if (op.getKind() == LAMBDA) |
108 |
|
{ |
109 |
|
return APPLY_UF; |
110 |
|
} |
111 |
131 |
return NodeManager::getKindForFunction(op); |
112 |
|
} |
113 |
|
|
114 |
|
struct SygusOpRewrittenAttributeId |
115 |
|
{ |
116 |
|
}; |
117 |
|
typedef expr::Attribute<SygusOpRewrittenAttributeId, Node> |
118 |
|
SygusOpRewrittenAttribute; |
119 |
|
|
120 |
162220 |
Kind getEliminateKind(Kind ok) |
121 |
|
{ |
122 |
162220 |
Kind nk = ok; |
123 |
|
// We also must ensure that builtin operators which are eliminated |
124 |
|
// during expand definitions are replaced by the proper operator. |
125 |
162220 |
if (ok == DIVISION) |
126 |
|
{ |
127 |
46 |
nk = DIVISION_TOTAL; |
128 |
|
} |
129 |
162174 |
else if (ok == INTS_DIVISION) |
130 |
|
{ |
131 |
|
nk = INTS_DIVISION_TOTAL; |
132 |
|
} |
133 |
162174 |
else if (ok == INTS_MODULUS) |
134 |
|
{ |
135 |
|
nk = INTS_MODULUS_TOTAL; |
136 |
|
} |
137 |
162220 |
return nk; |
138 |
|
} |
139 |
|
|
140 |
480691 |
Node mkSygusTerm(const DType& dt, |
141 |
|
unsigned i, |
142 |
|
const std::vector<Node>& children, |
143 |
|
bool doBetaReduction, |
144 |
|
bool isExternal) |
145 |
|
{ |
146 |
961382 |
Trace("dt-sygus-util") << "Make sygus term " << dt.getName() << "[" << i |
147 |
480691 |
<< "] with children: " << children << std::endl; |
148 |
480691 |
Assert(i < dt.getNumConstructors()); |
149 |
480691 |
Assert(dt.isSygus()); |
150 |
480691 |
Assert(!dt[i].getSygusOp().isNull()); |
151 |
961382 |
Node op = dt[i].getSygusOp(); |
152 |
961382 |
Node opn = op; |
153 |
480691 |
if (!isExternal) |
154 |
|
{ |
155 |
|
// Get the normalized version of the sygus operator. We do this by |
156 |
|
// expanding definitions, rewriting it, and eliminating partial operators. |
157 |
476352 |
if (!op.hasAttribute(SygusOpRewrittenAttribute())) |
158 |
|
{ |
159 |
164085 |
if (op.isConst()) |
160 |
|
{ |
161 |
|
// If it is a builtin operator, convert to total version if necessary. |
162 |
|
// First, get the kind for the operator. |
163 |
162220 |
Kind ok = NodeManager::operatorToKind(op); |
164 |
324440 |
Trace("sygus-grammar-normalize-debug") |
165 |
162220 |
<< "...builtin kind is " << ok << std::endl; |
166 |
162220 |
Kind nk = getEliminateKind(ok); |
167 |
162220 |
if (nk != ok) |
168 |
|
{ |
169 |
92 |
Trace("sygus-grammar-normalize-debug") |
170 |
46 |
<< "...replace by builtin operator " << nk << std::endl; |
171 |
46 |
opn = NodeManager::currentNM()->operatorOf(nk); |
172 |
|
} |
173 |
|
} |
174 |
|
else |
175 |
|
{ |
176 |
|
// Get the expanded definition form, if it has been marked. This ensures |
177 |
|
// that user-defined functions have been eliminated from op. |
178 |
1865 |
opn = getExpandedDefinitionForm(op); |
179 |
1865 |
opn = Rewriter::rewrite(opn); |
180 |
|
SygusOpRewrittenAttribute sora; |
181 |
1865 |
op.setAttribute(sora, opn); |
182 |
|
} |
183 |
|
} |
184 |
|
else |
185 |
|
{ |
186 |
312267 |
opn = op.getAttribute(SygusOpRewrittenAttribute()); |
187 |
|
} |
188 |
|
} |
189 |
961382 |
return mkSygusTerm(opn, children, doBetaReduction); |
190 |
|
} |
191 |
|
|
192 |
480693 |
Node mkSygusTerm(Node op, |
193 |
|
const std::vector<Node>& children, |
194 |
|
bool doBetaReduction) |
195 |
|
{ |
196 |
480693 |
Trace("dt-sygus-util") << "Operator is " << op << std::endl; |
197 |
480693 |
if (children.empty()) |
198 |
|
{ |
199 |
|
// no children, return immediately |
200 |
128140 |
Trace("dt-sygus-util") << "...return direct op" << std::endl; |
201 |
128140 |
return op; |
202 |
|
} |
203 |
|
// if it is the any constant, we simply return the child |
204 |
352553 |
if (op.getAttribute(SygusAnyConstAttribute())) |
205 |
|
{ |
206 |
447 |
Assert(children.size() == 1); |
207 |
447 |
return children[0]; |
208 |
|
} |
209 |
704212 |
std::vector<Node> schildren; |
210 |
|
// get the kind of the operator |
211 |
352106 |
Kind ok = op.getKind(); |
212 |
352106 |
if (ok != BUILTIN) |
213 |
|
{ |
214 |
312486 |
if (ok == LAMBDA && doBetaReduction) |
215 |
|
{ |
216 |
|
// Do immediate beta reduction. It suffices to use a normal substitution |
217 |
|
// since neither op nor children have quantifiers, since they are |
218 |
|
// generated by sygus grammars. |
219 |
622700 |
std::vector<Node> vars{op[0].begin(), op[0].end()}; |
220 |
311350 |
Assert(vars.size() == children.size()); |
221 |
|
Node ret = op[1].substitute( |
222 |
622700 |
vars.begin(), vars.end(), children.begin(), children.end()); |
223 |
311350 |
Trace("dt-sygus-util") << "...return (beta-reduce) " << ret << std::endl; |
224 |
311350 |
return ret; |
225 |
|
} |
226 |
|
else |
227 |
|
{ |
228 |
1136 |
schildren.push_back(op); |
229 |
|
} |
230 |
|
} |
231 |
40756 |
schildren.insert(schildren.end(), children.begin(), children.end()); |
232 |
81512 |
Node ret; |
233 |
40756 |
if (ok == BUILTIN) |
234 |
|
{ |
235 |
39620 |
ret = NodeManager::currentNM()->mkNode(op, schildren); |
236 |
39620 |
Trace("dt-sygus-util") << "...return (builtin) " << ret << std::endl; |
237 |
39620 |
return ret; |
238 |
|
} |
239 |
|
// get the kind used for applying op |
240 |
1136 |
Kind otk = NodeManager::operatorToKind(op); |
241 |
1136 |
Trace("dt-sygus-util") << "operator kind is " << otk << std::endl; |
242 |
1136 |
if (otk != UNDEFINED_KIND) |
243 |
|
{ |
244 |
|
// If it is an APPLY_UF operator, we should have at least an operator and |
245 |
|
// a child. |
246 |
1005 |
Assert(otk != APPLY_UF || schildren.size() != 1); |
247 |
1005 |
ret = NodeManager::currentNM()->mkNode(otk, schildren); |
248 |
1005 |
Trace("dt-sygus-util") << "...return (op) " << ret << std::endl; |
249 |
1005 |
return ret; |
250 |
|
} |
251 |
131 |
Kind tok = getOperatorKindForSygusBuiltin(op); |
252 |
131 |
if (schildren.size() == 1 && tok == UNDEFINED_KIND) |
253 |
|
{ |
254 |
|
ret = schildren[0]; |
255 |
|
} |
256 |
|
else |
257 |
|
{ |
258 |
131 |
ret = NodeManager::currentNM()->mkNode(tok, schildren); |
259 |
|
} |
260 |
131 |
Trace("dt-sygus-util") << "...return " << ret << std::endl; |
261 |
131 |
return ret; |
262 |
|
} |
263 |
|
|
264 |
|
struct SygusToBuiltinTermAttributeId |
265 |
|
{ |
266 |
|
}; |
267 |
|
typedef expr::Attribute<SygusToBuiltinTermAttributeId, Node> |
268 |
|
SygusToBuiltinTermAttribute; |
269 |
|
|
270 |
|
// A variant of the above attribute for cases where we introduce a fresh |
271 |
|
// variable. This is to support sygusToBuiltin on non-constant sygus terms, |
272 |
|
// where sygus variables should be mapped to canonical builtin variables. |
273 |
|
// It is important to cache this so that sygusToBuiltin is deterministic. |
274 |
|
struct SygusToBuiltinVarAttributeId |
275 |
|
{ |
276 |
|
}; |
277 |
|
typedef expr::Attribute<SygusToBuiltinVarAttributeId, Node> |
278 |
|
SygusToBuiltinVarAttribute; |
279 |
|
|
280 |
|
// A variant of the above attribute for cases where we introduce a fresh |
281 |
|
// variable. This is to support sygusToBuiltin on non-constant sygus terms, |
282 |
|
// where sygus variables should be mapped to canonical builtin variables. |
283 |
|
// It is important to cache this so that sygusToBuiltin is deterministic. |
284 |
|
struct BuiltinVarToSygusAttributeId |
285 |
|
{ |
286 |
|
}; |
287 |
|
typedef expr::Attribute<BuiltinVarToSygusAttributeId, Node> |
288 |
|
BuiltinVarToSygusAttribute; |
289 |
|
|
290 |
285805 |
Node sygusToBuiltin(Node n, bool isExternal) |
291 |
|
{ |
292 |
571610 |
std::unordered_map<TNode, Node> visited; |
293 |
285805 |
std::unordered_map<TNode, Node>::iterator it; |
294 |
571610 |
std::vector<TNode> visit; |
295 |
571610 |
TNode cur; |
296 |
|
unsigned index; |
297 |
285805 |
visit.push_back(n); |
298 |
185639 |
do |
299 |
|
{ |
300 |
471444 |
cur = visit.back(); |
301 |
471444 |
visit.pop_back(); |
302 |
471444 |
it = visited.find(cur); |
303 |
471444 |
if (it == visited.end()) |
304 |
|
{ |
305 |
|
// Notice this condition succeeds in roughly 99% of the executions of this |
306 |
|
// method (based on our coverage tests), hence the else if / else cases |
307 |
|
// below do not significantly impact performance. |
308 |
403825 |
if (cur.getKind() == APPLY_CONSTRUCTOR) |
309 |
|
{ |
310 |
395283 |
if (!isExternal && cur.hasAttribute(SygusToBuiltinTermAttribute())) |
311 |
|
{ |
312 |
330801 |
visited[cur] = cur.getAttribute(SygusToBuiltinTermAttribute()); |
313 |
|
} |
314 |
|
else |
315 |
|
{ |
316 |
64482 |
visited[cur] = Node::null(); |
317 |
64482 |
visit.push_back(cur); |
318 |
185639 |
for (const Node& cn : cur) |
319 |
|
{ |
320 |
121157 |
visit.push_back(cn); |
321 |
|
} |
322 |
|
} |
323 |
|
} |
324 |
8542 |
else if (cur.getType().isSygusDatatype()) |
325 |
|
{ |
326 |
8070 |
Assert (cur.isVar()); |
327 |
8070 |
if (cur.hasAttribute(SygusToBuiltinVarAttribute())) |
328 |
|
{ |
329 |
|
// use the previously constructed variable for it |
330 |
7983 |
visited[cur] = cur.getAttribute(SygusToBuiltinVarAttribute()); |
331 |
|
} |
332 |
|
else |
333 |
|
{ |
334 |
174 |
std::stringstream ss; |
335 |
87 |
ss << cur; |
336 |
87 |
const DType& dt = cur.getType().getDType(); |
337 |
|
// make a fresh variable |
338 |
87 |
NodeManager * nm = NodeManager::currentNM(); |
339 |
174 |
Node var = nm->mkBoundVar(ss.str(), dt.getSygusType()); |
340 |
|
SygusToBuiltinVarAttribute stbv; |
341 |
87 |
cur.setAttribute(stbv, var); |
342 |
87 |
visited[cur] = var; |
343 |
|
// create backwards mapping |
344 |
|
BuiltinVarToSygusAttribute bvtsa; |
345 |
87 |
var.setAttribute(bvtsa, cur); |
346 |
|
} |
347 |
|
} |
348 |
|
else |
349 |
|
{ |
350 |
|
// non-datatypes are themselves |
351 |
472 |
visited[cur] = cur; |
352 |
|
} |
353 |
|
} |
354 |
67619 |
else if (it->second.isNull()) |
355 |
|
{ |
356 |
128964 |
Node ret = cur; |
357 |
64482 |
Assert(cur.getKind() == APPLY_CONSTRUCTOR); |
358 |
64482 |
const DType& dt = cur.getType().getDType(); |
359 |
|
// Non sygus-datatype terms are also themselves. Notice we treat the |
360 |
|
// case of non-sygus datatypes this way since it avoids computing |
361 |
|
// the type / datatype of the node in the pre-traversal above. The |
362 |
|
// case of non-sygus datatypes is very rare, so the extra addition to |
363 |
|
// visited is justified performance-wise. |
364 |
64482 |
if (dt.isSygus()) |
365 |
|
{ |
366 |
128964 |
std::vector<Node> children; |
367 |
185639 |
for (const Node& cn : cur) |
368 |
|
{ |
369 |
121157 |
it = visited.find(cn); |
370 |
121157 |
Assert(it != visited.end()); |
371 |
121157 |
Assert(!it->second.isNull()); |
372 |
121157 |
children.push_back(it->second); |
373 |
|
} |
374 |
64482 |
index = indexOf(cur.getOperator()); |
375 |
64482 |
ret = mkSygusTerm(dt, index, children, true, isExternal); |
376 |
|
} |
377 |
64482 |
visited[cur] = ret; |
378 |
|
// cache |
379 |
64482 |
if (!isExternal) |
380 |
|
{ |
381 |
|
SygusToBuiltinTermAttribute stbt; |
382 |
60143 |
cur.setAttribute(stbt, ret); |
383 |
|
} |
384 |
|
} |
385 |
471444 |
} while (!visit.empty()); |
386 |
285805 |
Assert(visited.find(n) != visited.end()); |
387 |
285805 |
Assert(!visited.find(n)->second.isNull()); |
388 |
571610 |
return visited[n]; |
389 |
|
} |
390 |
|
|
391 |
41247 |
Node sygusToBuiltinEval(Node n, const std::vector<Node>& args) |
392 |
|
{ |
393 |
41247 |
NodeManager* nm = NodeManager::currentNM(); |
394 |
41247 |
Evaluator eval(nullptr); |
395 |
|
// constant arguments? |
396 |
41247 |
bool constArgs = true; |
397 |
181092 |
for (const Node& a : args) |
398 |
|
{ |
399 |
143299 |
if (!a.isConst()) |
400 |
|
{ |
401 |
3454 |
constArgs = false; |
402 |
3454 |
break; |
403 |
|
} |
404 |
|
} |
405 |
82494 |
std::vector<Node> eargs; |
406 |
41247 |
bool svarsInit = false; |
407 |
82494 |
std::vector<Node> svars; |
408 |
82494 |
std::unordered_map<TNode, Node> visited; |
409 |
41247 |
std::unordered_map<TNode, Node>::iterator it; |
410 |
82494 |
std::vector<TNode> visit; |
411 |
82494 |
TNode cur; |
412 |
|
unsigned index; |
413 |
41247 |
visit.push_back(n); |
414 |
79489 |
do |
415 |
|
{ |
416 |
120736 |
cur = visit.back(); |
417 |
120736 |
visit.pop_back(); |
418 |
120736 |
it = visited.find(cur); |
419 |
120736 |
if (it == visited.end()) |
420 |
|
{ |
421 |
184736 |
TypeNode tn = cur.getType(); |
422 |
92368 |
if (!tn.isDatatype() || !tn.getDType().isSygus()) |
423 |
|
{ |
424 |
98 |
visited[cur] = cur; |
425 |
|
} |
426 |
92270 |
else if (cur.isConst()) |
427 |
|
{ |
428 |
|
// convert to builtin term |
429 |
98274 |
Node bt = sygusToBuiltin(cur); |
430 |
|
// run the evaluator if possible |
431 |
49137 |
if (!svarsInit) |
432 |
|
{ |
433 |
40795 |
svarsInit = true; |
434 |
81590 |
TypeNode type = cur.getType(); |
435 |
81590 |
Node varList = type.getDType().getSygusVarList(); |
436 |
189685 |
for (const Node& v : varList) |
437 |
|
{ |
438 |
148890 |
svars.push_back(v); |
439 |
|
} |
440 |
|
} |
441 |
49137 |
Assert(args.size() == svars.size()); |
442 |
|
// try evaluation if we have constant arguments |
443 |
98274 |
Node ret = constArgs ? eval.eval(bt, svars, args) : Node::null(); |
444 |
49137 |
if (ret.isNull()) |
445 |
|
{ |
446 |
|
// if evaluation was not available, use a substitution |
447 |
5268 |
ret = bt.substitute( |
448 |
|
svars.begin(), svars.end(), args.begin(), args.end()); |
449 |
|
} |
450 |
49137 |
visited[cur] = ret; |
451 |
|
} |
452 |
|
else |
453 |
|
{ |
454 |
43133 |
if (cur.getKind() == APPLY_CONSTRUCTOR) |
455 |
|
{ |
456 |
26136 |
visited[cur] = Node::null(); |
457 |
26136 |
visit.push_back(cur); |
458 |
79489 |
for (const Node& cn : cur) |
459 |
|
{ |
460 |
53353 |
visit.push_back(cn); |
461 |
|
} |
462 |
|
} |
463 |
|
else |
464 |
|
{ |
465 |
|
// it is the evaluation of this term on the arguments |
466 |
16997 |
if (eargs.empty()) |
467 |
|
{ |
468 |
15143 |
eargs.push_back(cur); |
469 |
15143 |
eargs.insert(eargs.end(), args.begin(), args.end()); |
470 |
|
} |
471 |
|
else |
472 |
|
{ |
473 |
1854 |
eargs[0] = cur; |
474 |
|
} |
475 |
16997 |
visited[cur] = nm->mkNode(DT_SYGUS_EVAL, eargs); |
476 |
|
} |
477 |
|
} |
478 |
|
} |
479 |
28368 |
else if (it->second.isNull()) |
480 |
|
{ |
481 |
52272 |
Node ret = cur; |
482 |
26136 |
Assert(cur.getKind() == APPLY_CONSTRUCTOR); |
483 |
26136 |
const DType& dt = cur.getType().getDType(); |
484 |
|
// non sygus-datatype terms are also themselves |
485 |
26136 |
if (dt.isSygus()) |
486 |
|
{ |
487 |
52272 |
std::vector<Node> children; |
488 |
79489 |
for (const Node& cn : cur) |
489 |
|
{ |
490 |
53353 |
it = visited.find(cn); |
491 |
53353 |
Assert(it != visited.end()); |
492 |
53353 |
Assert(!it->second.isNull()); |
493 |
53353 |
children.push_back(it->second); |
494 |
|
} |
495 |
26136 |
index = indexOf(cur.getOperator()); |
496 |
|
// apply to children, which constructs the builtin term |
497 |
26136 |
ret = mkSygusTerm(dt, index, children); |
498 |
|
// now apply it to arguments in args |
499 |
26136 |
ret = applySygusArgs(dt, dt[index].getSygusOp(), ret, args); |
500 |
|
} |
501 |
26136 |
visited[cur] = ret; |
502 |
|
} |
503 |
120736 |
} while (!visit.empty()); |
504 |
41247 |
Assert(visited.find(n) != visited.end()); |
505 |
41247 |
Assert(!visited.find(n)->second.isNull()); |
506 |
82494 |
return visited[n]; |
507 |
|
} |
508 |
|
|
509 |
219 |
Node builtinVarToSygus(Node v) |
510 |
|
{ |
511 |
|
BuiltinVarToSygusAttribute bvtsa; |
512 |
219 |
if (v.hasAttribute(bvtsa)) |
513 |
|
{ |
514 |
219 |
return v.getAttribute(bvtsa); |
515 |
|
} |
516 |
|
return Node::null(); |
517 |
|
} |
518 |
|
|
519 |
|
void getFreeSymbolsSygusType(TypeNode sdt, std::unordered_set<Node>& syms) |
520 |
|
{ |
521 |
|
// datatype types we need to process |
522 |
|
std::vector<TypeNode> typeToProcess; |
523 |
|
// datatype types we have processed |
524 |
|
std::map<TypeNode, TypeNode> typesProcessed; |
525 |
|
typeToProcess.push_back(sdt); |
526 |
|
while (!typeToProcess.empty()) |
527 |
|
{ |
528 |
|
std::vector<TypeNode> typeNextToProcess; |
529 |
|
for (const TypeNode& curr : typeToProcess) |
530 |
|
{ |
531 |
|
Assert(curr.isDatatype() && curr.getDType().isSygus()); |
532 |
|
const DType& dtc = curr.getDType(); |
533 |
|
for (unsigned j = 0, ncons = dtc.getNumConstructors(); j < ncons; j++) |
534 |
|
{ |
535 |
|
// collect the symbols from the operator |
536 |
|
Node op = dtc[j].getSygusOp(); |
537 |
|
expr::getSymbols(op, syms); |
538 |
|
// traverse the argument types |
539 |
|
for (unsigned k = 0, nargs = dtc[j].getNumArgs(); k < nargs; k++) |
540 |
|
{ |
541 |
|
TypeNode argt = dtc[j].getArgType(k); |
542 |
|
if (!argt.isDatatype() || !argt.getDType().isSygus()) |
543 |
|
{ |
544 |
|
// not a sygus datatype |
545 |
|
continue; |
546 |
|
} |
547 |
|
if (typesProcessed.find(argt) == typesProcessed.end()) |
548 |
|
{ |
549 |
|
typeNextToProcess.push_back(argt); |
550 |
|
} |
551 |
|
} |
552 |
|
} |
553 |
|
} |
554 |
|
typeToProcess.clear(); |
555 |
|
typeToProcess.insert(typeToProcess.end(), |
556 |
|
typeNextToProcess.begin(), |
557 |
|
typeNextToProcess.end()); |
558 |
|
} |
559 |
|
} |
560 |
|
|
561 |
7 |
TypeNode substituteAndGeneralizeSygusType(TypeNode sdt, |
562 |
|
const std::vector<Node>& syms, |
563 |
|
const std::vector<Node>& vars) |
564 |
|
{ |
565 |
7 |
NodeManager* nm = NodeManager::currentNM(); |
566 |
7 |
const DType& sdtd = sdt.getDType(); |
567 |
|
// compute the new formal argument list |
568 |
14 |
std::vector<Node> formalVars; |
569 |
14 |
Node prevVarList = sdtd.getSygusVarList(); |
570 |
7 |
if (!prevVarList.isNull()) |
571 |
|
{ |
572 |
|
for (const Node& v : prevVarList) |
573 |
|
{ |
574 |
|
// if it is not being replaced |
575 |
|
if (std::find(syms.begin(), syms.end(), v) != syms.end()) |
576 |
|
{ |
577 |
|
formalVars.push_back(v); |
578 |
|
} |
579 |
|
} |
580 |
|
} |
581 |
29 |
for (const Node& v : vars) |
582 |
|
{ |
583 |
22 |
if (v.getKind() == BOUND_VARIABLE) |
584 |
|
{ |
585 |
22 |
formalVars.push_back(v); |
586 |
|
} |
587 |
|
} |
588 |
|
// make the sygus variable list for the formal argument list |
589 |
14 |
Node abvl = nm->mkNode(BOUND_VAR_LIST, formalVars); |
590 |
7 |
Trace("sygus-abduct-debug") << "...finish" << std::endl; |
591 |
|
|
592 |
|
// must convert all constructors to version with variables in "vars" |
593 |
14 |
std::vector<SygusDatatype> sdts; |
594 |
14 |
std::set<TypeNode> unres; |
595 |
|
|
596 |
7 |
Trace("dtsygus-gen-debug") << "Process sygus type:" << std::endl; |
597 |
7 |
Trace("dtsygus-gen-debug") << sdtd.getName() << std::endl; |
598 |
|
|
599 |
|
// datatype types we need to process |
600 |
14 |
std::vector<TypeNode> dtToProcess; |
601 |
|
// datatype types we have processed |
602 |
14 |
std::map<TypeNode, TypeNode> dtProcessed; |
603 |
7 |
dtToProcess.push_back(sdt); |
604 |
14 |
std::stringstream ssutn0; |
605 |
7 |
ssutn0 << sdtd.getName() << "_s"; |
606 |
|
TypeNode abdTNew = |
607 |
14 |
nm->mkSort(ssutn0.str(), NodeManager::SORT_FLAG_PLACEHOLDER); |
608 |
7 |
unres.insert(abdTNew); |
609 |
7 |
dtProcessed[sdt] = abdTNew; |
610 |
|
|
611 |
|
// We must convert all symbols in the sygus datatype type sdt to |
612 |
|
// apply the substitution { syms -> vars }, where syms is the free |
613 |
|
// variables of the input problem, and vars is the formal argument list |
614 |
|
// of the function-to-synthesize. |
615 |
|
|
616 |
|
// We are traversing over the subfield types of the datatype to convert |
617 |
|
// them into the form described above. |
618 |
31 |
while (!dtToProcess.empty()) |
619 |
|
{ |
620 |
24 |
std::vector<TypeNode> dtNextToProcess; |
621 |
25 |
for (const TypeNode& curr : dtToProcess) |
622 |
|
{ |
623 |
13 |
Assert(curr.isDatatype() && curr.getDType().isSygus()); |
624 |
13 |
const DType& dtc = curr.getDType(); |
625 |
26 |
std::stringstream ssdtn; |
626 |
13 |
ssdtn << dtc.getName() << "_s"; |
627 |
13 |
sdts.push_back(SygusDatatype(ssdtn.str())); |
628 |
26 |
Trace("dtsygus-gen-debug") |
629 |
13 |
<< "Process datatype " << sdts.back().getName() << "..." << std::endl; |
630 |
45 |
for (unsigned j = 0, ncons = dtc.getNumConstructors(); j < ncons; j++) |
631 |
|
{ |
632 |
64 |
Node op = dtc[j].getSygusOp(); |
633 |
|
// apply the substitution to the argument |
634 |
|
Node ops = |
635 |
64 |
op.substitute(syms.begin(), syms.end(), vars.begin(), vars.end()); |
636 |
64 |
Trace("dtsygus-gen-debug") << " Process constructor " << op << " / " |
637 |
32 |
<< ops << "..." << std::endl; |
638 |
64 |
std::vector<TypeNode> cargs; |
639 |
55 |
for (unsigned k = 0, nargs = dtc[j].getNumArgs(); k < nargs; k++) |
640 |
|
{ |
641 |
46 |
TypeNode argt = dtc[j].getArgType(k); |
642 |
23 |
std::map<TypeNode, TypeNode>::iterator itdp = dtProcessed.find(argt); |
643 |
46 |
TypeNode argtNew; |
644 |
23 |
if (itdp == dtProcessed.end()) |
645 |
|
{ |
646 |
12 |
std::stringstream ssutn; |
647 |
6 |
ssutn << argt.getDType().getName() << "_s"; |
648 |
6 |
argtNew = |
649 |
12 |
nm->mkSort(ssutn.str(), NodeManager::SORT_FLAG_PLACEHOLDER); |
650 |
12 |
Trace("dtsygus-gen-debug") << " ...unresolved type " << argtNew |
651 |
6 |
<< " for " << argt << std::endl; |
652 |
6 |
unres.insert(argtNew); |
653 |
6 |
dtProcessed[argt] = argtNew; |
654 |
6 |
dtNextToProcess.push_back(argt); |
655 |
|
} |
656 |
|
else |
657 |
|
{ |
658 |
17 |
argtNew = itdp->second; |
659 |
|
} |
660 |
46 |
Trace("dtsygus-gen-debug") |
661 |
23 |
<< " Arg #" << k << ": " << argtNew << std::endl; |
662 |
23 |
cargs.push_back(argtNew); |
663 |
|
} |
664 |
64 |
std::stringstream ss; |
665 |
32 |
ss << ops.getKind(); |
666 |
32 |
Trace("dtsygus-gen-debug") << "Add constructor : " << ops << std::endl; |
667 |
32 |
sdts.back().addConstructor(ops, ss.str(), cargs); |
668 |
|
} |
669 |
26 |
Trace("dtsygus-gen-debug") |
670 |
13 |
<< "Set sygus : " << dtc.getSygusType() << " " << abvl << std::endl; |
671 |
26 |
TypeNode stn = dtc.getSygusType(); |
672 |
39 |
sdts.back().initializeDatatype( |
673 |
26 |
stn, abvl, dtc.getSygusAllowConst(), dtc.getSygusAllowAll()); |
674 |
|
} |
675 |
12 |
dtToProcess.clear(); |
676 |
12 |
dtToProcess.insert( |
677 |
24 |
dtToProcess.end(), dtNextToProcess.begin(), dtNextToProcess.end()); |
678 |
|
} |
679 |
14 |
Trace("dtsygus-gen-debug") |
680 |
7 |
<< "Make " << sdts.size() << " datatype types..." << std::endl; |
681 |
|
// extract the datatypes |
682 |
14 |
std::vector<DType> datatypes; |
683 |
20 |
for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++) |
684 |
|
{ |
685 |
13 |
datatypes.push_back(sdts[i].getDatatype()); |
686 |
|
} |
687 |
|
// make the datatype types |
688 |
|
std::vector<TypeNode> datatypeTypes = nm->mkMutualDatatypeTypes( |
689 |
14 |
datatypes, unres, NodeManager::DATATYPE_FLAG_PLACEHOLDER); |
690 |
7 |
TypeNode sdtS = datatypeTypes[0]; |
691 |
7 |
if (Trace.isOn("dtsygus-gen-debug")) |
692 |
|
{ |
693 |
|
Trace("dtsygus-gen-debug") << "Made datatype types:" << std::endl; |
694 |
|
for (unsigned j = 0, ndts = datatypeTypes.size(); j < ndts; j++) |
695 |
|
{ |
696 |
|
const DType& dtj = datatypeTypes[j].getDType(); |
697 |
|
Trace("dtsygus-gen-debug") << "#" << j << ": " << dtj << std::endl; |
698 |
|
for (unsigned k = 0, ncons = dtj.getNumConstructors(); k < ncons; k++) |
699 |
|
{ |
700 |
|
for (unsigned l = 0, nargs = dtj[k].getNumArgs(); l < nargs; l++) |
701 |
|
{ |
702 |
|
if (!dtj[k].getArgType(l).isDatatype()) |
703 |
|
{ |
704 |
|
Trace("dtsygus-gen-debug") |
705 |
|
<< "Argument " << l << " of " << dtj[k] |
706 |
|
<< " is not datatype : " << dtj[k].getArgType(l) << std::endl; |
707 |
|
AlwaysAssert(false); |
708 |
|
} |
709 |
|
} |
710 |
|
} |
711 |
|
} |
712 |
|
} |
713 |
14 |
return sdtS; |
714 |
|
} |
715 |
|
|
716 |
307662 |
unsigned getSygusTermSize(Node n) |
717 |
|
{ |
718 |
307662 |
if (n.getKind() != APPLY_CONSTRUCTOR) |
719 |
|
{ |
720 |
21277 |
return 0; |
721 |
|
} |
722 |
286385 |
unsigned sum = 0; |
723 |
476349 |
for (const Node& nc : n) |
724 |
|
{ |
725 |
189964 |
sum += getSygusTermSize(nc); |
726 |
|
} |
727 |
286385 |
const DType& dt = datatypeOf(n.getOperator()); |
728 |
286385 |
int cindex = indexOf(n.getOperator()); |
729 |
286385 |
Assert(cindex >= 0 && static_cast<size_t>(cindex) < dt.getNumConstructors()); |
730 |
286385 |
unsigned weight = dt[cindex].getWeight(); |
731 |
286385 |
return weight + sum; |
732 |
|
} |
733 |
|
|
734 |
|
/** |
735 |
|
* Map terms to the result of expand definitions calling smt::expandDefinitions |
736 |
|
* on it. |
737 |
|
*/ |
738 |
|
struct SygusExpDefFormAttributeId |
739 |
|
{ |
740 |
|
}; |
741 |
|
typedef expr::Attribute<SygusExpDefFormAttributeId, Node> |
742 |
|
SygusExpDefFormAttribute; |
743 |
|
|
744 |
2455 |
void setExpandedDefinitionForm(Node op, Node eop) |
745 |
|
{ |
746 |
2455 |
op.setAttribute(SygusExpDefFormAttribute(), eop); |
747 |
2455 |
} |
748 |
|
|
749 |
1865 |
Node getExpandedDefinitionForm(Node op) |
750 |
|
{ |
751 |
3730 |
Node eop = op.getAttribute(SygusExpDefFormAttribute()); |
752 |
|
// if not set, assume original |
753 |
3730 |
return eop.isNull() ? op : eop; |
754 |
|
} |
755 |
|
|
756 |
|
} // namespace utils |
757 |
|
} // namespace datatypes |
758 |
|
} // namespace theory |
759 |
22755 |
} // namespace cvc5 |