Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Haniel Barbosa, Aina Niemetz
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 : : * The solver for SyGuS queries.
14 : : */
15 : :
16 : : #include "smt/sygus_solver.h"
17 : :
18 : : #include <sstream>
19 : :
20 : : #include "base/modal_exception.h"
21 : : #include "expr/dtype.h"
22 : : #include "expr/dtype_cons.h"
23 : : #include "expr/node_algorithm.h"
24 : : #include "expr/skolem_manager.h"
25 : : #include "options/base_options.h"
26 : : #include "options/option_exception.h"
27 : : #include "options/quantifiers_options.h"
28 : : #include "options/smt_options.h"
29 : : #include "smt/logic_exception.h"
30 : : #include "smt/preprocessor.h"
31 : : #include "smt/smt_driver.h"
32 : : #include "smt/smt_solver.h"
33 : : #include "theory/datatypes/sygus_datatype_utils.h"
34 : : #include "theory/quantifiers/quantifiers_attributes.h"
35 : : #include "theory/quantifiers/sygus/sygus_utils.h"
36 : : #include "theory/quantifiers_engine.h"
37 : : #include "theory/rewriter.h"
38 : : #include "theory/smt_engine_subsolver.h"
39 : : #include "theory/trust_substitutions.h"
40 : :
41 : : using namespace cvc5::internal::theory;
42 : : using namespace cvc5::internal::kind;
43 : :
44 : : namespace cvc5::internal {
45 : : namespace smt {
46 : :
47 : 71513 : SygusSolver::SygusSolver(Env& env, SmtSolver& sms)
48 : : : EnvObj(env),
49 : : d_smtSolver(sms),
50 : 143026 : d_sygusVars(userContext()),
51 : 143026 : d_sygusConstraints(userContext()),
52 : 143026 : d_sygusAssumps(userContext()),
53 : 143026 : d_sygusFunSymbols(userContext()),
54 : 0 : d_sygusConjectureStale(userContext(), true),
55 : 71513 : d_subsolverCd(userContext(), nullptr)
56 : : {
57 : 71513 : }
58 : :
59 : 133902 : SygusSolver::~SygusSolver() {}
60 : :
61 : 2699 : void SygusSolver::declareSygusVar(Node var)
62 : : {
63 [ + - ]: 5398 : Trace("smt") << "SygusSolver::declareSygusVar: " << var << " "
64 [ - + ][ - - ]: 2699 : << var.getType() << "\n";
65 : 2699 : d_sygusVars.push_back(var);
66 : : // don't need to set that the conjecture is stale
67 : 2699 : }
68 : :
69 : 2858 : void SygusSolver::declareSynthFun(Node fn,
70 : : TypeNode sygusType,
71 : : bool isInv,
72 : : const std::vector<Node>& vars)
73 : : {
74 [ + - ]: 2858 : Trace("smt") << "SygusSolver::declareSynthFun: " << fn << "\n";
75 : 2858 : NodeManager* nm = nodeManager();
76 : 2858 : d_sygusFunSymbols.push_back(fn);
77 [ + + ]: 2858 : if (!vars.empty())
78 : : {
79 : 1774 : Node bvl = nm->mkNode(Kind::BOUND_VAR_LIST, vars);
80 : : // use an attribute to mark its bound variable list
81 : 1774 : quantifiers::SygusUtils::setSygusArgumentList(fn, bvl);
82 : : }
83 : : // whether sygus type encodes syntax restrictions
84 [ + + ]: 5442 : if (!sygusType.isNull() && sygusType.isDatatype()
85 [ + + ][ + + ]: 5442 : && sygusType.getDType().isSygus())
[ + + ]
86 : : {
87 : : // use an attribute to mark its grammar
88 : 1381 : quantifiers::SygusUtils::setSygusType(fn, sygusType);
89 : : // we now check for free variables for sygus operators in the block
90 : 1383 : checkDefinitionsSygusDt(fn, sygusType);
91 : : }
92 : :
93 : : // sygus conjecture is now stale
94 : 2856 : d_sygusConjectureStale = true;
95 : 2856 : }
96 : :
97 : 3282 : void SygusSolver::assertSygusConstraint(Node n, bool isAssume)
98 : : {
99 [ + + ]: 3282 : if (n.getKind() == Kind::AND)
100 : : {
101 : : // miniscope, to account for forall handling below as child of AND
102 [ + + ]: 1024 : for (const Node& nc : n)
103 : : {
104 : 688 : assertSygusConstraint(nc, isAssume);
105 : : }
106 : 336 : return;
107 : : }
108 [ + + ]: 2946 : else if (n.getKind() == Kind::FORALL)
109 : : {
110 : : // forall as constraint is equivalent to introducing its variables and
111 : : // using a quantifier-free constraint.
112 [ + + ]: 6 : for (const Node& v : n[0])
113 : : {
114 : 4 : declareSygusVar(v);
115 : : }
116 : 2 : n = n[1];
117 : : }
118 [ + - ]: 5892 : Trace("smt") << "SygusSolver::assertSygusConstrant: " << n
119 : 2946 : << ", isAssume=" << isAssume << "\n";
120 [ + + ]: 2946 : if (isAssume)
121 : : {
122 : 329 : d_sygusAssumps.push_back(n);
123 : : }
124 : : else
125 : : {
126 : 2617 : d_sygusConstraints.push_back(n);
127 : : }
128 : :
129 : : // sygus conjecture is now stale
130 : 2946 : d_sygusConjectureStale = true;
131 : : }
132 : :
133 : 58 : std::vector<Node> SygusSolver::getSygusConstraints() const
134 : : {
135 : 58 : return listToVector(d_sygusConstraints);
136 : : }
137 : :
138 : 53 : std::vector<Node> SygusSolver::getSygusAssumptions() const
139 : : {
140 : 53 : return listToVector(d_sygusAssumps);
141 : : }
142 : :
143 : 263 : void SygusSolver::assertSygusInvConstraint(Node inv,
144 : : Node pre,
145 : : Node trans,
146 : : Node post)
147 : : {
148 [ + - ]: 526 : Trace("smt") << "SygusSolver::assertSygusInvConstrant: " << inv << " " << pre
149 : 263 : << " " << trans << " " << post << "\n";
150 : : // build invariant constraint
151 : :
152 : : // get variables (regular and their respective primed versions)
153 : 526 : std::vector<Node> terms;
154 : 526 : std::vector<Node> vars;
155 : 526 : std::vector<Node> primed_vars;
156 : 263 : terms.push_back(inv);
157 : 263 : terms.push_back(pre);
158 : 263 : terms.push_back(trans);
159 : 263 : terms.push_back(post);
160 : : // variables are built based on the invariant type
161 : 263 : NodeManager* nm = nodeManager();
162 : 526 : std::vector<TypeNode> argTypes = inv.getType().getArgTypes();
163 [ + + ]: 684 : for (const TypeNode& tn : argTypes)
164 : : {
165 : 421 : vars.push_back(NodeManager::mkBoundVar(tn));
166 : 421 : d_sygusVars.push_back(vars.back());
167 : 842 : std::stringstream ss;
168 : 421 : ss << vars.back() << "'";
169 : 421 : primed_vars.push_back(NodeManager::mkBoundVar(ss.str(), tn));
170 : 421 : d_sygusVars.push_back(primed_vars.back());
171 : : }
172 : :
173 : : // make relevant terms; 0 -> Inv, 1 -> Pre, 2 -> Trans, 3 -> Post
174 [ + + ]: 1315 : for (unsigned i = 0; i < 4; ++i)
175 : : {
176 : 2104 : Node op = terms[i];
177 [ + - ]: 2104 : Trace("smt-debug") << "Make inv-constraint term #" << i << " : " << op
178 [ - + ][ - - ]: 1052 : << " with type " << op.getType() << "...\n";
179 : 2104 : std::vector<Node> children;
180 : 1052 : children.push_back(op);
181 : : // transition relation applied over both variable lists
182 [ + + ]: 1052 : if (i == 2)
183 : : {
184 : 263 : children.insert(children.end(), vars.begin(), vars.end());
185 : 263 : children.insert(children.end(), primed_vars.begin(), primed_vars.end());
186 : : }
187 : : else
188 : : {
189 : 789 : children.insert(children.end(), vars.begin(), vars.end());
190 : : }
191 : 1052 : terms[i] = nm->mkNode(Kind::APPLY_UF, children);
192 : : // make application of Inv on primed variables
193 [ + + ]: 1052 : if (i == 0)
194 : : {
195 : 263 : children.clear();
196 : 263 : children.push_back(op);
197 : 263 : children.insert(children.end(), primed_vars.begin(), primed_vars.end());
198 : 263 : terms.push_back(nm->mkNode(Kind::APPLY_UF, children));
199 : : }
200 : : }
201 : : // make constraints
202 : 526 : std::vector<Node> conj;
203 : 263 : conj.push_back(nm->mkNode(Kind::IMPLIES, terms[1], terms[0]));
204 : 789 : Node term0_and_2 = nm->mkNode(Kind::AND, terms[0], terms[2]);
205 : 263 : conj.push_back(nm->mkNode(Kind::IMPLIES, term0_and_2, terms[4]));
206 : 263 : conj.push_back(nm->mkNode(Kind::IMPLIES, terms[0], terms[3]));
207 : 263 : Node constraint = nm->mkNode(Kind::AND, conj);
208 : :
209 : 263 : d_sygusConstraints.push_back(constraint);
210 : :
211 : : // sygus conjecture is now stale
212 : 263 : d_sygusConjectureStale = true;
213 : 263 : }
214 : :
215 : 1368 : SynthResult SygusSolver::checkSynth(bool isNext)
216 : : {
217 [ + - ]: 1368 : Trace("smt") << "SygusSolver::checkSynth" << std::endl;
218 : : // if applicable, check if the subsolver is the correct one
219 [ + + ]: 1368 : if (!isNext)
220 : : {
221 : : // if we are not using check-synth-next, we always reconstruct the solver.
222 : 1248 : d_sygusConjectureStale = true;
223 : : }
224 [ + + ][ + + ]: 1368 : if (usingSygusSubsolver() && d_subsolverCd.get() != d_subsolver.get())
[ + + ]
225 : : {
226 : : // this can occur if we backtrack to a place where we were using a different
227 : : // subsolver than the current one. In this case, we should reconstruct
228 : : // the subsolver.
229 : 2 : d_sygusConjectureStale = true;
230 : : }
231 [ + + ]: 1368 : if (d_sygusConjectureStale)
232 : : {
233 : 1248 : NodeManager* nm = nodeManager();
234 : : // build synthesis conjecture from asserted constraints and declared
235 : : // variables/functions
236 [ + - ]: 1248 : Trace("smt") << "Sygus : Constructing sygus constraint...\n";
237 : 2496 : Node body = nm->mkAnd(listToVector(d_sygusConstraints));
238 : : // note that if there are no constraints, then assumptions are irrelevant
239 [ + + ][ + + ]: 1248 : if (!d_sygusConstraints.empty() && !d_sygusAssumps.empty())
[ + + ]
240 : : {
241 : 6 : Node bodyAssump = nm->mkAnd(listToVector(d_sygusAssumps));
242 : 6 : body = nm->mkNode(Kind::IMPLIES, bodyAssump, body);
243 : : }
244 : 1248 : body = body.notNode();
245 [ + - ]: 2496 : Trace("smt-debug") << "...constructed sygus constraint " << body
246 : 1248 : << std::endl;
247 [ + + ]: 1248 : if (!d_sygusVars.empty())
248 : : {
249 : : Node boundVars =
250 : 597 : nm->mkNode(Kind::BOUND_VAR_LIST, listToVector(d_sygusVars));
251 : 597 : body = nm->mkNode(Kind::EXISTS, boundVars, body);
252 [ + - ]: 597 : Trace("smt-debug") << "...constructed exists " << body << std::endl;
253 : : }
254 : 1248 : bool inferTrivial = true;
255 : : // cannot omit unused functions if in incremental or sygus-stream
256 [ + + ][ + + ]: 1248 : if (options().quantifiers.sygusStream || options().base.incrementalSolving)
[ + + ]
257 : : {
258 : 525 : inferTrivial = false;
259 : : }
260 : : // Mark functions that do not occur in the conjecture as trivial,
261 : : // and do not solve for them.
262 : 2496 : std::vector<Node> ntrivSynthFuns;
263 [ + + ]: 1248 : if (inferTrivial)
264 : : {
265 : : // must expand definitions first
266 : : // We consider free variables in the rewritten form of the *body* of
267 : : // the existential, not the rewritten form of the existential itself,
268 : : // which could permit eliminating variables that are equal to terms
269 : : // involving functions to synthesize.
270 [ + + ]: 1446 : Node ppBody = body.getKind()==Kind::EXISTS ? body[1] : body;
271 : 723 : ppBody = d_smtSolver.getPreprocessor()->applySubstitutions(ppBody);
272 : 723 : ppBody = rewrite(ppBody);
273 : 1446 : std::unordered_set<Node> vs;
274 : 723 : expr::getVariables(ppBody, vs);
275 [ + - ]: 734 : for (size_t i = 0; i < 2; i++)
276 : : {
277 : 734 : d_trivialFuns.clear();
278 [ + + ]: 1809 : for (const Node& f : d_sygusFunSymbols)
279 : : {
280 [ + + ]: 1075 : if (vs.find(f) != vs.end())
281 : : {
282 : 894 : ntrivSynthFuns.push_back(f);
283 : : }
284 : : else
285 : : {
286 [ + - ]: 181 : Trace("smt-debug") << "...trivial function: " << f << std::endl;
287 : 181 : d_trivialFuns.push_back(f);
288 : : }
289 : : }
290 : : // we could have dependencies from the grammars of
291 : : // functions-to-synthesize to trivial functions, account for this as
292 : : // well
293 [ + + ][ + + ]: 734 : if (i == 0 && !d_trivialFuns.empty())
[ + + ]
294 : : {
295 : 122 : size_t prevSize = vs.size();
296 [ + + ]: 220 : for (const Node& f : ntrivSynthFuns)
297 : : {
298 : 98 : TypeNode tnp = quantifiers::SygusUtils::getSygusType(f);
299 [ + + ]: 98 : if (tnp.isNull())
300 : : {
301 : 87 : continue;
302 : : }
303 : 11 : theory::datatypes::utils::getFreeVariablesSygusType(tnp, vs);
304 : : }
305 [ + + ]: 122 : if (vs.size() == prevSize)
306 : : {
307 : : // no new symbols found
308 : 111 : break;
309 : : }
310 : : }
311 : : else
312 : : {
313 : 612 : break;
314 : : }
315 : : }
316 : : }
317 : : else
318 : : {
319 : 525 : ntrivSynthFuns = listToVector(d_sygusFunSymbols);
320 : : }
321 [ + + ]: 1248 : if (!ntrivSynthFuns.empty())
322 : : {
323 : 2212 : body = quantifiers::SygusUtils::mkSygusConjecture(
324 : 1106 : nodeManager(), ntrivSynthFuns, body);
325 : : }
326 [ + - ]: 1248 : Trace("smt-debug") << "...constructed forall " << body << std::endl;
327 : :
328 [ + - ]: 1248 : Trace("smt") << "Check synthesis conjecture: " << body << std::endl;
329 : :
330 : 1248 : d_sygusConjectureStale = false;
331 : :
332 : 1248 : d_conj = body;
333 : :
334 : : // if we are using a subsolver, initialize it now
335 [ + + ]: 1248 : if (usingSygusSubsolver())
336 : : {
337 : : // we generate a new solver engine to do the SyGuS query
338 : 521 : Assertions& as = d_smtSolver.getAssertions();
339 : 521 : initializeSygusSubsolver(d_subsolver, as);
340 : :
341 : : // store the pointer (context-dependent)
342 : 521 : d_subsolverCd = d_subsolver.get();
343 : :
344 : : // also assert the internal SyGuS conjecture
345 : 521 : d_subsolver->assertFormula(d_conj);
346 : : }
347 : : }
348 : : else
349 : : {
350 [ - + ][ - + ]: 120 : Assert(d_subsolver != nullptr);
[ - - ]
351 : : }
352 : 2736 : Result r;
353 [ + + ]: 1368 : if (usingSygusSubsolver())
354 : : {
355 [ + - ]: 641 : Trace("smt-sygus") << "SygusSolver: check sat with subsolver..." << std::endl;
356 : 641 : r = d_subsolver->checkSat();
357 : : }
358 : : else
359 : : {
360 [ + - ]: 727 : Trace("smt-sygus") << "SygusSolver: check sat with main solver..." << std::endl;
361 : 1454 : std::vector<Node> query;
362 : 727 : query.push_back(d_conj);
363 : : // use a single call driver
364 : 731 : SmtDriverSingleCall sdsc(d_env, d_smtSolver);
365 : 727 : r = sdsc.checkSat(query);
366 : : }
367 [ + - ]: 1364 : Trace("smt-sygus") << "...got " << r << std::endl;
368 : : // The result returned by the above call is typically "unknown", which may
369 : : // or may not correspond to a state in which we solved the conjecture
370 : : // successfully. Instead we call getSynthSolutions below. If this returns
371 : : // true, then we were successful. In this case, we set the synthesis result to
372 : : // "solution".
373 : : //
374 : : // This behavior is done for 2 reasons:
375 : : // (1) if we do not negate the synthesis conjecture, the subsolver in some
376 : : // cases cannot answer "sat", e.g. in the presence of recursive function
377 : : // definitions. Instead the SyGuS language standard itself indicates that
378 : : // a correct solution for a conjecture is one where the synthesis conjecture
379 : : // is *T-valid* (in the presence of defined recursive functions). In other
380 : : // words, a SyGuS query asks to prove that the conjecture is valid when
381 : : // witnessed by the given solution.
382 : : // (2) we do not want the solver to explicitly answer "unsat" by giving an
383 : : // unsatisfiable set of formulas to the underlying PropEngine, or otherwise
384 : : // we will not be able to ask for further solutions. This is critical for
385 : : // incremental solving where multiple solutions are returned for the same
386 : : // set of constraints. Thus, the internal SyGuS solver will mark unknown
387 : : // with IncompleteId::QUANTIFIERS_SYGUS_SOLVED. Furthermore, this id may be
388 : : // overwritten by other means of incompleteness, so we cannot rely on this
389 : : // identifier being the final reason for unknown.
390 : : //
391 : : // Thus, we use getSynthSolutions as means of knowing the conjecture was
392 : : // solved.
393 : 1364 : SynthResult sr;
394 : 1364 : std::map<Node, Node> sol_map;
395 [ + + ]: 1364 : if (getSynthSolutions(sol_map))
396 : : {
397 : : // if we have solutions, we return "solution"
398 : 1280 : sr = SynthResult(SynthResult::SOLUTION);
399 : : // Check that synthesis solutions satisfy the conjecture
400 [ + + ]: 1280 : if (options().smt.checkSynthSol)
401 : : {
402 : 216 : Assertions& as = d_smtSolver.getAssertions();
403 : 216 : checkSynthSolution(as, sol_map);
404 : : }
405 : : }
406 [ + + ]: 84 : else if (r.getStatus() == Result::UNSAT)
407 : : {
408 : : // unsat means no solution
409 : 74 : sr = SynthResult(SynthResult::NO_SOLUTION);
410 : : }
411 : : else
412 : : {
413 : : // otherwise, we return "unknown"
414 : 10 : sr = SynthResult(SynthResult::UNKNOWN, UnknownExplanation::UNKNOWN_REASON);
415 : : }
416 : 2728 : return sr;
417 : : }
418 : :
419 : 2265 : bool SygusSolver::getSynthSolutions(std::map<Node, Node>& solMap)
420 : : {
421 : 2265 : bool ret = false;
422 [ + - ]: 2265 : Trace("smt") << "SygusSolver::getSynthSolutions" << std::endl;
423 [ + + ]: 2265 : if (usingSygusSubsolver())
424 : : {
425 : : // use the call to get the synth solutions from the subsolver
426 [ + + ]: 1206 : if (d_subsolver)
427 : : {
428 : 1202 : ret = d_subsolver->getSubsolverSynthSolutions(solMap);
429 : : }
430 : : }
431 : : else
432 : : {
433 : 1059 : ret = getSubsolverSynthSolutions(solMap);
434 : : }
435 [ + + ]: 2265 : if (ret)
436 : : {
437 : : // also get solutions for trivial functions to synthesize
438 [ + + ]: 2470 : for (const Node& f : d_trivialFuns)
439 : : {
440 : 586 : Node sf = quantifiers::SygusUtils::mkSygusTermFor(f);
441 [ + - ]: 586 : Trace("smt-debug") << "Got " << sf << " for trivial function " << f
442 : 293 : << std::endl;
443 [ - + ][ - + ]: 293 : Assert(f.getType() == sf.getType());
[ - - ]
444 : 293 : solMap[f] = sf;
445 : : }
446 : : }
447 : 2265 : return ret;
448 : : }
449 : :
450 : 3003 : bool SygusSolver::getSubsolverSynthSolutions(std::map<Node, Node>& solMap)
451 : : {
452 [ + - ]: 3003 : Trace("smt") << "SygusSolver::getSubsolverSynthSolutions" << std::endl;
453 : 6006 : std::map<Node, std::map<Node, Node>> solMapn;
454 : : // fail if the theory engine does not have synthesis solutions
455 : 3003 : QuantifiersEngine* qe = d_smtSolver.getQuantifiersEngine();
456 [ + - ][ + + ]: 3003 : if (qe == nullptr || !qe->getSynthSolutions(solMapn))
[ + + ]
457 : : {
458 : 139 : return false;
459 : : }
460 [ + + ]: 5445 : for (std::pair<const Node, std::map<Node, Node>>& cs : solMapn)
461 : : {
462 [ + + ]: 5486 : for (std::pair<const Node, Node>& s : cs.second)
463 : : {
464 : 2905 : solMap[s.first] = s.second;
465 : : }
466 : : }
467 : 2864 : return true;
468 : : }
469 : :
470 : 263 : bool SygusSolver::canTrustSynthesisResult(const Options& opts)
471 : : {
472 [ + + ]: 263 : if (opts.quantifiers.cegisSample == options::CegisSampleMode::TRUST)
473 : : {
474 : 3 : return false;
475 : : }
476 : 260 : return true;
477 : : }
478 : :
479 : 216 : void SygusSolver::checkSynthSolution(Assertions& as,
480 : : const std::map<Node, Node>& sol_map)
481 : : {
482 [ + + ]: 216 : if (isVerboseOn(1))
483 : : {
484 : 1 : verbose(1) << "SyGuS::checkSynthSolution: checking synthesis solution"
485 : 1 : << std::endl;
486 : : }
487 : 216 : bool canTrustResult = canTrustSynthesisResult(options());
488 [ - + ]: 216 : if (!canTrustResult)
489 : : {
490 : 0 : warning() << "Running check-synth-sol is not guaranteed to pass with the "
491 : 0 : "current options."
492 : 0 : << std::endl;
493 : : }
494 [ - + ]: 216 : if (sol_map.empty())
495 : : {
496 : 0 : InternalError() << "SygusSolver::checkSynthSolution(): Got empty solution!";
497 : : return;
498 : : }
499 [ + - ]: 216 : Trace("check-synth-sol") << "Got solution map:\n";
500 : : // the set of synthesis conjectures in our assertions
501 : 432 : std::unordered_set<Node> conjs;
502 : 216 : conjs.insert(d_conj);
503 : : // For each of the above conjectures, the functions-to-synthesis and their
504 : : // solutions. This is used as a substitution below.
505 : 432 : Subs fsubs;
506 : 432 : Subs psubs;
507 : 432 : std::vector<Node> eqs;
508 [ + + ]: 591 : for (const std::pair<const Node, Node>& pair : sol_map)
509 : : {
510 [ + - ]: 750 : Trace("check-synth-sol")
511 : 375 : << " " << pair.first << " --> " << pair.second << "\n";
512 : 375 : fsubs.add(pair.first, pair.second);
513 : 375 : psubs.add(pair.first);
514 : 375 : eqs.push_back(pair.first.eqNode(pair.second));
515 : : }
516 : :
517 [ + - ]: 216 : Trace("check-synth-sol") << "Starting new SMT Engine\n";
518 : :
519 [ + - ]: 216 : Trace("check-synth-sol") << "Retrieving assertions\n";
520 : : // Build conjecture from original assertions
521 : : // check all conjectures
522 : 216 : NodeManager* nm = nodeManager();
523 [ + + ]: 432 : for (const Node& conj : conjs)
524 : : {
525 : : // Start new SMT engine to check solutions
526 : 0 : std::unique_ptr<SolverEngine> solChecker;
527 : 216 : initializeSygusSubsolver(solChecker, as);
528 : 216 : solChecker->getOptions().write_smt().checkSynthSol = false;
529 : 216 : solChecker->getOptions().write_quantifiers().sygusRecFun = false;
530 : 216 : Node conjBody = conj;
531 [ + + ]: 216 : if (conj.getKind() == Kind::FORALL)
532 : : {
533 : 206 : conjBody = conjBody[1];
534 : : }
535 : : // we must apply substitutions here, since define-fun may contain the
536 : : // function-to-synthesize, which needs to be substituted.
537 : 216 : conjBody = d_smtSolver.getPreprocessor()->applySubstitutions(conjBody);
538 : : // Apply solution map to conjecture body
539 : 216 : conjBody = rewrite(fsubs.apply(conjBody));
540 : : // if fwd-decls, the above may contain functions-to-synthesize as free
541 : : // variables. In this case, we add (higher-order) equalities and replace
542 : : // functions-to-synthesize with skolems.
543 [ + + ]: 216 : if (expr::hasFreeVar(conjBody))
544 : : {
545 : 2 : std::vector<Node> conjAndSol;
546 : 2 : conjAndSol.push_back(conjBody);
547 : 2 : conjAndSol.insert(conjAndSol.end(), eqs.begin(), eqs.end());
548 : 2 : conjBody = nm->mkAnd(conjAndSol);
549 : 2 : conjBody = rewrite(psubs.apply(conjBody));
550 : : }
551 : :
552 [ + + ]: 216 : if (isVerboseOn(1))
553 : : {
554 : 1 : verbose(1) << "SyGuS::checkSynthSolution: -- body substitutes to "
555 : 1 : << conjBody << std::endl;
556 : : }
557 [ + - ]: 432 : Trace("check-synth-sol")
558 : 216 : << "Substituted body of assertion to " << conjBody << "\n";
559 : 216 : solChecker->assertFormula(conjBody);
560 : 216 : Result r = solChecker->checkSat();
561 [ + + ]: 216 : if (isVerboseOn(1))
562 : : {
563 : 1 : verbose(1) << "SyGuS::checkSynthSolution: result is " << r << std::endl;
564 : : }
565 [ + - ]: 216 : Trace("check-synth-sol") << "Satsifiability check: " << r << "\n";
566 [ + - ]: 216 : if (r.getStatus() == Result::UNSAT)
567 : : {
568 : 216 : continue;
569 : : }
570 : 0 : std::stringstream ss;
571 : 0 : bool hardFailure = canTrustResult;
572 [ - - ]: 0 : if (r.getStatus() == Result::SAT)
573 : : {
574 : : ss << "SygusSolver::checkSynthSolution(): produced solution leads to "
575 : 0 : "satisfiable negated conjecture.";
576 : : }
577 : : else
578 : : {
579 : 0 : hardFailure = false;
580 : : ss << "SygusSolver::checkSynthSolution(): could not check "
581 : 0 : "solution, result unknown.";
582 : : }
583 [ - - ]: 0 : if (hardFailure)
584 : : {
585 : 0 : InternalError() << ss.str();
586 : : }
587 : : else
588 : : {
589 : 0 : warning() << ss.str() << std::endl;
590 : : }
591 : : }
592 : : }
593 : :
594 : 737 : void SygusSolver::initializeSygusSubsolver(std::unique_ptr<SolverEngine>& se,
595 : : Assertions& as)
596 : : {
597 : 737 : initializeSubsolver(se, d_env);
598 : 1474 : std::unordered_set<Node> processed;
599 : : // if we did not spawn a subsolver for the main check, the overall SyGuS
600 : : // conjecture has been added as an assertion. Do not add it here, which
601 : : // is important for check-synth-sol. Adding this also has no impact
602 : : // when spawning a subsolver for the main check.
603 : 737 : processed.insert(d_conj);
604 : : // carry the ordinary define-fun definitions
605 : 737 : const context::CDList<Node>& alistDefs = as.getAssertionListDefinitions();
606 [ + + ]: 1021 : for (const Node& def : alistDefs)
607 : : {
608 : : // only consider define-fun, represented as (= f (lambda ...)).
609 [ + + ]: 284 : if (def.getKind() == Kind::EQUAL)
610 : : {
611 [ - + ][ - + ]: 276 : Assert(def[0].isVar());
[ - - ]
612 : 552 : std::vector<Node> formals;
613 : 552 : Node dbody = def[1];
614 [ + + ]: 276 : if (def[1].getKind() == Kind::LAMBDA)
615 : : {
616 : 260 : formals.insert(formals.end(), def[1][0].begin(), def[1][0].end());
617 : 260 : dbody = dbody[1];
618 : : }
619 : 276 : se->defineFunction(def[0], formals, dbody);
620 : 276 : processed.insert(def);
621 : : }
622 : : }
623 : : // Also assert auxiliary assertions, which typically correspond to
624 : : // quantified formulas for define-fun-rec only.
625 : 737 : const context::CDList<Node>& alist = as.getAssertionList();
626 [ + + ]: 1227 : for (size_t i = 0, asize = alist.size(); i < asize; ++i)
627 : : {
628 : 980 : Node a = alist[i];
629 : : // ignore definitions here
630 [ + + ]: 490 : if (processed.find(a) == processed.end())
631 : : {
632 : 8 : se->assertFormula(a);
633 : : }
634 : : }
635 : 737 : }
636 : :
637 : 6249 : bool SygusSolver::usingSygusSubsolver() const
638 : : {
639 : : // use SyGuS subsolver if in incremental mode
640 : 6249 : return options().base.incrementalSolving;
641 : : }
642 : :
643 : 1381 : void SygusSolver::checkDefinitionsSygusDt(const Node& fn, TypeNode tn) const
644 : : {
645 : 2762 : std::unordered_set<TypeNode> processed;
646 : 2762 : std::vector<TypeNode> toProcess;
647 : 1381 : toProcess.push_back(tn);
648 : 1381 : size_t index = 0;
649 [ + + ]: 4188 : while (index < toProcess.size())
650 : : {
651 : 5618 : TypeNode tnp = toProcess[index];
652 : 2809 : index++;
653 [ - + ][ - + ]: 2809 : Assert(tnp.isDatatype());
[ - - ]
654 [ - + ][ - + ]: 2809 : Assert(tnp.getDType().isSygus());
[ - - ]
655 : 2809 : const DType& dt = tnp.getDType();
656 : : const std::vector<std::shared_ptr<DTypeConstructor>>& cons =
657 : 2809 : dt.getConstructors();
658 : 5618 : std::unordered_set<TNode> scope;
659 : : // we allow other functions
660 : 2809 : scope.insert(d_sygusFunSymbols.begin(), d_sygusFunSymbols.end());
661 : 5618 : Node dtl = dt.getSygusVarList();
662 [ + + ]: 2809 : if (!dtl.isNull())
663 : : {
664 : 2284 : scope.insert(dtl.begin(), dtl.end());
665 : : }
666 [ + + ]: 14208 : for (const std::shared_ptr<DTypeConstructor>& c : cons)
667 : : {
668 : 22802 : Node op = c->getSygusOp();
669 : : // check for free variables here
670 [ + + ]: 11401 : if (expr::hasFreeVariablesScope(op, scope))
671 : : {
672 : 4 : std::stringstream ss;
673 : 2 : ss << "ERROR: cannot process term " << op
674 : 2 : << " with free variables in grammar of " << fn;
675 : 2 : throw LogicException(ss.str());
676 : : }
677 : : // also must consider the arguments
678 [ + + ]: 22494 : for (unsigned j = 0, nargs = c->getNumArgs(); j < nargs; ++j)
679 : : {
680 : 22190 : TypeNode tnc = c->getArgType(j);
681 [ + + ][ + + ]: 11095 : if (tnc.isSygusDatatype() && processed.find(tnc) == processed.end())
[ + + ]
682 : : {
683 : 1428 : toProcess.push_back(tnc);
684 : 1428 : processed.insert(tnc);
685 : : }
686 : : }
687 : : }
688 : : }
689 : 1379 : }
690 : :
691 : 2487 : std::vector<Node> SygusSolver::listToVector(const NodeList& list)
692 : : {
693 : 2487 : std::vector<Node> vec;
694 [ + + ]: 7624 : for (const Node& n : list)
695 : : {
696 : 5137 : vec.push_back(n);
697 : : }
698 : 2487 : return vec;
699 : : }
700 : :
701 : 50 : std::vector<std::pair<Node, TypeNode>> SygusSolver::getSynthFunctions() const
702 : : {
703 : 50 : std::vector<std::pair<Node, TypeNode>> funs;
704 [ + + ]: 100 : for (const Node& f : d_sygusFunSymbols)
705 : : {
706 : 100 : TypeNode st = quantifiers::SygusUtils::getSygusType(f);
707 : 50 : funs.emplace_back(f, st);
708 : : }
709 : 50 : return funs;
710 : : }
711 : :
712 : : } // namespace smt
713 : : } // namespace cvc5::internal
|
