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