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