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