1 /******************************************************************************
2 * Top contributors (to current version):
3 * Andrew Reynolds, Haniel Barbosa, Mathias Preiner
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 sygus_unif_strat.
16 #include "theory/quantifiers/sygus/sygus_unif_strat.h"
18 #include "expr/dtype.h"
19 #include "expr/dtype_cons.h"
20 #include "expr/skolem_manager.h"
21 #include "theory/datatypes/theory_datatypes_utils.h"
22 #include "theory/quantifiers/sygus/sygus_eval_unfold.h"
23 #include "theory/quantifiers/sygus/sygus_unif.h"
24 #include "theory/quantifiers/sygus/term_database_sygus.h"
25 #include "theory/quantifiers/term_util.h"
28 using namespace cvc5::kind
;
32 namespace quantifiers
{
34 std::ostream
& operator<<(std::ostream
& os
, EnumRole r
)
38 case enum_invalid
: os
<< "INVALID"; break;
39 case enum_io
: os
<< "IO"; break;
40 case enum_ite_condition
: os
<< "CONDITION"; break;
41 case enum_concat_term
: os
<< "CTERM"; break;
42 default: os
<< "enum_" << static_cast<unsigned>(r
); break;
47 std::ostream
& operator<<(std::ostream
& os
, NodeRole r
)
51 case role_equal
: os
<< "equal"; break;
52 case role_string_prefix
: os
<< "string_prefix"; break;
53 case role_string_suffix
: os
<< "string_suffix"; break;
54 case role_ite_condition
: os
<< "ite_condition"; break;
55 default: os
<< "role_" << static_cast<unsigned>(r
); break;
60 EnumRole
getEnumeratorRoleForNodeRole(NodeRole r
)
64 case role_equal
: return enum_io
; break;
65 case role_string_prefix
: return enum_concat_term
; break;
66 case role_string_suffix
: return enum_concat_term
; break;
67 case role_ite_condition
: return enum_ite_condition
; break;
73 std::ostream
& operator<<(std::ostream
& os
, StrategyType st
)
77 case strat_ITE
: os
<< "ITE"; break;
78 case strat_CONCAT_PREFIX
: os
<< "CONCAT_PREFIX"; break;
79 case strat_CONCAT_SUFFIX
: os
<< "CONCAT_SUFFIX"; break;
80 case strat_ID
: os
<< "ID"; break;
81 default: os
<< "strat_" << static_cast<unsigned>(st
); break;
86 void SygusUnifStrategy::initialize(TermDbSygus
* tds
,
88 std::vector
<Node
>& enums
)
90 Assert(d_candidate
.isNull());
95 // collect the enumerator types and form the strategy
96 buildStrategyGraph(d_root
, role_equal
);
97 // add the enumerators
98 enums
.insert(enums
.end(), d_esym_list
.begin(), d_esym_list
.end());
99 // finish the initialization of the strategy
100 // this computes if each node is conditional
101 std::map
<Node
, std::map
<NodeRole
, bool> > visited
;
102 finishInit(getRootEnumerator(), role_equal
, visited
, false);
105 void SygusUnifStrategy::initializeType(TypeNode tn
)
107 Trace("sygus-unif") << "SygusUnifStrategy: initialize : " << tn
<< " for "
108 << d_candidate
<< std::endl
;
109 d_tinfo
[tn
].d_this_type
= tn
;
112 Node
SygusUnifStrategy::getRootEnumerator() const
114 std::map
<TypeNode
, EnumTypeInfo
>::const_iterator itt
= d_tinfo
.find(d_root
);
115 Assert(itt
!= d_tinfo
.end());
116 std::map
<EnumRole
, Node
>::const_iterator it
=
117 itt
->second
.d_enum
.find(enum_io
);
118 Assert(it
!= itt
->second
.d_enum
.end());
122 EnumInfo
& SygusUnifStrategy::getEnumInfo(Node e
)
124 std::map
<Node
, EnumInfo
>::iterator it
= d_einfo
.find(e
);
125 Assert(it
!= d_einfo
.end());
129 EnumTypeInfo
& SygusUnifStrategy::getEnumTypeInfo(TypeNode tn
)
131 Trace("sygus-unif") << "SygusUnifStrategy: get : " << tn
<< " for "
132 << d_candidate
<< std::endl
;
133 std::map
<TypeNode
, EnumTypeInfo
>::iterator it
= d_tinfo
.find(tn
);
134 Assert(it
!= d_tinfo
.end());
137 // ----------------------------- establishing enumeration types
139 void SygusUnifStrategy::registerStrategyPoint(Node et
,
144 if (d_einfo
.find(et
) == d_einfo
.end())
146 Trace("sygus-unif-debug")
147 << "...register " << et
<< " for " << tn
.getDType().getName();
148 Trace("sygus-unif-debug") << ", role = " << enum_role
149 << ", in search = " << inSearch
<< std::endl
;
150 d_einfo
[et
].initialize(enum_role
);
151 // if we are actually enumerating this (could be a compound node in the
155 std::map
<TypeNode
, Node
>::iterator itn
= d_master_enum
.find(tn
);
156 if (itn
== d_master_enum
.end())
158 // use this for the search
159 d_master_enum
[tn
] = et
;
160 d_esym_list
.push_back(et
);
161 d_einfo
[et
].d_enum_slave
.push_back(et
);
165 Trace("sygus-unif-debug") << "Make " << et
<< " a slave of "
166 << itn
->second
<< std::endl
;
167 d_einfo
[itn
->second
].d_enum_slave
.push_back(et
);
173 void SygusUnifStrategy::buildStrategyGraph(TypeNode tn
, NodeRole nrole
)
175 NodeManager
* nm
= NodeManager::currentNM();
176 SkolemManager
* sm
= nm
->getSkolemManager();
177 if (d_tinfo
.find(tn
) == d_tinfo
.end())
180 Trace("sygus-unif") << "Register enumerating type : " << tn
<< std::endl
;
183 EnumTypeInfo
& eti
= d_tinfo
[tn
];
184 std::map
<NodeRole
, StrategyNode
>::iterator itsn
= eti
.d_snodes
.find(nrole
);
185 if (itsn
!= eti
.d_snodes
.end())
187 // already initialized
190 StrategyNode
& snode
= eti
.d_snodes
[nrole
];
192 // get the enumerator for this
193 EnumRole erole
= getEnumeratorRoleForNodeRole(nrole
);
196 std::map
<EnumRole
, Node
>::iterator iten
= eti
.d_enum
.find(erole
);
197 if (iten
== eti
.d_enum
.end())
199 ee
= sm
->mkDummySkolem("ee", tn
);
200 eti
.d_enum
[erole
] = ee
;
201 Trace("sygus-unif-debug")
202 << "...enumerator " << ee
<< " for " << tn
.getDType().getName()
203 << ", role = " << erole
<< std::endl
;
210 // roles that we do not recurse on
211 if (nrole
== role_ite_condition
)
213 Trace("sygus-unif-debug") << "...this register (non-io)" << std::endl
;
214 registerStrategyPoint(ee
, tn
, erole
, true);
218 // look at information on how we will construct solutions for this type
219 // we know this is a sygus datatype since it is either the top-level type
220 // in the strategy graph, or was recursed by a strategy we inferred.
221 Assert(tn
.isDatatype());
222 const DType
& dt
= tn
.getDType();
223 Assert(dt
.isSygus());
225 std::map
<Node
, std::vector
<StrategyType
> > cop_to_strat
;
226 std::map
<Node
, unsigned> cop_to_cindex
;
227 std::map
<Node
, std::map
<unsigned, Node
> > cop_to_child_templ
;
228 std::map
<Node
, std::map
<unsigned, Node
> > cop_to_child_templ_arg
;
229 std::map
<Node
, std::vector
<unsigned> > cop_to_carg_list
;
230 std::map
<Node
, std::vector
<TypeNode
> > cop_to_child_types
;
231 std::map
<Node
, std::vector
<Node
> > cop_to_sks
;
233 // whether we will enumerate the current type
234 bool search_this
= false;
235 for (unsigned j
= 0, ncons
= dt
.getNumConstructors(); j
< ncons
; j
++)
237 Node cop
= dt
[j
].getConstructor();
238 Node op
= dt
[j
].getSygusOp();
239 Trace("sygus-unif-debug") << "--- Infer strategy from " << cop
240 << " with sygus op " << op
<< "..." << std::endl
;
242 // expand the evaluation to see if this constuctor induces a strategy
243 std::vector
<Node
> utchildren
;
244 utchildren
.push_back(cop
);
245 std::vector
<Node
> sks
;
246 std::vector
<TypeNode
> sktns
;
247 for (unsigned k
= 0, nargs
= dt
[j
].getNumArgs(); k
< nargs
; k
++)
249 TypeNode ttn
= dt
[j
][k
].getRangeType();
250 Node kv
= sm
->mkDummySkolem("ut", ttn
);
252 cop_to_sks
[cop
].push_back(kv
);
253 sktns
.push_back(ttn
);
254 utchildren
.push_back(kv
);
256 Node ut
= nm
->mkNode(APPLY_CONSTRUCTOR
, utchildren
);
257 std::vector
<Node
> echildren
;
258 echildren
.push_back(ut
);
259 Node sbvl
= dt
.getSygusVarList();
260 for (const Node
& sbv
: sbvl
)
262 echildren
.push_back(sbv
);
264 Node eut
= nm
->mkNode(DT_SYGUS_EVAL
, echildren
);
265 Trace("sygus-unif-debug2") << " Test evaluation of " << eut
<< "..."
267 eut
= d_tds
->rewriteNode(eut
);
268 Trace("sygus-unif-debug2") << " ...got " << eut
;
269 Trace("sygus-unif-debug2") << ", type : " << eut
.getType() << std::endl
;
271 // candidate strategy
272 if (eut
.getKind() == ITE
)
274 cop_to_strat
[cop
].push_back(strat_ITE
);
276 else if (eut
.getKind() == STRING_CONCAT
)
278 if (nrole
!= role_string_suffix
)
280 cop_to_strat
[cop
].push_back(strat_CONCAT_PREFIX
);
282 if (nrole
!= role_string_prefix
)
284 cop_to_strat
[cop
].push_back(strat_CONCAT_SUFFIX
);
287 else if (dt
[j
].isSygusIdFunc())
289 cop_to_strat
[cop
].push_back(strat_ID
);
292 // the kinds for which there is a strategy
293 if (cop_to_strat
.find(cop
) != cop_to_strat
.end())
295 // infer an injection from the arguments of the datatype
296 std::map
<unsigned, unsigned> templ_injection
;
297 std::vector
<Node
> vs
;
298 std::vector
<Node
> ss
;
299 std::map
<Node
, unsigned> templ_var_index
;
300 for (unsigned k
= 0, sksize
= sks
.size(); k
< sksize
; k
++)
302 Assert(sks
[k
].getType().isDatatype());
303 echildren
[0] = sks
[k
];
304 Trace("sygus-unif-debug2") << "...set eval dt to " << sks
[k
]
306 Node esk
= nm
->mkNode(DT_SYGUS_EVAL
, echildren
);
308 Node tvar
= sm
->mkDummySkolem("templ", esk
.getType());
309 templ_var_index
[tvar
] = k
;
310 Trace("sygus-unif-debug2") << "* template inference : looking for "
311 << tvar
<< " for arg " << k
<< std::endl
;
313 Trace("sygus-unif-debug2") << "* substitute : " << esk
<< " -> " << tvar
316 eut
= eut
.substitute(vs
.begin(), vs
.end(), ss
.begin(), ss
.end());
317 Trace("sygus-unif-debug2") << "Constructor " << j
<< ", base term is "
319 std::map
<unsigned, Node
> test_args
;
320 if (dt
[j
].isSygusIdFunc())
326 for (unsigned k
= 0, size
= eut
.getNumChildren(); k
< size
; k
++)
328 test_args
[k
] = eut
[k
];
332 // TODO : prefix grouping prefix/suffix
333 bool isAssoc
= TermUtil::isAssoc(eut
.getKind());
334 Trace("sygus-unif-debug2") << eut
.getKind() << " isAssoc = " << isAssoc
336 std::map
<unsigned, std::vector
<unsigned> > assoc_combine
;
337 std::vector
<unsigned> assoc_waiting
;
338 int assoc_last_valid_index
= -1;
339 for (std::pair
<const unsigned, Node
>& ta
: test_args
)
341 unsigned k
= ta
.first
;
342 Node eut_c
= ta
.second
;
343 // success if we can find a injection from args to sygus args
344 if (!inferTemplate(k
, eut_c
, templ_var_index
, templ_injection
))
346 Trace("sygus-unif-debug")
347 << "...fail: could not find injection (range)." << std::endl
;
348 cop_to_strat
.erase(cop
);
351 std::map
<unsigned, unsigned>::iterator itti
= templ_injection
.find(k
);
352 if (itti
!= templ_injection
.end())
354 // if associative, combine arguments if it is the same variable
355 if (isAssoc
&& assoc_last_valid_index
>= 0
356 && itti
->second
== templ_injection
[assoc_last_valid_index
])
358 templ_injection
.erase(k
);
359 assoc_combine
[assoc_last_valid_index
].push_back(k
);
363 assoc_last_valid_index
= (int)k
;
364 if (!assoc_waiting
.empty())
366 assoc_combine
[k
].insert(assoc_combine
[k
].end(),
367 assoc_waiting
.begin(),
368 assoc_waiting
.end());
369 assoc_waiting
.clear();
371 assoc_combine
[k
].push_back(k
);
379 Trace("sygus-unif-debug")
380 << "...fail: could not find injection (functional)."
382 cop_to_strat
.erase(cop
);
387 if (assoc_last_valid_index
>= 0)
389 assoc_combine
[assoc_last_valid_index
].push_back(k
);
393 assoc_waiting
.push_back(k
);
398 if (cop_to_strat
.find(cop
) != cop_to_strat
.end())
400 // construct the templates
401 if (!assoc_waiting
.empty())
403 // could not find a way to fit some arguments into injection
404 cop_to_strat
.erase(cop
);
408 for (std::pair
<const unsigned, Node
>& ta
: test_args
)
410 unsigned k
= ta
.first
;
411 Trace("sygus-unif-debug2") << "- processing argument " << k
<< "..."
413 if (templ_injection
.find(k
) != templ_injection
.end())
415 unsigned sk_index
= templ_injection
[k
];
416 if (std::find(cop_to_carg_list
[cop
].begin(),
417 cop_to_carg_list
[cop
].end(),
419 == cop_to_carg_list
[cop
].end())
421 cop_to_carg_list
[cop
].push_back(sk_index
);
425 Trace("sygus-unif-debug") << "...fail: duplicate argument used"
427 cop_to_strat
.erase(cop
);
430 // also store the template information, if necessary
434 std::vector
<unsigned>& ac
= assoc_combine
[k
];
436 std::vector
<Node
> children
;
437 for (unsigned ack
= 0, size_ac
= ac
.size(); ack
< size_ac
;
440 children
.push_back(eut
[ac
[ack
]]);
442 teut
= children
.size() == 1
444 : nm
->mkNode(eut
.getKind(), children
);
445 teut
= rewrite(teut
);
454 cop_to_child_templ
[cop
][k
] = teut
;
455 cop_to_child_templ_arg
[cop
][k
] = ss
[sk_index
];
456 Trace("sygus-unif-debug")
457 << " Arg " << k
<< " (template : " << teut
<< " arg "
458 << ss
[sk_index
] << "), index " << sk_index
<< std::endl
;
462 Trace("sygus-unif-debug") << " Arg " << k
<< ", index "
463 << sk_index
<< std::endl
;
464 Assert(teut
== ss
[sk_index
]);
476 std::map
<Node
, std::vector
<StrategyType
> >::iterator itcs
= cop_to_strat
.find(cop
);
477 if (itcs
!= cop_to_strat
.end())
479 Trace("sygus-unif") << "-> constructor " << cop
480 << " matches strategy for " << eut
.getKind() << "..."
482 // collect children types
483 for (unsigned k
= 0, size
= cop_to_carg_list
[cop
].size(); k
< size
; k
++)
485 TypeNode ctn
= sktns
[cop_to_carg_list
[cop
][k
]];
486 Trace("sygus-unif-debug") << " Child type " << k
<< " : "
487 << ctn
.getDType().getName() << std::endl
;
488 cop_to_child_types
[cop
].push_back(ctn
);
490 // if there are checks on the consistency of child types wrt strategies,
491 // these should be enforced here. We currently have none.
493 if (cop_to_strat
.find(cop
) == cop_to_strat
.end())
495 Trace("sygus-unif") << "...constructor " << cop
496 << " does not correspond to a strategy." << std::endl
;
501 // check whether we should also enumerate the current type
502 Trace("sygus-unif-debug2") << " register this strategy ..." << std::endl
;
503 registerStrategyPoint(ee
, tn
, erole
, search_this
);
505 if (cop_to_strat
.empty())
507 Trace("sygus-unif") << "...consider " << dt
.getName() << " a basic type"
512 for (std::pair
<const Node
, std::vector
<StrategyType
> >& cstr
: cop_to_strat
)
514 Node cop
= cstr
.first
;
515 Trace("sygus-unif-debug") << "Constructor " << cop
<< " has "
516 << cstr
.second
.size() << " strategies..."
518 for (unsigned s
= 0, ssize
= cstr
.second
.size(); s
< ssize
; s
++)
520 EnumTypeInfoStrat
* cons_strat
= new EnumTypeInfoStrat
;
521 StrategyType strat
= cstr
.second
[s
];
523 cons_strat
->d_this
= strat
;
524 cons_strat
->d_cons
= cop
;
525 Trace("sygus-unif-debug") << "Process strategy #" << s
526 << " for operator : " << cop
<< " : " << strat
528 Assert(cop_to_child_types
.find(cop
) != cop_to_child_types
.end());
529 std::vector
<TypeNode
>& childTypes
= cop_to_child_types
[cop
];
530 Assert(cop_to_carg_list
.find(cop
) != cop_to_carg_list
.end());
531 std::vector
<unsigned>& cargList
= cop_to_carg_list
[cop
];
533 std::vector
<Node
> sol_templ_children
;
534 sol_templ_children
.resize(cop_to_sks
[cop
].size());
536 for (unsigned j
= 0, csize
= childTypes
.size(); j
< csize
; j
++)
538 // calculate if we should allocate a new enumerator : should be true
539 // if we have a new role
540 NodeRole nrole_c
= nrole
;
541 if (strat
== strat_ITE
)
545 nrole_c
= role_ite_condition
;
548 else if (strat
== strat_CONCAT_PREFIX
)
550 if ((j
+ 1) < childTypes
.size())
552 nrole_c
= role_string_prefix
;
555 else if (strat
== strat_CONCAT_SUFFIX
)
559 nrole_c
= role_string_suffix
;
562 // in all other cases, role is same as parent
564 // register the child type
565 TypeNode ct
= childTypes
[j
];
566 Node csk
= cop_to_sks
[cop
][cargList
[j
]];
567 cons_strat
->d_sol_templ_args
.push_back(csk
);
568 sol_templ_children
[cargList
[j
]] = csk
;
570 EnumRole erole_c
= getEnumeratorRoleForNodeRole(nrole_c
);
571 // make the enumerator
573 // Build the strategy recursively, regardless of whether the
574 // enumerator is templated.
575 buildStrategyGraph(ct
, nrole_c
);
576 if (cop_to_child_templ
[cop
].find(j
) != cop_to_child_templ
[cop
].end())
578 // it is templated, allocate a fresh variable
579 et
= sm
->mkDummySkolem("et", ct
);
580 Trace("sygus-unif-debug") << "...enumerate " << et
<< " of type "
581 << ct
.getDType().getName();
582 Trace("sygus-unif-debug") << " for arg " << j
<< " of "
583 << tn
.getDType().getName() << std::endl
;
584 registerStrategyPoint(et
, ct
, erole_c
, true);
585 d_einfo
[et
].d_template
= cop_to_child_templ
[cop
][j
];
586 d_einfo
[et
].d_template_arg
= cop_to_child_templ_arg
[cop
][j
];
587 Assert(!d_einfo
[et
].d_template
.isNull());
588 Assert(!d_einfo
[et
].d_template_arg
.isNull());
592 Trace("sygus-unif-debug")
593 << "...child type enumerate " << ct
.getDType().getName()
594 << ", node role = " << nrole_c
<< std::endl
;
595 // otherwise use the previous
596 Assert(d_tinfo
[ct
].d_enum
.find(erole_c
)
597 != d_tinfo
[ct
].d_enum
.end());
598 et
= d_tinfo
[ct
].d_enum
[erole_c
];
600 Trace("sygus-unif-debug") << "Register child enumerator " << et
601 << ", arg " << j
<< " of " << cop
602 << ", role = " << erole_c
<< std::endl
;
603 Assert(!et
.isNull());
604 cons_strat
->d_cenum
.push_back(std::pair
<Node
, NodeRole
>(et
, nrole_c
));
606 // children that are unused in the strategy can be arbitrary
607 for (unsigned j
= 0, stsize
= sol_templ_children
.size(); j
< stsize
;
610 if (sol_templ_children
[j
].isNull())
612 sol_templ_children
[j
] = cop_to_sks
[cop
][j
].getType().mkGroundTerm();
615 sol_templ_children
.insert(sol_templ_children
.begin(), cop
);
616 cons_strat
->d_sol_templ
=
617 nm
->mkNode(APPLY_CONSTRUCTOR
, sol_templ_children
);
618 if (strat
== strat_CONCAT_SUFFIX
)
620 std::reverse(cons_strat
->d_cenum
.begin(), cons_strat
->d_cenum
.end());
621 std::reverse(cons_strat
->d_sol_templ_args
.begin(),
622 cons_strat
->d_sol_templ_args
.end());
624 if (Trace
.isOn("sygus-unif"))
626 Trace("sygus-unif") << "Initialized strategy " << strat
;
628 << " for " << tn
.getDType().getName() << ", operator " << cop
;
629 Trace("sygus-unif") << ", #children = " << cons_strat
->d_cenum
.size()
630 << ", solution template = (lambda ( ";
631 for (const Node
& targ
: cons_strat
->d_sol_templ_args
)
633 Trace("sygus-unif") << targ
<< " ";
635 Trace("sygus-unif") << ") " << cons_strat
->d_sol_templ
<< ")";
636 Trace("sygus-unif") << std::endl
;
639 snode
.d_strats
.push_back(cons_strat
);
645 bool SygusUnifStrategy::inferTemplate(
648 std::map
<Node
, unsigned>& templ_var_index
,
649 std::map
<unsigned, unsigned>& templ_injection
)
651 if (n
.getNumChildren() == 0)
653 std::map
<Node
, unsigned>::iterator itt
= templ_var_index
.find(n
);
654 if (itt
!= templ_var_index
.end())
656 unsigned kk
= itt
->second
;
657 std::map
<unsigned, unsigned>::iterator itti
= templ_injection
.find(k
);
658 if (itti
== templ_injection
.end())
660 Trace("sygus-unif-debug") << "...set template injection " << k
<< " -> "
662 templ_injection
[k
] = kk
;
664 else if (itti
->second
!= kk
)
666 // two distinct variables in this term, we fail
674 for (unsigned i
= 0; i
< n
.getNumChildren(); i
++)
676 if (!inferTemplate(k
, n
[i
], templ_var_index
, templ_injection
))
685 void SygusUnifStrategy::staticLearnRedundantOps(
686 std::map
<Node
, std::vector
<Node
>>& strategy_lemmas
)
688 StrategyRestrictions restrictions
;
689 staticLearnRedundantOps(strategy_lemmas
, restrictions
);
692 void SygusUnifStrategy::staticLearnRedundantOps(
693 std::map
<Node
, std::vector
<Node
>>& strategy_lemmas
,
694 StrategyRestrictions
& restrictions
)
696 for (unsigned i
= 0; i
< d_esym_list
.size(); i
++)
698 Node e
= d_esym_list
[i
];
699 std::map
<Node
, EnumInfo
>::iterator itn
= d_einfo
.find(e
);
700 Assert(itn
!= d_einfo
.end());
701 // see if there is anything we can eliminate
702 Trace("sygus-unif") << "* Search enumerator #" << i
<< " : type "
703 << e
.getType().getDType().getName() << " : ";
704 Trace("sygus-unif") << e
<< " has " << itn
->second
.d_enum_slave
.size()
705 << " slaves:" << std::endl
;
706 for (unsigned j
= 0; j
< itn
->second
.d_enum_slave
.size(); j
++)
708 Node es
= itn
->second
.d_enum_slave
[j
];
709 std::map
<Node
, EnumInfo
>::iterator itns
= d_einfo
.find(es
);
710 Assert(itns
!= d_einfo
.end());
711 Trace("sygus-unif") << " " << es
<< ", role = " << itns
->second
.getRole()
715 Trace("sygus-unif") << std::endl
;
716 Trace("sygus-unif") << "Strategy for candidate " << d_candidate
717 << " is : " << std::endl
;
718 debugPrint("sygus-unif");
719 std::map
<Node
, std::map
<NodeRole
, bool> > visited
;
720 std::map
<Node
, std::map
<unsigned, bool> > needs_cons
;
721 staticLearnRedundantOps(
722 getRootEnumerator(), role_equal
, visited
, needs_cons
, restrictions
);
723 // now, check the needs_cons map
724 for (std::pair
<const Node
, std::map
<unsigned, bool> >& nce
: needs_cons
)
727 const DType
& dt
= em
.getType().getDType();
728 std::vector
<Node
> lemmas
;
729 for (std::pair
<const unsigned, bool>& nc
: nce
.second
)
731 Assert(nc
.first
< dt
.getNumConstructors());
734 Node tst
= datatypes::utils::mkTester(em
, nc
.first
, dt
).negate();
736 if (std::find(lemmas
.begin(), lemmas
.end(), tst
) == lemmas
.end())
738 Trace("sygus-unif") << "...can exclude based on : " << tst
740 lemmas
.push_back(tst
);
746 strategy_lemmas
[em
] = lemmas
;
751 void SygusUnifStrategy::debugPrint(const char* c
)
755 std::map
<Node
, std::map
<NodeRole
, bool> > visited
;
756 debugPrint(c
, getRootEnumerator(), role_equal
, visited
, 0);
760 void SygusUnifStrategy::staticLearnRedundantOps(
763 std::map
<Node
, std::map
<NodeRole
, bool>>& visited
,
764 std::map
<Node
, std::map
<unsigned, bool>>& needs_cons
,
765 StrategyRestrictions
& restrictions
)
767 if (visited
[e
].find(nrole
) != visited
[e
].end())
771 Trace("sygus-strat-slearn") << "Learn redundant operators " << e
<< " "
772 << nrole
<< "..." << std::endl
;
773 visited
[e
][nrole
] = true;
774 EnumInfo
& ei
= getEnumInfo(e
);
775 if (ei
.isTemplated())
779 TypeNode etn
= e
.getType();
780 EnumTypeInfo
& tinfo
= getEnumTypeInfo(etn
);
781 StrategyNode
& snode
= tinfo
.getStrategyNode(nrole
);
782 // the constructors of the current strategy point we need
783 std::map
<unsigned, bool> needs_cons_curr
;
784 // get the unused strategies
785 std::map
<Node
, std::unordered_set
<unsigned>>::iterator itus
=
786 restrictions
.d_unused_strategies
.find(e
);
787 std::unordered_set
<unsigned> unused_strats
;
788 if (itus
!= restrictions
.d_unused_strategies
.end())
790 unused_strats
.insert(itus
->second
.begin(), itus
->second
.end());
792 for (unsigned j
= 0, size
= snode
.d_strats
.size(); j
< size
; j
++)
794 // if we are not using this strategy, there is nothing to do
795 if (unused_strats
.find(j
) != unused_strats
.end())
799 EnumTypeInfoStrat
* etis
= snode
.d_strats
[j
];
800 unsigned cindex
= datatypes::utils::indexOf(etis
->d_cons
);
801 // constructors that correspond to strategies are not needed
802 // the intuition is that the strategy itself is responsible for constructing
803 // all terms that use the given constructor
804 Trace("sygus-strat-slearn") << "...by strategy, can exclude operator "
805 << etis
->d_cons
<< std::endl
;
806 needs_cons_curr
[cindex
] = false;
807 // try to eliminate from etn's datatype all operators except TRUE/FALSE if
808 // arguments of ITE are the same BOOL type
809 if (restrictions
.d_iteReturnBoolConst
)
811 const DType
& dt
= etn
.getDType();
812 Node op
= dt
[cindex
].getSygusOp();
813 TypeNode sygus_tn
= dt
.getSygusType();
814 if (op
.getKind() == kind::BUILTIN
815 && NodeManager::operatorToKind(op
) == ITE
&& sygus_tn
.isBoolean()
816 && (dt
[cindex
].getArgType(1) == dt
[cindex
].getArgType(2)))
818 unsigned ncons
= dt
.getNumConstructors(), indexT
= ncons
,
820 for (unsigned k
= 0; k
< ncons
; ++k
)
822 Node op_arg
= dt
[k
].getSygusOp();
823 if (dt
[k
].getNumArgs() > 0 || !op_arg
.isConst())
827 if (op_arg
.getConst
<bool>())
836 if (indexT
< ncons
&& indexF
< ncons
)
838 Trace("sygus-strat-slearn")
839 << "...for ite boolean arg, can exclude all operators but T/F\n";
840 for (unsigned k
= 0; k
< ncons
; ++k
)
842 needs_cons_curr
[k
] = false;
844 needs_cons_curr
[indexT
] = true;
845 needs_cons_curr
[indexF
] = true;
849 for (std::pair
<Node
, NodeRole
>& cec
: etis
->d_cenum
)
851 staticLearnRedundantOps(
852 cec
.first
, cec
.second
, visited
, needs_cons
, restrictions
);
855 // get the current datatype
856 const DType
& dt
= etn
.getDType();
857 // do not use recursive Boolean connectives for conditions of ITEs
858 if (nrole
== role_ite_condition
&& restrictions
.d_iteCondOnlyAtoms
)
860 TypeNode sygus_tn
= dt
.getSygusType();
861 for (unsigned j
= 0, size
= dt
.getNumConstructors(); j
< size
; j
++)
863 Node op
= dt
[j
].getSygusOp();
864 Trace("sygus-strat-slearn")
865 << "...for ite condition, look at operator : " << op
<< std::endl
;
866 if (op
.isConst() && dt
[j
].getNumArgs() == 0)
868 Trace("sygus-strat-slearn")
869 << "...for ite condition, can exclude Boolean constant " << op
871 needs_cons_curr
[j
] = false;
874 if (op
.getKind() == kind::BUILTIN
)
876 Kind kind
= NodeManager::operatorToKind(op
);
877 if (kind
== NOT
|| kind
== OR
|| kind
== AND
|| kind
== ITE
)
879 // can eliminate if their argument types are simple loops to this type
881 for (unsigned k
= 0, nargs
= dt
[j
].getNumArgs(); k
< nargs
; k
++)
883 TypeNode tn
= dt
[j
].getArgType(k
);
892 Trace("sygus-strat-slearn")
893 << "...for ite condition, can exclude Boolean connective : "
895 needs_cons_curr
[j
] = false;
901 // all other constructors are needed
902 for (unsigned j
= 0, size
= dt
.getNumConstructors(); j
< size
; j
++)
904 if (needs_cons_curr
.find(j
) == needs_cons_curr
.end())
906 needs_cons_curr
[j
] = true;
909 // update the constructors that the master enumerator needs
910 if (needs_cons
.find(e
) == needs_cons
.end())
912 needs_cons
[e
] = needs_cons_curr
;
916 for (unsigned j
= 0, size
= dt
.getNumConstructors(); j
< size
; j
++)
918 needs_cons
[e
][j
] = needs_cons
[e
][j
] || needs_cons_curr
[j
];
923 void SygusUnifStrategy::finishInit(
926 std::map
<Node
, std::map
<NodeRole
, bool> >& visited
,
929 EnumInfo
& ei
= getEnumInfo(e
);
930 if (visited
[e
].find(nrole
) != visited
[e
].end()
931 && (!isCond
|| ei
.isConditional()))
935 visited
[e
][nrole
] = true;
941 if (ei
.isTemplated())
945 TypeNode etn
= e
.getType();
946 EnumTypeInfo
& tinfo
= getEnumTypeInfo(etn
);
947 StrategyNode
& snode
= tinfo
.getStrategyNode(nrole
);
948 for (unsigned j
= 0, size
= snode
.d_strats
.size(); j
< size
; j
++)
950 EnumTypeInfoStrat
* etis
= snode
.d_strats
[j
];
951 StrategyType strat
= etis
->d_this
;
952 bool newIsCond
= isCond
|| strat
== strat_ITE
;
953 for (std::pair
<Node
, NodeRole
>& cec
: etis
->d_cenum
)
955 finishInit(cec
.first
, cec
.second
, visited
, newIsCond
);
960 void SygusUnifStrategy::debugPrint(
964 std::map
<Node
, std::map
<NodeRole
, bool> >& visited
,
967 if (visited
[e
].find(nrole
) != visited
[e
].end())
970 Trace(c
) << e
<< " :: node role : " << nrole
<< std::endl
;
973 visited
[e
][nrole
] = true;
974 EnumInfo
& ei
= getEnumInfo(e
);
976 TypeNode etn
= e
.getType();
979 Trace(c
) << e
<< " :: node role : " << nrole
;
980 Trace(c
) << ", type : " << etn
.getDType().getName();
981 if (ei
.isConditional())
983 Trace(c
) << ", conditional";
985 Trace(c
) << ", enum role : " << ei
.getRole();
987 if (ei
.isTemplated())
989 Trace(c
) << ", templated : (lambda " << ei
.d_template_arg
<< " "
990 << ei
.d_template
<< ")" << std::endl
;
993 Trace(c
) << std::endl
;
995 EnumTypeInfo
& tinfo
= getEnumTypeInfo(etn
);
996 StrategyNode
& snode
= tinfo
.getStrategyNode(nrole
);
997 for (unsigned j
= 0, size
= snode
.d_strats
.size(); j
< size
; j
++)
999 EnumTypeInfoStrat
* etis
= snode
.d_strats
[j
];
1000 StrategyType strat
= etis
->d_this
;
1002 Trace(c
) << "Strategy : " << strat
<< ", from cons : " << etis
->d_cons
1004 for (std::pair
<Node
, NodeRole
>& cec
: etis
->d_cenum
)
1007 debugPrint(c
, cec
.first
, cec
.second
, visited
, ind
+ 2);
1012 void EnumInfo::initialize(EnumRole role
) { d_role
= role
; }
1014 StrategyNode
& EnumTypeInfo::getStrategyNode(NodeRole nrole
)
1016 std::map
<NodeRole
, StrategyNode
>::iterator it
= d_snodes
.find(nrole
);
1017 Assert(it
!= d_snodes
.end());
1021 bool EnumTypeInfoStrat::isValid(UnifContext
& x
)
1023 if ((x
.getCurrentRole() == role_string_prefix
1024 && d_this
== strat_CONCAT_SUFFIX
)
1025 || (x
.getCurrentRole() == role_string_suffix
1026 && d_this
== strat_CONCAT_PREFIX
))
1033 StrategyNode::~StrategyNode()
1035 for (unsigned j
= 0, size
= d_strats
.size(); j
< size
; j
++)
1042 void SygusUnifStrategy::indent(const char* c
, int ind
)
1046 for (int i
= 0; i
< ind
; i
++)
1053 } // namespace quantifiers
1054 } // namespace theory