Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Implementation of command objects.
11 : : */
12 : :
13 : : #include "parser/commands.h"
14 : :
15 : : #include <exception>
16 : : #include <iostream>
17 : : #include <iterator>
18 : : #include <sstream>
19 : : #include <utility>
20 : : #include <vector>
21 : :
22 : : #include "base/check.h"
23 : : #include "base/modal_exception.h"
24 : : #include "base/output.h"
25 : : #include "expr/node_manager.h"
26 : : #include "main/command_executor.h"
27 : : #include "options/io_utils.h"
28 : : #include "options/main_options.h"
29 : : #include "options/options.h"
30 : : #include "options/printer_options.h"
31 : : #include "options/smt_options.h"
32 : : #include "parser/command_status.h"
33 : : #include "parser/sym_manager.h"
34 : : #include "printer/printer.h"
35 : : #include "proof/unsat_core.h"
36 : : #include "util/smt2_quote_string.h"
37 : : #include "util/utility.h"
38 : :
39 : : using namespace std;
40 : :
41 : : namespace cvc5::parser {
42 : :
43 : 27164 : std::string sexprToString(cvc5::Term sexpr)
44 : : {
45 : : // if sexpr has a symbol, return its symbol. We don't
46 : : // call Term::toString as its result depends on the output language.
47 : : // Notice that we only check for terms with symbols. The sexprs generated by
48 : : // the parser don't contains other atomic terms, so we can ignore them.
49 [ + + ]: 27164 : if (sexpr.hasSymbol())
50 : : {
51 : 27135 : return sexpr.getSymbol();
52 : : }
53 : :
54 : : // if sexpr is not a spec constant, make sure it is an array of sub-sexprs
55 [ - + ][ - + ]: 29 : Assert(sexpr.getKind() == cvc5::Kind::SEXPR);
[ - - ]
56 : :
57 : 29 : std::stringstream ss;
58 : 29 : auto it = sexpr.begin();
59 : :
60 : : // recursively print the sub-sexprs
61 : 29 : ss << '(' << sexprToString(*it);
62 : 29 : ++it;
63 [ + + ]: 85 : while (it != sexpr.end())
64 : : {
65 : 56 : ss << ' ' << sexprToString(*it);
66 : 56 : ++it;
67 : : }
68 : 29 : ss << ')';
69 : :
70 : 29 : return ss.str();
71 : 29 : }
72 : :
73 : : /* -------------------------------------------------------------------------- */
74 : : /* Cmd */
75 : : /* -------------------------------------------------------------------------- */
76 : :
77 : 692587 : Cmd::Cmd() : d_commandStatus(nullptr) {}
78 : :
79 : 0 : Cmd::Cmd(const Cmd& cmd)
80 : : {
81 : 0 : d_commandStatus = (cmd.d_commandStatus == nullptr)
82 [ - - ]: 0 : ? nullptr
83 : 0 : : &cmd.d_commandStatus->clone();
84 : 0 : }
85 : :
86 : 692587 : Cmd::~Cmd()
87 : : {
88 : 1385174 : if (d_commandStatus != nullptr
89 [ + + ][ + + ]: 692587 : && d_commandStatus != CommandSuccess::instance())
[ + + ]
90 : : {
91 [ + - ]: 129 : delete d_commandStatus;
92 : : }
93 : 692587 : }
94 : :
95 : 1152426 : bool Cmd::ok() const
96 : : {
97 : : // either we haven't run the command yet, or it ran successfully
98 : 1152426 : return d_commandStatus == nullptr
99 [ + + ][ + - ]: 1152426 : || dynamic_cast<const CommandSuccess*>(d_commandStatus) != nullptr;
[ + + ]
100 : : }
101 : :
102 : 588939 : bool Cmd::fail() const
103 : : {
104 : 588939 : return d_commandStatus != nullptr
105 [ + + ][ + - ]: 588939 : && dynamic_cast<const CommandFailure*>(d_commandStatus) != nullptr;
[ + + ]
106 : : }
107 : :
108 : 90 : bool Cmd::interrupted() const
109 : : {
110 : 90 : return d_commandStatus != nullptr
111 [ + - ][ + - ]: 90 : && dynamic_cast<const CommandInterrupted*>(d_commandStatus) != nullptr;
[ - + ]
112 : : }
113 : :
114 : 733 : void Cmd::invoke(cvc5::Solver* solver,
115 : : parser::SymManager* sm,
116 : : std::ostream& out)
117 : : {
118 : 733 : invoke(solver, sm);
119 [ + + ]: 733 : if (!ok())
120 : : {
121 : 10 : out << *d_commandStatus;
122 : : }
123 : : else
124 : : {
125 : 723 : printResult(solver, out);
126 : : }
127 : : // always flush the output
128 : 733 : out << std::flush;
129 : 733 : }
130 : :
131 : 588941 : void Cmd::invokeAndPrintResult(cvc5::Solver* solver, parser::SymManager* sm)
132 : : {
133 : 588941 : invoke(solver, sm);
134 : : // the output stream reference is retrieved here since it might change after
135 : : // invoking a (set-option :out ...) command
136 : 588939 : std::ostream& out = solver->getDriverOptions().out();
137 [ + + ]: 588939 : if (!ok())
138 : : {
139 : 119 : out << *d_commandStatus;
140 : : }
141 : : else
142 : : {
143 : 588820 : printResult(solver, out);
144 : : }
145 : : // always flush the output
146 : 588939 : out << std::flush;
147 : 588939 : }
148 : :
149 : 140495 : std::string Cmd::toString() const
150 : : {
151 : 140495 : std::stringstream ss;
152 : 140495 : toStream(ss);
153 : 280990 : return ss.str();
154 : 140495 : }
155 : :
156 : 562754 : void Cmd::printResult(cvc5::Solver* solver, std::ostream& out) const
157 : : {
158 : 1688262 : if (!ok()
159 [ + - ][ + + ]: 1125348 : || (d_commandStatus != nullptr
160 : 1125348 : && solver->getOption("print-success") == "true"))
161 : : {
162 : 23 : out << *d_commandStatus;
163 : : }
164 : 562754 : }
165 : :
166 : 83 : void Cmd::resetSolver(cvc5::Solver* solver)
167 : : {
168 : : // Note that this command does not own the solver object, and other objects
169 : : // (e.g. the InputParser) hold a pointer to it, so the solver has to be reset
170 : : // in place rather than replaced.
171 : 83 : solver->resetInternal();
172 : 83 : }
173 : :
174 : 39892 : internal::Node Cmd::termToNode(const cvc5::Term& term)
175 : : {
176 : 39892 : return term.getNode();
177 : : }
178 : :
179 : 2917 : std::vector<internal::Node> Cmd::termVectorToNodes(
180 : : const std::vector<cvc5::Term>& terms)
181 : : {
182 : 2917 : return cvc5::Term::termVectorToNodes(terms);
183 : : }
184 : :
185 : 82436 : internal::TypeNode Cmd::sortToTypeNode(const cvc5::Sort& sort)
186 : : {
187 : 82436 : return sort.getTypeNode();
188 : : }
189 : :
190 : 80703 : std::vector<internal::TypeNode> Cmd::sortVectorToTypeNodes(
191 : : const std::vector<cvc5::Sort>& sorts)
192 : : {
193 : 80703 : return cvc5::Sort::sortVectorToTypeNodes(sorts);
194 : : }
195 : :
196 : 247 : internal::TypeNode Cmd::grammarToTypeNode(cvc5::Grammar* grammar)
197 : : {
198 : : return grammar == nullptr ? internal::TypeNode::null()
199 [ + + ][ + + ]: 494 : : sortToTypeNode(grammar->resolve());
[ - - ]
200 : : }
201 : :
202 : 0 : std::ostream& operator<<(std::ostream& out, const Cmd& c)
203 : : {
204 : 0 : out << c.toString();
205 : 0 : return out;
206 : : }
207 : :
208 : 0 : std::ostream& operator<<(std::ostream& out, const Cmd* c)
209 : : {
210 [ - - ]: 0 : if (c == nullptr)
211 : : {
212 : 0 : out << "null";
213 : : }
214 : : else
215 : : {
216 : 0 : out << *c;
217 : : }
218 : 0 : return out;
219 : : }
220 : :
221 : : /* -------------------------------------------------------------------------- */
222 : : /* class EmptyCommand */
223 : : /* -------------------------------------------------------------------------- */
224 : :
225 : 26 : EmptyCommand::EmptyCommand(std::string name) : d_name(name) {}
226 : 0 : std::string EmptyCommand::getName() const { return d_name; }
227 : 17 : void EmptyCommand::invoke(CVC5_UNUSED cvc5::Solver* solver,
228 : : CVC5_UNUSED SymManager* sm)
229 : : {
230 : : /* empty commands have no implementation */
231 : 17 : d_commandStatus = CommandSuccess::instance();
232 : 17 : }
233 : :
234 : 0 : std::string EmptyCommand::getCommandName() const { return "empty"; }
235 : :
236 : 9 : void EmptyCommand::toStream(std::ostream& out) const
237 : : {
238 : 9 : internal::Printer::getPrinter(out)->toStreamCmdEmpty(out, d_name);
239 : 9 : }
240 : :
241 : : /* -------------------------------------------------------------------------- */
242 : : /* class EchoCommand */
243 : : /* -------------------------------------------------------------------------- */
244 : :
245 : 28 : EchoCommand::EchoCommand(std::string output) : d_output(output) {}
246 : :
247 : 0 : std::string EchoCommand::getOutput() const { return d_output; }
248 : :
249 : 10 : void EchoCommand::invoke(CVC5_UNUSED cvc5::Solver* solver,
250 : : CVC5_UNUSED SymManager* sm)
251 : : {
252 : 10 : d_commandStatus = CommandSuccess::instance();
253 : 10 : }
254 : :
255 : 10 : void EchoCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
256 : : std::ostream& out) const
257 : : {
258 [ + - ]: 20 : Trace("dtview::command") << "* ~COMMAND: echo |" << d_output << "|~"
259 : 10 : << std::endl;
260 : 10 : out << cvc5::internal::quoteString(d_output) << std::endl;
261 : 10 : }
262 : :
263 : 0 : std::string EchoCommand::getCommandName() const { return "echo"; }
264 : :
265 : 9 : void EchoCommand::toStream(std::ostream& out) const
266 : : {
267 : 9 : internal::Printer::getPrinter(out)->toStreamCmdEcho(out, d_output);
268 : 9 : }
269 : :
270 : : /* -------------------------------------------------------------------------- */
271 : : /* class AssertCommand */
272 : : /* -------------------------------------------------------------------------- */
273 : :
274 : 212261 : AssertCommand::AssertCommand(const cvc5::Term& t) : d_term(t) {}
275 : :
276 : 0 : cvc5::Term AssertCommand::getTerm() const { return d_term; }
277 : 136863 : void AssertCommand::invoke(cvc5::Solver* solver, CVC5_UNUSED SymManager* sm)
278 : : {
279 : : try
280 : : {
281 : 136863 : solver->assertFormula(d_term);
282 : 136861 : d_commandStatus = CommandSuccess::instance();
283 : : }
284 [ - + ]: 2 : catch (exception& e)
285 : : {
286 : 2 : d_commandStatus = new CommandFailure(e.what());
287 : 2 : }
288 : 136863 : }
289 : :
290 : 0 : std::string AssertCommand::getCommandName() const { return "assert"; }
291 : :
292 : 37705 : void AssertCommand::toStream(std::ostream& out) const
293 : : {
294 : 75410 : internal::Printer::getPrinter(out)->toStreamCmdAssert(out,
295 : 75410 : termToNode(d_term));
296 : 37705 : }
297 : :
298 : : /* -------------------------------------------------------------------------- */
299 : : /* class PushCommand */
300 : : /* -------------------------------------------------------------------------- */
301 : :
302 : 5689 : PushCommand::PushCommand(uint32_t nscopes) : d_nscopes(nscopes) {}
303 : :
304 : 3623 : void PushCommand::invoke(cvc5::Solver* solver, CVC5_UNUSED SymManager* sm)
305 : : {
306 : : try
307 : : {
308 : 3623 : solver->push(d_nscopes);
309 : 3623 : d_commandStatus = CommandSuccess::instance();
310 : : }
311 [ - - ]: 0 : catch (exception& e)
312 : : {
313 : 0 : d_commandStatus = new CommandFailure(e.what());
314 : 0 : }
315 : 3623 : }
316 : :
317 : 0 : std::string PushCommand::getCommandName() const { return "push"; }
318 : :
319 : 1033 : void PushCommand::toStream(std::ostream& out) const
320 : : {
321 : 1033 : internal::Printer::getPrinter(out)->toStreamCmdPush(out, d_nscopes);
322 : 1033 : }
323 : :
324 : : /* -------------------------------------------------------------------------- */
325 : : /* class PopCommand */
326 : : /* -------------------------------------------------------------------------- */
327 : :
328 : 4564 : PopCommand::PopCommand(uint32_t nscopes) : d_nscopes(nscopes) {}
329 : :
330 : 2922 : void PopCommand::invoke(cvc5::Solver* solver, CVC5_UNUSED SymManager* sm)
331 : : {
332 : : try
333 : : {
334 : 2922 : solver->pop(d_nscopes);
335 : 2922 : d_commandStatus = CommandSuccess::instance();
336 : : }
337 [ - - ]: 0 : catch (exception& e)
338 : : {
339 : 0 : d_commandStatus = new CommandFailure(e.what());
340 : 0 : }
341 : 2922 : }
342 : :
343 : 0 : std::string PopCommand::getCommandName() const { return "pop"; }
344 : :
345 : 821 : void PopCommand::toStream(std::ostream& out) const
346 : : {
347 : 821 : internal::Printer::getPrinter(out)->toStreamCmdPop(out, d_nscopes);
348 : 821 : }
349 : :
350 : : /* -------------------------------------------------------------------------- */
351 : : /* class CheckSatCommand */
352 : : /* -------------------------------------------------------------------------- */
353 : :
354 : 27221 : CheckSatCommand::CheckSatCommand() {}
355 : :
356 : 17662 : void CheckSatCommand::invoke(cvc5::Solver* solver, CVC5_UNUSED SymManager* sm)
357 : : {
358 [ + - ][ - + ]: 35324 : Trace("dtview::command") << "* ~COMMAND: " << getCommandName() << "~"
[ - - ]
359 : 17662 : << std::endl;
360 : : try
361 : : {
362 : 17662 : d_result = solver->checkSat();
363 : 17619 : d_commandStatus = CommandSuccess::instance();
364 : : }
365 [ - + ]: 43 : catch (exception& e)
366 : : {
367 : 43 : d_commandStatus = new CommandFailure(e.what());
368 : 43 : }
369 : 17662 : }
370 : :
371 : 27214 : cvc5::Result CheckSatCommand::getResult() const { return d_result; }
372 : :
373 : 17619 : void CheckSatCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
374 : : std::ostream& out) const
375 : : {
376 : 17619 : out << d_result << endl;
377 : 17619 : }
378 : :
379 : 0 : std::string CheckSatCommand::getCommandName() const { return "check-sat"; }
380 : :
381 : 4780 : void CheckSatCommand::toStream(std::ostream& out) const
382 : : {
383 : 4780 : internal::Printer::getPrinter(out)->toStreamCmdCheckSat(out);
384 : 4780 : }
385 : :
386 : : /* -------------------------------------------------------------------------- */
387 : : /* class CheckSatAssumingCommand */
388 : : /* -------------------------------------------------------------------------- */
389 : :
390 : 0 : CheckSatAssumingCommand::CheckSatAssumingCommand(cvc5::Term term)
391 : 0 : : d_terms({term})
392 : : {
393 : 0 : }
394 : :
395 : 4188 : CheckSatAssumingCommand::CheckSatAssumingCommand(
396 : 4188 : const std::vector<cvc5::Term>& terms)
397 : 4188 : : d_terms(terms)
398 : : {
399 : 4188 : }
400 : :
401 : 0 : const std::vector<cvc5::Term>& CheckSatAssumingCommand::getTerms() const
402 : : {
403 : 0 : return d_terms;
404 : : }
405 : :
406 : 2828 : void CheckSatAssumingCommand::invoke(cvc5::Solver* solver,
407 : : CVC5_UNUSED SymManager* sm)
408 : : {
409 [ + - ]: 5656 : Trace("dtview::command") << "* ~COMMAND: (check-sat-assuming ( " << d_terms
410 : 2828 : << " )~" << std::endl;
411 : : try
412 : : {
413 : 2828 : d_result = solver->checkSatAssuming(d_terms);
414 : 2823 : d_commandStatus = CommandSuccess::instance();
415 : : }
416 [ - + ]: 5 : catch (exception& e)
417 : : {
418 : 5 : d_commandStatus = new CommandFailure(e.what());
419 : 5 : }
420 : 2828 : }
421 : :
422 : 4188 : cvc5::Result CheckSatAssumingCommand::getResult() const
423 : : {
424 [ + - ]: 4188 : Trace("dtview::command") << "* ~RESULT: " << d_result << "~" << std::endl;
425 : 4188 : return d_result;
426 : : }
427 : :
428 : 2823 : void CheckSatAssumingCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
429 : : std::ostream& out) const
430 : : {
431 : 2823 : out << d_result << endl;
432 : 2823 : }
433 : :
434 : 0 : std::string CheckSatAssumingCommand::getCommandName() const
435 : : {
436 : 0 : return "check-sat-assuming";
437 : : }
438 : :
439 : 683 : void CheckSatAssumingCommand::toStream(std::ostream& out) const
440 : : {
441 : 1366 : internal::Printer::getPrinter(out)->toStreamCmdCheckSatAssuming(
442 : 1366 : out, termVectorToNodes(d_terms));
443 : 683 : }
444 : :
445 : : /* -------------------------------------------------------------------------- */
446 : : /* class DeclareSygusVarCommand */
447 : : /* -------------------------------------------------------------------------- */
448 : :
449 : 1433 : DeclareSygusVarCommand::DeclareSygusVarCommand(const std::string& id,
450 : 1433 : cvc5::Sort sort)
451 : 1433 : : DeclarationDefinitionCommand(id), d_sort(sort)
452 : : {
453 : 1433 : }
454 : :
455 : 0 : cvc5::Sort DeclareSygusVarCommand::getSort() const { return d_sort; }
456 : :
457 : 1433 : void DeclareSygusVarCommand::invoke(cvc5::Solver* solver, SymManager* sm)
458 : : {
459 : 1433 : Term var = solver->declareSygusVar(d_symbol, d_sort);
460 [ - + ]: 1433 : if (!bindToTerm(sm, var, true))
461 : : {
462 : 0 : return;
463 : : }
464 : 1433 : d_commandStatus = CommandSuccess::instance();
465 [ + - ]: 1433 : }
466 : :
467 : 0 : std::string DeclareSygusVarCommand::getCommandName() const
468 : : {
469 : 0 : return "declare-var";
470 : : }
471 : :
472 : 358 : void DeclareSygusVarCommand::toStream(std::ostream& out) const
473 : : {
474 : 358 : internal::Printer::getPrinter(out)->toStreamCmdDeclareVar(
475 : 358 : out, d_symbol, sortToTypeNode(d_sort));
476 : 358 : }
477 : :
478 : : /* -------------------------------------------------------------------------- */
479 : : /* class SynthFunCommand */
480 : : /* -------------------------------------------------------------------------- */
481 : :
482 : 1599 : SynthFunCommand::SynthFunCommand(const std::string& id,
483 : : const std::vector<cvc5::Term>& vars,
484 : : cvc5::Sort sort,
485 : 1599 : cvc5::Grammar* g)
486 : 1599 : : DeclarationDefinitionCommand(id), d_vars(vars), d_sort(sort), d_grammar(g)
487 : : {
488 : 1599 : }
489 : :
490 : 0 : const std::vector<cvc5::Term>& SynthFunCommand::getVars() const
491 : : {
492 : 0 : return d_vars;
493 : : }
494 : :
495 : 0 : cvc5::Sort SynthFunCommand::getSort() const { return d_sort; }
496 : :
497 : 0 : const cvc5::Grammar* SynthFunCommand::getGrammar() const { return d_grammar; }
498 : :
499 : 1599 : void SynthFunCommand::invoke(cvc5::Solver* solver, SymManager* sm)
500 : : {
501 : 1599 : Term fun;
502 [ + + ]: 1599 : if (d_grammar != nullptr)
503 : : {
504 : 754 : fun = solver->synthFun(d_symbol, d_vars, d_sort, *d_grammar);
505 : : }
506 : : else
507 : : {
508 : 847 : fun = solver->synthFun(d_symbol, d_vars, d_sort);
509 : : }
510 [ - + ]: 1597 : if (!bindToTerm(sm, fun, true))
511 : : {
512 : 0 : return;
513 : : }
514 : 1597 : sm->addFunctionToSynthesize(fun);
515 : 1597 : d_commandStatus = CommandSuccess::instance();
516 [ + - ]: 1599 : }
517 : :
518 : 0 : std::string SynthFunCommand::getCommandName() const { return "synth-fun"; }
519 : :
520 : 400 : void SynthFunCommand::toStream(std::ostream& out) const
521 : : {
522 : 400 : std::vector<internal::Node> nodeVars = termVectorToNodes(d_vars);
523 : 400 : internal::Printer::getPrinter(out)->toStreamCmdSynthFun(
524 : : out,
525 : 400 : d_symbol,
526 : : nodeVars,
527 : 800 : sortToTypeNode(d_sort),
528 [ + + ]: 800 : d_grammar == nullptr ? internal::TypeNode::null()
529 : 189 : : grammarToTypeNode(d_grammar));
530 : 400 : }
531 : :
532 : : /* -------------------------------------------------------------------------- */
533 : : /* class SygusConstraintCommand */
534 : : /* -------------------------------------------------------------------------- */
535 : :
536 : 2788 : SygusConstraintCommand::SygusConstraintCommand(const cvc5::Term& t,
537 : 2788 : bool isAssume)
538 : 2788 : : d_term(t), d_isAssume(isAssume)
539 : : {
540 : 2788 : }
541 : :
542 : 1392 : void SygusConstraintCommand::invoke(cvc5::Solver* solver,
543 : : CVC5_UNUSED SymManager* sm)
544 : : {
545 : : try
546 : : {
547 [ + + ]: 1392 : if (d_isAssume)
548 : : {
549 : 8 : solver->addSygusAssume(d_term);
550 : : }
551 : : else
552 : : {
553 : 1384 : solver->addSygusConstraint(d_term);
554 : : }
555 : 1392 : d_commandStatus = CommandSuccess::instance();
556 : : }
557 [ - - ]: 0 : catch (exception& e)
558 : : {
559 : 0 : d_commandStatus = new CommandFailure(e.what());
560 : 0 : }
561 : 1392 : }
562 : :
563 : 0 : cvc5::Term SygusConstraintCommand::getTerm() const { return d_term; }
564 : :
565 : 0 : std::string SygusConstraintCommand::getCommandName() const
566 : : {
567 [ - - ]: 0 : return d_isAssume ? "assume" : "constraint";
568 : : }
569 : :
570 : 698 : void SygusConstraintCommand::toStream(std::ostream& out) const
571 : : {
572 [ + + ]: 698 : if (d_isAssume)
573 : : {
574 : 8 : internal::Printer::getPrinter(out)->toStreamCmdAssume(out,
575 : 8 : termToNode(d_term));
576 : : }
577 : : else
578 : : {
579 : 1388 : internal::Printer::getPrinter(out)->toStreamCmdConstraint(
580 : 1388 : out, termToNode(d_term));
581 : : }
582 : 698 : }
583 : :
584 : : /* -------------------------------------------------------------------------- */
585 : : /* class SygusInvConstraintCommand */
586 : : /* -------------------------------------------------------------------------- */
587 : :
588 : 53 : SygusInvConstraintCommand::SygusInvConstraintCommand(
589 : 53 : const std::vector<cvc5::Term>& predicates)
590 : 53 : : d_predicates(predicates)
591 : : {
592 : 53 : }
593 : :
594 : 0 : SygusInvConstraintCommand::SygusInvConstraintCommand(const cvc5::Term& inv,
595 : : const cvc5::Term& pre,
596 : : const cvc5::Term& trans,
597 : 0 : const cvc5::Term& post)
598 : 0 : : SygusInvConstraintCommand(std::vector<cvc5::Term>{inv, pre, trans, post})
599 : : {
600 : 0 : }
601 : :
602 : 27 : void SygusInvConstraintCommand::invoke(cvc5::Solver* solver,
603 : : CVC5_UNUSED SymManager* sm)
604 : : {
605 : : try
606 : : {
607 : 27 : solver->addSygusInvConstraint(
608 : 27 : d_predicates[0], d_predicates[1], d_predicates[2], d_predicates[3]);
609 : 27 : d_commandStatus = CommandSuccess::instance();
610 : : }
611 [ - - ]: 0 : catch (exception& e)
612 : : {
613 : 0 : d_commandStatus = new CommandFailure(e.what());
614 : 0 : }
615 : 27 : }
616 : :
617 : 0 : const std::vector<cvc5::Term>& SygusInvConstraintCommand::getPredicates() const
618 : : {
619 : 0 : return d_predicates;
620 : : }
621 : :
622 : 0 : std::string SygusInvConstraintCommand::getCommandName() const
623 : : {
624 : 0 : return "inv-constraint";
625 : : }
626 : :
627 : 13 : void SygusInvConstraintCommand::toStream(std::ostream& out) const
628 : : {
629 : 26 : internal::Printer::getPrinter(out)->toStreamCmdInvConstraint(
630 : : out,
631 : 26 : termToNode(d_predicates[0]),
632 : 26 : termToNode(d_predicates[1]),
633 : 26 : termToNode(d_predicates[2]),
634 : 26 : termToNode(d_predicates[3]));
635 : 13 : }
636 : :
637 : : /* -------------------------------------------------------------------------- */
638 : : /* class CheckSynthCommand */
639 : : /* -------------------------------------------------------------------------- */
640 : :
641 : 472 : void CheckSynthCommand::invoke(cvc5::Solver* solver, SymManager* sm)
642 : : {
643 : : try
644 : : {
645 [ + + ]: 472 : d_result = d_isNext ? solver->checkSynthNext() : solver->checkSynth();
646 : 466 : d_commandStatus = CommandSuccess::instance();
647 : 466 : d_solution.clear();
648 : : // check whether we should print the status
649 : 932 : std::string sygusOut = solver->getOption("sygus-out");
650 [ + - ]: 903 : if (!d_result.hasSolution() || sygusOut == "status-and-def"
651 [ + + ][ + + ]: 903 : || sygusOut == "status")
[ + + ]
652 : : {
653 [ + + ]: 446 : if (d_result.hasSolution())
654 : : {
655 : 417 : d_solution << "feasible" << std::endl;
656 : : }
657 [ + + ]: 29 : else if (d_result.hasNoSolution())
658 : : {
659 : 20 : d_solution << "infeasible" << std::endl;
660 : : }
661 : : else
662 : : {
663 : 9 : d_solution << "fail" << std::endl;
664 : : }
665 : : }
666 : : // check whether we should print the solution
667 [ + + ][ + + ]: 466 : if (d_result.hasSolution() && sygusOut != "status")
[ + + ]
668 : : {
669 : 20 : std::vector<cvc5::Term> synthFuns = sm->getFunctionsToSynthesize();
670 : 20 : d_solution << "(" << std::endl;
671 : 20 : internal::options::ioutils::Scope scope(d_solution);
672 : 20 : internal::options::ioutils::applyOutputLanguage(
673 : : d_solution, internal::Language::LANG_SYGUS_V2);
674 : 20 : internal::Printer* p = internal::Printer::getPrinter(d_solution);
675 [ + + ]: 42 : for (cvc5::Term& f : synthFuns)
676 : : {
677 : 22 : cvc5::Term sol = solver->getSynthSolution(f);
678 : 22 : std::vector<cvc5::Term> formals;
679 [ + + ]: 22 : if (sol.getKind() == cvc5::Kind::LAMBDA)
680 : : {
681 : 18 : formals.insert(formals.end(), sol[0].begin(), sol[0].end());
682 : 18 : sol = sol[1];
683 : : }
684 : 22 : cvc5::Sort rangeSort = f.getSort();
685 [ + + ]: 22 : if (rangeSort.isFunction())
686 : : {
687 : 18 : rangeSort = rangeSort.getFunctionCodomainSort();
688 : : }
689 : 22 : p->toStreamCmdDefineFunction(d_solution,
690 : 44 : f.toString(),
691 : 44 : termVectorToNodes(formals),
692 : 44 : sortToTypeNode(rangeSort),
693 : 44 : termToNode(sol));
694 : 22 : d_solution << std::endl;
695 : 22 : }
696 : 20 : d_solution << ")" << std::endl;
697 : 20 : }
698 : 466 : }
699 [ - + ]: 6 : catch (exception& e)
700 : : {
701 : 6 : d_commandStatus = new CommandFailure(e.what());
702 : 6 : }
703 : 472 : }
704 : :
705 : 0 : cvc5::SynthResult CheckSynthCommand::getResult() const { return d_result; }
706 : 466 : void CheckSynthCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
707 : : std::ostream& out) const
708 : : {
709 : 466 : out << d_solution.str();
710 : 466 : }
711 : :
712 : 0 : std::string CheckSynthCommand::getCommandName() const
713 : : {
714 [ - - ]: 0 : return d_isNext ? "check-synth-next" : "check-synth";
715 : : }
716 : :
717 : 236 : void CheckSynthCommand::toStream(std::ostream& out) const
718 : : {
719 [ + + ]: 236 : if (d_isNext)
720 : : {
721 : 6 : internal::Printer::getPrinter(out)->toStreamCmdCheckSynthNext(out);
722 : : }
723 : : else
724 : : {
725 : 230 : internal::Printer::getPrinter(out)->toStreamCmdCheckSynth(out);
726 : : }
727 : 236 : }
728 : :
729 : : /* -------------------------------------------------------------------------- */
730 : : /* class FindSynthCommand */
731 : : /* -------------------------------------------------------------------------- */
732 : :
733 : 41 : void FindSynthCommand::invoke(cvc5::Solver* solver, CVC5_UNUSED SymManager* sm)
734 : : {
735 : : try
736 : : {
737 [ + + ]: 41 : if (d_grammar != nullptr)
738 : : {
739 : 1 : d_result = solver->findSynth(d_fst, *d_grammar);
740 : : }
741 : : else
742 : : {
743 : 40 : d_result = solver->findSynth(d_fst);
744 : : }
745 : : }
746 [ - + ]: 7 : catch (exception& e)
747 : : {
748 : 7 : d_commandStatus = new CommandFailure(e.what());
749 : 7 : }
750 : 41 : }
751 : :
752 : 0 : Term FindSynthCommand::getResult() const { return d_result; }
753 : 34 : void FindSynthCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
754 : : std::ostream& out) const
755 : : {
756 [ + + ]: 34 : if (d_result.isNull())
757 : : {
758 : 31 : out << "fail" << std::endl;
759 : : }
760 : : else
761 : : {
762 : 3 : out << d_result << std::endl;
763 : : }
764 : 34 : }
765 : :
766 : 0 : std::string FindSynthCommand::getCommandName() const { return "find-synth"; }
767 : :
768 : 26 : void FindSynthCommand::toStream(std::ostream& out) const
769 : : {
770 : 26 : internal::Printer::getPrinter(out)->toStreamCmdFindSynth(
771 : : out,
772 : 26 : d_fst,
773 [ + + ]: 52 : d_grammar == nullptr ? internal::TypeNode::null()
774 : 1 : : grammarToTypeNode(d_grammar));
775 : 26 : }
776 : :
777 : : /* -------------------------------------------------------------------------- */
778 : : /* class FindSynthNextCommand */
779 : : /* -------------------------------------------------------------------------- */
780 : :
781 : 0 : cvc5::Term FindSynthNextCommand::getResult() const { return d_result; }
782 : :
783 : 1 : void FindSynthNextCommand::invoke(cvc5::Solver* solver,
784 : : CVC5_UNUSED SymManager* sm)
785 : : {
786 : : try
787 : : {
788 : : // Get the name of the abduct from the symbol manager
789 : 1 : d_result = solver->findSynthNext();
790 : 1 : d_commandStatus = CommandSuccess::instance();
791 : : }
792 [ - - ]: 0 : catch (exception& e)
793 : : {
794 : 0 : d_commandStatus = new CommandFailure(e.what());
795 : 0 : }
796 : 1 : }
797 : :
798 : 1 : void FindSynthNextCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
799 : : std::ostream& out) const
800 : : {
801 [ - + ]: 1 : if (d_result.isNull())
802 : : {
803 : 0 : out << "fail" << std::endl;
804 : : }
805 : : else
806 : : {
807 : 1 : out << d_result << std::endl;
808 : : }
809 : 1 : }
810 : :
811 : 0 : std::string FindSynthNextCommand::getCommandName() const
812 : : {
813 : 0 : return "find-synth-next";
814 : : }
815 : :
816 : 1 : void FindSynthNextCommand::toStream(std::ostream& out) const
817 : : {
818 : 1 : internal::Printer::getPrinter(out)->toStreamCmdFindSynthNext(out);
819 : 1 : }
820 : :
821 : : /* -------------------------------------------------------------------------- */
822 : : /* class ResetCommand */
823 : : /* -------------------------------------------------------------------------- */
824 : :
825 : 83 : void ResetCommand::invoke(cvc5::Solver* solver, SymManager* sm)
826 : : {
827 : : try
828 : : {
829 : 83 : sm->reset();
830 : 83 : resetSolver(solver);
831 : 83 : d_commandStatus = CommandSuccess::instance();
832 : : }
833 [ - - ]: 0 : catch (exception& e)
834 : : {
835 : 0 : d_commandStatus = new CommandFailure(e.what());
836 : 0 : }
837 : 83 : }
838 : :
839 : 0 : std::string ResetCommand::getCommandName() const { return "reset"; }
840 : :
841 : 17 : void ResetCommand::toStream(std::ostream& out) const
842 : : {
843 : 17 : internal::Printer::getPrinter(out)->toStreamCmdReset(out);
844 : 17 : }
845 : :
846 : : /* -------------------------------------------------------------------------- */
847 : : /* class ResetAssertionsCommand */
848 : : /* -------------------------------------------------------------------------- */
849 : :
850 : 38 : void ResetAssertionsCommand::invoke(cvc5::Solver* solver, SymManager* sm)
851 : : {
852 : : try
853 : : {
854 : 38 : sm->resetAssertions();
855 : 38 : solver->resetAssertions();
856 : 38 : d_commandStatus = CommandSuccess::instance();
857 : : }
858 [ - - ]: 0 : catch (exception& e)
859 : : {
860 : 0 : d_commandStatus = new CommandFailure(e.what());
861 : 0 : }
862 : 38 : }
863 : :
864 : 0 : std::string ResetAssertionsCommand::getCommandName() const
865 : : {
866 : 0 : return "reset-assertions";
867 : : }
868 : :
869 : 14 : void ResetAssertionsCommand::toStream(std::ostream& out) const
870 : : {
871 : 14 : internal::Printer::getPrinter(out)->toStreamCmdResetAssertions(out);
872 : 14 : }
873 : :
874 : : /* -------------------------------------------------------------------------- */
875 : : /* class QuitCommand */
876 : : /* -------------------------------------------------------------------------- */
877 : :
878 : 2116 : void QuitCommand::invoke(CVC5_UNUSED cvc5::Solver* solver,
879 : : CVC5_UNUSED SymManager* sm)
880 : : {
881 : 2116 : d_commandStatus = CommandSuccess::instance();
882 : 2116 : }
883 : :
884 : 0 : std::string QuitCommand::getCommandName() const { return "exit"; }
885 : :
886 : 466 : void QuitCommand::toStream(std::ostream& out) const
887 : : {
888 : 466 : internal::Printer::getPrinter(out)->toStreamCmdQuit(out);
889 : 466 : }
890 : :
891 : : /* -------------------------------------------------------------------------- */
892 : : /* class DeclarationDefinitionCommand */
893 : : /* -------------------------------------------------------------------------- */
894 : :
895 : 368333 : DeclarationDefinitionCommand::DeclarationDefinitionCommand(
896 : 368333 : const std::string& id)
897 : 368333 : : d_symbol(id)
898 : : {
899 : 368333 : }
900 : :
901 : 0 : std::string DeclarationDefinitionCommand::getSymbol() const { return d_symbol; }
902 : :
903 : 356663 : bool tryBindToTerm(SymManager* sm,
904 : : const std::string& sym,
905 : : Term t,
906 : : bool doOverload,
907 : : std::ostream* out = nullptr)
908 : : {
909 [ + + ]: 356663 : if (!sm->bind(sym, t, doOverload))
910 : : {
911 [ + + ]: 4 : if (out)
912 : : {
913 : 2 : (*out) << "Cannot bind " << sym << " to symbol of type " << t.getSort();
914 : 2 : (*out) << ", maybe the symbol has already been defined?";
915 : : }
916 : 4 : return false;
917 : : }
918 : 356659 : return true;
919 : : }
920 : :
921 : 355895 : bool DeclarationDefinitionCommand::bindToTerm(SymManager* sm,
922 : : Term t,
923 : : bool doOverload)
924 : : {
925 [ + + ]: 355895 : if (!tryBindToTerm(sm, d_symbol, t, doOverload))
926 : : {
927 : 2 : std::stringstream ss;
928 : 2 : tryBindToTerm(sm, d_symbol, t, doOverload, &ss);
929 : 2 : d_commandStatus = new CommandFailure(ss.str());
930 : 2 : return false;
931 : 2 : }
932 : 355893 : return true;
933 : : }
934 : :
935 : : /* -------------------------------------------------------------------------- */
936 : : /* class DeclareFunctionCommand */
937 : : /* -------------------------------------------------------------------------- */
938 : :
939 : 345429 : DeclareFunctionCommand::DeclareFunctionCommand(
940 : 345429 : const std::string& id, const std::vector<Sort>& argSorts, cvc5::Sort sort)
941 : 345429 : : DeclarationDefinitionCommand(id), d_argSorts(argSorts), d_sort(sort)
942 : : {
943 : 345429 : }
944 : 0 : std::vector<Sort> DeclareFunctionCommand::getArgSorts() const
945 : : {
946 : 0 : return d_argSorts;
947 : : }
948 : 0 : cvc5::Sort DeclareFunctionCommand::getSort() const { return d_sort; }
949 : :
950 : 345429 : void DeclareFunctionCommand::invoke(cvc5::Solver* solver, SymManager* sm)
951 : : {
952 : : // determine if this will be a fresh declaration
953 : 345429 : bool fresh = sm->getFreshDeclarations();
954 : 345429 : Term fun = solver->declareFun(d_symbol, d_argSorts, d_sort, fresh);
955 [ + + ]: 345429 : if (!bindToTerm(sm, fun, true))
956 : : {
957 : 2 : return;
958 : : }
959 : : // mark that it will be printed in the model
960 : 345427 : sm->addModelDeclarationTerm(fun);
961 : 345427 : d_commandStatus = CommandSuccess::instance();
962 [ + + ]: 345429 : }
963 : :
964 : 0 : std::string DeclareFunctionCommand::getCommandName() const
965 : : {
966 : 0 : return "declare-fun";
967 : : }
968 : :
969 : 79885 : void DeclareFunctionCommand::toStream(std::ostream& out) const
970 : : {
971 : : // Note we use the symbol of the function here. This makes a difference
972 : : // in the rare case we are binding a symbol in the parser to a variable
973 : : // whose name is different. For example, when converting TPTP to smt2,
974 : : // we require a namespace prefix. Using the function symbol name ensures
975 : : // that e.g. `-o raw-benchmark` results in a valid benchmark.
976 : 79885 : internal::Printer::getPrinter(out)->toStreamCmdDeclareFunction(
977 : 79885 : out, d_symbol, sortVectorToTypeNodes(d_argSorts), sortToTypeNode(d_sort));
978 : 79885 : }
979 : :
980 : : /* -------------------------------------------------------------------------- */
981 : : /* class DeclarePoolCommand */
982 : : /* -------------------------------------------------------------------------- */
983 : :
984 : 29 : DeclarePoolCommand::DeclarePoolCommand(const std::string& id,
985 : : cvc5::Sort sort,
986 : 29 : const std::vector<cvc5::Term>& initValue)
987 : 29 : : DeclarationDefinitionCommand(id), d_sort(sort), d_initValue(initValue)
988 : : {
989 : 29 : }
990 : :
991 : 0 : cvc5::Sort DeclarePoolCommand::getSort() const { return d_sort; }
992 : 0 : const std::vector<cvc5::Term>& DeclarePoolCommand::getInitialValue() const
993 : : {
994 : 0 : return d_initValue;
995 : : }
996 : :
997 : 29 : void DeclarePoolCommand::invoke(cvc5::Solver* solver, SymManager* sm)
998 : : {
999 : 29 : Term pool = solver->declarePool(d_symbol, d_sort, d_initValue);
1000 [ - + ]: 29 : if (!bindToTerm(sm, pool, true))
1001 : : {
1002 : 0 : return;
1003 : : }
1004 : : // Notice that the pool is already declared by the parser so that it the
1005 : : // symbol is bound eagerly. This is analogous to DeclareSygusVarCommand.
1006 : : // Hence, we do nothing here.
1007 : 29 : d_commandStatus = CommandSuccess::instance();
1008 [ + - ]: 29 : }
1009 : :
1010 : 0 : std::string DeclarePoolCommand::getCommandName() const
1011 : : {
1012 : 0 : return "declare-pool";
1013 : : }
1014 : :
1015 : 4 : void DeclarePoolCommand::toStream(std::ostream& out) const
1016 : : {
1017 : 4 : internal::Printer::getPrinter(out)->toStreamCmdDeclarePool(
1018 : 4 : out, d_symbol, sortToTypeNode(d_sort), termVectorToNodes(d_initValue));
1019 : 4 : }
1020 : :
1021 : : /* -------------------------------------------------------------------------- */
1022 : : /* class DeclareOracleFunCommand */
1023 : : /* -------------------------------------------------------------------------- */
1024 : :
1025 : 0 : DeclareOracleFunCommand::DeclareOracleFunCommand(
1026 : 0 : const std::string& id, const std::vector<Sort>& argSorts, Sort sort)
1027 : 0 : : d_id(id), d_argSorts(argSorts), d_sort(sort), d_binName("")
1028 : : {
1029 : 0 : }
1030 : 0 : DeclareOracleFunCommand::DeclareOracleFunCommand(
1031 : : const std::string& id,
1032 : : const std::vector<Sort>& argSorts,
1033 : : Sort sort,
1034 : 0 : const std::string& binName)
1035 : 0 : : d_id(id), d_argSorts(argSorts), d_sort(sort), d_binName(binName)
1036 : : {
1037 : 0 : }
1038 : :
1039 : 0 : const std::string& DeclareOracleFunCommand::getIdentifier() const
1040 : : {
1041 : 0 : return d_id;
1042 : : }
1043 : :
1044 : 0 : Sort DeclareOracleFunCommand::getSort() const { return d_sort; }
1045 : :
1046 : 0 : const std::string& DeclareOracleFunCommand::getBinaryName() const
1047 : : {
1048 : 0 : return d_binName;
1049 : : }
1050 : :
1051 : 0 : void DeclareOracleFunCommand::invoke(CVC5_UNUSED Solver* solver,
1052 : : CVC5_UNUSED SymManager* sm)
1053 : : {
1054 : 0 : std::vector<Sort> args;
1055 : 0 : Sort ret;
1056 [ - - ]: 0 : if (d_sort.isFunction())
1057 : : {
1058 : 0 : args = d_sort.getFunctionDomainSorts();
1059 : 0 : ret = d_sort.getFunctionCodomainSort();
1060 : : }
1061 : : else
1062 : : {
1063 : 0 : ret = d_sort;
1064 : : }
1065 : : // will call solver declare oracle function when available in API
1066 : 0 : d_commandStatus = CommandSuccess::instance();
1067 : 0 : }
1068 : :
1069 : 0 : std::string DeclareOracleFunCommand::getCommandName() const
1070 : : {
1071 : 0 : return "declare-oracle-fun";
1072 : : }
1073 : :
1074 : 0 : void DeclareOracleFunCommand::toStream(std::ostream& out) const
1075 : : {
1076 : 0 : internal::Printer::getPrinter(out)->toStreamCmdDeclareOracleFun(
1077 : : out,
1078 : 0 : d_id,
1079 : 0 : sortVectorToTypeNodes(d_argSorts),
1080 : 0 : sortToTypeNode(d_sort),
1081 : 0 : d_binName);
1082 : 0 : }
1083 : :
1084 : : /* -------------------------------------------------------------------------- */
1085 : : /* class DeclareSortCommand */
1086 : : /* -------------------------------------------------------------------------- */
1087 : :
1088 : 11680 : DeclareSortCommand::DeclareSortCommand(const std::string& id, size_t arity)
1089 : 11680 : : DeclarationDefinitionCommand(id), d_arity(arity)
1090 : : {
1091 : 11680 : }
1092 : :
1093 : 0 : size_t DeclareSortCommand::getArity() const { return d_arity; }
1094 : 11680 : void DeclareSortCommand::invoke(cvc5::Solver* solver, SymManager* sm)
1095 : : {
1096 : : // determine if this will be a fresh declaration
1097 : 11680 : bool fresh = sm->getFreshDeclarations();
1098 : 11680 : Sort sort = solver->declareSort(d_symbol, d_arity, fresh);
1099 [ - + ]: 11680 : if (!sm->bindType(d_symbol, std::vector<Sort>(d_arity), sort, true))
1100 : : {
1101 : 0 : std::stringstream ss;
1102 : 0 : ss << "Cannot bind " << d_symbol
1103 : 0 : << " to sort, maybe it has already been defined?";
1104 : 0 : d_commandStatus = new CommandFailure(ss.str());
1105 : 0 : return;
1106 : 0 : }
1107 : : // mark that it will be printed in the model, if it is an uninterpreted
1108 : : // sort (arity 0)
1109 [ + + ]: 11680 : if (d_arity == 0)
1110 : : {
1111 : 11587 : sm->addModelDeclarationSort(sort);
1112 : : }
1113 : 11680 : d_commandStatus = CommandSuccess::instance();
1114 [ + - ]: 11680 : }
1115 : :
1116 : 0 : std::string DeclareSortCommand::getCommandName() const
1117 : : {
1118 : 0 : return "declare-sort";
1119 : : }
1120 : :
1121 : 1704 : void DeclareSortCommand::toStream(std::ostream& out) const
1122 : : {
1123 : 1704 : internal::Printer::getPrinter(out)->toStreamCmdDeclareType(
1124 : 1704 : out, d_symbol, d_arity);
1125 : 1704 : }
1126 : :
1127 : : /* -------------------------------------------------------------------------- */
1128 : : /* class DefineSortCommand */
1129 : : /* -------------------------------------------------------------------------- */
1130 : :
1131 : 0 : DefineSortCommand::DefineSortCommand(const std::string& id, cvc5::Sort sort)
1132 : 0 : : DeclarationDefinitionCommand(id), d_params(), d_sort(sort)
1133 : : {
1134 : 0 : }
1135 : :
1136 : 753 : DefineSortCommand::DefineSortCommand(const std::string& id,
1137 : : const std::vector<cvc5::Sort>& params,
1138 : 753 : cvc5::Sort sort)
1139 : 753 : : DeclarationDefinitionCommand(id), d_params(params), d_sort(sort)
1140 : : {
1141 : 753 : }
1142 : :
1143 : 0 : const std::vector<cvc5::Sort>& DefineSortCommand::getParameters() const
1144 : : {
1145 : 0 : return d_params;
1146 : : }
1147 : :
1148 : 0 : cvc5::Sort DefineSortCommand::getSort() const { return d_sort; }
1149 : 753 : void DefineSortCommand::invoke(CVC5_UNUSED cvc5::Solver* solver, SymManager* sm)
1150 : : {
1151 : : // This name is not its own distinct sort, it's an alias.
1152 [ - + ]: 753 : if (!sm->bindType(d_symbol, d_params, d_sort, true))
1153 : : {
1154 : 0 : std::stringstream ss;
1155 : 0 : ss << "Cannot bind " << d_symbol
1156 : 0 : << " to sort, maybe it has already been defined?";
1157 : 0 : d_commandStatus = new CommandFailure(ss.str());
1158 : 0 : return;
1159 : 0 : }
1160 : 753 : d_commandStatus = CommandSuccess::instance();
1161 : : }
1162 : :
1163 : 0 : std::string DefineSortCommand::getCommandName() const { return "define-sort"; }
1164 : :
1165 : 128 : void DefineSortCommand::toStream(std::ostream& out) const
1166 : : {
1167 : 128 : internal::Printer::getPrinter(out)->toStreamCmdDefineType(
1168 : 128 : out, d_symbol, sortVectorToTypeNodes(d_params), sortToTypeNode(d_sort));
1169 : 128 : }
1170 : :
1171 : : /* -------------------------------------------------------------------------- */
1172 : : /* class DefineFunctionCommand */
1173 : : /* -------------------------------------------------------------------------- */
1174 : :
1175 : 38 : DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
1176 : : cvc5::Sort sort,
1177 : 38 : cvc5::Term formula)
1178 : : : DeclarationDefinitionCommand(id),
1179 : 38 : d_formals(),
1180 : 38 : d_sort(sort),
1181 : 76 : d_formula(formula)
1182 : : {
1183 : 38 : }
1184 : :
1185 : 7372 : DefineFunctionCommand::DefineFunctionCommand(
1186 : : const std::string& id,
1187 : : const std::vector<cvc5::Term>& formals,
1188 : : cvc5::Sort sort,
1189 : 7372 : cvc5::Term formula)
1190 : : : DeclarationDefinitionCommand(id),
1191 : 7372 : d_formals(formals),
1192 : 7372 : d_sort(sort),
1193 : 14744 : d_formula(formula)
1194 : : {
1195 : 7372 : }
1196 : :
1197 : 0 : const std::vector<cvc5::Term>& DefineFunctionCommand::getFormals() const
1198 : : {
1199 : 0 : return d_formals;
1200 : : }
1201 : :
1202 : 0 : cvc5::Sort DefineFunctionCommand::getSort() const { return d_sort; }
1203 : :
1204 : 0 : cvc5::Term DefineFunctionCommand::getFormula() const { return d_formula; }
1205 : :
1206 : 7410 : void DefineFunctionCommand::invoke(cvc5::Solver* solver, SymManager* sm)
1207 : : {
1208 : : try
1209 : : {
1210 : 7410 : bool global = sm->getGlobalDeclarations();
1211 : : cvc5::Term fun =
1212 : 7410 : solver->defineFun(d_symbol, d_formals, d_sort, d_formula, global);
1213 [ - + ]: 7407 : if (!bindToTerm(sm, fun, true))
1214 : : {
1215 : 0 : return;
1216 : : }
1217 : 7407 : d_commandStatus = CommandSuccess::instance();
1218 [ + - ]: 7407 : }
1219 [ - + ]: 3 : catch (exception& e)
1220 : : {
1221 : 3 : d_commandStatus = new CommandFailure(e.what());
1222 : 3 : }
1223 : : }
1224 : :
1225 : 0 : std::string DefineFunctionCommand::getCommandName() const
1226 : : {
1227 : 0 : return "define-fun";
1228 : : }
1229 : :
1230 : 1339 : void DefineFunctionCommand::toStream(std::ostream& out) const
1231 : : {
1232 : 1339 : internal::Printer::getPrinter(out)->toStreamCmdDefineFunction(
1233 : : out,
1234 : 1339 : d_symbol,
1235 : 2678 : termVectorToNodes(d_formals),
1236 : 2678 : sortToTypeNode(d_sort),
1237 : 2678 : termToNode(d_formula));
1238 : 1339 : }
1239 : :
1240 : : /* -------------------------------------------------------------------------- */
1241 : : /* class DefineFunctionRecCommand */
1242 : : /* -------------------------------------------------------------------------- */
1243 : :
1244 : 569 : DefineFunctionRecCommand::DefineFunctionRecCommand(
1245 : 569 : cvc5::Term func, const std::vector<cvc5::Term>& formals, cvc5::Term formula)
1246 : : {
1247 : 569 : d_funcs.push_back(func);
1248 : 569 : d_formals.push_back(formals);
1249 : 569 : d_formulas.push_back(formula);
1250 : 569 : }
1251 : :
1252 : 78 : DefineFunctionRecCommand::DefineFunctionRecCommand(
1253 : : const std::vector<cvc5::Term>& funcs,
1254 : : const std::vector<std::vector<cvc5::Term>>& formals,
1255 : 78 : const std::vector<cvc5::Term>& formulas)
1256 : 78 : : d_funcs(funcs), d_formals(formals), d_formulas(formulas)
1257 : : {
1258 : 78 : }
1259 : :
1260 : 0 : const std::vector<cvc5::Term>& DefineFunctionRecCommand::getFunctions() const
1261 : : {
1262 : 0 : return d_funcs;
1263 : : }
1264 : :
1265 : : const std::vector<std::vector<cvc5::Term>>&
1266 : 0 : DefineFunctionRecCommand::getFormals() const
1267 : : {
1268 : 0 : return d_formals;
1269 : : }
1270 : :
1271 : 0 : const std::vector<cvc5::Term>& DefineFunctionRecCommand::getFormulas() const
1272 : : {
1273 : 0 : return d_formulas;
1274 : : }
1275 : :
1276 : 647 : void DefineFunctionRecCommand::invoke(cvc5::Solver* solver, SymManager* sm)
1277 : : {
1278 : : try
1279 : : {
1280 : : // bind each, returning if failure if we fail to bind
1281 [ + + ]: 1413 : for (const Term& f : d_funcs)
1282 : : {
1283 [ - + ][ - + ]: 766 : Assert(f.hasSymbol());
[ - - ]
1284 : 766 : const std::string s = f.getSymbol();
1285 [ - + ]: 766 : if (!tryBindToTerm(sm, s, f, true))
1286 : : {
1287 : 0 : std::stringstream ss;
1288 : 0 : tryBindToTerm(sm, s, f, true, &ss);
1289 : 0 : d_commandStatus = new CommandFailure(ss.str());
1290 : 0 : return;
1291 : 0 : }
1292 [ + - ]: 766 : }
1293 : 647 : bool global = sm->getGlobalDeclarations();
1294 : 647 : solver->defineFunsRec(d_funcs, d_formals, d_formulas, global);
1295 : 643 : d_commandStatus = CommandSuccess::instance();
1296 : : }
1297 [ - + ]: 4 : catch (exception& e)
1298 : : {
1299 : 4 : d_commandStatus = new CommandFailure(e.what());
1300 : 4 : }
1301 : : }
1302 : :
1303 : 0 : std::string DefineFunctionRecCommand::getCommandName() const
1304 : : {
1305 : 0 : return "define-fun-rec";
1306 : : }
1307 : :
1308 : 122 : void DefineFunctionRecCommand::toStream(std::ostream& out) const
1309 : : {
1310 : 122 : std::vector<std::vector<internal::Node>> formals;
1311 : 122 : formals.reserve(d_formals.size());
1312 [ + + ]: 273 : for (const std::vector<cvc5::Term>& formal : d_formals)
1313 : : {
1314 : 151 : formals.push_back(termVectorToNodes(formal));
1315 : : }
1316 : :
1317 : 244 : internal::Printer::getPrinter(out)->toStreamCmdDefineFunctionRec(
1318 : 244 : out, termVectorToNodes(d_funcs), formals, termVectorToNodes(d_formulas));
1319 : 122 : }
1320 : : /* -------------------------------------------------------------------------- */
1321 : : /* class DeclareHeapCommand */
1322 : : /* -------------------------------------------------------------------------- */
1323 : 258 : DeclareHeapCommand::DeclareHeapCommand(cvc5::Sort locSort, cvc5::Sort dataSort)
1324 : 258 : : d_locSort(locSort), d_dataSort(dataSort)
1325 : : {
1326 : 258 : }
1327 : :
1328 : 0 : cvc5::Sort DeclareHeapCommand::getLocationSort() const { return d_locSort; }
1329 : 0 : cvc5::Sort DeclareHeapCommand::getDataSort() const { return d_dataSort; }
1330 : :
1331 : 160 : void DeclareHeapCommand::invoke(cvc5::Solver* solver,
1332 : : CVC5_UNUSED SymManager* sm)
1333 : : {
1334 : 160 : solver->declareSepHeap(d_locSort, d_dataSort);
1335 : 160 : }
1336 : :
1337 : 0 : std::string DeclareHeapCommand::getCommandName() const
1338 : : {
1339 : 0 : return "declare-heap";
1340 : : }
1341 : :
1342 : 49 : void DeclareHeapCommand::toStream(std::ostream& out) const
1343 : : {
1344 : 98 : internal::Printer::getPrinter(out)->toStreamCmdDeclareHeap(
1345 : 98 : out, sortToTypeNode(d_locSort), sortToTypeNode(d_dataSort));
1346 : 49 : }
1347 : :
1348 : : /* -------------------------------------------------------------------------- */
1349 : : /* class SimplifyCommand */
1350 : : /* -------------------------------------------------------------------------- */
1351 : :
1352 : 0 : SimplifyCommand::SimplifyCommand(cvc5::Term term) : d_term(term) {}
1353 : 0 : cvc5::Term SimplifyCommand::getTerm() const { return d_term; }
1354 : 0 : void SimplifyCommand::invoke(cvc5::Solver* solver, CVC5_UNUSED SymManager* sm)
1355 : : {
1356 : : try
1357 : : {
1358 : 0 : d_result = solver->simplify(d_term);
1359 : 0 : d_commandStatus = CommandSuccess::instance();
1360 : : }
1361 [ - - ]: 0 : catch (exception& e)
1362 : : {
1363 : 0 : d_commandStatus = new CommandFailure(e.what());
1364 : 0 : }
1365 : 0 : }
1366 : :
1367 : 0 : cvc5::Term SimplifyCommand::getResult() const { return d_result; }
1368 : 0 : void SimplifyCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
1369 : : std::ostream& out) const
1370 : : {
1371 : 0 : out << d_result << endl;
1372 : 0 : }
1373 : :
1374 : 0 : std::string SimplifyCommand::getCommandName() const { return "simplify"; }
1375 : :
1376 : 0 : void SimplifyCommand::toStream(std::ostream& out) const
1377 : : {
1378 : 0 : internal::Printer::getPrinter(out)->toStreamCmdSimplify(out,
1379 : 0 : termToNode(d_term));
1380 : 0 : }
1381 : :
1382 : : /* -------------------------------------------------------------------------- */
1383 : : /* class GetValueCommand */
1384 : : /* -------------------------------------------------------------------------- */
1385 : :
1386 : 0 : GetValueCommand::GetValueCommand(cvc5::Term term) : d_terms()
1387 : : {
1388 : 0 : d_terms.push_back(term);
1389 : 0 : }
1390 : :
1391 : 218 : GetValueCommand::GetValueCommand(const std::vector<cvc5::Term>& terms)
1392 : 218 : : d_terms(terms)
1393 : : {
1394 [ - + ][ - + ]: 218 : Assert(terms.size() >= 1) << "cannot get-value of an empty set of terms";
[ - - ]
1395 : 218 : }
1396 : :
1397 : 0 : const std::vector<cvc5::Term>& GetValueCommand::getTerms() const
1398 : : {
1399 : 0 : return d_terms;
1400 : : }
1401 : 114 : void GetValueCommand::invoke(cvc5::Solver* solver, CVC5_UNUSED SymManager* sm)
1402 : : {
1403 : : try
1404 : : {
1405 : 114 : d_result = solver->getValue(d_terms);
1406 [ - + ][ - + ]: 106 : Assert(d_result.size() == d_terms.size());
[ - - ]
1407 : 106 : d_commandStatus = CommandSuccess::instance();
1408 : : }
1409 [ - + ][ - ]: 8 : catch (cvc5::CVC5ApiRecoverableException& e)
1410 : : {
1411 : 8 : d_commandStatus = new CommandRecoverableFailure(e.what());
1412 : 8 : }
1413 : 0 : catch (exception& e)
1414 : : {
1415 : 0 : d_commandStatus = new CommandFailure(e.what());
1416 : 0 : }
1417 : 114 : }
1418 : :
1419 : 0 : const std::vector<cvc5::Term>& GetValueCommand::getResult() const
1420 : : {
1421 : 0 : return d_result;
1422 : : }
1423 : 106 : void GetValueCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
1424 : : std::ostream& out) const
1425 : : {
1426 [ - + ][ - + ]: 106 : Assert(d_result.size() == d_terms.size());
[ - - ]
1427 : : // we print each of the values separately since we do not want
1428 : : // to letify across key/value pairs in this list.
1429 : 106 : out << "(";
1430 : 106 : bool firstTime = true;
1431 [ + + ]: 244 : for (size_t i = 0, rsize = d_result.size(); i < rsize; i++)
1432 : : {
1433 [ + + ]: 138 : if (firstTime)
1434 : : {
1435 : 106 : firstTime = false;
1436 : : }
1437 : : else
1438 : : {
1439 : 32 : out << " ";
1440 : : }
1441 : 138 : out << "(" << d_terms[i] << " " << d_result[i] << ")";
1442 : : }
1443 : 106 : out << ")" << std::endl;
1444 : 106 : }
1445 : :
1446 : 0 : std::string GetValueCommand::getCommandName() const { return "get-value"; }
1447 : :
1448 : 52 : void GetValueCommand::toStream(std::ostream& out) const
1449 : : {
1450 : 104 : internal::Printer::getPrinter(out)->toStreamCmdGetValue(
1451 : 104 : out, termVectorToNodes(d_terms));
1452 : 52 : }
1453 : :
1454 : : /* -------------------------------------------------------------------------- */
1455 : : /* class GetModelDomainElementsCommand */
1456 : : /* -------------------------------------------------------------------------- */
1457 : :
1458 : 8 : GetModelDomainElementsCommand::GetModelDomainElementsCommand(cvc5::Sort sort)
1459 : 8 : : d_sort(sort)
1460 : : {
1461 : 8 : }
1462 : :
1463 : 0 : cvc5::Sort GetModelDomainElementsCommand::getSort() const { return d_sort; }
1464 : :
1465 : 6 : void GetModelDomainElementsCommand::invoke(cvc5::Solver* solver,
1466 : : CVC5_UNUSED SymManager* sm)
1467 : : {
1468 : : try
1469 : : {
1470 : 6 : d_result = solver->getModelDomainElements(d_sort);
1471 : 6 : d_commandStatus = CommandSuccess::instance();
1472 : : }
1473 [ - - ][ - ]: 0 : catch (cvc5::CVC5ApiRecoverableException& e)
1474 : : {
1475 : 0 : d_commandStatus = new CommandRecoverableFailure(e.what());
1476 : 0 : }
1477 : 0 : catch (exception& e)
1478 : : {
1479 : 0 : d_commandStatus = new CommandFailure(e.what());
1480 : 0 : }
1481 : 6 : }
1482 : :
1483 : 0 : const std::vector<cvc5::Term>& GetModelDomainElementsCommand::getResult() const
1484 : : {
1485 : 0 : return d_result;
1486 : : }
1487 : :
1488 : 6 : void GetModelDomainElementsCommand::printResult(
1489 : : CVC5_UNUSED cvc5::Solver* solver, std::ostream& out) const
1490 : : {
1491 : 6 : out << "(";
1492 : 6 : bool firstTime = true;
1493 [ + + ]: 16 : for (size_t i = 0, rsize = d_result.size(); i < rsize; i++)
1494 : : {
1495 [ + + ]: 10 : if (firstTime)
1496 : : {
1497 : 6 : firstTime = false;
1498 : : }
1499 : : else
1500 : : {
1501 : 4 : out << " ";
1502 : : }
1503 : 10 : out << d_result[i];
1504 : : }
1505 : 6 : out << ")" << std::endl;
1506 : 6 : }
1507 : :
1508 : 0 : std::string GetModelDomainElementsCommand::getCommandName() const
1509 : : {
1510 : 0 : return "get-model-domain-elements";
1511 : : }
1512 : :
1513 : 1 : void GetModelDomainElementsCommand::toStream(std::ostream& out) const
1514 : : {
1515 : 2 : internal::Printer::getPrinter(out)->toStreamCmdGetModelDomainElements(
1516 : 2 : out, sortToTypeNode(d_sort));
1517 : 1 : }
1518 : :
1519 : : /* -------------------------------------------------------------------------- */
1520 : : /* class GetAssignmentCommand */
1521 : : /* -------------------------------------------------------------------------- */
1522 : :
1523 : 20 : GetAssignmentCommand::GetAssignmentCommand() {}
1524 : 10 : void GetAssignmentCommand::invoke(cvc5::Solver* solver, SymManager* sm)
1525 : : {
1526 : : try
1527 : : {
1528 : 10 : TermManager& tm = solver->getTermManager();
1529 : 10 : std::map<cvc5::Term, std::string> enames = sm->getExpressionNames();
1530 : 10 : std::vector<cvc5::Term> terms;
1531 : 10 : std::vector<std::string> names;
1532 [ + + ]: 22 : for (const std::pair<const cvc5::Term, std::string>& e : enames)
1533 : : {
1534 : 12 : terms.push_back(e.first);
1535 : 12 : names.push_back(e.second);
1536 : : }
1537 : : // Must use vector version of getValue to ensure error is thrown regardless
1538 : : // of whether terms is empty.
1539 : 10 : std::vector<cvc5::Term> values = solver->getValue(terms);
1540 [ - + ][ - + ]: 8 : Assert(values.size() == names.size());
[ - - ]
1541 : 8 : std::vector<cvc5::Term> sexprs;
1542 [ + + ]: 20 : for (size_t i = 0, nterms = terms.size(); i < nterms; i++)
1543 : : {
1544 : : // Treat the expression name as a variable name as opposed to a string
1545 : : // constant to avoid printing double quotes around the name.
1546 : 24 : cvc5::Term name = tm.mkVar(tm.getBooleanSort(), names[i]);
1547 [ + + ][ - - ]: 36 : sexprs.push_back(tm.mkTerm(cvc5::Kind::SEXPR, {name, values[i]}));
1548 : 12 : }
1549 : 8 : d_result = tm.mkTerm(cvc5::Kind::SEXPR, sexprs);
1550 : 8 : d_commandStatus = CommandSuccess::instance();
1551 : 14 : }
1552 [ - + ][ - ]: 2 : catch (cvc5::CVC5ApiRecoverableException& e)
1553 : : {
1554 : 2 : d_commandStatus = new CommandRecoverableFailure(e.what());
1555 : 2 : }
1556 : 0 : catch (exception& e)
1557 : : {
1558 : 0 : d_commandStatus = new CommandFailure(e.what());
1559 : 0 : }
1560 : 10 : }
1561 : :
1562 : 0 : cvc5::Term GetAssignmentCommand::getResult() const { return d_result; }
1563 : 8 : void GetAssignmentCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
1564 : : std::ostream& out) const
1565 : : {
1566 : 8 : out << d_result << endl;
1567 : 8 : }
1568 : :
1569 : 0 : std::string GetAssignmentCommand::getCommandName() const
1570 : : {
1571 : 0 : return "get-assignment";
1572 : : }
1573 : :
1574 : 5 : void GetAssignmentCommand::toStream(std::ostream& out) const
1575 : : {
1576 : 5 : internal::Printer::getPrinter(out)->toStreamCmdGetAssignment(out);
1577 : 5 : }
1578 : :
1579 : : /* -------------------------------------------------------------------------- */
1580 : : /* class GetModelCommand */
1581 : : /* -------------------------------------------------------------------------- */
1582 : :
1583 : 109 : GetModelCommand::GetModelCommand() {}
1584 : 57 : void GetModelCommand::invoke(cvc5::Solver* solver, SymManager* sm)
1585 : : {
1586 : : try
1587 : : {
1588 : 57 : std::vector<cvc5::Sort> declareSorts = sm->getDeclaredSorts();
1589 : 57 : std::vector<cvc5::Term> declareTerms = sm->getDeclaredTerms();
1590 : 57 : d_result = solver->getModel(declareSorts, declareTerms);
1591 : 48 : d_commandStatus = CommandSuccess::instance();
1592 : 66 : }
1593 [ - + ][ - ]: 9 : catch (cvc5::CVC5ApiRecoverableException& e)
1594 : : {
1595 : 9 : d_commandStatus = new CommandRecoverableFailure(e.what());
1596 : 9 : }
1597 : 0 : catch (exception& e)
1598 : : {
1599 : 0 : d_commandStatus = new CommandFailure(e.what());
1600 : 0 : }
1601 : 57 : }
1602 : :
1603 : 48 : void GetModelCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
1604 : : std::ostream& out) const
1605 : : {
1606 : 48 : out << d_result;
1607 : 48 : }
1608 : :
1609 : 2 : std::string GetModelCommand::getCommandName() const { return "get-model"; }
1610 : :
1611 : 25 : void GetModelCommand::toStream(std::ostream& out) const
1612 : : {
1613 : 25 : internal::Printer::getPrinter(out)->toStreamCmdGetModel(out);
1614 : 25 : }
1615 : :
1616 : : /* -------------------------------------------------------------------------- */
1617 : : /* class BlockModelCommand */
1618 : : /* -------------------------------------------------------------------------- */
1619 : :
1620 : 38 : BlockModelCommand::BlockModelCommand(modes::BlockModelsMode mode) : d_mode(mode)
1621 : : {
1622 : 38 : }
1623 : 24 : void BlockModelCommand::invoke(cvc5::Solver* solver, CVC5_UNUSED SymManager* sm)
1624 : : {
1625 : : try
1626 : : {
1627 : 24 : solver->blockModel(d_mode);
1628 : 24 : d_commandStatus = CommandSuccess::instance();
1629 : : }
1630 [ - - ][ - ]: 0 : catch (cvc5::CVC5ApiRecoverableException& e)
1631 : : {
1632 : 0 : d_commandStatus = new CommandRecoverableFailure(e.what());
1633 : 0 : }
1634 : 0 : catch (exception& e)
1635 : : {
1636 : 0 : d_commandStatus = new CommandFailure(e.what());
1637 : 0 : }
1638 : 24 : }
1639 : :
1640 : 0 : std::string BlockModelCommand::getCommandName() const { return "block-model"; }
1641 : :
1642 : 7 : void BlockModelCommand::toStream(std::ostream& out) const
1643 : : {
1644 : 7 : internal::Printer::getPrinter(out)->toStreamCmdBlockModel(out, d_mode);
1645 : 7 : }
1646 : :
1647 : : /* -------------------------------------------------------------------------- */
1648 : : /* class BlockModelValuesCommand */
1649 : : /* -------------------------------------------------------------------------- */
1650 : :
1651 : 18 : BlockModelValuesCommand::BlockModelValuesCommand(
1652 : 18 : const std::vector<cvc5::Term>& terms)
1653 : 18 : : d_terms(terms)
1654 : : {
1655 [ - + ][ - + ]: 18 : Assert(terms.size() >= 1)
[ - - ]
1656 : 0 : << "cannot block-model-values of an empty set of terms";
1657 : 18 : }
1658 : :
1659 : 0 : const std::vector<cvc5::Term>& BlockModelValuesCommand::getTerms() const
1660 : : {
1661 : 0 : return d_terms;
1662 : : }
1663 : 12 : void BlockModelValuesCommand::invoke(cvc5::Solver* solver,
1664 : : CVC5_UNUSED SymManager* sm)
1665 : : {
1666 : : try
1667 : : {
1668 : 12 : solver->blockModelValues(d_terms);
1669 : 12 : d_commandStatus = CommandSuccess::instance();
1670 : : }
1671 [ - - ][ - ]: 0 : catch (cvc5::CVC5ApiRecoverableException& e)
1672 : : {
1673 : 0 : d_commandStatus = new CommandRecoverableFailure(e.what());
1674 : 0 : }
1675 : 0 : catch (exception& e)
1676 : : {
1677 : 0 : d_commandStatus = new CommandFailure(e.what());
1678 : 0 : }
1679 : 12 : }
1680 : :
1681 : 0 : std::string BlockModelValuesCommand::getCommandName() const
1682 : : {
1683 : 0 : return "block-model-values";
1684 : : }
1685 : :
1686 : 3 : void BlockModelValuesCommand::toStream(std::ostream& out) const
1687 : : {
1688 : 6 : internal::Printer::getPrinter(out)->toStreamCmdBlockModelValues(
1689 : 6 : out, termVectorToNodes(d_terms));
1690 : 3 : }
1691 : :
1692 : : /* -------------------------------------------------------------------------- */
1693 : : /* class GetProofCommand */
1694 : : /* -------------------------------------------------------------------------- */
1695 : :
1696 : 5372 : GetProofCommand::GetProofCommand(modes::ProofComponent c) : d_component(c) {}
1697 : 5358 : void GetProofCommand::invoke(cvc5::Solver* solver, SymManager* sm)
1698 : : {
1699 : : try
1700 : : {
1701 : 5358 : stringstream ss;
1702 : 5358 : const vector<cvc5::Proof> ps = solver->getProof(d_component);
1703 : :
1704 [ + + ]: 10711 : bool commentProves = !(d_component == modes::ProofComponent::SAT
1705 [ + + ]: 5354 : || d_component == modes::ProofComponent::FULL);
1706 : 5357 : modes::ProofFormat format = modes::ProofFormat::DEFAULT;
1707 : : // Ignore proof format, if the proof is not the full proof
1708 [ + + ]: 5357 : if (d_component != modes::ProofComponent::FULL)
1709 : : {
1710 : 12 : format = modes::ProofFormat::NONE;
1711 : : }
1712 : :
1713 [ + + ]: 5357 : if (format == modes::ProofFormat::NONE)
1714 : : {
1715 : 12 : ss << "(" << std::endl;
1716 : : }
1717 [ + + ]: 10741 : for (Proof p : ps)
1718 : : {
1719 [ + + ]: 5384 : if (commentProves)
1720 : : {
1721 : 36 : ss << "(!" << std::endl;
1722 : : }
1723 : : // get assertions, and build a map between them and their names
1724 : : std::map<cvc5::Term, std::string> assertionNames =
1725 : 5384 : sm->getExpressionNames(true);
1726 : 5384 : ss << solver->proofToString(p, format, assertionNames);
1727 [ + + ]: 5384 : if (commentProves)
1728 : : {
1729 : 36 : ss << ":proves " << p.getResult() << ")" << std::endl;
1730 : : }
1731 : 5384 : }
1732 [ + + ]: 5357 : if (format == modes::ProofFormat::NONE)
1733 : : {
1734 : 12 : ss << ")" << std::endl;
1735 : : }
1736 : 5357 : d_result = ss.str();
1737 : 5357 : d_commandStatus = CommandSuccess::instance();
1738 : 5358 : }
1739 [ - - ][ + ]: 1 : catch (cvc5::CVC5ApiRecoverableException& e)
1740 : : {
1741 : 0 : d_commandStatus = new CommandRecoverableFailure(e.what());
1742 : 0 : }
1743 : 1 : catch (exception& e)
1744 : : {
1745 : 1 : d_commandStatus = new CommandFailure(e.what());
1746 : 1 : }
1747 : 5358 : }
1748 : :
1749 : 5357 : void GetProofCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
1750 : : std::ostream& out) const
1751 : : {
1752 : 5357 : out << d_result;
1753 : 5357 : }
1754 : :
1755 : 0 : std::string GetProofCommand::getCommandName() const { return "get-proof"; }
1756 : :
1757 : 7 : void GetProofCommand::toStream(std::ostream& out) const
1758 : : {
1759 : 7 : internal::Printer::getPrinter(out)->toStreamCmdGetProof(out, d_component);
1760 : 7 : }
1761 : :
1762 : : /* -------------------------------------------------------------------------- */
1763 : : /* class GetInstantiationsCommand */
1764 : : /* -------------------------------------------------------------------------- */
1765 : :
1766 : 12 : GetInstantiationsCommand::GetInstantiationsCommand() : d_solver(nullptr) {}
1767 : 22 : bool GetInstantiationsCommand::isEnabled(CVC5_UNUSED cvc5::Solver* solver,
1768 : : const cvc5::Result& res)
1769 : : {
1770 : 22 : return (res.isSat()
1771 [ - + ]: 22 : || (res.isUnknown()
1772 [ - - ]: 0 : && res.getUnknownExplanation()
1773 : : == cvc5::UnknownExplanation::INCOMPLETE))
1774 [ + - ][ + + ]: 44 : || res.isUnsat();
1775 : : }
1776 : 12 : void GetInstantiationsCommand::invoke(cvc5::Solver* solver,
1777 : : CVC5_UNUSED SymManager* sm)
1778 : : {
1779 : : try
1780 : : {
1781 : 12 : d_solver = solver;
1782 : 12 : d_commandStatus = CommandSuccess::instance();
1783 : : }
1784 : : catch (exception& e)
1785 : : {
1786 : : d_commandStatus = new CommandFailure(e.what());
1787 : : }
1788 : 12 : }
1789 : :
1790 : 12 : void GetInstantiationsCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
1791 : : std::ostream& out) const
1792 : : {
1793 : 12 : out << d_solver->getInstantiations();
1794 : 12 : }
1795 : :
1796 : 0 : std::string GetInstantiationsCommand::getCommandName() const
1797 : : {
1798 : 0 : return "get-instantiations";
1799 : : }
1800 : :
1801 : 0 : void GetInstantiationsCommand::toStream(std::ostream& out) const
1802 : : {
1803 : 0 : internal::Printer::getPrinter(out)->toStreamCmdGetInstantiations(out);
1804 : 0 : }
1805 : :
1806 : : /* -------------------------------------------------------------------------- */
1807 : : /* class GetInterpolCommand */
1808 : : /* -------------------------------------------------------------------------- */
1809 : :
1810 : 0 : GetInterpolantCommand::GetInterpolantCommand(const std::string& name, Term conj)
1811 : 0 : : d_name(name), d_conj(conj), d_sygus_grammar(nullptr)
1812 : : {
1813 : 0 : }
1814 : 72 : GetInterpolantCommand::GetInterpolantCommand(const std::string& name,
1815 : : Term conj,
1816 : 72 : Grammar* g)
1817 : 72 : : d_name(name), d_conj(conj), d_sygus_grammar(g)
1818 : : {
1819 : 72 : }
1820 : :
1821 : 0 : Term GetInterpolantCommand::getConjecture() const { return d_conj; }
1822 : :
1823 : 0 : const Grammar* GetInterpolantCommand::getGrammar() const
1824 : : {
1825 : 0 : return d_sygus_grammar;
1826 : : }
1827 : :
1828 : 0 : Term GetInterpolantCommand::getResult() const { return d_result; }
1829 : :
1830 : 24 : void GetInterpolantCommand::invoke(Solver* solver, SymManager* sm)
1831 : : {
1832 : : try
1833 : : {
1834 : : // we must remember the name of the interpolant, in case
1835 : : // get-interpolant-next is called later.
1836 : 24 : sm->setLastSynthName(d_name);
1837 [ + + ]: 24 : if (d_sygus_grammar == nullptr)
1838 : : {
1839 : 19 : d_result = solver->getInterpolant(d_conj);
1840 : : }
1841 : : else
1842 : : {
1843 : 5 : d_result = solver->getInterpolant(d_conj, *d_sygus_grammar);
1844 : : }
1845 : 23 : d_commandStatus = CommandSuccess::instance();
1846 : : }
1847 [ - + ]: 1 : catch (exception& e)
1848 : : {
1849 : 1 : d_commandStatus = new CommandFailure(e.what());
1850 : 1 : }
1851 : 24 : }
1852 : :
1853 : 23 : void GetInterpolantCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
1854 : : std::ostream& out) const
1855 : : {
1856 [ + + ]: 23 : if (!d_result.isNull())
1857 : : {
1858 : 19 : out << "(define-fun " << d_name << " () Bool " << d_result << ")"
1859 : 19 : << std::endl;
1860 : : }
1861 : : else
1862 : : {
1863 : 4 : out << "fail" << std::endl;
1864 : : }
1865 : 23 : }
1866 : :
1867 : 0 : std::string GetInterpolantCommand::getCommandName() const
1868 : : {
1869 : 0 : return "get-interpolant";
1870 : : }
1871 : :
1872 : 24 : void GetInterpolantCommand::toStream(std::ostream& out) const
1873 : : {
1874 : 24 : internal::Printer::getPrinter(out)->toStreamCmdGetInterpol(
1875 : 24 : out, d_name, termToNode(d_conj), grammarToTypeNode(d_sygus_grammar));
1876 : 24 : }
1877 : :
1878 : : /* -------------------------------------------------------------------------- */
1879 : : /* class GetInterpolNextCommand */
1880 : : /* -------------------------------------------------------------------------- */
1881 : :
1882 : 3 : GetInterpolantNextCommand::GetInterpolantNextCommand() {}
1883 : :
1884 : 0 : Term GetInterpolantNextCommand::getResult() const { return d_result; }
1885 : :
1886 : 1 : void GetInterpolantNextCommand::invoke(Solver* solver, SymManager* sm)
1887 : : {
1888 : : try
1889 : : {
1890 : : // Get the name of the interpolant from the symbol manager
1891 : 1 : d_name = sm->getLastSynthName();
1892 : 1 : d_result = solver->getInterpolantNext();
1893 : 1 : d_commandStatus = CommandSuccess::instance();
1894 : : }
1895 [ - - ]: 0 : catch (exception& e)
1896 : : {
1897 : 0 : d_commandStatus = new CommandFailure(e.what());
1898 : 0 : }
1899 : 1 : }
1900 : :
1901 : 1 : void GetInterpolantNextCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
1902 : : std::ostream& out) const
1903 : : {
1904 [ + - ]: 1 : if (!d_result.isNull())
1905 : : {
1906 : 1 : out << "(define-fun " << d_name << " () Bool " << d_result << ")"
1907 : 1 : << std::endl;
1908 : : }
1909 : : else
1910 : : {
1911 : 0 : out << "fail" << std::endl;
1912 : : }
1913 : 1 : }
1914 : :
1915 : 0 : std::string GetInterpolantNextCommand::getCommandName() const
1916 : : {
1917 : 0 : return "get-interpolant-next";
1918 : : }
1919 : :
1920 : 1 : void GetInterpolantNextCommand::toStream(std::ostream& out) const
1921 : : {
1922 : 1 : internal::Printer::getPrinter(out)->toStreamCmdGetInterpolNext(out);
1923 : 1 : }
1924 : :
1925 : : /* -------------------------------------------------------------------------- */
1926 : : /* class GetAbductCommand */
1927 : : /* -------------------------------------------------------------------------- */
1928 : :
1929 : 0 : GetAbductCommand::GetAbductCommand(const std::string& name, cvc5::Term conj)
1930 : 0 : : d_name(name), d_conj(conj), d_sygus_grammar(nullptr)
1931 : : {
1932 : 0 : }
1933 : 132 : GetAbductCommand::GetAbductCommand(const std::string& name,
1934 : : cvc5::Term conj,
1935 : 132 : cvc5::Grammar* g)
1936 : 132 : : d_name(name), d_conj(conj), d_sygus_grammar(g)
1937 : : {
1938 : 132 : }
1939 : :
1940 : 0 : cvc5::Term GetAbductCommand::getConjecture() const { return d_conj; }
1941 : :
1942 : 0 : const cvc5::Grammar* GetAbductCommand::getGrammar() const
1943 : : {
1944 : 0 : return d_sygus_grammar;
1945 : : }
1946 : :
1947 : 0 : std::string GetAbductCommand::getAbductName() const { return d_name; }
1948 : 0 : cvc5::Term GetAbductCommand::getResult() const { return d_result; }
1949 : :
1950 : 66 : void GetAbductCommand::invoke(cvc5::Solver* solver, SymManager* sm)
1951 : : {
1952 : : try
1953 : : {
1954 : : // we must remember the name of the abduct, in case get-abduct-next is
1955 : : // called later.
1956 : 66 : sm->setLastSynthName(d_name);
1957 [ + + ]: 66 : if (d_sygus_grammar == nullptr)
1958 : : {
1959 : 54 : d_result = solver->getAbduct(d_conj);
1960 : : }
1961 : : else
1962 : : {
1963 : 12 : d_result = solver->getAbduct(d_conj, *d_sygus_grammar);
1964 : : }
1965 : 62 : d_commandStatus = CommandSuccess::instance();
1966 : : }
1967 [ - + ]: 4 : catch (exception& e)
1968 : : {
1969 : 4 : d_commandStatus = new CommandFailure(e.what());
1970 : 4 : }
1971 : 66 : }
1972 : :
1973 : 62 : void GetAbductCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
1974 : : std::ostream& out) const
1975 : : {
1976 [ + + ]: 62 : if (!d_result.isNull())
1977 : : {
1978 : 52 : out << "(define-fun " << d_name << " () Bool " << d_result << ")"
1979 : 52 : << std::endl;
1980 : : }
1981 : : else
1982 : : {
1983 : 10 : out << "fail" << std::endl;
1984 : : }
1985 : 62 : }
1986 : :
1987 : 0 : std::string GetAbductCommand::getCommandName() const { return "get-abduct"; }
1988 : :
1989 : 33 : void GetAbductCommand::toStream(std::ostream& out) const
1990 : : {
1991 : 33 : internal::Printer::getPrinter(out)->toStreamCmdGetAbduct(
1992 : 33 : out, d_name, termToNode(d_conj), grammarToTypeNode(d_sygus_grammar));
1993 : 33 : }
1994 : :
1995 : : /* -------------------------------------------------------------------------- */
1996 : : /* class GetAbductNextCommand */
1997 : : /* -------------------------------------------------------------------------- */
1998 : :
1999 : 24 : GetAbductNextCommand::GetAbductNextCommand() {}
2000 : :
2001 : 0 : cvc5::Term GetAbductNextCommand::getResult() const { return d_result; }
2002 : :
2003 : 12 : void GetAbductNextCommand::invoke(cvc5::Solver* solver, SymManager* sm)
2004 : : {
2005 : : try
2006 : : {
2007 : : // Get the name of the abduct from the symbol manager
2008 : 12 : d_name = sm->getLastSynthName();
2009 : 12 : d_result = solver->getAbductNext();
2010 : 12 : d_commandStatus = CommandSuccess::instance();
2011 : : }
2012 [ - - ]: 0 : catch (exception& e)
2013 : : {
2014 : 0 : d_commandStatus = new CommandFailure(e.what());
2015 : 0 : }
2016 : 12 : }
2017 : :
2018 : 12 : void GetAbductNextCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
2019 : : std::ostream& out) const
2020 : : {
2021 [ + - ]: 12 : if (!d_result.isNull())
2022 : : {
2023 : 12 : out << "(define-fun " << d_name << " () Bool " << d_result << ")"
2024 : 12 : << std::endl;
2025 : : }
2026 : : else
2027 : : {
2028 : 0 : out << "fail" << std::endl;
2029 : : }
2030 : 12 : }
2031 : :
2032 : 0 : std::string GetAbductNextCommand::getCommandName() const
2033 : : {
2034 : 0 : return "get-abduct-next";
2035 : : }
2036 : :
2037 : 6 : void GetAbductNextCommand::toStream(std::ostream& out) const
2038 : : {
2039 : 6 : internal::Printer::getPrinter(out)->toStreamCmdGetAbductNext(out);
2040 : 6 : }
2041 : :
2042 : : /* -------------------------------------------------------------------------- */
2043 : : /* class GetQuantifierEliminationCommand */
2044 : : /* -------------------------------------------------------------------------- */
2045 : :
2046 : 0 : GetQuantifierEliminationCommand::GetQuantifierEliminationCommand()
2047 : 0 : : d_term(), d_doFull(true)
2048 : : {
2049 : 0 : }
2050 : 57 : GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(
2051 : 57 : const cvc5::Term& term, bool doFull)
2052 : 57 : : d_term(term), d_doFull(doFull)
2053 : : {
2054 : 57 : }
2055 : :
2056 : 0 : cvc5::Term GetQuantifierEliminationCommand::getTerm() const { return d_term; }
2057 : 0 : bool GetQuantifierEliminationCommand::getDoFull() const { return d_doFull; }
2058 : 19 : void GetQuantifierEliminationCommand::invoke(cvc5::Solver* solver,
2059 : : CVC5_UNUSED SymManager* sm)
2060 : : {
2061 : : try
2062 : : {
2063 [ + + ]: 19 : if (d_doFull)
2064 : : {
2065 : 18 : d_result = solver->getQuantifierElimination(d_term);
2066 : : }
2067 : : else
2068 : : {
2069 : 1 : d_result = solver->getQuantifierEliminationDisjunct(d_term);
2070 : : }
2071 : 19 : d_commandStatus = CommandSuccess::instance();
2072 : : }
2073 [ - - ]: 0 : catch (exception& e)
2074 : : {
2075 : 0 : d_commandStatus = new CommandFailure(e.what());
2076 : 0 : }
2077 : 19 : }
2078 : :
2079 : 0 : cvc5::Term GetQuantifierEliminationCommand::getResult() const
2080 : : {
2081 : 0 : return d_result;
2082 : : }
2083 : 19 : void GetQuantifierEliminationCommand::printResult(
2084 : : CVC5_UNUSED cvc5::Solver* solver, std::ostream& out) const
2085 : : {
2086 : 19 : out << d_result << endl;
2087 : 19 : }
2088 : :
2089 : 0 : std::string GetQuantifierEliminationCommand::getCommandName() const
2090 : : {
2091 [ - - ]: 0 : return d_doFull ? "get-qe" : "get-qe-disjunct";
2092 : : }
2093 : :
2094 : 19 : void GetQuantifierEliminationCommand::toStream(std::ostream& out) const
2095 : : {
2096 : 38 : internal::Printer::getPrinter(out)->toStreamCmdGetQuantifierElimination(
2097 : 38 : out, termToNode(d_term), d_doFull);
2098 : 19 : }
2099 : :
2100 : : /* -------------------------------------------------------------------------- */
2101 : : /* class GetUnsatAssumptionsCommand */
2102 : : /* -------------------------------------------------------------------------- */
2103 : :
2104 : 32 : GetUnsatAssumptionsCommand::GetUnsatAssumptionsCommand() {}
2105 : :
2106 : 20 : void GetUnsatAssumptionsCommand::invoke(cvc5::Solver* solver,
2107 : : CVC5_UNUSED SymManager* sm)
2108 : : {
2109 : : try
2110 : : {
2111 : 20 : d_result = solver->getUnsatAssumptions();
2112 : 20 : d_commandStatus = CommandSuccess::instance();
2113 : : }
2114 [ - - ][ - ]: 0 : catch (cvc5::CVC5ApiRecoverableException& e)
2115 : : {
2116 : 0 : d_commandStatus = new CommandRecoverableFailure(e.what());
2117 : 0 : }
2118 : 0 : catch (exception& e)
2119 : : {
2120 : 0 : d_commandStatus = new CommandFailure(e.what());
2121 : 0 : }
2122 : 20 : }
2123 : :
2124 : 0 : std::vector<cvc5::Term> GetUnsatAssumptionsCommand::getResult() const
2125 : : {
2126 : 0 : return d_result;
2127 : : }
2128 : :
2129 : 20 : void GetUnsatAssumptionsCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
2130 : : std::ostream& out) const
2131 : : {
2132 : 20 : internal::container_to_stream(out, d_result, "(", ")\n", " ");
2133 : 20 : }
2134 : :
2135 : 0 : std::string GetUnsatAssumptionsCommand::getCommandName() const
2136 : : {
2137 : 0 : return "get-unsat-assumptions";
2138 : : }
2139 : :
2140 : 6 : void GetUnsatAssumptionsCommand::toStream(std::ostream& out) const
2141 : : {
2142 : 6 : internal::Printer::getPrinter(out)->toStreamCmdGetUnsatAssumptions(out);
2143 : 6 : }
2144 : :
2145 : : /* -------------------------------------------------------------------------- */
2146 : : /* class GetUnsatCoreCommand */
2147 : : /* -------------------------------------------------------------------------- */
2148 : :
2149 : 59 : GetUnsatCoreCommand::GetUnsatCoreCommand() : d_solver(nullptr), d_sm(nullptr) {}
2150 : 35 : void GetUnsatCoreCommand::invoke(cvc5::Solver* solver, SymManager* sm)
2151 : : {
2152 : : try
2153 : : {
2154 : 35 : d_sm = sm;
2155 : 35 : d_solver = solver;
2156 : 35 : d_result = solver->getUnsatCore();
2157 : :
2158 : 28 : d_commandStatus = CommandSuccess::instance();
2159 : : }
2160 [ - + ][ + ]: 7 : catch (cvc5::CVC5ApiRecoverableException& e)
2161 : : {
2162 : 6 : d_commandStatus = new CommandRecoverableFailure(e.what());
2163 : 6 : }
2164 : 1 : catch (exception& e)
2165 : : {
2166 : 1 : d_commandStatus = new CommandFailure(e.what());
2167 : 1 : }
2168 : 35 : }
2169 : :
2170 : 28 : void GetUnsatCoreCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
2171 : : std::ostream& out) const
2172 : : {
2173 [ + + ]: 28 : if (d_solver->getOption("print-cores-full") == "true")
2174 : : {
2175 : : // use the assertions
2176 : 6 : internal::UnsatCore ucr(termVectorToNodes(d_result));
2177 : 6 : ucr.toStream(out);
2178 : 6 : }
2179 : : else
2180 : : {
2181 : : // otherwise, use the names
2182 : 22 : std::vector<std::string> names;
2183 : 22 : d_sm->getExpressionNames(d_result, names, true);
2184 : 22 : internal::UnsatCore ucr(names);
2185 : 22 : ucr.toStream(out);
2186 : 22 : }
2187 : 28 : }
2188 : :
2189 : 0 : const std::vector<cvc5::Term>& GetUnsatCoreCommand::getUnsatCore() const
2190 : : {
2191 : : // of course, this will be empty if the command hasn't been invoked
2192 : : // yet
2193 : 0 : return d_result;
2194 : : }
2195 : :
2196 : 0 : std::string GetUnsatCoreCommand::getCommandName() const
2197 : : {
2198 : 0 : return "get-unsat-core";
2199 : : }
2200 : :
2201 : 11 : void GetUnsatCoreCommand::toStream(std::ostream& out) const
2202 : : {
2203 : 11 : internal::Printer::getPrinter(out)->toStreamCmdGetUnsatCore(out);
2204 : 11 : }
2205 : :
2206 : : /* -------------------------------------------------------------------------- */
2207 : : /* class GetUnsatCoreLemmasCommand */
2208 : : /* -------------------------------------------------------------------------- */
2209 : :
2210 : 8 : GetUnsatCoreLemmasCommand::GetUnsatCoreLemmasCommand() : d_solver(nullptr) {}
2211 : 6 : void GetUnsatCoreLemmasCommand::invoke(cvc5::Solver* solver,
2212 : : CVC5_UNUSED SymManager* sm)
2213 : : {
2214 : : try
2215 : : {
2216 : 6 : d_solver = solver;
2217 : 6 : d_result = solver->getUnsatCoreLemmas();
2218 : :
2219 : 6 : d_commandStatus = CommandSuccess::instance();
2220 : : }
2221 [ - - ][ - ]: 0 : catch (cvc5::CVC5ApiRecoverableException& e)
2222 : : {
2223 : 0 : d_commandStatus = new CommandRecoverableFailure(e.what());
2224 : 0 : }
2225 : 0 : catch (exception& e)
2226 : : {
2227 : 0 : d_commandStatus = new CommandFailure(e.what());
2228 : 0 : }
2229 : 6 : }
2230 : :
2231 : 6 : void GetUnsatCoreLemmasCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
2232 : : std::ostream& out) const
2233 : : {
2234 : : // use the assertions
2235 : 6 : internal::UnsatCore ucr(termVectorToNodes(d_result));
2236 : 6 : ucr.toStream(out);
2237 : 6 : }
2238 : :
2239 : 0 : std::string GetUnsatCoreLemmasCommand::getCommandName() const
2240 : : {
2241 : 0 : return "get-unsat-core-lemmas";
2242 : : }
2243 : :
2244 : 2 : void GetUnsatCoreLemmasCommand::toStream(std::ostream& out) const
2245 : : {
2246 : 2 : internal::Printer::getPrinter(out)->toStreamCmdGetUnsatCore(out);
2247 : 2 : }
2248 : :
2249 : : /* -------------------------------------------------------------------------- */
2250 : : /* class GetDifficultyCommand */
2251 : : /* -------------------------------------------------------------------------- */
2252 : :
2253 : 21 : GetDifficultyCommand::GetDifficultyCommand() : d_sm(nullptr) {}
2254 : 15 : void GetDifficultyCommand::invoke(cvc5::Solver* solver, SymManager* sm)
2255 : : {
2256 : : try
2257 : : {
2258 : 15 : d_sm = sm;
2259 : 15 : d_result = solver->getDifficulty();
2260 : :
2261 : 15 : d_commandStatus = CommandSuccess::instance();
2262 : : }
2263 [ - - ][ - ]: 0 : catch (cvc5::CVC5ApiRecoverableException& e)
2264 : : {
2265 : 0 : d_commandStatus = new CommandRecoverableFailure(e.what());
2266 : 0 : }
2267 : 0 : catch (exception& e)
2268 : : {
2269 : 0 : d_commandStatus = new CommandFailure(e.what());
2270 : 0 : }
2271 : 15 : }
2272 : :
2273 : 15 : void GetDifficultyCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
2274 : : std::ostream& out) const
2275 : : {
2276 : 15 : out << "(" << std::endl;
2277 [ + + ]: 40 : for (const std::pair<const cvc5::Term, cvc5::Term>& d : d_result)
2278 : : {
2279 : 25 : out << "(";
2280 : : // use name if it has one
2281 : 25 : std::string name;
2282 [ + + ]: 25 : if (d_sm->getExpressionName(d.first, name, true))
2283 : : {
2284 : 1 : out << name;
2285 : : }
2286 : : else
2287 : : {
2288 : 24 : out << d.first;
2289 : : }
2290 : 25 : out << " " << d.second << ")" << std::endl;
2291 : 25 : }
2292 : 15 : out << ")" << std::endl;
2293 : 15 : }
2294 : :
2295 : 0 : const std::map<cvc5::Term, cvc5::Term>& GetDifficultyCommand::getDifficultyMap()
2296 : : const
2297 : : {
2298 : 0 : return d_result;
2299 : : }
2300 : :
2301 : 0 : std::string GetDifficultyCommand::getCommandName() const
2302 : : {
2303 : 0 : return "get-difficulty";
2304 : : }
2305 : :
2306 : 3 : void GetDifficultyCommand::toStream(std::ostream& out) const
2307 : : {
2308 : 3 : internal::Printer::getPrinter(out)->toStreamCmdGetDifficulty(out);
2309 : 3 : }
2310 : :
2311 : : /* -------------------------------------------------------------------------- */
2312 : : /* class GetTimeoutCoreCommand */
2313 : : /* -------------------------------------------------------------------------- */
2314 : :
2315 : 27 : GetTimeoutCoreCommand::GetTimeoutCoreCommand()
2316 : 27 : : d_solver(nullptr), d_sm(nullptr), d_assumptions()
2317 : : {
2318 : 27 : }
2319 : 16 : GetTimeoutCoreCommand::GetTimeoutCoreCommand(
2320 : 16 : const std::vector<Term>& assumptions)
2321 : 16 : : d_solver(nullptr), d_sm(nullptr), d_assumptions(assumptions)
2322 : : {
2323 : : // providing an empty list of assumptions will make us call getTimeoutCore
2324 : : // below instead of getTimeoutCoreAssuming.
2325 [ - + ][ - + ]: 16 : Assert(!d_assumptions.empty());
[ - - ]
2326 : 16 : }
2327 : 25 : void GetTimeoutCoreCommand::invoke(cvc5::Solver* solver, SymManager* sm)
2328 : : {
2329 : : try
2330 : : {
2331 : 25 : d_sm = sm;
2332 : 25 : d_solver = solver;
2333 [ + + ]: 25 : if (!d_assumptions.empty())
2334 : : {
2335 : 10 : d_result = solver->getTimeoutCoreAssuming(d_assumptions);
2336 : : }
2337 : : else
2338 : : {
2339 : 15 : d_result = solver->getTimeoutCore();
2340 : : }
2341 : 25 : d_commandStatus = CommandSuccess::instance();
2342 : : }
2343 [ - - ][ - ]: 0 : catch (cvc5::CVC5ApiRecoverableException& e)
2344 : : {
2345 : 0 : d_commandStatus = new CommandRecoverableFailure(e.what());
2346 : 0 : }
2347 : 0 : catch (exception& e)
2348 : : {
2349 : 0 : d_commandStatus = new CommandFailure(e.what());
2350 : 0 : }
2351 : 25 : }
2352 : :
2353 : 25 : void GetTimeoutCoreCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
2354 : : std::ostream& out) const
2355 : : {
2356 : 25 : cvc5::Result res = d_result.first;
2357 : 25 : out << res << std::endl;
2358 : 25 : if (res.isUnsat()
2359 [ + + ][ + + ]: 29 : || (res.isUnknown()
[ + + ]
2360 [ + - ]: 4 : && res.getUnknownExplanation() == UnknownExplanation::TIMEOUT))
2361 : : {
2362 [ + + ]: 17 : if (d_solver->getOption("print-cores-full") == "true")
2363 : : {
2364 : : // use the assertions
2365 : 4 : internal::UnsatCore ucr(termVectorToNodes(d_result.second));
2366 : 4 : ucr.toStream(out);
2367 : 4 : }
2368 : : else
2369 : : {
2370 : : // otherwise, use the names
2371 : 13 : std::vector<std::string> names;
2372 : 13 : d_sm->getExpressionNames(d_result.second, names, true);
2373 : 13 : internal::UnsatCore ucr(names);
2374 : 13 : ucr.toStream(out);
2375 : 13 : }
2376 : : }
2377 : 25 : }
2378 : 0 : cvc5::Result GetTimeoutCoreCommand::getResult() const { return d_result.first; }
2379 : 0 : const std::vector<cvc5::Term>& GetTimeoutCoreCommand::getTimeoutCore() const
2380 : : {
2381 : 0 : return d_result.second;
2382 : : }
2383 : :
2384 : 0 : std::string GetTimeoutCoreCommand::getCommandName() const
2385 : : {
2386 : 0 : return d_assumptions.empty() ? "get-timeout-core"
2387 [ - - ]: 0 : : "get-timeout-core-assuming";
2388 : : }
2389 : :
2390 : 9 : void GetTimeoutCoreCommand::toStream(std::ostream& out) const
2391 : : {
2392 [ + + ]: 9 : if (d_assumptions.empty())
2393 : : {
2394 : 6 : internal::Printer::getPrinter(out)->toStreamCmdGetTimeoutCore(out);
2395 : : }
2396 : : else
2397 : : {
2398 : 6 : internal::Printer::getPrinter(out)->toStreamCmdGetTimeoutCoreAssuming(
2399 : 6 : out, termVectorToNodes(d_assumptions));
2400 : : }
2401 : 9 : }
2402 : :
2403 : : /* -------------------------------------------------------------------------- */
2404 : : /* class GetLearnedLiteralsCommand */
2405 : : /* -------------------------------------------------------------------------- */
2406 : :
2407 : 28 : GetLearnedLiteralsCommand::GetLearnedLiteralsCommand(modes::LearnedLitType t)
2408 : 28 : : d_type(t)
2409 : : {
2410 : 28 : }
2411 : 14 : void GetLearnedLiteralsCommand::invoke(cvc5::Solver* solver,
2412 : : CVC5_UNUSED SymManager* sm)
2413 : : {
2414 : : try
2415 : : {
2416 : 14 : d_result = solver->getLearnedLiterals(d_type);
2417 : :
2418 : 14 : d_commandStatus = CommandSuccess::instance();
2419 : : }
2420 [ - - ][ - ]: 0 : catch (cvc5::CVC5ApiRecoverableException& e)
2421 : : {
2422 : 0 : d_commandStatus = new CommandRecoverableFailure(e.what());
2423 : 0 : }
2424 : 0 : catch (exception& e)
2425 : : {
2426 : 0 : d_commandStatus = new CommandFailure(e.what());
2427 : 0 : }
2428 : 14 : }
2429 : :
2430 : 14 : void GetLearnedLiteralsCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
2431 : : std::ostream& out) const
2432 : : {
2433 : 14 : out << "(" << std::endl;
2434 [ + + ]: 26 : for (const cvc5::Term& lit : d_result)
2435 : : {
2436 : 12 : out << lit << std::endl;
2437 : : }
2438 : 14 : out << ")" << std::endl;
2439 : 14 : }
2440 : :
2441 : 0 : const std::vector<cvc5::Term>& GetLearnedLiteralsCommand::getLearnedLiterals()
2442 : : const
2443 : : {
2444 : 0 : return d_result;
2445 : : }
2446 : :
2447 : 0 : std::string GetLearnedLiteralsCommand::getCommandName() const
2448 : : {
2449 : 0 : return "get-learned-literals";
2450 : : }
2451 : :
2452 : 7 : void GetLearnedLiteralsCommand::toStream(std::ostream& out) const
2453 : : {
2454 : 7 : internal::Printer::getPrinter(out)->toStreamCmdGetLearnedLiterals(out,
2455 : 7 : d_type);
2456 : 7 : }
2457 : :
2458 : : /* -------------------------------------------------------------------------- */
2459 : : /* class GetAssertionsCommand */
2460 : : /* -------------------------------------------------------------------------- */
2461 : :
2462 : 4 : GetAssertionsCommand::GetAssertionsCommand() {}
2463 : 2 : void GetAssertionsCommand::invoke(cvc5::Solver* solver,
2464 : : CVC5_UNUSED SymManager* sm)
2465 : : {
2466 : : try
2467 : : {
2468 : 2 : stringstream ss;
2469 : 2 : const vector<cvc5::Term> v = solver->getAssertions();
2470 : 2 : ss << "(\n";
2471 : 2 : copy(v.begin(), v.end(), ostream_iterator<cvc5::Term>(ss, "\n"));
2472 : 2 : ss << ")\n";
2473 : 2 : d_result = ss.str();
2474 : 2 : d_commandStatus = CommandSuccess::instance();
2475 : 2 : }
2476 [ - - ]: 0 : catch (exception& e)
2477 : : {
2478 : 0 : d_commandStatus = new CommandFailure(e.what());
2479 : 0 : }
2480 : 2 : }
2481 : :
2482 : 0 : std::string GetAssertionsCommand::getResult() const { return d_result; }
2483 : 2 : void GetAssertionsCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
2484 : : std::ostream& out) const
2485 : : {
2486 : 2 : out << d_result;
2487 : 2 : }
2488 : :
2489 : 0 : std::string GetAssertionsCommand::getCommandName() const
2490 : : {
2491 : 0 : return "get-assertions";
2492 : : }
2493 : :
2494 : 1 : void GetAssertionsCommand::toStream(std::ostream& out) const
2495 : : {
2496 : 1 : internal::Printer::getPrinter(out)->toStreamCmdGetAssertions(out);
2497 : 1 : }
2498 : :
2499 : : /* -------------------------------------------------------------------------- */
2500 : : /* class SetBenchmarkLogicCommand */
2501 : : /* -------------------------------------------------------------------------- */
2502 : :
2503 : 24844 : SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic)
2504 : 24844 : : d_logic(logic)
2505 : : {
2506 : 24844 : }
2507 : :
2508 : 2 : std::string SetBenchmarkLogicCommand::getLogic() const { return d_logic; }
2509 : 24842 : void SetBenchmarkLogicCommand::invoke(cvc5::Solver* solver, SymManager* sm)
2510 : : {
2511 : : try
2512 : : {
2513 : 24842 : sm->setLogic(d_logic);
2514 : 24842 : solver->setLogic(d_logic);
2515 : 24842 : d_commandStatus = CommandSuccess::instance();
2516 : : }
2517 [ - - ]: 0 : catch (exception& e)
2518 : : {
2519 : 0 : d_commandStatus = new CommandFailure(e.what());
2520 : 0 : }
2521 : 24842 : }
2522 : :
2523 : 0 : std::string SetBenchmarkLogicCommand::getCommandName() const
2524 : : {
2525 : 0 : return "set-logic";
2526 : : }
2527 : :
2528 : 4370 : void SetBenchmarkLogicCommand::toStream(std::ostream& out) const
2529 : : {
2530 : 4370 : internal::Printer::getPrinter(out)->toStreamCmdSetBenchmarkLogic(out,
2531 : 4370 : d_logic);
2532 : 4370 : }
2533 : :
2534 : : /* -------------------------------------------------------------------------- */
2535 : : /* class SetInfoCommand */
2536 : : /* -------------------------------------------------------------------------- */
2537 : :
2538 : 19242 : SetInfoCommand::SetInfoCommand(const std::string& flag,
2539 : 19242 : const std::string& value)
2540 : 19242 : : d_flag(flag), d_value(value)
2541 : : {
2542 : 19242 : }
2543 : :
2544 : 0 : const std::string& SetInfoCommand::getFlag() const { return d_flag; }
2545 : 0 : const std::string& SetInfoCommand::getValue() const { return d_value; }
2546 : 12841 : void SetInfoCommand::invoke(cvc5::Solver* solver, CVC5_UNUSED SymManager* sm)
2547 : : {
2548 : : try
2549 : : {
2550 : 12841 : solver->setInfo(d_flag, d_value);
2551 : 12800 : d_commandStatus = CommandSuccess::instance();
2552 : : }
2553 [ - + ][ - - ]: 41 : catch (cvc5::CVC5ApiUnsupportedException&)
2554 : : {
2555 : : // As per SMT-LIB spec, silently accept unknown set-info keys
2556 : 41 : d_commandStatus = CommandSuccess::instance();
2557 : 41 : }
2558 : 0 : catch (cvc5::CVC5ApiRecoverableException& e)
2559 : : {
2560 : 0 : d_commandStatus = new CommandRecoverableFailure(e.getMessage());
2561 : 0 : }
2562 : 0 : catch (exception& e)
2563 : : {
2564 : 0 : d_commandStatus = new CommandFailure(e.what());
2565 : 0 : }
2566 : 12841 : }
2567 : :
2568 : 0 : std::string SetInfoCommand::getCommandName() const { return "set-info"; }
2569 : :
2570 : 3200 : void SetInfoCommand::toStream(std::ostream& out) const
2571 : : {
2572 : 3200 : internal::Printer::getPrinter(out)->toStreamCmdSetInfo(out, d_flag, d_value);
2573 : 3200 : }
2574 : :
2575 : : /* -------------------------------------------------------------------------- */
2576 : : /* class GetInfoCommand */
2577 : : /* -------------------------------------------------------------------------- */
2578 : :
2579 : 50 : GetInfoCommand::GetInfoCommand(std::string flag) : d_flag(flag) {}
2580 : 0 : std::string GetInfoCommand::getFlag() const { return d_flag; }
2581 : 34 : void GetInfoCommand::invoke(cvc5::Solver* solver, CVC5_UNUSED SymManager* sm)
2582 : : {
2583 : : try
2584 : : {
2585 : 34 : TermManager& tm = solver->getTermManager();
2586 : 34 : std::vector<cvc5::Term> v;
2587 : 34 : Sort bt = tm.getBooleanSort();
2588 : 34 : v.push_back(tm.mkVar(bt, ":" + d_flag));
2589 : 34 : v.push_back(tm.mkVar(bt, solver->getInfo(d_flag)));
2590 : 23 : d_result = sexprToString(tm.mkTerm(cvc5::Kind::SEXPR, {v}));
2591 : 23 : d_commandStatus = CommandSuccess::instance();
2592 : 45 : }
2593 [ - + ][ + - ]: 11 : catch (cvc5::CVC5ApiUnsupportedException&)
2594 : : {
2595 : 7 : d_commandStatus = new CommandUnsupported();
2596 : 7 : }
2597 : 4 : catch (cvc5::CVC5ApiRecoverableException& e)
2598 : : {
2599 : 4 : d_commandStatus = new CommandRecoverableFailure(e.getMessage());
2600 : 4 : }
2601 : 0 : catch (exception& e)
2602 : : {
2603 : 0 : d_commandStatus = new CommandFailure(e.what());
2604 : 0 : }
2605 : 34 : }
2606 : :
2607 : 0 : std::string GetInfoCommand::getResult() const { return d_result; }
2608 : 23 : void GetInfoCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
2609 : : std::ostream& out) const
2610 : : {
2611 [ + - ]: 23 : if (d_result != "")
2612 : : {
2613 : 23 : out << d_result << endl;
2614 : : }
2615 : 23 : }
2616 : :
2617 : 0 : std::string GetInfoCommand::getCommandName() const { return "get-info"; }
2618 : :
2619 : 18 : void GetInfoCommand::toStream(std::ostream& out) const
2620 : : {
2621 : 18 : internal::Printer::getPrinter(out)->toStreamCmdGetInfo(out, d_flag);
2622 : 18 : }
2623 : :
2624 : : /* -------------------------------------------------------------------------- */
2625 : : /* class SetOptionCommand */
2626 : : /* -------------------------------------------------------------------------- */
2627 : :
2628 : 7813 : SetOptionCommand::SetOptionCommand(const std::string& flag,
2629 : 7813 : const std::string& value)
2630 : 7813 : : d_flag(flag), d_value(value)
2631 : : {
2632 : 7813 : }
2633 : :
2634 : 0 : const std::string& SetOptionCommand::getFlag() const { return d_flag; }
2635 : 0 : const std::string& SetOptionCommand::getValue() const { return d_value; }
2636 : 4911 : void SetOptionCommand::invoke(cvc5::Solver* solver, CVC5_UNUSED SymManager* sm)
2637 : : {
2638 : : try
2639 : : {
2640 : 4911 : solver->setOption(d_flag, d_value);
2641 : 4898 : d_commandStatus = CommandSuccess::instance();
2642 : : }
2643 [ - + ][ + + ]: 13 : catch (cvc5::CVC5ApiUnsupportedException&)
2644 : : {
2645 : 1 : d_commandStatus = new CommandUnsupported();
2646 : 1 : }
2647 : 7 : catch (cvc5::CVC5ApiRecoverableException& e)
2648 : : {
2649 : 7 : d_commandStatus = new CommandRecoverableFailure(e.getMessage());
2650 : 7 : }
2651 : 5 : catch (exception& e)
2652 : : {
2653 : 5 : d_commandStatus = new CommandFailure(e.what());
2654 : 5 : }
2655 : 4911 : }
2656 : :
2657 : 0 : std::string SetOptionCommand::getCommandName() const { return "set-option"; }
2658 : :
2659 : 1451 : void SetOptionCommand::toStream(std::ostream& out) const
2660 : : {
2661 : 1451 : internal::Printer::getPrinter(out)->toStreamCmdSetOption(
2662 : 1451 : out, d_flag, d_value);
2663 : 1451 : }
2664 : :
2665 : : /* -------------------------------------------------------------------------- */
2666 : : /* class GetOptionCommand */
2667 : : /* -------------------------------------------------------------------------- */
2668 : :
2669 : 138 : GetOptionCommand::GetOptionCommand(std::string flag) : d_flag(flag) {}
2670 : 0 : std::string GetOptionCommand::getFlag() const { return d_flag; }
2671 : 50 : void GetOptionCommand::invoke(cvc5::Solver* solver, CVC5_UNUSED SymManager* sm)
2672 : : {
2673 : : try
2674 : : {
2675 : 50 : d_result = solver->getOption(d_flag);
2676 : 49 : d_commandStatus = CommandSuccess::instance();
2677 : : }
2678 [ - + ][ - ]: 1 : catch (cvc5::CVC5ApiUnsupportedException&)
2679 : : {
2680 : 1 : d_commandStatus = new CommandUnsupported();
2681 : 1 : }
2682 : 0 : catch (exception& e)
2683 : : {
2684 : 0 : d_commandStatus = new CommandFailure(e.what());
2685 : 0 : }
2686 : 50 : }
2687 : :
2688 : 0 : std::string GetOptionCommand::getResult() const { return d_result; }
2689 : 49 : void GetOptionCommand::printResult(CVC5_UNUSED cvc5::Solver* solver,
2690 : : std::ostream& out) const
2691 : : {
2692 [ + - ]: 49 : if (d_result != "")
2693 : : {
2694 : 49 : out << d_result << endl;
2695 : : }
2696 : 49 : }
2697 : :
2698 : 0 : std::string GetOptionCommand::getCommandName() const { return "get-option"; }
2699 : :
2700 : 44 : void GetOptionCommand::toStream(std::ostream& out) const
2701 : : {
2702 : 44 : internal::Printer::getPrinter(out)->toStreamCmdGetOption(out, d_flag);
2703 : 44 : }
2704 : :
2705 : : /* -------------------------------------------------------------------------- */
2706 : : /* class DatatypeDeclarationCommand */
2707 : : /* -------------------------------------------------------------------------- */
2708 : :
2709 : 0 : DatatypeDeclarationCommand::DatatypeDeclarationCommand(
2710 : 0 : const cvc5::Sort& datatype)
2711 : 0 : : d_datatypes()
2712 : : {
2713 : 0 : d_datatypes.push_back(datatype);
2714 : 0 : }
2715 : :
2716 : 3929 : DatatypeDeclarationCommand::DatatypeDeclarationCommand(
2717 : 3929 : const std::vector<cvc5::Sort>& datatypes)
2718 : 3929 : : d_datatypes(datatypes)
2719 : : {
2720 : 3929 : }
2721 : :
2722 : 0 : const std::vector<cvc5::Sort>& DatatypeDeclarationCommand::getDatatypes() const
2723 : : {
2724 : 0 : return d_datatypes;
2725 : : }
2726 : :
2727 : 3929 : void DatatypeDeclarationCommand::invoke(cvc5::Solver* solver, SymManager* sm)
2728 : : {
2729 : : // Implement the bindings. We bind tester names is-C if strict parsing is
2730 : : // disabled.
2731 : 3929 : bool bindTesters = solver->getOption("strict-parsing") != "true";
2732 [ - + ]: 3929 : if (!sm->bindMutualDatatypeTypes(d_datatypes, bindTesters))
2733 : : {
2734 : : // this should generally never happen since we look ahead to check whether
2735 : : // binding will succeed in Parser::mkMutualDatatypeTypes.
2736 : 0 : std::stringstream ss;
2737 : : ss << "Failed to implement bindings for symbols in definition of datatype "
2738 : 0 : "in block containing "
2739 : 0 : << d_datatypes[0];
2740 : 0 : d_commandStatus = new CommandFailure(ss.str());
2741 : 0 : }
2742 : : else
2743 : : {
2744 : 3929 : d_commandStatus = CommandSuccess::instance();
2745 : : }
2746 : 3929 : }
2747 : :
2748 : 0 : std::string DatatypeDeclarationCommand::getCommandName() const
2749 : : {
2750 : 0 : return "declare-datatypes";
2751 : : }
2752 : :
2753 : 690 : void DatatypeDeclarationCommand::toStream(std::ostream& out) const
2754 : : {
2755 : 1380 : internal::Printer::getPrinter(out)->toStreamCmdDatatypeDeclaration(
2756 : 1380 : out, sortVectorToTypeNodes(d_datatypes));
2757 : 690 : }
2758 : :
2759 : : } // namespace cvc5::parser
|
