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