1 /********************* */
2 /*! \file cegis_unif.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Haniel Barbosa
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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
11 **
12 ** \brief implementation of class for cegis with unification techniques
13 **/
14
15 #include "theory/quantifiers/sygus/cegis_unif.h"
16
17 #include "options/base_options.h"
18 #include "options/quantifiers_options.h"
19 #include "printer/printer.h"
20 #include "theory/quantifiers/sygus/sygus_unif_rl.h"
21 #include "theory/quantifiers/sygus/synth_conjecture.h"
22 #include "theory/quantifiers/sygus/term_database_sygus.h"
23 #include "theory/theory_engine.h"
24
25 using namespace CVC4::kind;
26
27 namespace CVC4 {
28 namespace theory {
29 namespace quantifiers {
30
CegisUnif(QuantifiersEngine * qe,SynthConjecture * p)31 CegisUnif::CegisUnif(QuantifiersEngine* qe, SynthConjecture* p)
32 : Cegis(qe, p), d_sygus_unif(p), d_u_enum_manager(qe, p)
33 {
34 }
35
~CegisUnif()36 CegisUnif::~CegisUnif() {}
processInitialize(Node n,const std::vector<Node> & candidates,std::vector<Node> & lemmas)37 bool CegisUnif::processInitialize(Node n,
38 const std::vector<Node>& candidates,
39 std::vector<Node>& lemmas)
40 {
41 // list of strategy points for unification candidates
42 std::vector<Node> unif_candidate_pts;
43 // map from strategy points to their conditions
44 std::map<Node, Node> pt_to_cond;
45 // strategy lemmas for each strategy point
46 std::map<Node, std::vector<Node>> strategy_lemmas;
47 // Initialize strategies for all functions-to-synthesize
48 // The role of non-unification enumerators is to be either the single solution
49 // or part of a solution involving multiple enumerators.
50 EnumeratorRole eroleNonUnif = candidates.size() == 1
51 ? ROLE_ENUM_SINGLE_SOLUTION
52 : ROLE_ENUM_MULTI_SOLUTION;
53 for (const Node& f : candidates)
54 {
55 // Init UNIF util for this candidate
56 d_sygus_unif.initializeCandidate(
57 d_qe, f, d_cand_to_strat_pt[f], strategy_lemmas);
58 if (!d_sygus_unif.usingUnif(f))
59 {
60 Trace("cegis-unif") << "* non-unification candidate : " << f << std::endl;
61 d_tds->registerEnumerator(f, f, d_parent, eroleNonUnif);
62 d_non_unif_candidates.push_back(f);
63 }
64 else
65 {
66 d_unif_candidates.push_back(f);
67 Trace("cegis-unif") << "* unification candidate : " << f
68 << " with strategy points:" << std::endl;
69 std::vector<Node>& enums = d_cand_to_strat_pt[f];
70 unif_candidate_pts.insert(
71 unif_candidate_pts.end(), enums.begin(), enums.end());
72 // map strategy point to its condition in pt_to_cond
73 for (const Node& e : enums)
74 {
75 Node cond = d_sygus_unif.getConditionForEvaluationPoint(e);
76 Assert(!cond.isNull());
77 Trace("cegis-unif")
78 << " " << e << " with condition : " << cond << std::endl;
79 pt_to_cond[e] = cond;
80 }
81 }
82 }
83 // initialize the enumeration manager
84 d_u_enum_manager.initialize(unif_candidate_pts, pt_to_cond, strategy_lemmas);
85 return true;
86 }
87
getTermList(const std::vector<Node> & candidates,std::vector<Node> & enums)88 void CegisUnif::getTermList(const std::vector<Node>& candidates,
89 std::vector<Node>& enums)
90 {
91 // Non-unif candidate are themselves the enumerators
92 enums.insert(
93 enums.end(), d_non_unif_candidates.begin(), d_non_unif_candidates.end());
94 for (const Node& c : d_unif_candidates)
95 {
96 // Collect heads of candidates
97 for (const Node& hd : d_sygus_unif.getEvalPointHeads(c))
98 {
99 Trace("cegis-unif-enum-debug")
100 << "......cand " << c << " with enum hd " << hd << "\n";
101 enums.push_back(hd);
102 }
103 // get unification enumerators
104 for (const Node& e : d_cand_to_strat_pt[c])
105 {
106 for (unsigned index = 0; index < 2; index++)
107 {
108 std::vector<Node> uenums;
109 // get the current unification enumerators
110 d_u_enum_manager.getEnumeratorsForStrategyPt(e, uenums, index);
111 // get the model value of each enumerator
112 enums.insert(enums.end(), uenums.begin(), uenums.end());
113 }
114 }
115 }
116 }
117
getEnumValues(const std::vector<Node> & enums,const std::vector<Node> & enum_values,std::map<Node,std::vector<Node>> & unif_cenums,std::map<Node,std::vector<Node>> & unif_cvalues,std::vector<Node> & lems)118 bool CegisUnif::getEnumValues(const std::vector<Node>& enums,
119 const std::vector<Node>& enum_values,
120 std::map<Node, std::vector<Node>>& unif_cenums,
121 std::map<Node, std::vector<Node>>& unif_cvalues,
122 std::vector<Node>& lems)
123 {
124 NodeManager* nm = NodeManager::currentNM();
125 Node cost_lit = d_u_enum_manager.getAssertedLiteral();
126 std::map<Node, std::vector<Node>> unif_renums, unif_rvalues;
127 // build model value map
128 std::map<Node, Node> mvMap;
129 for (unsigned i = 0, size = enums.size(); i < size; i++)
130 {
131 mvMap[enums[i]] = enum_values[i];
132 }
133 bool addedUnifEnumSymBreakLemma = false;
134 // populate maps between unification enumerators and their model values
135 for (const Node& c : d_unif_candidates)
136 {
137 // for each decision tree strategy allocated for c (these are referenced
138 // by strategy points in d_cand_to_strat_pt[c])
139 for (const Node& e : d_cand_to_strat_pt[c])
140 {
141 for (unsigned index = 0; index < 2; index++)
142 {
143 std::vector<Node> es, vs;
144 Trace("cegis-unif")
145 << " " << (index == 0 ? "Return values" : "Conditions") << " for "
146 << e << ":\n";
147 // get the current unification enumerators
148 d_u_enum_manager.getEnumeratorsForStrategyPt(e, es, index);
149 // set enums for condition enumerators
150 if (index == 1)
151 {
152 if (options::sygusUnifCondIndependent())
153 {
154 Assert(es.size() == 1);
155 // whether valueus exhausted
156 if (mvMap.find(es[0]) == mvMap.end())
157 {
158 Trace("cegis-unif") << " " << es[0] << " -> N/A\n";
159 es.clear();
160 }
161 }
162 unif_cenums[e] = es;
163 }
164 // get the model value of each enumerator
165 for (const Node& eu : es)
166 {
167 Assert(mvMap.find(eu) != mvMap.end());
168 Node m_eu = mvMap[eu];
169 if (Trace.isOn("cegis-unif"))
170 {
171 Trace("cegis-unif") << " " << eu << " -> ";
172 TermDbSygus::toStreamSygus("cegis-unif", m_eu);
173 Trace("cegis-unif") << "\n";
174 }
175 vs.push_back(m_eu);
176 }
177 // set values for condition enumerators of e
178 if (index == 1)
179 {
180 unif_cvalues[e] = vs;
181 }
182 // inter-enumerator symmetry breaking for return values
183 else
184 {
185 // given a pool of unification enumerators eu_1, ..., eu_n,
186 // CegisUnifEnumDecisionStrategy insists that size(eu_1) <= ... <=
187 // size(eu_n). We additionally insist that M(eu_i) < M(eu_{i+1}) when
188 // size(eu_i) = size(eu_{i+1}), where < is pointer comparison.
189 // We enforce this below by adding symmetry breaking lemmas of the
190 // form ~( eu_i = M(eu_i) ^ eu_{i+1} = M(eu_{i+1} ) )
191 // when applicable.
192 // we only do this for return value enumerators, since condition
193 // enumerators cannot be ordered (their order is based on the
194 // seperation resolution scheme during model construction).
195 for (unsigned j = 1, nenum = vs.size(); j < nenum; j++)
196 {
197 Node prev_val = vs[j - 1];
198 Node curr_val = vs[j];
199 // compare the node values
200 if (curr_val < prev_val)
201 {
202 // must have the same size
203 unsigned prev_size = d_tds->getSygusTermSize(prev_val);
204 unsigned curr_size = d_tds->getSygusTermSize(curr_val);
205 Assert(prev_size <= curr_size);
206 if (curr_size == prev_size)
207 {
208 Node slem =
209 nm->mkNode(
210 AND, es[j - 1].eqNode(vs[j - 1]), es[j].eqNode(vs[j]))
211 .negate();
212 Trace("cegis-unif")
213 << "CegisUnif::lemma, inter-unif-enumerator "
214 "symmetry breaking lemma : "
215 << slem << "\n";
216 d_qe->getOutputChannel().lemma(slem);
217 addedUnifEnumSymBreakLemma = true;
218 break;
219 }
220 }
221 }
222 }
223 }
224 }
225 }
226 return !addedUnifEnumSymBreakLemma;
227 }
228
setConditions(const std::map<Node,std::vector<Node>> & unif_cenums,const std::map<Node,std::vector<Node>> & unif_cvalues,std::vector<Node> & lems)229 void CegisUnif::setConditions(
230 const std::map<Node, std::vector<Node>>& unif_cenums,
231 const std::map<Node, std::vector<Node>>& unif_cvalues,
232 std::vector<Node>& lems)
233 {
234 Node cost_lit = d_u_enum_manager.getAssertedLiteral();
235 NodeManager* nm = NodeManager::currentNM();
236 // set the conditions
237 for (const Node& c : d_unif_candidates)
238 {
239 for (const Node& e : d_cand_to_strat_pt[c])
240 {
241 Assert(unif_cenums.find(e) != unif_cenums.end());
242 Assert(unif_cvalues.find(e) != unif_cvalues.end());
243 std::map<Node, std::vector<Node>>::const_iterator itc =
244 unif_cenums.find(e);
245 std::map<Node, std::vector<Node>>::const_iterator itv =
246 unif_cvalues.find(e);
247 d_sygus_unif.setConditions(e, cost_lit, itc->second, itv->second);
248 // d_sygus_unif.setConditions(e, cost_lit, unif_cenums[e],
249 // unif_cvalues[e]); if condition enumerator had value and it is being
250 // passively generated, exclude this value
251 if (options::sygusUnifCondIndependent() && !itc->second.empty())
252 {
253 Node eu = itc->second[0];
254 Assert(d_tds->isEnumerator(eu));
255 Assert(!itv->second.empty());
256 if (d_tds->isPassiveEnumerator(eu))
257 {
258 Node g = d_tds->getActiveGuardForEnumerator(eu);
259 Node exp_exc = d_tds->getExplain()
260 ->getExplanationForEquality(eu, itv->second[0])
261 .negate();
262 lems.push_back(nm->mkNode(OR, g.negate(), exp_exc));
263 }
264 }
265 }
266 }
267 }
268
processConstructCandidates(const std::vector<Node> & enums,const std::vector<Node> & enum_values,const std::vector<Node> & candidates,std::vector<Node> & candidate_values,bool satisfiedRl,std::vector<Node> & lems)269 bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
270 const std::vector<Node>& enum_values,
271 const std::vector<Node>& candidates,
272 std::vector<Node>& candidate_values,
273 bool satisfiedRl,
274 std::vector<Node>& lems)
275 {
276 if (d_unif_candidates.empty())
277 {
278 Assert(d_non_unif_candidates.size() == candidates.size());
279 return Cegis::processConstructCandidates(
280 enums, enum_values, candidates, candidate_values, satisfiedRl, lems);
281 }
282 if (Trace.isOn("cegis-unif"))
283 {
284 for (const Node& c : d_unif_candidates)
285 {
286 // Collect heads of candidates
287 Trace("cegis-unif") << " Evaluation heads for " << c << " :\n";
288 for (const Node& hd : d_sygus_unif.getEvalPointHeads(c))
289 {
290 bool isUnit = false;
291 // d_rl_eval_hds accumulates eval apps, so need to look at operators
292 for (const Node& hd_unit : d_rl_eval_hds)
293 {
294 if (hd == hd_unit[0])
295 {
296 isUnit = true;
297 break;
298 }
299 }
300 Trace("cegis-unif") << " " << hd << (isUnit ? "*" : "") << " -> ";
301 Assert(std::find(enums.begin(), enums.end(), hd) != enums.end());
302 unsigned i = std::distance(enums.begin(),
303 std::find(enums.begin(), enums.end(), hd));
304 Assert(i >= 0 && i < enum_values.size());
305 TermDbSygus::toStreamSygus("cegis-unif", enum_values[i]);
306 Trace("cegis-unif") << "\n";
307 }
308 }
309 }
310 // the unification enumerators for conditions and their model values
311 std::map<Node, std::vector<Node>> unif_cenums;
312 std::map<Node, std::vector<Node>> unif_cvalues;
313 // we only proceed to solution building if we are not introducing symmetry
314 // breaking lemmas between return values and if we have not previously
315 // introduced return values refinement lemmas
316 if (!getEnumValues(enums, enum_values, unif_cenums, unif_cvalues, lems)
317 || !satisfiedRl)
318 {
319 // if condition values are being indepedently enumerated, they should be
320 // communicated to the decision tree strategies indepedently of we
321 // proceeding to attempt solution building
322 if (options::sygusUnifCondIndependent())
323 {
324 setConditions(unif_cenums, unif_cvalues, lems);
325 }
326 Trace("cegis-unif") << (!satisfiedRl
327 ? "..added refinement lemmas"
328 : "..added unif enum symmetry breaking")
329 << "\n---CegisUnif Engine---\n";
330 // if we didn't satisfy the specification, there is no way to repair
331 return false;
332 }
333 setConditions(unif_cenums, unif_cvalues, lems);
334 // build solutions (for unif candidates a divide-and-conquer approach is used)
335 std::vector<Node> sols;
336 std::vector<Node> lemmas;
337 if (d_sygus_unif.constructSolution(sols, lemmas))
338 {
339 candidate_values.insert(candidate_values.end(), sols.begin(), sols.end());
340 if (Trace.isOn("cegis-unif"))
341 {
342 Trace("cegis-unif") << "* Candidate solutions are:\n";
343 for (const Node& sol : sols)
344 {
345 Trace("cegis-unif")
346 << "... " << d_tds->sygusToBuiltin(sol, sol.getType()) << "\n";
347 }
348 Trace("cegis-unif") << "---CegisUnif Engine---\n";
349 }
350 return true;
351 }
352
353 // TODO tie this to the lemma for getting a new condition value
354 Assert(options::sygusUnifCondIndependent() || !lemmas.empty());
355 for (const Node& lem : lemmas)
356 {
357 Trace("cegis-unif-lemma")
358 << "CegisUnif::lemma, separation lemma : " << lem << "\n";
359 d_qe->getOutputChannel().lemma(lem);
360 }
361 Trace("cegis-unif") << "..failed to separate heads\n---CegisUnif Engine---\n";
362 return false;
363 }
364
registerRefinementLemma(const std::vector<Node> & vars,Node lem,std::vector<Node> & lems)365 void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars,
366 Node lem,
367 std::vector<Node>& lems)
368 {
369 // Notify lemma to unification utility and get its purified form
370 std::map<Node, std::vector<Node>> eval_pts;
371 Node plem = d_sygus_unif.addRefLemma(lem, eval_pts);
372 addRefinementLemma(plem);
373 Trace("cegis-unif-lemma")
374 << "CegisUnif::lemma, refinement lemma : " << plem << "\n";
375 // Notify the enumeration manager if there are new evaluation points
376 for (const std::pair<const Node, std::vector<Node>>& ep : eval_pts)
377 {
378 Assert(d_cand_to_strat_pt.find(ep.first) != d_cand_to_strat_pt.end());
379 // Notify each strategy point of the respective candidate
380 for (const Node& n : d_cand_to_strat_pt[ep.first])
381 {
382 d_u_enum_manager.registerEvalPts(ep.second, n);
383 }
384 }
385 // Make the refinement lemma and add it to lems. This lemma is guarded by the
386 // parent's guard, which has the semantics "this conjecture has a solution",
387 // hence this lemma states: if the parent conjecture has a solution, it
388 // satisfies the specification for the given concrete point.
389 lems.push_back(NodeManager::currentNM()->mkNode(
390 OR, d_parent->getGuard().negate(), plem));
391 }
392
CegisUnifEnumDecisionStrategy(QuantifiersEngine * qe,SynthConjecture * parent)393 CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(
394 QuantifiersEngine* qe, SynthConjecture* parent)
395 : DecisionStrategyFmf(qe->getSatContext(), qe->getValuation()),
396 d_qe(qe),
397 d_parent(parent)
398 {
399 d_initialized = false;
400 d_tds = d_qe->getTermDatabaseSygus();
401 }
402
mkLiteral(unsigned n)403 Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
404 {
405 NodeManager* nm = NodeManager::currentNM();
406 Node new_lit = nm->mkSkolem("G_cost", nm->booleanType());
407 unsigned new_size = n + 1;
408
409 // allocate an enumerator for each candidate
410 for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info)
411 {
412 Node c = ci.first;
413 TypeNode ct = c.getType();
414 Node eu = nm->mkSkolem("eu", ct);
415 Node ceu;
416 if (!options::sygusUnifCondIndependent() && !ci.second.d_enums[0].empty())
417 {
418 // make a new conditional enumerator as well, starting the
419 // second type around
420 ceu = nm->mkSkolem("cu", ci.second.d_ce_type);
421 }
422 // register the new enumerators
423 for (unsigned index = 0; index < 2; index++)
424 {
425 Node e = index == 0 ? eu : ceu;
426 if (e.isNull())
427 {
428 continue;
429 }
430 setUpEnumerator(e, ci.second, index);
431 }
432 }
433 // register the evaluation points at the new value
434 for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info)
435 {
436 Node c = ci.first;
437 for (const Node& ei : ci.second.d_eval_points)
438 {
439 Trace("cegis-unif-enum") << "...increasing enum number for hd " << ei
440 << " to new size " << new_size << "\n";
441 registerEvalPtAtSize(c, ei, new_lit, new_size);
442 }
443 }
444 // enforce fairness between number of enumerators and enumerator size
445 if (new_size > 1)
446 {
447 // construct the "virtual enumerator"
448 if (d_virtual_enum.isNull())
449 {
450 // we construct the default integer grammar with no variables, e.g.:
451 // A -> 0 | 1 | A+A
452 TypeNode intTn = nm->integerType();
453 // use a null variable list
454 Node bvl;
455 std::stringstream ss;
456 ss << "_virtual_enum_grammar";
457 std::string virtualEnumName(ss.str());
458 std::map<TypeNode, std::vector<Node>> extra_cons;
459 std::map<TypeNode, std::vector<Node>> exclude_cons;
460 // do not include "-", which is included by default for integers
461 exclude_cons[intTn].push_back(nm->operatorOf(MINUS));
462 std::unordered_set<Node, NodeHashFunction> term_irrelevant;
463 TypeNode vtn = CegGrammarConstructor::mkSygusDefaultType(intTn,
464 bvl,
465 virtualEnumName,
466 extra_cons,
467 exclude_cons,
468 term_irrelevant);
469 d_virtual_enum = nm->mkSkolem("_ve", vtn);
470 d_tds->registerEnumerator(
471 d_virtual_enum, Node::null(), d_parent, ROLE_ENUM_CONSTRAINED);
472 }
473 // if new_size is a power of two, then isPow2 returns log2(new_size)+1
474 // otherwise, this returns 0. In the case it returns 0, we don't care
475 // since the floor( log2( i ) ) = floor( log2( i - 1 ) ) and we do not
476 // increase our size bound.
477 unsigned pow_two = Integer(new_size).isPow2();
478 if (pow_two > 0)
479 {
480 Node size_ve = nm->mkNode(DT_SIZE, d_virtual_enum);
481 Node fair_lemma =
482 nm->mkNode(GEQ, size_ve, nm->mkConst(Rational(pow_two - 1)));
483 fair_lemma = nm->mkNode(OR, new_lit, fair_lemma);
484 Trace("cegis-unif-enum-lemma")
485 << "CegisUnifEnum::lemma, fairness size:" << fair_lemma << "\n";
486 // this lemma relates the number of conditions we enumerate and the
487 // maximum size of a term that is part of our solution. It is of the
488 // form:
489 // G_uq_i => size(ve) >= log_2( i-1 )
490 // In other words, if we use i conditions, then we allow terms in our
491 // solution whose size is at most log_2(i-1).
492 d_qe->getOutputChannel().lemma(fair_lemma);
493 }
494 }
495
496 return new_lit;
497 }
498
initialize(const std::vector<Node> & es,const std::map<Node,Node> & e_to_cond,const std::map<Node,std::vector<Node>> & strategy_lemmas)499 void CegisUnifEnumDecisionStrategy::initialize(
500 const std::vector<Node>& es,
501 const std::map<Node, Node>& e_to_cond,
502 const std::map<Node, std::vector<Node>>& strategy_lemmas)
503 {
504 Assert(!d_initialized);
505 d_initialized = true;
506 if (es.empty())
507 {
508 return;
509 }
510 // initialize type information for candidates
511 NodeManager* nm = NodeManager::currentNM();
512 for (const Node& e : es)
513 {
514 Trace("cegis-unif-enum-debug") << "...adding strategy point " << e << "\n";
515 // currently, we allocate the same enumerators for candidates of the same
516 // type
517 d_ce_info[e].d_pt = e;
518 std::map<Node, Node>::const_iterator itcc = e_to_cond.find(e);
519 Assert(itcc != e_to_cond.end());
520 Node cond = itcc->second;
521 Trace("cegis-unif-enum-debug")
522 << "...its condition strategy point is " << cond << "\n";
523 d_ce_info[e].d_ce_type = cond.getType();
524 // initialize the symmetry breaking lemma templates
525 for (unsigned index = 0; index < 2; index++)
526 {
527 Assert(d_ce_info[e].d_sbt_lemma_tmpl[index].first.isNull());
528 Node sp = index == 0 ? e : cond;
529 std::map<Node, std::vector<Node>>::const_iterator it =
530 strategy_lemmas.find(sp);
531 if (it == strategy_lemmas.end())
532 {
533 continue;
534 }
535 // collect lemmas for removing redundant ops for this candidate's type
536 Node d_sbt_lemma =
537 it->second.size() == 1 ? it->second[0] : nm->mkNode(AND, it->second);
538 Trace("cegis-unif-enum-debug")
539 << "...adding lemma template to remove redundant operators for " << sp
540 << " --> lambda " << sp << ". " << d_sbt_lemma << "\n";
541 d_ce_info[e].d_sbt_lemma_tmpl[index] =
542 std::pair<Node, Node>(d_sbt_lemma, sp);
543 }
544 }
545
546 // register this strategy
547 d_qe->getTheoryEngine()->getDecisionManager()->registerStrategy(
548 DecisionManager::STRAT_QUANT_CEGIS_UNIF_NUM_ENUMS, this);
549
550 // create single condition enumerator for each decision tree strategy
551 if (options::sygusUnifCondIndependent())
552 {
553 // allocate a condition enumerator for each candidate
554 for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info)
555 {
556 Node ceu = nm->mkSkolem("cu", ci.second.d_ce_type);
557 setUpEnumerator(ceu, ci.second, 1);
558 }
559 }
560 }
561
getEnumeratorsForStrategyPt(Node e,std::vector<Node> & es,unsigned index) const562 void CegisUnifEnumDecisionStrategy::getEnumeratorsForStrategyPt(
563 Node e, std::vector<Node>& es, unsigned index) const
564 {
565 // the number of active enumerators is related to the current cost value
566 unsigned num_enums = 0;
567 bool has_num_enums = getAssertedLiteralIndex(num_enums);
568 AlwaysAssert(has_num_enums);
569 num_enums = num_enums + 1;
570 if (index == 1)
571 {
572 // we always use (cost-1) conditions, or 1 if in the indepedent case
573 num_enums = !options::sygusUnifCondIndependent() ? num_enums - 1 : 1;
574 }
575 if (num_enums > 0)
576 {
577 std::map<Node, StrategyPtInfo>::const_iterator itc = d_ce_info.find(e);
578 Assert(itc != d_ce_info.end());
579 Assert(num_enums <= itc->second.d_enums[index].size());
580 es.insert(es.end(),
581 itc->second.d_enums[index].begin(),
582 itc->second.d_enums[index].begin() + num_enums);
583 }
584 }
585
setUpEnumerator(Node e,StrategyPtInfo & si,unsigned index)586 void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e,
587 StrategyPtInfo& si,
588 unsigned index)
589 {
590 NodeManager* nm = NodeManager::currentNM();
591 // instantiate template for removing redundant operators
592 if (!si.d_sbt_lemma_tmpl[index].first.isNull())
593 {
594 Node templ = si.d_sbt_lemma_tmpl[index].first;
595 TNode templ_var = si.d_sbt_lemma_tmpl[index].second;
596 Node sym_break_red_ops = templ.substitute(templ_var, e);
597 Trace("cegis-unif-enum-lemma")
598 << "CegisUnifEnum::lemma, remove redundant ops of " << e << " : "
599 << sym_break_red_ops << "\n";
600 d_qe->getOutputChannel().lemma(sym_break_red_ops);
601 }
602 // symmetry breaking between enumerators
603 if (!si.d_enums[index].empty() && index == 0)
604 {
605 Node e_prev = si.d_enums[index].back();
606 Node size_e = nm->mkNode(DT_SIZE, e);
607 Node size_e_prev = nm->mkNode(DT_SIZE, e_prev);
608 Node sym_break = nm->mkNode(GEQ, size_e, size_e_prev);
609 Trace("cegis-unif-enum-lemma")
610 << "CegisUnifEnum::lemma, enum sym break:" << sym_break << "\n";
611 d_qe->getOutputChannel().lemma(sym_break);
612 }
613 // register the enumerator
614 si.d_enums[index].push_back(e);
615 EnumeratorRole erole = ROLE_ENUM_CONSTRAINED;
616 // if we are using a single independent enumerator for conditions, then we
617 // allocate an active guard, and are eligible to use variable-agnostic
618 // enumeration.
619 if (options::sygusUnifCondIndependent() && index == 1)
620 {
621 erole = ROLE_ENUM_POOL;
622 }
623 Trace("cegis-unif-enum") << "* Registering new enumerator " << e
624 << " to strategy point " << si.d_pt << "\n";
625 d_tds->registerEnumerator(e, si.d_pt, d_parent, erole, false);
626 }
627
registerEvalPts(const std::vector<Node> & eis,Node e)628 void CegisUnifEnumDecisionStrategy::registerEvalPts(
629 const std::vector<Node>& eis, Node e)
630 {
631 // candidates of the same type are managed
632 std::map<Node, StrategyPtInfo>::iterator it = d_ce_info.find(e);
633 Assert(it != d_ce_info.end());
634 it->second.d_eval_points.insert(
635 it->second.d_eval_points.end(), eis.begin(), eis.end());
636 // register at all already allocated sizes
637 for (const Node& ei : eis)
638 {
639 Assert(ei.getType() == e.getType());
640 for (unsigned j = 0, size = d_literals.size(); j < size; j++)
641 {
642 Trace("cegis-unif-enum") << "...for cand " << e << " adding hd " << ei
643 << " at size " << j << "\n";
644 registerEvalPtAtSize(e, ei, d_literals[j], j + 1);
645 }
646 }
647 }
648
registerEvalPtAtSize(Node e,Node ei,Node guq_lit,unsigned n)649 void CegisUnifEnumDecisionStrategy::registerEvalPtAtSize(Node e,
650 Node ei,
651 Node guq_lit,
652 unsigned n)
653 {
654 // must be equal to one of the first n enums
655 std::map<Node, StrategyPtInfo>::iterator itc = d_ce_info.find(e);
656 Assert(itc != d_ce_info.end());
657 Assert(itc->second.d_enums[0].size() >= n);
658 std::vector<Node> disj;
659 disj.push_back(guq_lit.negate());
660 for (unsigned i = 0; i < n; i++)
661 {
662 disj.push_back(ei.eqNode(itc->second.d_enums[0][i]));
663 }
664 Node lem = NodeManager::currentNM()->mkNode(OR, disj);
665 Trace("cegis-unif-enum-lemma")
666 << "CegisUnifEnum::lemma, domain:" << lem << "\n";
667 d_qe->getOutputChannel().lemma(lem);
668 }
669
670 } // namespace quantifiers
671 } // namespace theory
672 } // namespace CVC4
673