1 /********************* */
2 /*! \file sygus_unif_strat.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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.\endverbatim
12 ** \brief Implementation of sygus_unif_strat
15 #include "theory/quantifiers/sygus/sygus_unif_strat.h"
17 #include "theory/datatypes/datatypes_rewriter.h"
18 #include "theory/quantifiers/sygus/sygus_unif.h"
19 #include "theory/quantifiers/sygus/term_database_sygus.h"
20 #include "theory/quantifiers/term_util.h"
23 using namespace CVC4::kind
;
27 namespace quantifiers
{
29 std::ostream
& operator<<(std::ostream
& os
, EnumRole r
)
33 case enum_invalid
: os
<< "INVALID"; break;
34 case enum_io
: os
<< "IO"; break;
35 case enum_ite_condition
: os
<< "CONDITION"; break;
36 case enum_concat_term
: os
<< "CTERM"; break;
37 default: os
<< "enum_" << static_cast<unsigned>(r
); break;
42 std::ostream
& operator<<(std::ostream
& os
, NodeRole r
)
46 case role_equal
: os
<< "equal"; break;
47 case role_string_prefix
: os
<< "string_prefix"; break;
48 case role_string_suffix
: os
<< "string_suffix"; break;
49 case role_ite_condition
: os
<< "ite_condition"; break;
50 default: os
<< "role_" << static_cast<unsigned>(r
); break;
55 EnumRole
getEnumeratorRoleForNodeRole(NodeRole r
)
59 case role_equal
: return enum_io
; break;
60 case role_string_prefix
: return enum_concat_term
; break;
61 case role_string_suffix
: return enum_concat_term
; break;
62 case role_ite_condition
: return enum_ite_condition
; break;
68 std::ostream
& operator<<(std::ostream
& os
, StrategyType st
)
72 case strat_ITE
: os
<< "ITE"; break;
73 case strat_CONCAT_PREFIX
: os
<< "CONCAT_PREFIX"; break;
74 case strat_CONCAT_SUFFIX
: os
<< "CONCAT_SUFFIX"; break;
75 case strat_ID
: os
<< "ID"; break;
76 default: os
<< "strat_" << static_cast<unsigned>(st
); break;
81 void SygusUnifStrategy::initialize(QuantifiersEngine
* qe
,
83 std::vector
<Node
>& enums
)
85 Assert(d_candidate
.isNull());
90 // collect the enumerator types and form the strategy
91 collectEnumeratorTypes(d_root
, role_equal
);
92 // add the enumerators
93 enums
.insert(enums
.end(), d_esym_list
.begin(), d_esym_list
.end());
94 // finish the initialization of the strategy
95 // this computes if each node is conditional
96 std::map
<Node
, std::map
<NodeRole
, bool> > visited
;
97 finishInit(getRootEnumerator(), role_equal
, visited
, false);
100 void SygusUnifStrategy::initializeType(TypeNode tn
)
102 d_tinfo
[tn
].d_this_type
= tn
;
105 Node
SygusUnifStrategy::getRootEnumerator() const
107 std::map
<TypeNode
, EnumTypeInfo
>::const_iterator itt
= d_tinfo
.find(d_root
);
108 Assert(itt
!= d_tinfo
.end());
109 std::map
<EnumRole
, Node
>::const_iterator it
=
110 itt
->second
.d_enum
.find(enum_io
);
111 Assert(it
!= itt
->second
.d_enum
.end());
115 EnumInfo
& SygusUnifStrategy::getEnumInfo(Node e
)
117 std::map
<Node
, EnumInfo
>::iterator it
= d_einfo
.find(e
);
118 Assert(it
!= d_einfo
.end());
122 EnumTypeInfo
& SygusUnifStrategy::getEnumTypeInfo(TypeNode tn
)
124 std::map
<TypeNode
, EnumTypeInfo
>::iterator it
= d_tinfo
.find(tn
);
125 Assert(it
!= d_tinfo
.end());
128 // ----------------------------- establishing enumeration types
130 void SygusUnifStrategy::registerEnumerator(Node et
,
135 if (d_einfo
.find(et
) == d_einfo
.end())
137 Trace("sygus-unif-debug")
138 << "...register " << et
<< " for "
139 << static_cast<DatatypeType
>(tn
.toType()).getDatatype().getName();
140 Trace("sygus-unif-debug") << ", role = " << enum_role
141 << ", in search = " << inSearch
<< std::endl
;
142 d_einfo
[et
].initialize(enum_role
);
143 // if we are actually enumerating this (could be a compound node in the
147 std::map
<TypeNode
, Node
>::iterator itn
= d_master_enum
.find(tn
);
148 if (itn
== d_master_enum
.end())
150 // use this for the search
151 d_master_enum
[tn
] = et
;
152 d_esym_list
.push_back(et
);
153 d_einfo
[et
].d_enum_slave
.push_back(et
);
157 Trace("sygus-unif-debug") << "Make " << et
<< " a slave of "
158 << itn
->second
<< std::endl
;
159 d_einfo
[itn
->second
].d_enum_slave
.push_back(et
);
165 void SygusUnifStrategy::collectEnumeratorTypes(TypeNode tn
, NodeRole nrole
)
167 NodeManager
* nm
= NodeManager::currentNM();
168 if (d_tinfo
.find(tn
) == d_tinfo
.end())
171 Trace("sygus-unif") << "Register enumerating type : " << tn
<< std::endl
;
174 EnumTypeInfo
& eti
= d_tinfo
[tn
];
175 std::map
<NodeRole
, StrategyNode
>::iterator itsn
= eti
.d_snodes
.find(nrole
);
176 if (itsn
!= eti
.d_snodes
.end())
178 // already initialized
181 StrategyNode
& snode
= eti
.d_snodes
[nrole
];
183 // get the enumerator for this
184 EnumRole erole
= getEnumeratorRoleForNodeRole(nrole
);
187 std::map
<EnumRole
, Node
>::iterator iten
= eti
.d_enum
.find(erole
);
188 if (iten
== eti
.d_enum
.end())
190 ee
= nm
->mkSkolem("ee", tn
);
191 eti
.d_enum
[erole
] = ee
;
192 Trace("sygus-unif-debug")
193 << "...enumerator " << ee
<< " for "
194 << static_cast<DatatypeType
>(tn
.toType()).getDatatype().getName()
195 << ", role = " << erole
<< std::endl
;
202 // roles that we do not recurse on
203 if (nrole
== role_ite_condition
)
205 Trace("sygus-unif-debug") << "...this register (non-io)" << std::endl
;
206 registerEnumerator(ee
, tn
, erole
, true);
210 // look at information on how we will construct solutions for this type
211 Assert(tn
.isDatatype());
212 const Datatype
& dt
= static_cast<DatatypeType
>(tn
.toType()).getDatatype();
213 Assert(dt
.isSygus());
215 std::map
<Node
, std::vector
<StrategyType
> > cop_to_strat
;
216 std::map
<Node
, unsigned> cop_to_cindex
;
217 std::map
<Node
, std::map
<unsigned, Node
> > cop_to_child_templ
;
218 std::map
<Node
, std::map
<unsigned, Node
> > cop_to_child_templ_arg
;
219 std::map
<Node
, std::vector
<unsigned> > cop_to_carg_list
;
220 std::map
<Node
, std::vector
<TypeNode
> > cop_to_child_types
;
221 std::map
<Node
, std::vector
<Node
> > cop_to_sks
;
223 // whether we will enumerate the current type
224 bool search_this
= false;
225 for (unsigned j
= 0, ncons
= dt
.getNumConstructors(); j
< ncons
; j
++)
227 Node cop
= Node::fromExpr(dt
[j
].getConstructor());
228 Node op
= Node::fromExpr(dt
[j
].getSygusOp());
229 Trace("sygus-unif-debug") << "--- Infer strategy from " << cop
230 << " with sygus op " << op
<< "..." << std::endl
;
232 // expand the evaluation to see if this constuctor induces a strategy
233 std::vector
<Node
> utchildren
;
234 utchildren
.push_back(cop
);
235 std::vector
<Node
> sks
;
236 std::vector
<TypeNode
> sktns
;
237 for (unsigned k
= 0, nargs
= dt
[j
].getNumArgs(); k
< nargs
; k
++)
239 Type t
= dt
[j
][k
].getRangeType();
240 TypeNode ttn
= TypeNode::fromType(t
);
241 Node kv
= nm
->mkSkolem("ut", ttn
);
243 cop_to_sks
[cop
].push_back(kv
);
244 sktns
.push_back(ttn
);
245 utchildren
.push_back(kv
);
247 Node ut
= nm
->mkNode(APPLY_CONSTRUCTOR
, utchildren
);
248 std::vector
<Node
> echildren
;
249 echildren
.push_back(Node::fromExpr(dt
.getSygusEvaluationFunc()));
250 echildren
.push_back(ut
);
251 Node sbvl
= Node::fromExpr(dt
.getSygusVarList());
252 for (const Node
& sbv
: sbvl
)
254 echildren
.push_back(sbv
);
256 Node eut
= nm
->mkNode(APPLY_UF
, echildren
);
257 Trace("sygus-unif-debug2") << " Test evaluation of " << eut
<< "..."
259 eut
= d_qe
->getTermDatabaseSygus()->unfold(eut
);
260 Trace("sygus-unif-debug2") << " ...got " << eut
;
261 Trace("sygus-unif-debug2") << ", type : " << eut
.getType() << std::endl
;
263 // candidate strategy
264 if (eut
.getKind() == ITE
)
266 cop_to_strat
[cop
].push_back(strat_ITE
);
268 else if (eut
.getKind() == STRING_CONCAT
)
270 if (nrole
!= role_string_suffix
)
272 cop_to_strat
[cop
].push_back(strat_CONCAT_PREFIX
);
274 if (nrole
!= role_string_prefix
)
276 cop_to_strat
[cop
].push_back(strat_CONCAT_SUFFIX
);
279 else if (dt
[j
].isSygusIdFunc())
281 cop_to_strat
[cop
].push_back(strat_ID
);
284 // the kinds for which there is a strategy
285 if (cop_to_strat
.find(cop
) != cop_to_strat
.end())
287 // infer an injection from the arguments of the datatype
288 std::map
<unsigned, unsigned> templ_injection
;
289 std::vector
<Node
> vs
;
290 std::vector
<Node
> ss
;
291 std::map
<Node
, unsigned> templ_var_index
;
292 for (unsigned k
= 0, sksize
= sks
.size(); k
< sksize
; k
++)
294 Assert(sks
[k
].getType().isDatatype());
295 const Datatype
& cdt
=
296 static_cast<DatatypeType
>(sks
[k
].getType().toType()).getDatatype();
297 echildren
[0] = Node::fromExpr(cdt
.getSygusEvaluationFunc());
298 echildren
[1] = sks
[k
];
299 Trace("sygus-unif-debug2") << "...set eval dt to " << sks
[k
]
301 Node esk
= nm
->mkNode(APPLY_UF
, echildren
);
303 Node tvar
= nm
->mkSkolem("templ", esk
.getType());
304 templ_var_index
[tvar
] = k
;
305 Trace("sygus-unif-debug2") << "* template inference : looking for "
306 << tvar
<< " for arg " << k
<< std::endl
;
308 Trace("sygus-unif-debug2") << "* substitute : " << esk
<< " -> " << tvar
311 eut
= eut
.substitute(vs
.begin(), vs
.end(), ss
.begin(), ss
.end());
312 Trace("sygus-unif-debug2") << "Constructor " << j
<< ", base term is "
314 std::map
<unsigned, Node
> test_args
;
315 if (dt
[j
].isSygusIdFunc())
321 for (unsigned k
= 0, size
= eut
.getNumChildren(); k
< size
; k
++)
323 test_args
[k
] = eut
[k
];
327 // TODO : prefix grouping prefix/suffix
328 bool isAssoc
= TermUtil::isAssoc(eut
.getKind());
329 Trace("sygus-unif-debug2") << eut
.getKind() << " isAssoc = " << isAssoc
331 std::map
<unsigned, std::vector
<unsigned> > assoc_combine
;
332 std::vector
<unsigned> assoc_waiting
;
333 int assoc_last_valid_index
= -1;
334 for (std::pair
<const unsigned, Node
>& ta
: test_args
)
336 unsigned k
= ta
.first
;
337 Node eut_c
= ta
.second
;
338 // success if we can find a injection from args to sygus args
339 if (!inferTemplate(k
, eut_c
, templ_var_index
, templ_injection
))
341 Trace("sygus-unif-debug")
342 << "...fail: could not find injection (range)." << std::endl
;
343 cop_to_strat
.erase(cop
);
346 std::map
<unsigned, unsigned>::iterator itti
= templ_injection
.find(k
);
347 if (itti
!= templ_injection
.end())
349 // if associative, combine arguments if it is the same variable
350 if (isAssoc
&& assoc_last_valid_index
>= 0
351 && itti
->second
== templ_injection
[assoc_last_valid_index
])
353 templ_injection
.erase(k
);
354 assoc_combine
[assoc_last_valid_index
].push_back(k
);
358 assoc_last_valid_index
= (int)k
;
359 if (!assoc_waiting
.empty())
361 assoc_combine
[k
].insert(assoc_combine
[k
].end(),
362 assoc_waiting
.begin(),
363 assoc_waiting
.end());
364 assoc_waiting
.clear();
366 assoc_combine
[k
].push_back(k
);
374 Trace("sygus-unif-debug")
375 << "...fail: could not find injection (functional)."
377 cop_to_strat
.erase(cop
);
382 if (assoc_last_valid_index
>= 0)
384 assoc_combine
[assoc_last_valid_index
].push_back(k
);
388 assoc_waiting
.push_back(k
);
393 if (cop_to_strat
.find(cop
) != cop_to_strat
.end())
395 // construct the templates
396 if (!assoc_waiting
.empty())
398 // could not find a way to fit some arguments into injection
399 cop_to_strat
.erase(cop
);
403 for (std::pair
<const unsigned, Node
>& ta
: test_args
)
405 unsigned k
= ta
.first
;
406 Trace("sygus-unif-debug2") << "- processing argument " << k
<< "..."
408 if (templ_injection
.find(k
) != templ_injection
.end())
410 unsigned sk_index
= templ_injection
[k
];
411 if (std::find(cop_to_carg_list
[cop
].begin(),
412 cop_to_carg_list
[cop
].end(),
414 == cop_to_carg_list
[cop
].end())
416 cop_to_carg_list
[cop
].push_back(sk_index
);
420 Trace("sygus-unif-debug") << "...fail: duplicate argument used"
422 cop_to_strat
.erase(cop
);
425 // also store the template information, if necessary
429 std::vector
<unsigned>& ac
= assoc_combine
[k
];
431 std::vector
<Node
> children
;
432 for (unsigned ack
= 0, size_ac
= ac
.size(); ack
< size_ac
;
435 children
.push_back(eut
[ac
[ack
]]);
437 teut
= children
.size() == 1
439 : nm
->mkNode(eut
.getKind(), children
);
440 teut
= Rewriter::rewrite(teut
);
449 cop_to_child_templ
[cop
][k
] = teut
;
450 cop_to_child_templ_arg
[cop
][k
] = ss
[sk_index
];
451 Trace("sygus-unif-debug")
452 << " Arg " << k
<< " (template : " << teut
<< " arg "
453 << ss
[sk_index
] << "), index " << sk_index
<< std::endl
;
457 Trace("sygus-unif-debug") << " Arg " << k
<< ", index "
458 << sk_index
<< std::endl
;
459 Assert(teut
== ss
[sk_index
]);
470 if (cop_to_strat
.find(cop
) == cop_to_strat
.end())
472 Trace("sygus-unif") << "...constructor " << cop
473 << " does not correspond to a strategy." << std::endl
;
478 Trace("sygus-unif") << "-> constructor " << cop
479 << " matches strategy for " << eut
.getKind() << "..."
481 // collect children types
482 for (unsigned k
= 0, size
= cop_to_carg_list
[cop
].size(); k
< size
; k
++)
484 TypeNode tn
= sktns
[cop_to_carg_list
[cop
][k
]];
485 Trace("sygus-unif-debug")
486 << " Child type " << k
<< " : "
487 << static_cast<DatatypeType
>(tn
.toType()).getDatatype().getName()
489 cop_to_child_types
[cop
].push_back(tn
);
494 // check whether we should also enumerate the current type
495 Trace("sygus-unif-debug2") << " register this enumerator..." << std::endl
;
496 registerEnumerator(ee
, tn
, erole
, search_this
);
498 if (cop_to_strat
.empty())
500 Trace("sygus-unif") << "...consider " << dt
.getName() << " a basic type"
505 for (std::pair
<const Node
, std::vector
<StrategyType
> >& cstr
: cop_to_strat
)
507 Node cop
= cstr
.first
;
508 Trace("sygus-unif-debug") << "Constructor " << cop
<< " has "
509 << cstr
.second
.size() << " strategies..."
511 for (unsigned s
= 0, ssize
= cstr
.second
.size(); s
< ssize
; s
++)
513 EnumTypeInfoStrat
* cons_strat
= new EnumTypeInfoStrat
;
514 StrategyType strat
= cstr
.second
[s
];
516 cons_strat
->d_this
= strat
;
517 cons_strat
->d_cons
= cop
;
518 Trace("sygus-unif-debug") << "Process strategy #" << s
519 << " for operator : " << cop
<< " : " << strat
521 Assert(cop_to_child_types
.find(cop
) != cop_to_child_types
.end());
522 std::vector
<TypeNode
>& childTypes
= cop_to_child_types
[cop
];
523 Assert(cop_to_carg_list
.find(cop
) != cop_to_carg_list
.end());
524 std::vector
<unsigned>& cargList
= cop_to_carg_list
[cop
];
526 std::vector
<Node
> sol_templ_children
;
527 sol_templ_children
.resize(cop_to_sks
[cop
].size());
529 for (unsigned j
= 0, csize
= childTypes
.size(); j
< csize
; j
++)
531 // calculate if we should allocate a new enumerator : should be true
532 // if we have a new role
533 NodeRole nrole_c
= nrole
;
534 if (strat
== strat_ITE
)
538 nrole_c
= role_ite_condition
;
541 else if (strat
== strat_CONCAT_PREFIX
)
543 if ((j
+ 1) < childTypes
.size())
545 nrole_c
= role_string_prefix
;
548 else if (strat
== strat_CONCAT_SUFFIX
)
552 nrole_c
= role_string_suffix
;
555 // in all other cases, role is same as parent
557 // register the child type
558 TypeNode ct
= childTypes
[j
];
559 Node csk
= cop_to_sks
[cop
][cargList
[j
]];
560 cons_strat
->d_sol_templ_args
.push_back(csk
);
561 sol_templ_children
[cargList
[j
]] = csk
;
563 EnumRole erole_c
= getEnumeratorRoleForNodeRole(nrole_c
);
564 // make the enumerator
566 if (cop_to_child_templ
[cop
].find(j
) != cop_to_child_templ
[cop
].end())
568 // it is templated, allocate a fresh variable
569 et
= nm
->mkSkolem("et", ct
);
570 Trace("sygus-unif-debug")
571 << "...enumerate " << et
<< " of type "
572 << ((DatatypeType
)ct
.toType()).getDatatype().getName();
573 Trace("sygus-unif-debug") << " for arg " << j
<< " of "
574 << static_cast<DatatypeType
>(tn
.toType())
578 registerEnumerator(et
, ct
, erole_c
, true);
579 d_einfo
[et
].d_template
= cop_to_child_templ
[cop
][j
];
580 d_einfo
[et
].d_template_arg
= cop_to_child_templ_arg
[cop
][j
];
581 Assert(!d_einfo
[et
].d_template
.isNull());
582 Assert(!d_einfo
[et
].d_template_arg
.isNull());
586 Trace("sygus-unif-debug")
587 << "...child type enumerate "
588 << ((DatatypeType
)ct
.toType()).getDatatype().getName()
589 << ", node role = " << nrole_c
<< std::endl
;
590 collectEnumeratorTypes(ct
, nrole_c
);
591 // otherwise use the previous
592 Assert(d_tinfo
[ct
].d_enum
.find(erole_c
)
593 != d_tinfo
[ct
].d_enum
.end());
594 et
= d_tinfo
[ct
].d_enum
[erole_c
];
596 Trace("sygus-unif-debug") << "Register child enumerator " << et
597 << ", arg " << j
<< " of " << cop
598 << ", role = " << erole_c
<< std::endl
;
599 Assert(!et
.isNull());
600 cons_strat
->d_cenum
.push_back(std::pair
<Node
, NodeRole
>(et
, nrole_c
));
602 // children that are unused in the strategy can be arbitrary
603 for (unsigned j
= 0, stsize
= sol_templ_children
.size(); j
< stsize
;
606 if (sol_templ_children
[j
].isNull())
608 sol_templ_children
[j
] = cop_to_sks
[cop
][j
].getType().mkGroundTerm();
611 sol_templ_children
.insert(sol_templ_children
.begin(), cop
);
612 cons_strat
->d_sol_templ
=
613 nm
->mkNode(APPLY_CONSTRUCTOR
, sol_templ_children
);
614 if (strat
== strat_CONCAT_SUFFIX
)
616 std::reverse(cons_strat
->d_cenum
.begin(), cons_strat
->d_cenum
.end());
617 std::reverse(cons_strat
->d_sol_templ_args
.begin(),
618 cons_strat
->d_sol_templ_args
.end());
620 if (Trace
.isOn("sygus-unif"))
622 Trace("sygus-unif") << "Initialized strategy " << strat
;
625 << static_cast<DatatypeType
>(tn
.toType()).getDatatype().getName()
626 << ", operator " << cop
;
627 Trace("sygus-unif") << ", #children = " << cons_strat
->d_cenum
.size()
628 << ", solution template = (lambda ( ";
629 for (const Node
& targ
: cons_strat
->d_sol_templ_args
)
631 Trace("sygus-unif") << targ
<< " ";
633 Trace("sygus-unif") << ") " << cons_strat
->d_sol_templ
<< ")";
634 Trace("sygus-unif") << std::endl
;
637 snode
.d_strats
.push_back(cons_strat
);
643 bool SygusUnifStrategy::inferTemplate(
646 std::map
<Node
, unsigned>& templ_var_index
,
647 std::map
<unsigned, unsigned>& templ_injection
)
649 if (n
.getNumChildren() == 0)
651 std::map
<Node
, unsigned>::iterator itt
= templ_var_index
.find(n
);
652 if (itt
!= templ_var_index
.end())
654 unsigned kk
= itt
->second
;
655 std::map
<unsigned, unsigned>::iterator itti
= templ_injection
.find(k
);
656 if (itti
== templ_injection
.end())
658 Trace("sygus-unif-debug") << "...set template injection " << k
<< " -> "
660 templ_injection
[k
] = kk
;
662 else if (itti
->second
!= kk
)
664 // two distinct variables in this term, we fail
672 for (unsigned i
= 0; i
< n
.getNumChildren(); i
++)
674 if (!inferTemplate(k
, n
[i
], templ_var_index
, templ_injection
))
683 void SygusUnifStrategy::staticLearnRedundantOps(
684 std::map
<Node
, std::vector
<Node
>>& strategy_lemmas
)
686 for (unsigned i
= 0; i
< d_esym_list
.size(); i
++)
688 Node e
= d_esym_list
[i
];
689 std::map
<Node
, EnumInfo
>::iterator itn
= d_einfo
.find(e
);
690 Assert(itn
!= d_einfo
.end());
691 // see if there is anything we can eliminate
693 << "* Search enumerator #" << i
<< " : type "
694 << ((DatatypeType
)e
.getType().toType()).getDatatype().getName()
696 Trace("sygus-unif") << e
<< " has " << itn
->second
.d_enum_slave
.size()
697 << " slaves:" << std::endl
;
698 for (unsigned j
= 0; j
< itn
->second
.d_enum_slave
.size(); j
++)
700 Node es
= itn
->second
.d_enum_slave
[j
];
701 std::map
<Node
, EnumInfo
>::iterator itns
= d_einfo
.find(es
);
702 Assert(itns
!= d_einfo
.end());
703 Trace("sygus-unif") << " " << es
<< ", role = " << itns
->second
.getRole()
707 Trace("sygus-unif") << std::endl
;
708 Trace("sygus-unif") << "Strategy for candidate " << d_candidate
709 << " is : " << std::endl
;
710 debugPrint("sygus-unif");
711 std::map
<Node
, std::map
<NodeRole
, bool> > visited
;
712 std::map
<Node
, std::map
<unsigned, bool> > needs_cons
;
713 staticLearnRedundantOps(getRootEnumerator(), role_equal
, visited
, needs_cons
);
714 // now, check the needs_cons map
715 for (std::pair
<const Node
, std::map
<unsigned, bool> >& nce
: needs_cons
)
719 static_cast<DatatypeType
>(em
.getType().toType()).getDatatype();
720 std::vector
<Node
> lemmas
;
721 for (std::pair
<const unsigned, bool>& nc
: nce
.second
)
723 Assert(nc
.first
< dt
.getNumConstructors());
727 datatypes::DatatypesRewriter::mkTester(em
, nc
.first
, dt
).negate();
729 if (std::find(lemmas
.begin(), lemmas
.end(), tst
) == lemmas
.end())
731 Trace("sygus-unif") << "...can exclude based on : " << tst
733 lemmas
.push_back(tst
);
739 strategy_lemmas
[em
] = lemmas
;
744 void SygusUnifStrategy::debugPrint(const char* c
)
748 std::map
<Node
, std::map
<NodeRole
, bool> > visited
;
749 debugPrint(c
, getRootEnumerator(), role_equal
, visited
, 0);
753 void SygusUnifStrategy::staticLearnRedundantOps(
756 std::map
<Node
, std::map
<NodeRole
, bool> >& visited
,
757 std::map
<Node
, std::map
<unsigned, bool> >& needs_cons
)
759 if (visited
[e
].find(nrole
) != visited
[e
].end())
763 Trace("sygus-strat-slearn") << "Learn redundant operators " << e
<< " "
764 << nrole
<< "..." << std::endl
;
765 visited
[e
][nrole
] = true;
766 EnumInfo
& ei
= getEnumInfo(e
);
767 if (ei
.isTemplated())
771 TypeNode etn
= e
.getType();
772 EnumTypeInfo
& tinfo
= getEnumTypeInfo(etn
);
773 StrategyNode
& snode
= tinfo
.getStrategyNode(nrole
);
774 std::map
<unsigned, bool> needs_cons_curr
;
775 // constructors that correspond to strategies are not needed
776 // the intuition is that the strategy itself is responsible for constructing
777 // all terms that use the given constructor
778 for (unsigned j
= 0, size
= snode
.d_strats
.size(); j
< size
; j
++)
780 EnumTypeInfoStrat
* etis
= snode
.d_strats
[j
];
781 int cindex
= Datatype::indexOf(etis
->d_cons
.toExpr());
782 Assert(cindex
!= -1);
783 Trace("sygus-strat-slearn")
784 << "...by strategy, can exclude operator " << etis
->d_cons
<< std::endl
;
785 needs_cons_curr
[static_cast<unsigned>(cindex
)] = false;
786 for (std::pair
<Node
, NodeRole
>& cec
: etis
->d_cenum
)
788 staticLearnRedundantOps(cec
.first
, cec
.second
, visited
, needs_cons
);
791 // get the current datatype
792 const Datatype
& dt
= static_cast<DatatypeType
>(etn
.toType()).getDatatype();
793 // do not use recursive Boolean connectives for conditions of ITEs
794 if (nrole
== role_ite_condition
)
796 for (unsigned j
= 0, size
= dt
.getNumConstructors(); j
< size
; j
++)
798 Node op
= Node::fromExpr(dt
[j
].getSygusOp());
799 Trace("sygus-strat-slearn")
800 << "...for ite condition, look at operator : " << op
<< std::endl
;
801 if (op
.getKind() == kind::BUILTIN
)
803 Kind k
= NodeManager::operatorToKind(op
);
804 if (k
== NOT
|| k
== OR
|| k
== AND
)
806 // can eliminate if their argument types are simple loops to this type
808 for (unsigned k
= 0, nargs
= dt
[j
].getNumArgs(); k
< nargs
; k
++)
810 TypeNode tn
= TypeNode::fromType(dt
[j
].getArgType(k
));
819 Trace("sygus-strat-slearn")
820 << "...for ite condition, can exclude Boolean connective : "
822 needs_cons_curr
[j
] = false;
828 // all other constructors are needed
829 for (unsigned j
= 0, size
= dt
.getNumConstructors(); j
< size
; j
++)
831 if (needs_cons_curr
.find(j
) == needs_cons_curr
.end())
833 needs_cons_curr
[j
] = true;
836 // update the constructors that the master enumerator needs
837 if (needs_cons
.find(e
) == needs_cons
.end())
839 needs_cons
[e
] = needs_cons_curr
;
843 for (unsigned j
= 0, size
= dt
.getNumConstructors(); j
< size
; j
++)
845 needs_cons
[e
][j
] = needs_cons
[e
][j
] || needs_cons_curr
[j
];
850 void SygusUnifStrategy::finishInit(
853 std::map
<Node
, std::map
<NodeRole
, bool> >& visited
,
856 EnumInfo
& ei
= getEnumInfo(e
);
857 if (visited
[e
].find(nrole
) != visited
[e
].end()
858 && (!isCond
|| ei
.isConditional()))
862 visited
[e
][nrole
] = true;
868 if (ei
.isTemplated())
872 TypeNode etn
= e
.getType();
873 EnumTypeInfo
& tinfo
= getEnumTypeInfo(etn
);
874 StrategyNode
& snode
= tinfo
.getStrategyNode(nrole
);
875 for (unsigned j
= 0, size
= snode
.d_strats
.size(); j
< size
; j
++)
877 EnumTypeInfoStrat
* etis
= snode
.d_strats
[j
];
878 StrategyType strat
= etis
->d_this
;
879 bool newIsCond
= isCond
|| strat
== strat_ITE
;
880 for (std::pair
<Node
, NodeRole
>& cec
: etis
->d_cenum
)
882 finishInit(cec
.first
, cec
.second
, visited
, newIsCond
);
887 void SygusUnifStrategy::debugPrint(
891 std::map
<Node
, std::map
<NodeRole
, bool> >& visited
,
894 if (visited
[e
].find(nrole
) != visited
[e
].end())
897 Trace(c
) << e
<< " :: node role : " << nrole
<< std::endl
;
900 visited
[e
][nrole
] = true;
901 EnumInfo
& ei
= getEnumInfo(e
);
903 TypeNode etn
= e
.getType();
906 Trace(c
) << e
<< " :: node role : " << nrole
;
907 Trace(c
) << ", type : "
908 << static_cast<DatatypeType
>(etn
.toType()).getDatatype().getName();
909 if (ei
.isConditional())
911 Trace(c
) << ", conditional";
913 Trace(c
) << ", enum role : " << ei
.getRole();
915 if (ei
.isTemplated())
917 Trace(c
) << ", templated : (lambda " << ei
.d_template_arg
<< " "
918 << ei
.d_template
<< ")";
920 Trace(c
) << std::endl
;
922 EnumTypeInfo
& tinfo
= getEnumTypeInfo(etn
);
923 StrategyNode
& snode
= tinfo
.getStrategyNode(nrole
);
924 for (unsigned j
= 0, size
= snode
.d_strats
.size(); j
< size
; j
++)
926 EnumTypeInfoStrat
* etis
= snode
.d_strats
[j
];
927 StrategyType strat
= etis
->d_this
;
929 Trace(c
) << "Strategy : " << strat
<< ", from cons : " << etis
->d_cons
931 for (std::pair
<Node
, NodeRole
>& cec
: etis
->d_cenum
)
934 debugPrint(c
, cec
.first
, cec
.second
, visited
, ind
+ 2);
939 void EnumInfo::initialize(EnumRole role
) { d_role
= role
; }
941 StrategyNode
& EnumTypeInfo::getStrategyNode(NodeRole nrole
)
943 std::map
<NodeRole
, StrategyNode
>::iterator it
= d_snodes
.find(nrole
);
944 Assert(it
!= d_snodes
.end());
948 bool EnumTypeInfoStrat::isValid(UnifContext
& x
)
950 if ((x
.getCurrentRole() == role_string_prefix
951 && d_this
== strat_CONCAT_SUFFIX
)
952 || (x
.getCurrentRole() == role_string_suffix
953 && d_this
== strat_CONCAT_PREFIX
))
960 StrategyNode::~StrategyNode()
962 for (unsigned j
= 0, size
= d_strats
.size(); j
< size
; j
++)
969 void SygusUnifStrategy::indent(const char* c
, int ind
)
973 for (int i
= 0; i
< ind
; i
++)
980 } /* CVC4::theory::quantifiers namespace */
981 } /* CVC4::theory namespace */
982 } /* CVC4 namespace */