Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Abdalrhman Mohamed, Andrew Reynolds, Mathias Preiner
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 : : * ****************************************************************************
12 : : *
13 : : * Implementation for Sygus reconstruct.
14 : : */
15 : :
16 : : #include "theory/quantifiers/sygus/sygus_reconstruct.h"
17 : :
18 : : #include "expr/dtype_cons.h"
19 : : #include "expr/node_algorithm.h"
20 : : #include "options/quantifiers_options.h"
21 : : #include "printer/printer.h"
22 : : #include "theory/datatypes/sygus_datatype_utils.h"
23 : : #include "theory/rewriter.h"
24 : :
25 : : using namespace cvc5::internal::kind;
26 : :
27 : : namespace cvc5::internal {
28 : : namespace theory {
29 : : namespace quantifiers {
30 : :
31 : 7270 : SygusReconstruct::SygusReconstruct(Env& env,
32 : : TermDbSygus* tds,
33 : 7270 : SygusStatistics& s)
34 : 7270 : : NodeConverter(env.getNodeManager()), EnvObj(env), d_tds(tds), d_stats(s)
35 : : {
36 : 7270 : }
37 : :
38 : 54 : Node SygusReconstruct::reconstructSolution(Node sol,
39 : : TypeNode stn,
40 : : int8_t& reconstructed,
41 : : uint64_t enumLimit)
42 : : {
43 [ + - ]: 108 : Trace("sygus-rcons") << "SygusReconstruct::reconstructSolution: " << sol
44 : 54 : << std::endl;
45 [ + - ]: 54 : Trace("sygus-rcons") << "- target sygus type is " << stn << std::endl;
46 [ + - ]: 54 : Trace("sygus-rcons") << "- enumeration limit is " << enumLimit << std::endl;
47 : :
48 : : // this method may get called multiple times with the same object. We need to
49 : : // reset the state to avoid conflicts
50 : 54 : clear();
51 : :
52 : 54 : initialize(stn);
53 : :
54 : : // add the main obligation to the set of obligations
55 : : // paramaters stn and sol constitute the main obligation to satisfy
56 : 54 : d_obs.push_back(std::make_unique<RConsObligation>(stn, sol));
57 : 54 : d_stnInfo[stn].setBuiltinToOb(sol, d_obs[0].get());
58 : 54 : RConsObligation* ob0 = d_obs[0].get();
59 : 108 : Node k0 = ob0->getSkolem();
60 : :
61 : 54 : if (options().quantifiers.cegqiSingleInvReconstruct
62 [ + + ]: 54 : == cvc5::internal::options::CegqiSingleInvRconsMode::TRY)
63 : : {
64 : 4 : fast(sol, stn, reconstructed);
65 : : }
66 : : else
67 : : {
68 : 50 : main(sol, stn, reconstructed, enumLimit);
69 : : }
70 : :
71 [ + - ][ - + ]: 54 : if (Trace("sygus-rcons").isConnected())
72 : : {
73 : 0 : RConsObligation::printCandSols(ob0, d_obs);
74 : 0 : printPool();
75 : : }
76 : :
77 : : // if the main obligation is solved, return the solution
78 [ + + ]: 54 : if (!d_sol[k0].isNull())
79 : : {
80 : 50 : reconstructed = 1;
81 : : // The algorithm mostly works with rewritten terms and may not notice that
82 : : // the original terms contain variables eliminated by the rewriter. For
83 : : // example, rewrite((ite true 0 z)) = 0. In such cases, we replace those
84 : : // variables with ground values.
85 : 50 : return d_sol[k0].isConst() ? Node(d_sol[k0]) : mkGround(d_sol[k0]);
86 : : }
87 : :
88 : : // we ran out of elements, return null
89 : 4 : reconstructed = -1;
90 : 8 : Printer::getPrinter(warning())->toStreamCmdFailure(
91 : 4 : warning(), "Cannot get synth function: reconstruction to syntax failed.");
92 : 4 : return Node::null();
93 : : }
94 : :
95 : 50 : void SygusReconstruct::main(Node sol,
96 : : TypeNode stn,
97 : : int8_t& reconstructed,
98 : : uint64_t enumLimit)
99 : : {
100 : 50 : bool noLimit = options().quantifiers.cegqiSingleInvReconstruct
101 : 50 : == cvc5::internal::options::CegqiSingleInvRconsMode::ALL;
102 : :
103 : : // Skolem of the main obligation
104 : 100 : Node k0 = d_obs[0]->getSkolem();
105 : :
106 : : // a set of builtin terms to reconstruct for each sygus datatype
107 : 100 : TypeBuiltinSetMap termsToRecons;
108 : 50 : termsToRecons[stn].emplace(sol);
109 : :
110 : 50 : uint64_t count = 0;
111 : :
112 : : // We need to add the main obligation to the crd in case it cannot be broken
113 : : // down by matching. By doing so, we can solve the obligation using
114 : : // enumeration and crd (if it is in the grammar)
115 : 50 : d_stnInfo[stn].addTerm(sol);
116 : :
117 : : // procedure
118 [ + + ][ + + ]: 5140 : while (d_sol[k0].isNull() && (noLimit || count < enumLimit))
[ - + ][ + - ]
[ + + ][ - - ]
119 : : {
120 : : // enumeration phase
121 : : // a temporary set of new terms to reconstruct cached for processing in the
122 : : // match phase
123 : 5090 : TypeBuiltinSetMap termsToReconsPrime;
124 [ + + ]: 12310 : for (const std::pair<const TypeNode, BuiltinSet>& pair : termsToRecons)
125 : : {
126 : : // enumerate a new term
127 [ + - ]: 7220 : Trace("sygus-rcons") << "enum: " << stn << ": ";
128 : 7220 : Node sz = d_stnInfo[pair.first].nextEnum();
129 [ + + ]: 7220 : if (sz.isNull())
130 : : {
131 : 3076 : continue;
132 : : }
133 : 8288 : Node builtin = rewrite(datatypes::utils::sygusToBuiltin(sz));
134 : : // if enumerated term does not contain free variables, then its
135 : : // corresponding obligation can be solved immediately
136 [ + + ]: 4144 : if (sz.isConst())
137 : : {
138 : 3752 : Node rep = d_stnInfo[pair.first].addTerm(builtin);
139 : 1876 : RConsObligation* ob = d_stnInfo[pair.first].builtinToOb(rep);
140 : : // check if the enumerated term solves an obligation
141 [ + + ]: 1876 : if (ob == nullptr)
142 : : {
143 : : // if not, create an "artifical" obligation whose solution would be
144 : : // the enumerated term
145 : 1810 : d_obs.push_back(
146 : 3620 : std::make_unique<RConsObligation>(pair.first, builtin));
147 : 1810 : d_stnInfo[pair.first].setBuiltinToOb(builtin, d_obs.back().get());
148 : 1810 : ob = d_obs.back().get();
149 : : }
150 : : // mark the obligation as solved
151 : 1876 : markSolved(ob, sz);
152 : : // Since we added the term to the candidate rewrite database, there is
153 : : // no point in adding it to the pool too
154 : 1876 : continue;
155 : : }
156 : : // if there are no matches (all calls to notify return true)...
157 [ + - ]: 2268 : if (d_poolTrie.getMatches(builtin, this))
158 : : {
159 : : // then, this is a new term and we should add it to pool
160 : 2268 : d_poolTrie.addTerm(builtin);
161 : 2268 : d_pool[pair.first].push_back(sz);
162 [ + + ]: 4750 : for (const Node& t : pair.second)
163 : : {
164 : 2482 : RConsObligation* ob = d_stnInfo[pair.first].builtinToOb(t);
165 [ + + ]: 2482 : if (d_sol[ob->getSkolem()].isNull())
166 : : {
167 [ + - ]: 2468 : Trace("sygus-rcons") << "ob: " << *ob << std::endl;
168 : : // try to match builtin term `t` with the enumerated term sz
169 : 7404 : TypeBuiltinSetMap temp = matchNewObs(t, sz);
170 : : // cache the new obligations for processing in the match phase
171 [ + + ]: 2494 : for (const std::pair<const TypeNode, BuiltinSet>& tempPair : temp)
172 : : {
173 : 26 : termsToReconsPrime[tempPair.first].insert(
174 : : tempPair.second.cbegin(), tempPair.second.cend());
175 : : }
176 : : }
177 : : }
178 : : }
179 : : }
180 : : // match phase
181 [ + + ]: 5122 : while (!termsToReconsPrime.empty())
182 : : {
183 : : // a temporary set of new terms to reconstruct cached for later processing
184 : 64 : TypeBuiltinSetMap termsToReconsDPrime;
185 : 36 : for (const std::pair<const TypeNode, BuiltinSet>& pair :
186 [ + + ]: 104 : termsToReconsPrime)
187 : : {
188 [ + + ]: 90 : for (const Node& t : pair.second)
189 : : {
190 : 54 : termsToRecons[pair.first].emplace(t);
191 : 54 : RConsObligation* ob = d_stnInfo[pair.first].builtinToOb(t);
192 [ + - ]: 54 : if (d_sol[ob->getSkolem()].isNull())
193 : : {
194 [ + - ]: 54 : Trace("sygus-rcons") << "ob: " << *ob << std::endl;
195 [ + + ]: 398 : for (const Node& sz : d_pool[pair.first])
196 : : {
197 : : // try to match each newly generated and cached term with patterns
198 : : // in pool
199 : 1032 : TypeBuiltinSetMap temp = matchNewObs(t, sz);
200 : : // cache the new terms for later processing
201 [ + + ]: 358 : for (const std::pair<const TypeNode, BuiltinSet>& tempPair : temp)
202 : : {
203 : 14 : termsToReconsDPrime[tempPair.first].insert(
204 : : tempPair.second.cbegin(), tempPair.second.cend());
205 : : }
206 : : }
207 : : }
208 : : }
209 : : }
210 : 32 : termsToReconsPrime = std::move(termsToReconsDPrime);
211 : : }
212 : : // remove reconstructed terms from termsToRecons
213 : 5090 : removeReconstructedTerms(termsToRecons);
214 : 5090 : ++count;
215 : : }
216 : 50 : }
217 : :
218 : 4 : void SygusReconstruct::fast(Node sol, TypeNode stn, int8_t& reconstructed)
219 : : {
220 : 4 : NodeManager* nm = nodeManager();
221 : :
222 [ - + ][ - + ]: 4 : Assert(stn.isDatatype());
[ - - ]
223 [ - + ][ - + ]: 4 : Assert(stn.getDType().isSygus());
[ - - ]
224 : 8 : SygusTypeInfo sti;
225 : 4 : sti.initialize(d_tds, stn);
226 : 8 : std::vector<TypeNode> stns;
227 : 4 : sti.getSubfieldTypes(stns);
228 : 8 : std::map<TypeNode, size_t> varCount;
229 : :
230 : : // add the constructors for each sygus datatype to the pool
231 [ + + ]: 8 : for (const TypeNode& cstn : stns)
232 : : {
233 : 16 : for (const std::shared_ptr<DTypeConstructor>& cons :
234 [ + + ]: 36 : cstn.getDType().getConstructors())
235 : : {
236 [ + + ]: 16 : if (cons->getNumArgs() == 0)
237 : : {
238 : : // just like in the main procedure, add no-argument constructors
239 : : // directly to the crd
240 : 36 : Node sz = nm->mkNode(Kind::APPLY_CONSTRUCTOR, cons->getConstructor());
241 : 24 : Node builtin = datatypes::utils::sygusToBuiltin(sz);
242 : 12 : Node rep = d_stnInfo[cstn].addTerm(builtin);
243 : 12 : RConsObligation* ob = d_stnInfo[cstn].builtinToOb(rep);
244 : : // check if the enumerated term solves an obligation
245 [ + - ]: 12 : if (ob == nullptr)
246 : : {
247 : : // if not, create an "artifical" obligation whose solution would be
248 : : // the enumerated term
249 : 12 : d_obs.push_back(std::make_unique<RConsObligation>(cstn, builtin));
250 : 12 : d_stnInfo[cstn].setBuiltinToOb(builtin, d_obs.back().get());
251 : 12 : ob = d_obs.back().get();
252 : : }
253 : : // mark the obligation as solved
254 : 12 : markSolved(ob, sz);
255 : : }
256 : : else
257 : : {
258 : 8 : std::vector<Node> args;
259 : 4 : args.push_back(cons->getConstructor());
260 : : // populate each constructor argument with a free variable of the
261 : : // corresponding type
262 [ + + ]: 12 : for (const std::shared_ptr<cvc5::internal::DTypeSelector>& arg : cons->getArgs())
263 : : {
264 : 8 : args.push_back(d_tds->getFreeVarInc(arg->getRangeType(), varCount));
265 : : }
266 : 8 : Node sz = nm->mkNode(Kind::APPLY_CONSTRUCTOR, args);
267 : 4 : d_pool[cstn].push_back(sz);
268 : : }
269 : : }
270 : : }
271 : :
272 : : // a set of builtin terms to reconstruct for each sygus datatype
273 : 8 : TypeBuiltinSetMap termsToRecons;
274 : 4 : termsToRecons[stn].emplace(sol);
275 : :
276 : : // match phase of the rcons procedure
277 [ + + ]: 8 : while (!termsToRecons.empty())
278 : : {
279 : : // a temporary set of new terms to reconstruct cached for later processing
280 : 8 : TypeBuiltinSetMap termsToReconsPrime;
281 [ + + ]: 8 : for (const std::pair<const TypeNode, BuiltinSet>& pair : termsToRecons)
282 : : {
283 [ + + ]: 8 : for (const Node& t : pair.second)
284 : : {
285 : 4 : RConsObligation* ob = d_stnInfo[pair.first].builtinToOb(t);
286 [ + - ]: 4 : if (d_sol[ob->getSkolem()].isNull())
287 : : {
288 [ + - ]: 4 : Trace("sygus-rcons") << "ob: " << *ob << std::endl;
289 [ + + ]: 8 : for (const Node& sz : d_pool[pair.first])
290 : : {
291 : : // try to match each newly generated and cached term with patterns
292 : : // in pool
293 : 12 : TypeBuiltinSetMap temp = matchNewObs(t, sz);
294 : : // cache the new terms for later processing
295 [ - + ]: 4 : for (const std::pair<const TypeNode, BuiltinSet>& tempPair : temp)
296 : : {
297 : 0 : termsToReconsPrime[tempPair.first].insert(
298 : : tempPair.second.cbegin(), tempPair.second.cend());
299 : : }
300 : : }
301 : : }
302 : : }
303 : : }
304 : 4 : termsToRecons = std::move(termsToReconsPrime);
305 : : }
306 : 4 : }
307 : :
308 : 2816 : TypeBuiltinSetMap SygusReconstruct::matchNewObs(Node t, Node sz)
309 : : {
310 : 2816 : TypeBuiltinSetMap termsToReconsPrime;
311 : :
312 : : // substitutions generated by match. Note that we might have already seen (and
313 : : // even solved) obligations corresponsing to those substitutions
314 : 5632 : NodePairMap matches;
315 : : // the builtin terms corresponding to sygus variables in the grammar are bound
316 : : // variables. However, we want the `match` method to treat them as ground
317 : : // terms. So, we add redundant substitutions
318 : 2816 : matches.insert(d_sygusVars.cbegin(), d_sygusVars.cend());
319 : :
320 : : // try to match the builtin term with the pattern sz
321 [ + + ]: 2816 : if (match(t, datatypes::utils::sygusToBuiltin(sz), matches))
322 : : {
323 : : // the bound variables z generated by the enumerators are reused across
324 : : // enumerated terms, so we need to replace them with our own skolems
325 : 364 : NodePairMap subs;
326 [ + - ]: 182 : Trace("sygus-rcons") << "-- ct: " << sz << std::endl;
327 : : // remove redundant substitutions
328 [ + + ]: 648 : for (const std::pair<const Node, Node>& pair : d_sygusVars)
329 : : {
330 : 466 : matches.erase(pair.first);
331 : : }
332 : : // for each match
333 [ + + ]: 462 : for (const std::pair<const Node, Node>& match : matches)
334 : : {
335 : 840 : TypeNode stn = datatypes::utils::builtinVarToSygus(match.first).getType();
336 : : RConsObligation* newOb;
337 : : // did we come across an equivalent obligation before?
338 : 280 : Node rep = d_stnInfo[stn].addTerm(match.second);
339 : 280 : RConsObligation* repOb = d_stnInfo[stn].builtinToOb(rep);
340 [ + + ]: 280 : if (repOb != nullptr)
341 : : {
342 : : // if so, use the original obligation
343 : 230 : newOb = repOb;
344 : : // while `match.second` is equivalent to `rep`, it may be easier to
345 : : // reconstruct than `rep`. For example:
346 : : //
347 : : // Grammar: S -> p | q | (not S) | (and S S) | (or S S)
348 : : // rep = (= p q)
349 : : // match.second = (or (and p q) (and (not p) (not q)))
350 : : //
351 : : // In this case, `match.second` is easy to reconstruct by matching
352 : : // because it only uses operators that are already in the grammar.
353 : : // `rep`, on the other hand, cannot be reconstructed by matching and
354 : : // can only be solved by enumeration (currently).
355 : : //
356 : : // At this point, we do not know which one is easier to reconstruct by
357 : : // matching, so we add `match.second` to the set of equivalent builtin
358 : : // terms in `repOb` and match against both terms.
359 : 230 : if (repOb->getBuiltins().find(match.second)
360 [ + + ]: 460 : == repOb->getBuiltins().cend())
361 : : {
362 : 6 : repOb->addBuiltin(match.second);
363 : 6 : d_stnInfo[stn].setBuiltinToOb(match.second, repOb);
364 : 6 : termsToReconsPrime[stn].emplace(match.second);
365 : : }
366 : : }
367 : : else
368 : : {
369 : : // otherwise, create a new obligation of the corresponding sygus type
370 : 50 : d_obs.push_back(std::make_unique<RConsObligation>(stn, match.second));
371 : 50 : d_stnInfo[stn].setBuiltinToOb(match.second, d_obs.back().get());
372 : 50 : newOb = d_obs.back().get();
373 : : // if the match is a constant and the grammar allows random constants
374 [ + + ][ + + ]: 50 : if (match.second.isConst() && stn.getDType().getSygusAllowConst())
[ + + ]
375 : : {
376 : : // then immediately solve the obligation
377 : 2 : markSolved(newOb, d_tds->getProxyVariable(stn, match.second));
378 : : }
379 : : else
380 : : {
381 : : // otherwise, add this match to the list of obligations
382 : 48 : termsToReconsPrime[stn].emplace(match.second);
383 : : }
384 : : }
385 : 560 : subs.emplace(datatypes::utils::builtinVarToSygus(match.first),
386 : 840 : newOb->getSkolem());
387 : : }
388 : : // replace original free vars in sz with new ones
389 [ + - ]: 182 : if (!subs.empty())
390 : : {
391 : 182 : sz = sz.substitute(subs.cbegin(), subs.cend());
392 : : }
393 : : // sz is solved if it has no sub-obligations or if all of them are solved
394 : 182 : bool isSolved = true;
395 [ + + ]: 462 : for (const std::pair<const Node, Node>& match : matches)
396 : : {
397 : 840 : TypeNode stn = datatypes::utils::builtinVarToSygus(match.first).getType();
398 : 280 : RConsObligation* ob = d_stnInfo[stn].builtinToOb(match.second);
399 [ + + ]: 280 : if (d_sol[ob->getSkolem()].isNull())
400 : : {
401 : 180 : isSolved = false;
402 : 180 : d_subObs[sz].push_back(ob);
403 : : }
404 : : }
405 : :
406 : 182 : RConsObligation* ob = d_stnInfo[sz.getType()].builtinToOb(t);
407 : :
408 [ + + ]: 182 : if (isSolved)
409 : : {
410 : : // As it traverses sz, substitute populates its input cache with TNodes
411 : : // that are not preserved by this module and maybe destroyed after the
412 : : // method call. To avoid referencing those unsafe TNodes throughout this
413 : : // module, we pass a iterators of d_sol instead.
414 : 28 : Node s = sz.substitute(d_sol.cbegin(), d_sol.cend());
415 : 28 : markSolved(ob, s);
416 : : }
417 : : else
418 : : {
419 : : // add sz as a possible solution to ob
420 : 154 : ob->addCandidateSolution(sz);
421 : 154 : d_parentOb[sz] = ob;
422 : 154 : d_subObs[sz].back()->addCandidateSolutionToWatchSet(sz);
423 : : }
424 : : }
425 : :
426 : 5632 : return termsToReconsPrime;
427 : : }
428 : :
429 : 2816 : bool SygusReconstruct::match(Node t, Node tz, NodePairMap& subs)
430 : : {
431 : : // rewrite pattern and replace n-ary ops with binary ones before performing
432 : : // simple pattern-matching.
433 : 2816 : return expr::match(convert(rewrite(tz)), convert(t), subs);
434 : : }
435 : :
436 : 1918 : void SygusReconstruct::markSolved(RConsObligation* ob, Node s)
437 : : {
438 : : // return if ob is already solved
439 [ + + ]: 1918 : if (!d_sol[ob->getSkolem()].isNull())
440 : : {
441 : 28 : return;
442 : : }
443 : :
444 [ + - ]: 1890 : Trace("sygus-rcons") << "sol: " << s << std::endl;
445 : 3780 : Trace("sygus-rcons") << "builtin sol: " << datatypes::utils::sygusToBuiltin(s)
446 : 1890 : << std::endl;
447 : :
448 : : // First, mark ob as solved
449 : 1890 : ob->addCandidateSolution(s);
450 : 1890 : d_sol[ob->getSkolem()] = s;
451 : 1890 : d_parentOb[s] = ob;
452 : :
453 : 3780 : std::vector<RConsObligation*> stack;
454 : 1890 : stack.push_back(ob);
455 : :
456 [ + + ]: 3808 : while (!stack.empty())
457 : : {
458 : 1918 : RConsObligation* curr = stack.back();
459 : 1918 : stack.pop_back();
460 : :
461 : : // for each partial solution/parent of the now solved obligation `curr`
462 [ + + ]: 2064 : for (const Node& parent : curr->getWatchSet())
463 : : {
464 : : // remove `curr` and (possibly) other solved obligations from its list
465 : : // of children
466 : 486 : while (!d_subObs[parent].empty()
467 : 632 : && !d_sol[d_subObs[parent].back()->getSkolem()].isNull())
468 : : {
469 : 170 : d_subObs[parent].pop_back();
470 : : }
471 : :
472 : : // if the partial solution does not have any more children...
473 [ + + ]: 146 : if (d_subObs[parent].empty())
474 : : {
475 : : // then it is completely solved and can be used as a solution of its
476 : : // corresponding obligation
477 : : // pass iterators of d_sol to avoid populating it with unsafe TNodes
478 : 268 : Node parentSol = parent.substitute(d_sol.cbegin(), d_sol.cend());
479 : 134 : RConsObligation* parentOb = d_parentOb[parent];
480 : : // proceed only if parent obligation is not already solved
481 [ + + ]: 134 : if (d_sol[parentOb->getSkolem()].isNull())
482 : : {
483 : 28 : parentOb->addCandidateSolution(parentSol);
484 : 28 : d_sol[parentOb->getSkolem()] = parentSol;
485 : 28 : d_parentOb[parentSol] = parentOb;
486 : : // repeat the same process for the parent obligation
487 : 28 : stack.push_back(parentOb);
488 : : }
489 : : }
490 : : else
491 : : {
492 : : // if it does have remaining children, add it to the watch list of one
493 : : // of them (picked arbitrarily)
494 : 12 : d_subObs[parent].back()->addCandidateSolutionToWatchSet(parent);
495 : : }
496 : : }
497 : : }
498 : : }
499 : :
500 : 54 : void SygusReconstruct::initialize(TypeNode stn)
501 : : {
502 : 108 : std::vector<Node> builtinVars;
503 : :
504 : : // Cache the sygus variables introduced by the problem (which we treat as
505 : : // ground terms when calling the `match` method) as opposed to the sygus
506 : : // variables introduced by the enumerators (which we treat as bound
507 : : // variables).
508 [ + + ]: 152 : for (Node sv : stn.getDType().getSygusVarList())
509 : : {
510 : 98 : builtinVars.push_back(datatypes::utils::sygusToBuiltin(sv));
511 : 196 : d_sygusVars.emplace(datatypes::utils::sygusToBuiltin(sv),
512 : 294 : datatypes::utils::sygusToBuiltin(sv));
513 : : }
514 : :
515 : 108 : SygusTypeInfo stnInfo;
516 : 54 : stnInfo.initialize(d_tds, stn);
517 : :
518 : : // find the non-terminals of the grammar
519 : 108 : std::vector<TypeNode> sfTypes;
520 : 54 : stnInfo.getSubfieldTypes(sfTypes);
521 : :
522 : : // initialize the enumerators and candidate rewrite databases. Notice here
523 : : // that we treat the sygus variables introduced by the problem as bound
524 : : // variables (needed for making sure that obligations are equal). This is fine
525 : : // as we will never add variables that were introduced by the enumerators to
526 : : // the database.
527 [ + + ]: 180 : for (TypeNode tn : sfTypes)
528 : : {
529 : 126 : d_stnInfo[tn].initialize(d_env, d_tds, d_stats, tn, builtinVars);
530 : : }
531 : 54 : }
532 : :
533 : 5090 : void SygusReconstruct::removeReconstructedTerms(
534 : : TypeBuiltinSetMap& termsToRecons)
535 : : {
536 [ + + ]: 12318 : for (std::pair<const TypeNode, BuiltinSet>& pair : termsToRecons)
537 : : {
538 : 7228 : BuiltinSet::iterator it = pair.second.begin();
539 [ + + ]: 15138 : while (it != pair.second.end())
540 : : {
541 [ + + ]: 7910 : if (d_sol[d_stnInfo[pair.first].builtinToOb(*it)->getSkolem()].isNull())
542 : : {
543 : 7812 : ++it;
544 : : }
545 : : else
546 : : {
547 : 98 : it = pair.second.erase(it);
548 : : }
549 : : }
550 : : }
551 : 5090 : }
552 : :
553 : 0 : Node SygusReconstruct::mkGround(Node n) const
554 : : {
555 : : // get the set of bound variables in n
556 : 0 : std::unordered_set<Node> vars;
557 : 0 : expr::getVariables(n, vars);
558 : :
559 : 0 : std::unordered_map<TNode, TNode> subs;
560 : :
561 : : // generate a ground value for each one of those variables
562 [ - - ]: 0 : for (const Node& var : vars)
563 : : {
564 : 0 : subs.emplace(var, NodeManager::mkGroundValue(var.getType()));
565 : : }
566 : :
567 : : // substitute the variables with ground values
568 : 0 : return n.substitute(subs);
569 : : }
570 : :
571 : 31476 : bool SygusReconstruct::notify(Node s,
572 : : Node n,
573 : : std::vector<Node>& vars,
574 : : std::vector<Node>& subs)
575 : : {
576 : : // If we are too aggressive in filtering enumerated shapes, we may miss some
577 : : // that speedup reconstruction time. So, for now, we disable filtering.
578 : 31476 : return true;
579 : : }
580 : :
581 : 3282 : Node SygusReconstruct::postConvert(Node n)
582 : : {
583 : 3282 : Kind k = n.getKind();
584 [ + + ]: 3282 : if (NodeManager::isNAryKind(n.getKind()))
585 : : {
586 [ + + ]: 558 : if (n.getNumChildren() > 2)
587 : : {
588 : 38 : NodeManager* nm = nodeManager();
589 : 76 : Node np = n[0];
590 [ + + ]: 114 : for (size_t i = 1, num = n.getNumChildren(); i < num; ++i)
591 : : {
592 : 76 : np = nm->mkNode(k, np, n[i]);
593 : : }
594 : 38 : return np;
595 : : }
596 : : }
597 : 3244 : return Node::null();
598 : : }
599 : :
600 : 54 : void SygusReconstruct::clear()
601 : : {
602 : 54 : d_obs.clear();
603 : 54 : d_stnInfo.clear();
604 : 54 : d_sol.clear();
605 : 54 : d_subObs.clear();
606 : 54 : d_parentOb.clear();
607 : 54 : d_sygusVars.clear();
608 : 54 : d_pool.clear();
609 : 54 : d_poolTrie.clear();
610 : 54 : }
611 : :
612 : 0 : void SygusReconstruct::printPool() const
613 : : {
614 [ - - ]: 0 : Trace("sygus-rcons") << std::endl << "Pool:" << std::endl << '{';
615 : :
616 [ - - ]: 0 : for (const std::pair<const TypeNode, std::vector<Node>>& pair : d_pool)
617 : : {
618 [ - - ]: 0 : Trace("sygus-rcons") << std::endl
619 : 0 : << " " << pair.first << ':' << std::endl
620 : 0 : << " [" << std::endl;
621 : :
622 [ - - ]: 0 : for (const Node& sygusTerm : pair.second)
623 : : {
624 [ - - ]: 0 : Trace("sygus-rcons")
625 : 0 : << " "
626 : 0 : << rewrite(datatypes::utils::sygusToBuiltin(sygusTerm)).toString()
627 : 0 : << std::endl;
628 : : }
629 : :
630 [ - - ]: 0 : Trace("sygus-rcons") << " ]" << std::endl;
631 : : }
632 : :
633 [ - - ]: 0 : Trace("sygus-rcons") << '}' << std::endl;
634 : 0 : }
635 : :
636 : : } // namespace quantifiers
637 : : } // namespace theory
638 : : } // namespace cvc5::internal
|
