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