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