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