Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Implementation of the command pattern on SolverEngines.
11 : : *
12 : : * Command objects are generated by the parser (typically) to implement the
13 : : * commands in parsed input (see Parser::parseNextCommand()), or by client
14 : : * code.
15 : : */
16 : :
17 : : #include "cvc5_public.h"
18 : :
19 : : #ifndef CVC5__PARSER__COMMANDS_H
20 : : #define CVC5__PARSER__COMMANDS_H
21 : :
22 : : #include <cvc5/cvc5.h>
23 : :
24 : : #include <iosfwd>
25 : : #include <sstream>
26 : : #include <string>
27 : : #include <vector>
28 : :
29 : : #include "options/language.h"
30 : :
31 : : namespace cvc5 {
32 : :
33 : : class TermManager;
34 : : class Solver;
35 : : class Term;
36 : :
37 : : namespace main {
38 : : class CommandExecutor;
39 : : }
40 : :
41 : : namespace parser {
42 : :
43 : : class CommandStatus;
44 : : class SymManager;
45 : :
46 : : /**
47 : : * Convert a symbolic expression to string. This method differs from
48 : : * Term::toString in that it does not depend on the output language.
49 : : *
50 : : * @param sexpr the symbolic expression to convert
51 : : * @return the symbolic expression as string
52 : : */
53 : : std::string sexprToString(cvc5::Term sexpr) CVC5_EXPORT;
54 : :
55 : : /**
56 : : * Encapsulation of a command.
57 : : *
58 : : * Commands are constructed by the input parser and can be invoked on
59 : : * the solver and symbol manager.
60 : : */
61 : : class CVC5_EXPORT Cmd
62 : : {
63 : : friend class main::CommandExecutor;
64 : :
65 : : public:
66 : : Cmd();
67 : : Cmd(const Cmd& cmd);
68 : :
69 : : virtual ~Cmd();
70 : :
71 : : /**
72 : : * Invoke the command on the solver and symbol manager sm.
73 : : */
74 : : virtual void invoke(cvc5::Solver* solver, parser::SymManager* sm) = 0;
75 : : /**
76 : : * Same as above, and prints the result to output stream out.
77 : : */
78 : : virtual void invoke(cvc5::Solver* solver,
79 : : parser::SymManager* sm,
80 : : std::ostream& out);
81 : : /**
82 : : * Same as invoke, but prints the result to the output stream associated to
83 : : * the solver.
84 : : */
85 : : virtual void invokeAndPrintResult(cvc5::Solver* solver,
86 : : parser::SymManager* sm);
87 : :
88 : : /**
89 : : * @return A string representation of this result.
90 : : */
91 : : std::string toString() const;
92 : :
93 : : /**
94 : : * Get the name for this command, e.g. "assert".
95 : : *
96 : : * @return The name of this command.
97 : : */
98 : : virtual std::string getCommandName() const = 0;
99 : :
100 : : /**
101 : : * Either the command hasn't run yet, or it completed successfully
102 : : * (CommandSuccess, not CommandUnsupported or CommandFailure).
103 : : *
104 : : * @return Whether the command was successfully invoked.
105 : : */
106 : : bool ok() const;
107 : :
108 : : /**
109 : : * The command completed in a failure state (CommandFailure, not
110 : : * CommandSuccess or CommandUnsupported).
111 : : *
112 : : * @return Whether the command failed.
113 : : */
114 : : bool fail() const;
115 : :
116 : : /**
117 : : * The command was ran but was interrupted due to resource limiting.
118 : : *
119 : : * @return Whether the command was interrupted.
120 : : */
121 : : bool interrupted() const;
122 : :
123 : : protected:
124 : : virtual void toStream(std::ostream& out) const = 0;
125 : : /**
126 : : * This field contains a command status if the command has been
127 : : * invoked, or NULL if it has not. This field is either a
128 : : * dynamically-allocated pointer, or it's a pointer to the singleton
129 : : * CommandSuccess instance. Doing so is somewhat asymmetric, but
130 : : * it avoids the need to dynamically allocate memory in the common
131 : : * case of a successful command.
132 : : */
133 : : const CommandStatus* d_commandStatus;
134 : : /**
135 : : * Print the result of running the command. This method is only called if the
136 : : * command ran successfully.
137 : : */
138 : : virtual void printResult(cvc5::Solver* solver, std::ostream& out) const;
139 : : /**
140 : : * Reset the given solver in-place (keep the object at the same memory
141 : : * location).
142 : : */
143 : : static void resetSolver(cvc5::Solver* solver);
144 : :
145 : : // These methods rely on Command being a friend of classes in the API.
146 : : // Subclasses of command should use these methods for conversions,
147 : : // which is currently necessary for e.g. printing commands.
148 : : /** Helper to convert a Term to an internal internal::Node */
149 : : static internal::Node termToNode(const cvc5::Term& term);
150 : : /** Helper to convert a vector of Terms to internal Nodes. */
151 : : static std::vector<internal::Node> termVectorToNodes(
152 : : const std::vector<cvc5::Term>& terms);
153 : : /** Helper to convert a Sort to an internal internal::TypeNode */
154 : : static internal::TypeNode sortToTypeNode(const cvc5::Sort& sort);
155 : : /** Helper to convert a vector of Sorts to internal TypeNodes. */
156 : : static std::vector<internal::TypeNode> sortVectorToTypeNodes(
157 : : const std::vector<cvc5::Sort>& sorts);
158 : : /** Helper to convert a Grammar to an internal internal::TypeNode */
159 : : static internal::TypeNode grammarToTypeNode(cvc5::Grammar* grammar);
160 : : }; /* class Command */
161 : :
162 : : /**
163 : : * EmptyCommands are the residue of a command after the parser handles
164 : : * them (and there's nothing left to do).
165 : : */
166 : : class CVC5_EXPORT EmptyCommand : public Cmd
167 : : {
168 : : public:
169 : : EmptyCommand(std::string name = "");
170 : : std::string getName() const;
171 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
172 : : std::string getCommandName() const override;
173 : : void toStream(std::ostream& out) const override;
174 : :
175 : : protected:
176 : : std::string d_name;
177 : : }; /* class EmptyCommand */
178 : :
179 : : class CVC5_EXPORT EchoCommand : public Cmd
180 : : {
181 : : public:
182 : : EchoCommand(std::string output = "");
183 : :
184 : : std::string getOutput() const;
185 : :
186 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
187 : : /** The result is the printed string */
188 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
189 : :
190 : : std::string getCommandName() const override;
191 : : void toStream(std::ostream& out) const override;
192 : :
193 : : protected:
194 : : std::string d_output;
195 : : }; /* class EchoCommand */
196 : :
197 : : class CVC5_EXPORT AssertCommand : public Cmd
198 : : {
199 : : protected:
200 : : cvc5::Term d_term;
201 : :
202 : : public:
203 : : AssertCommand(const cvc5::Term& t);
204 : :
205 : : cvc5::Term getTerm() const;
206 : :
207 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
208 : :
209 : : std::string getCommandName() const override;
210 : : void toStream(std::ostream& out) const override;
211 : : }; /* class AssertCommand */
212 : :
213 : : class CVC5_EXPORT PushCommand : public Cmd
214 : : {
215 : : public:
216 : : PushCommand(uint32_t nscopes);
217 : :
218 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
219 : : std::string getCommandName() const override;
220 : : void toStream(std::ostream& out) const override;
221 : :
222 : : private:
223 : : uint32_t d_nscopes;
224 : : }; /* class PushCommand */
225 : :
226 : : class CVC5_EXPORT PopCommand : public Cmd
227 : : {
228 : : public:
229 : : PopCommand(uint32_t nscopes);
230 : :
231 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
232 : : std::string getCommandName() const override;
233 : : void toStream(std::ostream& out) const override;
234 : :
235 : : private:
236 : : uint32_t d_nscopes;
237 : : }; /* class PopCommand */
238 : :
239 : : class CVC5_EXPORT DeclarationDefinitionCommand : public Cmd
240 : : {
241 : : protected:
242 : : std::string d_symbol;
243 : : /**
244 : : * Bind the symbol of this command to the given term. Return false if the
245 : : * binding was invalid. In this case, set command status to CommandFailure.
246 : : */
247 : : bool bindToTerm(parser::SymManager* sm, cvc5::Term t, bool doOverload);
248 : :
249 : : public:
250 : : DeclarationDefinitionCommand(const std::string& id);
251 : :
252 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override = 0;
253 : : std::string getSymbol() const;
254 : : }; /* class DeclarationDefinitionCommand */
255 : :
256 : : class CVC5_EXPORT DeclareFunctionCommand : public DeclarationDefinitionCommand
257 : : {
258 : : protected:
259 : : std::vector<Sort> d_argSorts;
260 : : cvc5::Sort d_sort;
261 : :
262 : : public:
263 : : DeclareFunctionCommand(const std::string& id,
264 : : const std::vector<Sort>& argSorts,
265 : : cvc5::Sort sort);
266 : : std::vector<Sort> getArgSorts() const;
267 : : cvc5::Sort getSort() const;
268 : :
269 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
270 : : std::string getCommandName() const override;
271 : : void toStream(std::ostream& out) const override;
272 : : }; /* class DeclareFunctionCommand */
273 : :
274 : : class CVC5_EXPORT DeclarePoolCommand : public DeclarationDefinitionCommand
275 : : {
276 : : protected:
277 : : cvc5::Sort d_sort;
278 : : std::vector<cvc5::Term> d_initValue;
279 : :
280 : : public:
281 : : DeclarePoolCommand(const std::string& id,
282 : : cvc5::Sort sort,
283 : : const std::vector<cvc5::Term>& initValue);
284 : : cvc5::Sort getSort() const;
285 : : const std::vector<cvc5::Term>& getInitialValue() const;
286 : :
287 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
288 : : std::string getCommandName() const override;
289 : : void toStream(std::ostream& out) const override;
290 : : }; /* class DeclarePoolCommand */
291 : :
292 : : class CVC5_EXPORT DeclareOracleFunCommand : public Cmd
293 : : {
294 : : public:
295 : : DeclareOracleFunCommand(const std::string& id,
296 : : const std::vector<Sort>& argSorts,
297 : : Sort sort);
298 : : DeclareOracleFunCommand(const std::string& id,
299 : : const std::vector<Sort>& argSorts,
300 : : Sort sort,
301 : : const std::string& binName);
302 : : const std::string& getIdentifier() const;
303 : : std::vector<Sort> getArgSorts() const;
304 : : Sort getSort() const;
305 : : const std::string& getBinaryName() const;
306 : :
307 : : void invoke(Solver* solver, parser::SymManager* sm) override;
308 : : std::string getCommandName() const override;
309 : : void toStream(std::ostream& out) const override;
310 : :
311 : : protected:
312 : : /** The identifier */
313 : : std::string d_id;
314 : : /** Argument sorts */
315 : : std::vector<Sort> d_argSorts;
316 : : /** The return sort */
317 : : Sort d_sort;
318 : : /** The binary name, or "" if none is provided */
319 : : std::string d_binName;
320 : : };
321 : :
322 : : class CVC5_EXPORT DeclareSortCommand : public DeclarationDefinitionCommand
323 : : {
324 : : protected:
325 : : size_t d_arity;
326 : :
327 : : public:
328 : : DeclareSortCommand(const std::string& id, size_t arity);
329 : :
330 : : size_t getArity() const;
331 : :
332 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
333 : : std::string getCommandName() const override;
334 : : void toStream(std::ostream& out) const override;
335 : : }; /* class DeclareSortCommand */
336 : :
337 : : class CVC5_EXPORT DefineSortCommand : public DeclarationDefinitionCommand
338 : : {
339 : : protected:
340 : : std::vector<cvc5::Sort> d_params;
341 : : cvc5::Sort d_sort;
342 : :
343 : : public:
344 : : DefineSortCommand(const std::string& id, cvc5::Sort sort);
345 : : DefineSortCommand(const std::string& id,
346 : : const std::vector<cvc5::Sort>& params,
347 : : cvc5::Sort sort);
348 : :
349 : : const std::vector<cvc5::Sort>& getParameters() const;
350 : : cvc5::Sort getSort() const;
351 : :
352 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
353 : : std::string getCommandName() const override;
354 : : void toStream(std::ostream& out) const override;
355 : : }; /* class DefineSortCommand */
356 : :
357 : : class CVC5_EXPORT DefineFunctionCommand : public DeclarationDefinitionCommand
358 : : {
359 : : public:
360 : : DefineFunctionCommand(const std::string& id,
361 : : cvc5::Sort sort,
362 : : cvc5::Term formula);
363 : : DefineFunctionCommand(const std::string& id,
364 : : const std::vector<cvc5::Term>& formals,
365 : : cvc5::Sort sort,
366 : : cvc5::Term formula);
367 : :
368 : : const std::vector<cvc5::Term>& getFormals() const;
369 : : cvc5::Sort getSort() const;
370 : : cvc5::Term getFormula() const;
371 : :
372 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
373 : : std::string getCommandName() const override;
374 : : void toStream(std::ostream& out) const override;
375 : :
376 : : protected:
377 : : /** The formal arguments for the function we are defining */
378 : : std::vector<cvc5::Term> d_formals;
379 : : /** The co-domain sort of the function we are defining */
380 : : cvc5::Sort d_sort;
381 : : /** The formula corresponding to the body of the function we are defining */
382 : : cvc5::Term d_formula;
383 : : }; /* class DefineFunctionCommand */
384 : :
385 : : /**
386 : : * The command when parsing define-fun-rec or define-funs-rec.
387 : : * This command will assert a set of quantified formulas that specify
388 : : * the (mutually recursive) function definitions provided to it.
389 : : */
390 : : class CVC5_EXPORT DefineFunctionRecCommand : public Cmd
391 : : {
392 : : public:
393 : : DefineFunctionRecCommand(cvc5::Term func,
394 : : const std::vector<cvc5::Term>& formals,
395 : : cvc5::Term formula);
396 : : DefineFunctionRecCommand(const std::vector<cvc5::Term>& funcs,
397 : : const std::vector<std::vector<cvc5::Term>>& formals,
398 : : const std::vector<cvc5::Term>& formula);
399 : :
400 : : const std::vector<cvc5::Term>& getFunctions() const;
401 : : const std::vector<std::vector<cvc5::Term>>& getFormals() const;
402 : : const std::vector<cvc5::Term>& getFormulas() const;
403 : :
404 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
405 : : std::string getCommandName() const override;
406 : : void toStream(std::ostream& out) const override;
407 : :
408 : : protected:
409 : : /** functions we are defining */
410 : : std::vector<cvc5::Term> d_funcs;
411 : : /** formal arguments for each of the functions we are defining */
412 : : std::vector<std::vector<cvc5::Term>> d_formals;
413 : : /** formulas corresponding to the bodies of the functions we are defining */
414 : : std::vector<cvc5::Term> d_formulas;
415 : : }; /* class DefineFunctionRecCommand */
416 : :
417 : : /**
418 : : * In separation logic inputs, which is an extension of smt2 inputs, this
419 : : * corresponds to the command:
420 : : * (declare-heap (T U))
421 : : * where T is the location sort and U is the data sort.
422 : : */
423 : : class CVC5_EXPORT DeclareHeapCommand : public Cmd
424 : : {
425 : : public:
426 : : DeclareHeapCommand(cvc5::Sort locSort, cvc5::Sort dataSort);
427 : : cvc5::Sort getLocationSort() const;
428 : : cvc5::Sort getDataSort() const;
429 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
430 : : std::string getCommandName() const override;
431 : : void toStream(std::ostream& out) const override;
432 : :
433 : : protected:
434 : : /** The location sort */
435 : : cvc5::Sort d_locSort;
436 : : /** The data sort */
437 : : cvc5::Sort d_dataSort;
438 : : };
439 : :
440 : : /**
441 : : * The command when parsing check-sat.
442 : : * This command will check satisfiability of the input formula.
443 : : */
444 : : class CVC5_EXPORT CheckSatCommand : public Cmd
445 : : {
446 : : public:
447 : : CheckSatCommand();
448 : : cvc5::Result getResult() const;
449 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
450 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
451 : : std::string getCommandName() const override;
452 : : void toStream(std::ostream& out) const override;
453 : :
454 : : private:
455 : : cvc5::Result d_result;
456 : : }; /* class CheckSatCommand */
457 : :
458 : : /**
459 : : * The command when parsing check-sat-assuming.
460 : : * This command will assume a set of formulas and check satisfiability of the
461 : : * input formula under these assumptions.
462 : : */
463 : : class CVC5_EXPORT CheckSatAssumingCommand : public Cmd
464 : : {
465 : : public:
466 : : CheckSatAssumingCommand(cvc5::Term term);
467 : : CheckSatAssumingCommand(const std::vector<cvc5::Term>& terms);
468 : :
469 : : const std::vector<cvc5::Term>& getTerms() const;
470 : : cvc5::Result getResult() const;
471 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
472 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
473 : : std::string getCommandName() const override;
474 : : void toStream(std::ostream& out) const override;
475 : :
476 : : private:
477 : : std::vector<cvc5::Term> d_terms;
478 : : cvc5::Result d_result;
479 : : }; /* class CheckSatAssumingCommand */
480 : :
481 : : /* ------------------- sygus commands ------------------ */
482 : :
483 : : /** Declares a sygus universal variable */
484 : : class CVC5_EXPORT DeclareSygusVarCommand : public DeclarationDefinitionCommand
485 : : {
486 : : public:
487 : : DeclareSygusVarCommand(const std::string& id, cvc5::Sort sort);
488 : : /** returns the declared variable */
489 : : cvc5::Term getVar() const;
490 : : /** returns the declared variable's sort */
491 : : cvc5::Sort getSort() const;
492 : : /** invokes this command
493 : : *
494 : : * The declared sygus variable is communicated to the SMT engine in case a
495 : : * synthesis conjecture is built later on.
496 : : */
497 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
498 : : /** returns this command's name */
499 : : std::string getCommandName() const override;
500 : : /** prints this command */
501 : : void toStream(std::ostream& out) const override;
502 : :
503 : : protected:
504 : : /** the declared variable's sort */
505 : : cvc5::Sort d_sort;
506 : : };
507 : :
508 : : /** Declares a sygus function-to-synthesize
509 : : *
510 : : * This command is also used for the special case in which we are declaring an
511 : : * invariant-to-synthesize
512 : : */
513 : : class CVC5_EXPORT SynthFunCommand : public DeclarationDefinitionCommand
514 : : {
515 : : public:
516 : : SynthFunCommand(const std::string& id,
517 : : const std::vector<cvc5::Term>& vars,
518 : : cvc5::Sort sort,
519 : : cvc5::Grammar* g);
520 : : /** returns the input variables of the function-to-synthesize */
521 : : const std::vector<cvc5::Term>& getVars() const;
522 : : /** returns the sygus sort of the function-to-synthesize */
523 : : cvc5::Sort getSort() const;
524 : : /** Get the sygus grammar given for the synth fun command */
525 : : const cvc5::Grammar* getGrammar() const;
526 : :
527 : : /** invokes this command
528 : : *
529 : : * The declared function-to-synthesize is communicated to the SMT engine in
530 : : * case a synthesis conjecture is built later on.
531 : : */
532 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
533 : : /** returns this command's name */
534 : : std::string getCommandName() const override;
535 : : /** prints this command */
536 : : void toStream(std::ostream& out) const override;
537 : :
538 : : protected:
539 : : /** the input variables of the function-to-synthesize */
540 : : std::vector<cvc5::Term> d_vars;
541 : : /** sort of the function-to-synthesize */
542 : : cvc5::Sort d_sort;
543 : : /** optional grammar for the possible values of the function-to-sytnhesize */
544 : : cvc5::Grammar* d_grammar;
545 : : };
546 : :
547 : : /** Declares a sygus constraint */
548 : : class CVC5_EXPORT SygusConstraintCommand : public Cmd
549 : : {
550 : : public:
551 : : SygusConstraintCommand(const cvc5::Term& t, bool isAssume = false);
552 : : /** returns the declared constraint */
553 : : cvc5::Term getTerm() const;
554 : : /** invokes this command
555 : : *
556 : : * The declared constraint is communicated to the SMT engine in case a
557 : : * synthesis conjecture is built later on.
558 : : */
559 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
560 : : /** returns this command's name */
561 : : std::string getCommandName() const override;
562 : : /** prints this command */
563 : : void toStream(std::ostream& out) const override;
564 : :
565 : : protected:
566 : : /** the declared constraint */
567 : : cvc5::Term d_term;
568 : : /** true if this is a sygus assumption */
569 : : bool d_isAssume;
570 : : };
571 : :
572 : : /** Declares a sygus invariant constraint
573 : : *
574 : : * Invarint constraints are declared in a somewhat implicit manner in the SyGuS
575 : : * language: they are declared in terms of the previously declared
576 : : * invariant-to-synthesize, precondition, transition relation and condition.
577 : : *
578 : : * The actual constraint must be built such that the invariant is not stronger
579 : : * than the precondition, not weaker than the postcondition and inductive
580 : : * w.r.t. the transition relation.
581 : : */
582 : : class CVC5_EXPORT SygusInvConstraintCommand : public Cmd
583 : : {
584 : : public:
585 : : SygusInvConstraintCommand(const std::vector<cvc5::Term>& predicates);
586 : : SygusInvConstraintCommand(const cvc5::Term& inv,
587 : : const cvc5::Term& pre,
588 : : const cvc5::Term& trans,
589 : : const cvc5::Term& post);
590 : : /** returns the place holder predicates */
591 : : const std::vector<cvc5::Term>& getPredicates() const;
592 : : /** invokes this command
593 : : *
594 : : * The place holders are communicated to the SMT engine and the actual
595 : : * invariant constraint is built, in case an actual synthesis conjecture is
596 : : * built later on.
597 : : */
598 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
599 : : /** returns this command's name */
600 : : std::string getCommandName() const override;
601 : : /** prints this command */
602 : : void toStream(std::ostream& out) const override;
603 : :
604 : : protected:
605 : : /** the place holder predicates with which to build the actual constraint
606 : : * (i.e. the invariant, precondition, transition relation and postcondition)
607 : : */
608 : : std::vector<cvc5::Term> d_predicates;
609 : : };
610 : :
611 : : /** Declares a synthesis conjecture */
612 : : class CVC5_EXPORT CheckSynthCommand : public Cmd
613 : : {
614 : : public:
615 : 950 : CheckSynthCommand(bool isNext = false) : d_isNext(isNext) {};
616 : : /** returns the result of the check-synth call */
617 : : cvc5::SynthResult getResult() const;
618 : : /** prints the result of the check-synth-call */
619 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
620 : : /** invokes this command
621 : : *
622 : : * This invocation makes the SMT engine build a synthesis conjecture based on
623 : : * previously declared information (such as universal variables,
624 : : * functions-to-synthesize and so on), set up attributes to guide the solving,
625 : : * and then perform a satisfiability check, whose result is stored in
626 : : * d_result.
627 : : */
628 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
629 : : /** returns this command's name */
630 : : std::string getCommandName() const override;
631 : : /** prints this command */
632 : : void toStream(std::ostream& out) const override;
633 : :
634 : : protected:
635 : : /** Whether this is a check-synth-next call */
636 : : bool d_isNext;
637 : : /** result of the check-synth call */
638 : : cvc5::SynthResult d_result;
639 : : /** string stream that stores the output of the solution */
640 : : std::stringstream d_solution;
641 : : };
642 : :
643 : : /** Find synth command */
644 : : class CVC5_EXPORT FindSynthCommand : public Cmd
645 : : {
646 : : public:
647 : 93 : FindSynthCommand(modes::FindSynthTarget fst, cvc5::Grammar* g)
648 : 93 : : d_fst(fst), d_grammar(g) {};
649 : : /** returns the result of the find-synth call */
650 : : Term getResult() const;
651 : : /** prints the result of the find-synth call */
652 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
653 : : /** invokes this command
654 : : */
655 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
656 : : /** returns this command's name */
657 : : std::string getCommandName() const override;
658 : : /** prints this command */
659 : : void toStream(std::ostream& out) const override;
660 : :
661 : : protected:
662 : : /** The target type */
663 : : modes::FindSynthTarget d_fst;
664 : : /** optional grammar for the possible values */
665 : : cvc5::Grammar* d_grammar;
666 : : /** result of the check-synth call */
667 : : Term d_result;
668 : : };
669 : :
670 : : /** Find synth next command */
671 : : class CVC5_EXPORT FindSynthNextCommand : public Cmd
672 : : {
673 : : public:
674 : 3 : FindSynthNextCommand() {};
675 : : /** returns the result of the find-synth call */
676 : : Term getResult() const;
677 : : /** prints the result of the find-synth call */
678 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
679 : : /** invokes this command
680 : : */
681 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
682 : : /** returns this command's name */
683 : : std::string getCommandName() const override;
684 : : /** prints this command */
685 : : void toStream(std::ostream& out) const override;
686 : :
687 : : protected:
688 : : /** result of the check-synth call */
689 : : Term d_result;
690 : : };
691 : :
692 : : /* ------------------- sygus commands ------------------ */
693 : :
694 : : // this is TRANSFORM in the CVC presentation language
695 : : class CVC5_EXPORT SimplifyCommand : public Cmd
696 : : {
697 : : protected:
698 : : cvc5::Term d_term;
699 : : cvc5::Term d_result;
700 : :
701 : : public:
702 : : SimplifyCommand(cvc5::Term term);
703 : :
704 : : cvc5::Term getTerm() const;
705 : : cvc5::Term getResult() const;
706 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
707 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
708 : : std::string getCommandName() const override;
709 : : void toStream(std::ostream& out) const override;
710 : : }; /* class SimplifyCommand */
711 : :
712 : : class CVC5_EXPORT GetValueCommand : public Cmd
713 : : {
714 : : protected:
715 : : std::vector<cvc5::Term> d_terms;
716 : : std::vector<cvc5::Term> d_result;
717 : :
718 : : public:
719 : : GetValueCommand(cvc5::Term term);
720 : : GetValueCommand(const std::vector<cvc5::Term>& terms);
721 : :
722 : : const std::vector<cvc5::Term>& getTerms() const;
723 : : const std::vector<cvc5::Term>& getResult() const;
724 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
725 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
726 : : std::string getCommandName() const override;
727 : : void toStream(std::ostream& out) const override;
728 : : }; /* class GetValueCommand */
729 : :
730 : : class CVC5_EXPORT GetModelDomainElementsCommand : public Cmd
731 : : {
732 : : protected:
733 : : cvc5::Sort d_sort;
734 : : std::vector<cvc5::Term> d_result;
735 : :
736 : : public:
737 : : GetModelDomainElementsCommand(cvc5::Sort sort);
738 : : cvc5::Sort getSort() const;
739 : : const std::vector<cvc5::Term>& getResult() const;
740 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
741 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
742 : : std::string getCommandName() const override;
743 : : void toStream(std::ostream& out) const override;
744 : : }; /* class GetModelDomainElementsCommand */
745 : :
746 : : class CVC5_EXPORT GetAssignmentCommand : public Cmd
747 : : {
748 : : protected:
749 : : cvc5::Term d_result;
750 : :
751 : : public:
752 : : GetAssignmentCommand();
753 : :
754 : : cvc5::Term getResult() const;
755 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
756 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
757 : : std::string getCommandName() const override;
758 : : void toStream(std::ostream& out) const override;
759 : : }; /* class GetAssignmentCommand */
760 : :
761 : : class CVC5_EXPORT GetModelCommand : public Cmd
762 : : {
763 : : public:
764 : : GetModelCommand();
765 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
766 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
767 : : std::string getCommandName() const override;
768 : : void toStream(std::ostream& out) const override;
769 : :
770 : : protected:
771 : : /** Result of printing the model */
772 : : std::string d_result;
773 : : }; /* class GetModelCommand */
774 : :
775 : : /** The command to block models. */
776 : : class CVC5_EXPORT BlockModelCommand : public Cmd
777 : : {
778 : : public:
779 : : BlockModelCommand(modes::BlockModelsMode mode);
780 : :
781 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
782 : : std::string getCommandName() const override;
783 : : void toStream(std::ostream& out) const override;
784 : :
785 : : private:
786 : : /** The mode to use for blocking. */
787 : : modes::BlockModelsMode d_mode;
788 : : }; /* class BlockModelCommand */
789 : :
790 : : /** The command to block model values. */
791 : : class CVC5_EXPORT BlockModelValuesCommand : public Cmd
792 : : {
793 : : public:
794 : : BlockModelValuesCommand(const std::vector<cvc5::Term>& terms);
795 : :
796 : : const std::vector<cvc5::Term>& getTerms() const;
797 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
798 : : std::string getCommandName() const override;
799 : : void toStream(std::ostream& out) const override;
800 : :
801 : : protected:
802 : : /** The terms we are blocking */
803 : : std::vector<cvc5::Term> d_terms;
804 : : }; /* class BlockModelValuesCommand */
805 : :
806 : : class CVC5_EXPORT GetProofCommand : public Cmd
807 : : {
808 : : public:
809 : : GetProofCommand(modes::ProofComponent c = modes::ProofComponent::FULL);
810 : :
811 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
812 : :
813 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
814 : :
815 : : std::string getCommandName() const override;
816 : : void toStream(std::ostream& out) const override;
817 : :
818 : : private:
819 : : /** the result of the getProof call */
820 : : std::string d_result;
821 : : /** the requested proof component */
822 : : modes::ProofComponent d_component;
823 : : }; /* class GetProofCommand */
824 : :
825 : : class CVC5_EXPORT GetInstantiationsCommand : public Cmd
826 : : {
827 : : public:
828 : : GetInstantiationsCommand();
829 : :
830 : : static bool isEnabled(cvc5::Solver* solver, const cvc5::Result& res);
831 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
832 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
833 : : std::string getCommandName() const override;
834 : : void toStream(std::ostream& out) const override;
835 : :
836 : : protected:
837 : : cvc5::Solver* d_solver;
838 : : }; /* class GetInstantiationsCommand */
839 : :
840 : : /** The command (get-interpolant s B (G)?)
841 : : *
842 : : * This command asks for an interpolant from the current set of assertions and
843 : : * conjecture (goal) B.
844 : : *
845 : : * The symbol s is the name for the interpolation predicate. If we successfully
846 : : * find a predicate P, then the output response of this command is: (define-fun
847 : : * s () Bool P)
848 : : */
849 : : class CVC5_EXPORT GetInterpolantCommand : public Cmd
850 : : {
851 : : public:
852 : : GetInterpolantCommand(const std::string& name, Term conj);
853 : : /** The argument g is the grammar of the interpolation query */
854 : : GetInterpolantCommand(const std::string& name, Term conj, Grammar* g);
855 : :
856 : : /** Get the conjecture of the interpolation query */
857 : : cvc5::Term getConjecture() const;
858 : : /** Get the sygus grammar given for the interpolation query */
859 : : const cvc5::Grammar* getGrammar() const;
860 : : /** Get the result of the query, which is the solution to the interpolation
861 : : * query. */
862 : : cvc5::Term getResult() const;
863 : :
864 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
865 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
866 : : std::string getCommandName() const override;
867 : : void toStream(std::ostream& out) const override;
868 : :
869 : : protected:
870 : : /** The name of the interpolation predicate */
871 : : std::string d_name;
872 : : /** The conjecture of the interpolation query */
873 : : cvc5::Term d_conj;
874 : : /** The (optional) grammar of the interpolation query */
875 : : cvc5::Grammar* d_sygus_grammar;
876 : : /** the return expression of the command */
877 : : cvc5::Term d_result;
878 : : }; /* class GetInterpolCommand */
879 : :
880 : : /** The command (get-interpolant-next) */
881 : : class CVC5_EXPORT GetInterpolantNextCommand : public Cmd
882 : : {
883 : : public:
884 : : GetInterpolantNextCommand();
885 : : /**
886 : : * Get the result of the query, which is the solution to the interpolation
887 : : * query.
888 : : */
889 : : cvc5::Term getResult() const;
890 : :
891 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
892 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
893 : : std::string getCommandName() const override;
894 : : void toStream(std::ostream& out) const override;
895 : :
896 : : protected:
897 : : /** The name of the interpolation predicate */
898 : : std::string d_name;
899 : : /** the return expression of the command */
900 : : cvc5::Term d_result;
901 : : };
902 : :
903 : : /** The command (get-abduct s B (G)?)
904 : : *
905 : : * This command asks for an abduct from the current set of assertions and
906 : : * conjecture (goal) given by the argument B.
907 : : *
908 : : * The symbol s is the name for the abduction predicate. If we successfully
909 : : * find a predicate P, then the output response of this command is:
910 : : * (define-fun s () Bool P)
911 : : *
912 : : * A grammar G can be optionally provided to indicate the syntactic restrictions
913 : : * on the possible solutions returned.
914 : : */
915 : : class CVC5_EXPORT GetAbductCommand : public Cmd
916 : : {
917 : : public:
918 : : GetAbductCommand(const std::string& name, cvc5::Term conj);
919 : : GetAbductCommand(const std::string& name, cvc5::Term conj, cvc5::Grammar* g);
920 : :
921 : : /** Get the conjecture of the abduction query */
922 : : cvc5::Term getConjecture() const;
923 : : /** Get the grammar given for the abduction query */
924 : : const cvc5::Grammar* getGrammar() const;
925 : : /** Get the name of the abduction predicate for the abduction query */
926 : : std::string getAbductName() const;
927 : : /** Get the result of the query, which is the solution to the abduction query.
928 : : */
929 : : cvc5::Term getResult() const;
930 : :
931 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
932 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
933 : : std::string getCommandName() const override;
934 : : void toStream(std::ostream& out) const override;
935 : :
936 : : protected:
937 : : /** The name of the abduction predicate */
938 : : std::string d_name;
939 : : /** The conjecture of the abduction query */
940 : : cvc5::Term d_conj;
941 : : /** The (optional) grammar of the abduction query */
942 : : cvc5::Grammar* d_sygus_grammar;
943 : : /** the return expression of the command */
944 : : cvc5::Term d_result;
945 : : }; /* class GetAbductCommand */
946 : :
947 : : /** The command (get-abduct-next) */
948 : : class CVC5_EXPORT GetAbductNextCommand : public Cmd
949 : : {
950 : : public:
951 : : GetAbductNextCommand();
952 : : /**
953 : : * Get the result of the query, which is the solution to the abduction query.
954 : : */
955 : : cvc5::Term getResult() const;
956 : :
957 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
958 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
959 : : std::string getCommandName() const override;
960 : : void toStream(std::ostream& out) const override;
961 : :
962 : : protected:
963 : : /** The name of the abduction predicate */
964 : : std::string d_name;
965 : : /** the return expression of the command */
966 : : cvc5::Term d_result;
967 : : };
968 : :
969 : : class CVC5_EXPORT GetQuantifierEliminationCommand : public Cmd
970 : : {
971 : : protected:
972 : : cvc5::Term d_term;
973 : : bool d_doFull;
974 : : cvc5::Term d_result;
975 : :
976 : : public:
977 : : GetQuantifierEliminationCommand();
978 : : GetQuantifierEliminationCommand(const cvc5::Term& term, bool doFull);
979 : :
980 : : cvc5::Term getTerm() const;
981 : : bool getDoFull() const;
982 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
983 : : cvc5::Term getResult() const;
984 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
985 : :
986 : : std::string getCommandName() const override;
987 : : void toStream(std::ostream& out) const override;
988 : : }; /* class GetQuantifierEliminationCommand */
989 : :
990 : : class CVC5_EXPORT GetUnsatAssumptionsCommand : public Cmd
991 : : {
992 : : public:
993 : : GetUnsatAssumptionsCommand();
994 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
995 : : std::vector<cvc5::Term> getResult() const;
996 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
997 : : std::string getCommandName() const override;
998 : : void toStream(std::ostream& out) const override;
999 : :
1000 : : protected:
1001 : : std::vector<cvc5::Term> d_result;
1002 : : }; /* class GetUnsatAssumptionsCommand */
1003 : :
1004 : : class CVC5_EXPORT GetUnsatCoreCommand : public Cmd
1005 : : {
1006 : : public:
1007 : : GetUnsatCoreCommand();
1008 : : const std::vector<cvc5::Term>& getUnsatCore() const;
1009 : :
1010 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
1011 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
1012 : :
1013 : : std::string getCommandName() const override;
1014 : : void toStream(std::ostream& out) const override;
1015 : :
1016 : : protected:
1017 : : /** The solver we were invoked with */
1018 : : cvc5::Solver* d_solver;
1019 : : /** The symbol manager we were invoked with */
1020 : : parser::SymManager* d_sm;
1021 : : /** the result of the unsat core call */
1022 : : std::vector<cvc5::Term> d_result;
1023 : : }; /* class GetUnsatCoreCommand */
1024 : :
1025 : : class CVC5_EXPORT GetUnsatCoreLemmasCommand : public Cmd
1026 : : {
1027 : : public:
1028 : : GetUnsatCoreLemmasCommand();
1029 : : const std::vector<cvc5::Term>& getUnsatCoreLemmas() const;
1030 : :
1031 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
1032 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
1033 : :
1034 : : std::string getCommandName() const override;
1035 : : void toStream(std::ostream& out) const override;
1036 : :
1037 : : protected:
1038 : : /** The solver we were invoked with */
1039 : : cvc5::Solver* d_solver;
1040 : : /** the result of the unsat core call */
1041 : : std::vector<cvc5::Term> d_result;
1042 : : }; /* class GetUnsatCoreLemmasCommand */
1043 : :
1044 : : class CVC5_EXPORT GetDifficultyCommand : public Cmd
1045 : : {
1046 : : public:
1047 : : GetDifficultyCommand();
1048 : : const std::map<cvc5::Term, cvc5::Term>& getDifficultyMap() const;
1049 : :
1050 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
1051 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
1052 : :
1053 : : std::string getCommandName() const override;
1054 : : void toStream(std::ostream& out) const override;
1055 : :
1056 : : protected:
1057 : : /** The symbol manager we were invoked with */
1058 : : parser::SymManager* d_sm;
1059 : : /** the result of the get difficulty call */
1060 : : std::map<cvc5::Term, cvc5::Term> d_result;
1061 : : };
1062 : :
1063 : : class CVC5_EXPORT GetTimeoutCoreCommand : public Cmd
1064 : : {
1065 : : public:
1066 : : GetTimeoutCoreCommand(const std::vector<Term>& assumptions);
1067 : : GetTimeoutCoreCommand();
1068 : : cvc5::Result getResult() const;
1069 : : const std::vector<cvc5::Term>& getTimeoutCore() const;
1070 : :
1071 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
1072 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
1073 : :
1074 : : std::string getCommandName() const override;
1075 : : void toStream(std::ostream& out) const override;
1076 : :
1077 : : protected:
1078 : : /** The solver we were invoked with */
1079 : : cvc5::Solver* d_solver;
1080 : : /** The symbol manager we were invoked with */
1081 : : parser::SymManager* d_sm;
1082 : : /** Assumptions */
1083 : : std::vector<Term> d_assumptions;
1084 : : /** the result of the timeout core call */
1085 : : std::pair<cvc5::Result, std::vector<cvc5::Term>> d_result;
1086 : : };
1087 : :
1088 : : class CVC5_EXPORT GetLearnedLiteralsCommand : public Cmd
1089 : : {
1090 : : public:
1091 : : GetLearnedLiteralsCommand(modes::LearnedLitType t);
1092 : : const std::vector<cvc5::Term>& getLearnedLiterals() const;
1093 : :
1094 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
1095 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
1096 : :
1097 : : std::string getCommandName() const override;
1098 : : void toStream(std::ostream& out) const override;
1099 : :
1100 : : protected:
1101 : : /** the result of the get learned literals call */
1102 : : std::vector<cvc5::Term> d_result;
1103 : : /** The type of learned literals to get */
1104 : : modes::LearnedLitType d_type;
1105 : : };
1106 : :
1107 : : class CVC5_EXPORT GetAssertionsCommand : public Cmd
1108 : : {
1109 : : protected:
1110 : : std::string d_result;
1111 : :
1112 : : public:
1113 : : GetAssertionsCommand();
1114 : :
1115 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
1116 : : std::string getResult() const;
1117 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
1118 : : std::string getCommandName() const override;
1119 : : void toStream(std::ostream& out) const override;
1120 : : }; /* class GetAssertionsCommand */
1121 : :
1122 : : class CVC5_EXPORT SetBenchmarkLogicCommand : public Cmd
1123 : : {
1124 : : protected:
1125 : : std::string d_logic;
1126 : :
1127 : : public:
1128 : : SetBenchmarkLogicCommand(std::string logic);
1129 : :
1130 : : std::string getLogic() const;
1131 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
1132 : : std::string getCommandName() const override;
1133 : : void toStream(std::ostream& out) const override;
1134 : : }; /* class SetBenchmarkLogicCommand */
1135 : :
1136 : : class CVC5_EXPORT SetInfoCommand : public Cmd
1137 : : {
1138 : : protected:
1139 : : std::string d_flag;
1140 : : std::string d_value;
1141 : :
1142 : : public:
1143 : : SetInfoCommand(const std::string& flag, const std::string& value);
1144 : :
1145 : : const std::string& getFlag() const;
1146 : : const std::string& getValue() const;
1147 : :
1148 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
1149 : : std::string getCommandName() const override;
1150 : : void toStream(std::ostream& out) const override;
1151 : : }; /* class SetInfoCommand */
1152 : :
1153 : : class CVC5_EXPORT GetInfoCommand : public Cmd
1154 : : {
1155 : : protected:
1156 : : std::string d_flag;
1157 : : std::string d_result;
1158 : :
1159 : : public:
1160 : : GetInfoCommand(std::string flag);
1161 : :
1162 : : std::string getFlag() const;
1163 : : std::string getResult() const;
1164 : :
1165 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
1166 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
1167 : : std::string getCommandName() const override;
1168 : : void toStream(std::ostream& out) const override;
1169 : : }; /* class GetInfoCommand */
1170 : :
1171 : : class CVC5_EXPORT SetOptionCommand : public Cmd
1172 : : {
1173 : : protected:
1174 : : std::string d_flag;
1175 : : std::string d_value;
1176 : :
1177 : : public:
1178 : : SetOptionCommand(const std::string& flag, const std::string& value);
1179 : :
1180 : : const std::string& getFlag() const;
1181 : : const std::string& getValue() const;
1182 : :
1183 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
1184 : : std::string getCommandName() const override;
1185 : : void toStream(std::ostream& out) const override;
1186 : : }; /* class SetOptionCommand */
1187 : :
1188 : : class CVC5_EXPORT GetOptionCommand : public Cmd
1189 : : {
1190 : : protected:
1191 : : std::string d_flag;
1192 : : std::string d_result;
1193 : :
1194 : : public:
1195 : : GetOptionCommand(std::string flag);
1196 : :
1197 : : std::string getFlag() const;
1198 : : std::string getResult() const;
1199 : :
1200 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
1201 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
1202 : : std::string getCommandName() const override;
1203 : : void toStream(std::ostream& out) const override;
1204 : : }; /* class GetOptionCommand */
1205 : :
1206 : : class CVC5_EXPORT DatatypeDeclarationCommand : public Cmd
1207 : : {
1208 : : private:
1209 : : std::vector<cvc5::Sort> d_datatypes;
1210 : :
1211 : : public:
1212 : : DatatypeDeclarationCommand(const cvc5::Sort& datatype);
1213 : :
1214 : : DatatypeDeclarationCommand(const std::vector<cvc5::Sort>& datatypes);
1215 : : const std::vector<cvc5::Sort>& getDatatypes() const;
1216 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
1217 : : std::string getCommandName() const override;
1218 : : void toStream(std::ostream& out) const override;
1219 : : }; /* class DatatypeDeclarationCommand */
1220 : :
1221 : : class CVC5_EXPORT ResetCommand : public Cmd
1222 : : {
1223 : : public:
1224 : 83 : ResetCommand() {}
1225 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
1226 : : std::string getCommandName() const override;
1227 : : void toStream(std::ostream& out) const override;
1228 : : }; /* class ResetCommand */
1229 : :
1230 : : class CVC5_EXPORT ResetAssertionsCommand : public Cmd
1231 : : {
1232 : : public:
1233 : 62 : ResetAssertionsCommand() {}
1234 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
1235 : : std::string getCommandName() const override;
1236 : : void toStream(std::ostream& out) const override;
1237 : : }; /* class ResetAssertionsCommand */
1238 : :
1239 : : class CVC5_EXPORT QuitCommand : public Cmd
1240 : : {
1241 : : public:
1242 : 3036 : QuitCommand() {}
1243 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
1244 : : std::string getCommandName() const override;
1245 : : void toStream(std::ostream& out) const override;
1246 : : }; /* class QuitCommand */
1247 : :
1248 : : } // namespace parser
1249 : : } // namespace cvc5
1250 : :
1251 : : #endif /* CVC5__PARSER__COMMAND_H */
|
