1 /******************************************************************************
2 * Top contributors (to current version):
3 * Andrew Reynolds, Mathias Preiner, Aina Niemetz
5 * This file is part of the cvc5 project.
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 * ****************************************************************************
13 * Implementation of rewriter for the theory of (co)inductive datatypes.
16 #include "theory/datatypes/sygus_datatype_utils.h"
20 #include "expr/dtype.h"
21 #include "expr/dtype_cons.h"
22 #include "expr/node_algorithm.h"
23 #include "expr/sygus_datatype.h"
25 #include "theory/evaluator.h"
26 #include "theory/rewriter.h"
29 using namespace cvc5::kind
;
36 Node
applySygusArgs(const DType
& dt
,
39 const std::vector
<Node
>& args
)
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 if (n
.getKind() == BOUND_VARIABLE
)
46 if (n
.hasAttribute(SygusVarNumAttribute()))
48 int vn
= n
.getAttribute(SygusVarNumAttribute());
49 Assert(dt
.getSygusVarList()[vn
] == n
);
52 // it is a different bound variable, it is unchanged
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.
59 if (!op
.hasAttribute(SygusVarFreeAttribute()))
61 std::unordered_set
<Node
> fvs
;
62 if (expr::getFreeVariables(op
, fvs
))
66 for (const Node
& v
: fvs
)
76 Trace("dt-sygus-fv") << "Free var in " << op
<< " : " << val
<< std::endl
;
77 op
.setAttribute(SygusVarFreeAttribute(), val
);
81 val
= op
.getAttribute(SygusVarFreeAttribute());
87 if (val
.getKind() == BOUND_VARIABLE
)
89 // single substitution case
90 int vn
= val
.getAttribute(SygusVarNumAttribute());
92 return n
.substitute(val
, sub
);
94 // do the full substitution
95 std::vector
<Node
> vars
;
96 Node bvl
= dt
.getSygusVarList();
97 for (unsigned i
= 0, nvars
= bvl
.getNumChildren(); i
< nvars
; i
++)
99 vars
.push_back(bvl
[i
]);
101 return n
.substitute(vars
.begin(), vars
.end(), args
.begin(), args
.end());
104 Kind
getOperatorKindForSygusBuiltin(Node op
)
106 Assert(op
.getKind() != BUILTIN
);
107 if (op
.getKind() == LAMBDA
)
111 return NodeManager::getKindForFunction(op
);
114 struct SygusOpRewrittenAttributeId
117 typedef expr::Attribute
<SygusOpRewrittenAttributeId
, Node
>
118 SygusOpRewrittenAttribute
;
120 Kind
getEliminateKind(Kind ok
)
123 // We also must ensure that builtin operators which are eliminated
124 // during expand definitions are replaced by the proper operator.
129 else if (ok
== INTS_DIVISION
)
131 nk
= INTS_DIVISION_TOTAL
;
133 else if (ok
== INTS_MODULUS
)
135 nk
= INTS_MODULUS_TOTAL
;
140 Node
mkSygusTerm(const DType
& dt
,
142 const std::vector
<Node
>& children
,
143 bool doBetaReduction
,
146 Trace("dt-sygus-util") << "Make sygus term " << dt
.getName() << "[" << i
147 << "] with children: " << children
<< std::endl
;
148 Assert(i
< dt
.getNumConstructors());
149 Assert(dt
.isSygus());
150 Assert(!dt
[i
].getSygusOp().isNull());
151 Node op
= dt
[i
].getSygusOp();
155 // Get the normalized version of the sygus operator. We do this by
156 // expanding definitions, rewriting it, and eliminating partial operators.
157 if (!op
.hasAttribute(SygusOpRewrittenAttribute()))
161 // If it is a builtin operator, convert to total version if necessary.
162 // First, get the kind for the operator.
163 Kind ok
= NodeManager::operatorToKind(op
);
164 Trace("sygus-grammar-normalize-debug")
165 << "...builtin kind is " << ok
<< std::endl
;
166 Kind nk
= getEliminateKind(ok
);
169 Trace("sygus-grammar-normalize-debug")
170 << "...replace by builtin operator " << nk
<< std::endl
;
171 opn
= NodeManager::currentNM()->operatorOf(nk
);
176 // Get the expanded definition form, if it has been marked. This ensures
177 // that user-defined functions have been eliminated from op.
178 opn
= getExpandedDefinitionForm(op
);
179 opn
= Rewriter::rewrite(opn
);
180 SygusOpRewrittenAttribute sora
;
181 op
.setAttribute(sora
, opn
);
186 opn
= op
.getAttribute(SygusOpRewrittenAttribute());
189 return mkSygusTerm(opn
, children
, doBetaReduction
);
192 Node
mkSygusTerm(Node op
,
193 const std::vector
<Node
>& children
,
194 bool doBetaReduction
)
196 Trace("dt-sygus-util") << "Operator is " << op
<< std::endl
;
197 if (children
.empty())
199 // no children, return immediately
200 Trace("dt-sygus-util") << "...return direct op" << std::endl
;
203 // if it is the any constant, we simply return the child
204 if (op
.getAttribute(SygusAnyConstAttribute()))
206 Assert(children
.size() == 1);
209 std::vector
<Node
> schildren
;
210 // get the kind of the operator
211 Kind ok
= op
.getKind();
214 if (ok
== LAMBDA
&& doBetaReduction
)
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 std::vector
<Node
> vars
{op
[0].begin(), op
[0].end()};
220 Assert(vars
.size() == children
.size());
221 Node ret
= op
[1].substitute(
222 vars
.begin(), vars
.end(), children
.begin(), children
.end());
223 Trace("dt-sygus-util") << "...return (beta-reduce) " << ret
<< std::endl
;
228 schildren
.push_back(op
);
231 schildren
.insert(schildren
.end(), children
.begin(), children
.end());
235 ret
= NodeManager::currentNM()->mkNode(op
, schildren
);
236 Trace("dt-sygus-util") << "...return (builtin) " << ret
<< std::endl
;
239 // get the kind used for applying op
240 Kind otk
= NodeManager::operatorToKind(op
);
241 Trace("dt-sygus-util") << "operator kind is " << otk
<< std::endl
;
242 if (otk
!= UNDEFINED_KIND
)
244 // If it is an APPLY_UF operator, we should have at least an operator and
246 Assert(otk
!= APPLY_UF
|| schildren
.size() != 1);
247 ret
= NodeManager::currentNM()->mkNode(otk
, schildren
);
248 Trace("dt-sygus-util") << "...return (op) " << ret
<< std::endl
;
251 Kind tok
= getOperatorKindForSygusBuiltin(op
);
252 if (schildren
.size() == 1 && tok
== UNDEFINED_KIND
)
258 ret
= NodeManager::currentNM()->mkNode(tok
, schildren
);
260 Trace("dt-sygus-util") << "...return " << ret
<< std::endl
;
264 struct SygusToBuiltinTermAttributeId
267 typedef expr::Attribute
<SygusToBuiltinTermAttributeId
, Node
>
268 SygusToBuiltinTermAttribute
;
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
277 typedef expr::Attribute
<SygusToBuiltinVarAttributeId
, Node
>
278 SygusToBuiltinVarAttribute
;
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
287 typedef expr::Attribute
<BuiltinVarToSygusAttributeId
, Node
>
288 BuiltinVarToSygusAttribute
;
290 Node
sygusToBuiltin(Node n
, bool isExternal
)
292 std::unordered_map
<TNode
, Node
> visited
;
293 std::unordered_map
<TNode
, Node
>::iterator it
;
294 std::vector
<TNode
> visit
;
302 it
= visited
.find(cur
);
303 if (it
== visited
.end())
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 if (cur
.getKind() == APPLY_CONSTRUCTOR
)
310 if (!isExternal
&& cur
.hasAttribute(SygusToBuiltinTermAttribute()))
312 visited
[cur
] = cur
.getAttribute(SygusToBuiltinTermAttribute());
316 visited
[cur
] = Node::null();
317 visit
.push_back(cur
);
318 for (const Node
& cn
: cur
)
324 else if (cur
.getType().isSygusDatatype())
326 Assert (cur
.isVar());
327 if (cur
.hasAttribute(SygusToBuiltinVarAttribute()))
329 // use the previously constructed variable for it
330 visited
[cur
] = cur
.getAttribute(SygusToBuiltinVarAttribute());
334 std::stringstream ss
;
336 const DType
& dt
= cur
.getType().getDType();
337 // make a fresh variable
338 NodeManager
* nm
= NodeManager::currentNM();
339 Node var
= nm
->mkBoundVar(ss
.str(), dt
.getSygusType());
340 SygusToBuiltinVarAttribute stbv
;
341 cur
.setAttribute(stbv
, var
);
343 // create backwards mapping
344 BuiltinVarToSygusAttribute bvtsa
;
345 var
.setAttribute(bvtsa
, cur
);
350 // non-datatypes are themselves
354 else if (it
->second
.isNull())
357 Assert(cur
.getKind() == APPLY_CONSTRUCTOR
);
358 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.
366 std::vector
<Node
> children
;
367 for (const Node
& cn
: cur
)
369 it
= visited
.find(cn
);
370 Assert(it
!= visited
.end());
371 Assert(!it
->second
.isNull());
372 children
.push_back(it
->second
);
374 index
= indexOf(cur
.getOperator());
375 ret
= mkSygusTerm(dt
, index
, children
, true, isExternal
);
381 SygusToBuiltinTermAttribute stbt
;
382 cur
.setAttribute(stbt
, ret
);
385 } while (!visit
.empty());
386 Assert(visited
.find(n
) != visited
.end());
387 Assert(!visited
.find(n
)->second
.isNull());
391 Node
builtinVarToSygus(Node v
)
393 BuiltinVarToSygusAttribute bvtsa
;
394 if (v
.hasAttribute(bvtsa
))
396 return v
.getAttribute(bvtsa
);
401 void getFreeSymbolsSygusType(TypeNode sdt
, std::unordered_set
<Node
>& syms
)
403 // datatype types we need to process
404 std::vector
<TypeNode
> typeToProcess
;
405 // datatype types we have processed
406 std::map
<TypeNode
, TypeNode
> typesProcessed
;
407 typeToProcess
.push_back(sdt
);
408 while (!typeToProcess
.empty())
410 std::vector
<TypeNode
> typeNextToProcess
;
411 for (const TypeNode
& curr
: typeToProcess
)
413 Assert(curr
.isDatatype() && curr
.getDType().isSygus());
414 const DType
& dtc
= curr
.getDType();
415 for (unsigned j
= 0, ncons
= dtc
.getNumConstructors(); j
< ncons
; j
++)
417 // collect the symbols from the operator
418 Node op
= dtc
[j
].getSygusOp();
419 expr::getSymbols(op
, syms
);
420 // traverse the argument types
421 for (unsigned k
= 0, nargs
= dtc
[j
].getNumArgs(); k
< nargs
; k
++)
423 TypeNode argt
= dtc
[j
].getArgType(k
);
424 if (!argt
.isDatatype() || !argt
.getDType().isSygus())
426 // not a sygus datatype
429 if (typesProcessed
.find(argt
) == typesProcessed
.end())
431 typeNextToProcess
.push_back(argt
);
436 typeToProcess
.clear();
437 typeToProcess
.insert(typeToProcess
.end(),
438 typeNextToProcess
.begin(),
439 typeNextToProcess
.end());
443 TypeNode
substituteAndGeneralizeSygusType(TypeNode sdt
,
444 const std::vector
<Node
>& syms
,
445 const std::vector
<Node
>& vars
)
447 NodeManager
* nm
= NodeManager::currentNM();
448 const DType
& sdtd
= sdt
.getDType();
449 // compute the new formal argument list
450 std::vector
<Node
> formalVars
;
451 Node prevVarList
= sdtd
.getSygusVarList();
452 if (!prevVarList
.isNull())
454 for (const Node
& v
: prevVarList
)
456 // if it is not being replaced
457 if (std::find(syms
.begin(), syms
.end(), v
) != syms
.end())
459 formalVars
.push_back(v
);
463 for (const Node
& v
: vars
)
465 if (v
.getKind() == BOUND_VARIABLE
)
467 formalVars
.push_back(v
);
470 // make the sygus variable list for the formal argument list
471 Node abvl
= nm
->mkNode(BOUND_VAR_LIST
, formalVars
);
472 Trace("sygus-abduct-debug") << "...finish" << std::endl
;
474 // must convert all constructors to version with variables in "vars"
475 std::vector
<SygusDatatype
> sdts
;
476 std::set
<TypeNode
> unres
;
478 Trace("dtsygus-gen-debug") << "Process sygus type:" << std::endl
;
479 Trace("dtsygus-gen-debug") << sdtd
.getName() << std::endl
;
481 // datatype types we need to process
482 std::vector
<TypeNode
> dtToProcess
;
483 // datatype types we have processed
484 std::map
<TypeNode
, TypeNode
> dtProcessed
;
485 dtToProcess
.push_back(sdt
);
486 std::stringstream ssutn0
;
487 ssutn0
<< sdtd
.getName() << "_s";
489 nm
->mkSort(ssutn0
.str(), NodeManager::SORT_FLAG_PLACEHOLDER
);
490 unres
.insert(abdTNew
);
491 dtProcessed
[sdt
] = abdTNew
;
493 // We must convert all symbols in the sygus datatype type sdt to
494 // apply the substitution { syms -> vars }, where syms is the free
495 // variables of the input problem, and vars is the formal argument list
496 // of the function-to-synthesize.
498 // We are traversing over the subfield types of the datatype to convert
499 // them into the form described above.
500 while (!dtToProcess
.empty())
502 std::vector
<TypeNode
> dtNextToProcess
;
503 for (const TypeNode
& curr
: dtToProcess
)
505 Assert(curr
.isDatatype() && curr
.getDType().isSygus());
506 const DType
& dtc
= curr
.getDType();
507 std::stringstream ssdtn
;
508 ssdtn
<< dtc
.getName() << "_s";
509 sdts
.push_back(SygusDatatype(ssdtn
.str()));
510 Trace("dtsygus-gen-debug")
511 << "Process datatype " << sdts
.back().getName() << "..." << std::endl
;
512 for (unsigned j
= 0, ncons
= dtc
.getNumConstructors(); j
< ncons
; j
++)
514 Node op
= dtc
[j
].getSygusOp();
515 // apply the substitution to the argument
517 op
.substitute(syms
.begin(), syms
.end(), vars
.begin(), vars
.end());
518 Trace("dtsygus-gen-debug") << " Process constructor " << op
<< " / "
519 << ops
<< "..." << std::endl
;
520 std::vector
<TypeNode
> cargs
;
521 for (unsigned k
= 0, nargs
= dtc
[j
].getNumArgs(); k
< nargs
; k
++)
523 TypeNode argt
= dtc
[j
].getArgType(k
);
524 std::map
<TypeNode
, TypeNode
>::iterator itdp
= dtProcessed
.find(argt
);
526 if (itdp
== dtProcessed
.end())
528 std::stringstream ssutn
;
529 ssutn
<< argt
.getDType().getName() << "_s";
531 nm
->mkSort(ssutn
.str(), NodeManager::SORT_FLAG_PLACEHOLDER
);
532 Trace("dtsygus-gen-debug") << " ...unresolved type " << argtNew
533 << " for " << argt
<< std::endl
;
534 unres
.insert(argtNew
);
535 dtProcessed
[argt
] = argtNew
;
536 dtNextToProcess
.push_back(argt
);
540 argtNew
= itdp
->second
;
542 Trace("dtsygus-gen-debug")
543 << " Arg #" << k
<< ": " << argtNew
<< std::endl
;
544 cargs
.push_back(argtNew
);
546 std::stringstream ss
;
548 Trace("dtsygus-gen-debug") << "Add constructor : " << ops
<< std::endl
;
549 sdts
.back().addConstructor(ops
, ss
.str(), cargs
);
551 Trace("dtsygus-gen-debug")
552 << "Set sygus : " << dtc
.getSygusType() << " " << abvl
<< std::endl
;
553 TypeNode stn
= dtc
.getSygusType();
554 sdts
.back().initializeDatatype(
555 stn
, abvl
, dtc
.getSygusAllowConst(), dtc
.getSygusAllowAll());
559 dtToProcess
.end(), dtNextToProcess
.begin(), dtNextToProcess
.end());
561 Trace("dtsygus-gen-debug")
562 << "Make " << sdts
.size() << " datatype types..." << std::endl
;
563 // extract the datatypes
564 std::vector
<DType
> datatypes
;
565 for (unsigned i
= 0, ndts
= sdts
.size(); i
< ndts
; i
++)
567 datatypes
.push_back(sdts
[i
].getDatatype());
569 // make the datatype types
570 std::vector
<TypeNode
> datatypeTypes
= nm
->mkMutualDatatypeTypes(
571 datatypes
, unres
, NodeManager::DATATYPE_FLAG_PLACEHOLDER
);
572 TypeNode sdtS
= datatypeTypes
[0];
573 if (Trace
.isOn("dtsygus-gen-debug"))
575 Trace("dtsygus-gen-debug") << "Made datatype types:" << std::endl
;
576 for (unsigned j
= 0, ndts
= datatypeTypes
.size(); j
< ndts
; j
++)
578 const DType
& dtj
= datatypeTypes
[j
].getDType();
579 Trace("dtsygus-gen-debug") << "#" << j
<< ": " << dtj
<< std::endl
;
580 for (unsigned k
= 0, ncons
= dtj
.getNumConstructors(); k
< ncons
; k
++)
582 for (unsigned l
= 0, nargs
= dtj
[k
].getNumArgs(); l
< nargs
; l
++)
584 if (!dtj
[k
].getArgType(l
).isDatatype())
586 Trace("dtsygus-gen-debug")
587 << "Argument " << l
<< " of " << dtj
[k
]
588 << " is not datatype : " << dtj
[k
].getArgType(l
) << std::endl
;
598 unsigned getSygusTermSize(Node n
)
600 if (n
.getKind() != APPLY_CONSTRUCTOR
)
605 for (const Node
& nc
: n
)
607 sum
+= getSygusTermSize(nc
);
609 const DType
& dt
= datatypeOf(n
.getOperator());
610 int cindex
= indexOf(n
.getOperator());
611 Assert(cindex
>= 0 && static_cast<size_t>(cindex
) < dt
.getNumConstructors());
612 unsigned weight
= dt
[cindex
].getWeight();
617 * Map terms to the result of expand definitions calling smt::expandDefinitions
620 struct SygusExpDefFormAttributeId
623 typedef expr::Attribute
<SygusExpDefFormAttributeId
, Node
>
624 SygusExpDefFormAttribute
;
626 void setExpandedDefinitionForm(Node op
, Node eop
)
628 op
.setAttribute(SygusExpDefFormAttribute(), eop
);
631 Node
getExpandedDefinitionForm(Node op
)
633 Node eop
= op
.getAttribute(SygusExpDefFormAttribute());
634 // if not set, assume original
635 return eop
.isNull() ? op
: eop
;
639 } // namespace datatypes
640 } // namespace theory