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 the solver.
83 : : */
84 : : virtual void invokeAndPrintResult(cvc5::Solver* solver,
85 : : parser::SymManager* sm);
86 : :
87 : : /**
88 : : * @return A string representation of this result.
89 : : */
90 : : std::string toString() const;
91 : :
92 : : /**
93 : : * Get the name for this command, e.g. "assert".
94 : : *
95 : : * @return The name of this command.
96 : : */
97 : : virtual std::string getCommandName() const = 0;
98 : :
99 : : /**
100 : : * Either the command hasn't run yet, or it completed successfully
101 : : * (CommandSuccess, not CommandUnsupported or CommandFailure).
102 : : *
103 : : * @return Whether the command was successfully invoked.
104 : : */
105 : : bool ok() const;
106 : :
107 : : /**
108 : : * The command completed in a failure state (CommandFailure, not
109 : : * CommandSuccess or CommandUnsupported).
110 : : *
111 : : * @return Whether the command failed.
112 : : */
113 : : bool fail() const;
114 : :
115 : : /**
116 : : * The command was ran but was interrupted due to resource limiting.
117 : : *
118 : : * @return Whether the command was interrupted.
119 : : */
120 : : bool interrupted() const;
121 : :
122 : : protected:
123 : : virtual void toStream(std::ostream& out) const = 0;
124 : : /**
125 : : * This field contains a command status if the command has been
126 : : * invoked, or NULL if it has not. This field is either a
127 : : * dynamically-allocated pointer, or it's a pointer to the singleton
128 : : * CommandSuccess instance. Doing so is somewhat asymmetric, but
129 : : * it avoids the need to dynamically allocate memory in the common
130 : : * case of a successful command.
131 : : */
132 : : const CommandStatus* d_commandStatus;
133 : : /**
134 : : * Print the result of running the command. This method is only called if the
135 : : * command ran successfully.
136 : : */
137 : : virtual void printResult(cvc5::Solver* solver, std::ostream& out) const;
138 : : /**
139 : : * Reset the given solver in-place (keep the object at the same memory
140 : : * location).
141 : : */
142 : : static void resetSolver(cvc5::Solver* solver);
143 : :
144 : : // These methods rely on Command being a friend of classes in the API.
145 : : // Subclasses of command should use these methods for conversions,
146 : : // which is currently necessary for e.g. printing commands.
147 : : /** Helper to convert a Term to an internal internal::Node */
148 : : static internal::Node termToNode(const cvc5::Term& term);
149 : : /** Helper to convert a vector of Terms to internal Nodes. */
150 : : static std::vector<internal::Node> termVectorToNodes(
151 : : const std::vector<cvc5::Term>& terms);
152 : : /** Helper to convert a Sort to an internal internal::TypeNode */
153 : : static internal::TypeNode sortToTypeNode(const cvc5::Sort& sort);
154 : : /** Helper to convert a vector of Sorts to internal TypeNodes. */
155 : : static std::vector<internal::TypeNode> sortVectorToTypeNodes(
156 : : const std::vector<cvc5::Sort>& sorts);
157 : : /** Helper to convert a Grammar to an internal internal::TypeNode */
158 : : static internal::TypeNode grammarToTypeNode(cvc5::Grammar* grammar);
159 : : }; /* class Command */
160 : :
161 : : /**
162 : : * EmptyCommands are the residue of a command after the parser handles
163 : : * them (and there's nothing left to do).
164 : : */
165 : : class CVC5_EXPORT EmptyCommand : public Cmd
166 : : {
167 : : public:
168 : : EmptyCommand(std::string name = "");
169 : : std::string getName() const;
170 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
171 : : std::string getCommandName() const override;
172 : : void toStream(std::ostream& out) const override;
173 : :
174 : : protected:
175 : : std::string d_name;
176 : : }; /* class EmptyCommand */
177 : :
178 : : class CVC5_EXPORT EchoCommand : public Cmd
179 : : {
180 : : public:
181 : : EchoCommand(std::string output = "");
182 : :
183 : : std::string getOutput() const;
184 : :
185 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
186 : : /** The result is the printed string */
187 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
188 : :
189 : : std::string getCommandName() const override;
190 : : void toStream(std::ostream& out) const override;
191 : :
192 : : protected:
193 : : std::string d_output;
194 : : }; /* class EchoCommand */
195 : :
196 : : class CVC5_EXPORT AssertCommand : public Cmd
197 : : {
198 : : protected:
199 : : cvc5::Term d_term;
200 : :
201 : : public:
202 : : AssertCommand(const cvc5::Term& t);
203 : :
204 : : cvc5::Term getTerm() const;
205 : :
206 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
207 : :
208 : : std::string getCommandName() const override;
209 : : void toStream(std::ostream& out) const override;
210 : : }; /* class AssertCommand */
211 : :
212 : : class CVC5_EXPORT PushCommand : public Cmd
213 : : {
214 : : public:
215 : : PushCommand(uint32_t nscopes);
216 : :
217 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
218 : : std::string getCommandName() const override;
219 : : void toStream(std::ostream& out) const override;
220 : :
221 : : private:
222 : : uint32_t d_nscopes;
223 : : }; /* class PushCommand */
224 : :
225 : : class CVC5_EXPORT PopCommand : public Cmd
226 : : {
227 : : public:
228 : : PopCommand(uint32_t nscopes);
229 : :
230 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
231 : : std::string getCommandName() const override;
232 : : void toStream(std::ostream& out) const override;
233 : :
234 : : private:
235 : : uint32_t d_nscopes;
236 : : }; /* class PopCommand */
237 : :
238 : : class CVC5_EXPORT DeclarationDefinitionCommand : public Cmd
239 : : {
240 : : protected:
241 : : std::string d_symbol;
242 : : /**
243 : : * Bind the symbol of this command to the given term. Return false if the
244 : : * binding was invalid. In this case, set command status to CommandFailure.
245 : : */
246 : : bool bindToTerm(parser::SymManager* sm, cvc5::Term t, bool doOverload);
247 : :
248 : : public:
249 : : DeclarationDefinitionCommand(const std::string& id);
250 : :
251 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override = 0;
252 : : std::string getSymbol() const;
253 : : }; /* class DeclarationDefinitionCommand */
254 : :
255 : : class CVC5_EXPORT DeclareFunctionCommand : public DeclarationDefinitionCommand
256 : : {
257 : : protected:
258 : : std::vector<Sort> d_argSorts;
259 : : cvc5::Sort d_sort;
260 : :
261 : : public:
262 : : DeclareFunctionCommand(const std::string& id,
263 : : const std::vector<Sort>& argSorts,
264 : : cvc5::Sort sort);
265 : : std::vector<Sort> getArgSorts() const;
266 : : cvc5::Sort getSort() const;
267 : :
268 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
269 : : std::string getCommandName() const override;
270 : : void toStream(std::ostream& out) const override;
271 : : }; /* class DeclareFunctionCommand */
272 : :
273 : : class CVC5_EXPORT DeclarePoolCommand : public DeclarationDefinitionCommand
274 : : {
275 : : protected:
276 : : cvc5::Sort d_sort;
277 : : std::vector<cvc5::Term> d_initValue;
278 : :
279 : : public:
280 : : DeclarePoolCommand(const std::string& id,
281 : : cvc5::Sort sort,
282 : : const std::vector<cvc5::Term>& initValue);
283 : : cvc5::Sort getSort() const;
284 : : const std::vector<cvc5::Term>& getInitialValue() const;
285 : :
286 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
287 : : std::string getCommandName() const override;
288 : : void toStream(std::ostream& out) const override;
289 : : }; /* class DeclarePoolCommand */
290 : :
291 : : class CVC5_EXPORT DeclareOracleFunCommand : public Cmd
292 : : {
293 : : public:
294 : : DeclareOracleFunCommand(const std::string& id,
295 : : const std::vector<Sort>& argSorts,
296 : : Sort sort);
297 : : DeclareOracleFunCommand(const std::string& id,
298 : : const std::vector<Sort>& argSorts,
299 : : Sort sort,
300 : : const std::string& binName);
301 : : const std::string& getIdentifier() const;
302 : : std::vector<Sort> getArgSorts() const;
303 : : Sort getSort() const;
304 : : const std::string& getBinaryName() const;
305 : :
306 : : void invoke(Solver* solver, parser::SymManager* sm) override;
307 : : std::string getCommandName() const override;
308 : : void toStream(std::ostream& out) const override;
309 : :
310 : : protected:
311 : : /** The identifier */
312 : : std::string d_id;
313 : : /** Argument sorts */
314 : : std::vector<Sort> d_argSorts;
315 : : /** The return sort */
316 : : Sort d_sort;
317 : : /** The binary name, or "" if none is provided */
318 : : std::string d_binName;
319 : : };
320 : :
321 : : class CVC5_EXPORT DeclareSortCommand : public DeclarationDefinitionCommand
322 : : {
323 : : protected:
324 : : size_t d_arity;
325 : : public:
326 : : DeclareSortCommand(const std::string& id, size_t arity);
327 : :
328 : : size_t getArity() const;
329 : :
330 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
331 : : std::string getCommandName() const override;
332 : : void toStream(std::ostream& out) const override;
333 : : }; /* class DeclareSortCommand */
334 : :
335 : : class CVC5_EXPORT DefineSortCommand : public DeclarationDefinitionCommand
336 : : {
337 : : protected:
338 : : std::vector<cvc5::Sort> d_params;
339 : : cvc5::Sort d_sort;
340 : :
341 : : public:
342 : : DefineSortCommand(const std::string& id, cvc5::Sort sort);
343 : : DefineSortCommand(const std::string& id,
344 : : const std::vector<cvc5::Sort>& params,
345 : : cvc5::Sort sort);
346 : :
347 : : const std::vector<cvc5::Sort>& getParameters() const;
348 : : cvc5::Sort getSort() const;
349 : :
350 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
351 : : std::string getCommandName() const override;
352 : : void toStream(std::ostream& out) const override;
353 : : }; /* class DefineSortCommand */
354 : :
355 : : class CVC5_EXPORT DefineFunctionCommand : public DeclarationDefinitionCommand
356 : : {
357 : : public:
358 : : DefineFunctionCommand(const std::string& id,
359 : : cvc5::Sort sort,
360 : : cvc5::Term formula);
361 : : DefineFunctionCommand(const std::string& id,
362 : : const std::vector<cvc5::Term>& formals,
363 : : cvc5::Sort sort,
364 : : cvc5::Term formula);
365 : :
366 : : const std::vector<cvc5::Term>& getFormals() const;
367 : : cvc5::Sort getSort() const;
368 : : cvc5::Term getFormula() const;
369 : :
370 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
371 : : std::string getCommandName() const override;
372 : : void toStream(std::ostream& out) const override;
373 : :
374 : : protected:
375 : : /** The formal arguments for the function we are defining */
376 : : std::vector<cvc5::Term> d_formals;
377 : : /** The co-domain sort of the function we are defining */
378 : : cvc5::Sort d_sort;
379 : : /** The formula corresponding to the body of the function we are defining */
380 : : cvc5::Term d_formula;
381 : : }; /* class DefineFunctionCommand */
382 : :
383 : : /**
384 : : * The command when parsing define-fun-rec or define-funs-rec.
385 : : * This command will assert a set of quantified formulas that specify
386 : : * the (mutually recursive) function definitions provided to it.
387 : : */
388 : : class CVC5_EXPORT DefineFunctionRecCommand : public Cmd
389 : : {
390 : : public:
391 : : DefineFunctionRecCommand(cvc5::Term func,
392 : : const std::vector<cvc5::Term>& formals,
393 : : cvc5::Term formula);
394 : : DefineFunctionRecCommand(const std::vector<cvc5::Term>& funcs,
395 : : const std::vector<std::vector<cvc5::Term> >& formals,
396 : : const std::vector<cvc5::Term>& formula);
397 : :
398 : : const std::vector<cvc5::Term>& getFunctions() const;
399 : : const std::vector<std::vector<cvc5::Term> >& getFormals() const;
400 : : const std::vector<cvc5::Term>& getFormulas() const;
401 : :
402 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
403 : : std::string getCommandName() const override;
404 : : void toStream(std::ostream& out) const override;
405 : :
406 : : protected:
407 : : /** functions we are defining */
408 : : std::vector<cvc5::Term> d_funcs;
409 : : /** formal arguments for each of the functions we are defining */
410 : : std::vector<std::vector<cvc5::Term> > d_formals;
411 : : /** formulas corresponding to the bodies of the functions we are defining */
412 : : std::vector<cvc5::Term> d_formulas;
413 : : }; /* class DefineFunctionRecCommand */
414 : :
415 : : /**
416 : : * In separation logic inputs, which is an extension of smt2 inputs, this
417 : : * corresponds to the command:
418 : : * (declare-heap (T U))
419 : : * where T is the location sort and U is the data sort.
420 : : */
421 : : class CVC5_EXPORT DeclareHeapCommand : public Cmd
422 : : {
423 : : public:
424 : : DeclareHeapCommand(cvc5::Sort locSort, cvc5::Sort dataSort);
425 : : cvc5::Sort getLocationSort() const;
426 : : cvc5::Sort getDataSort() const;
427 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
428 : : std::string getCommandName() const override;
429 : : void toStream(std::ostream& out) const override;
430 : :
431 : : protected:
432 : : /** The location sort */
433 : : cvc5::Sort d_locSort;
434 : : /** The data sort */
435 : : cvc5::Sort d_dataSort;
436 : : };
437 : :
438 : : /**
439 : : * The command when parsing check-sat.
440 : : * This command will check satisfiability of the input formula.
441 : : */
442 : : class CVC5_EXPORT CheckSatCommand : public Cmd
443 : : {
444 : : public:
445 : : CheckSatCommand();
446 : : cvc5::Result getResult() const;
447 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
448 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
449 : : std::string getCommandName() const override;
450 : : void toStream(std::ostream& out) const override;
451 : :
452 : : private:
453 : : cvc5::Result d_result;
454 : : }; /* class CheckSatCommand */
455 : :
456 : : /**
457 : : * The command when parsing check-sat-assuming.
458 : : * This command will assume a set of formulas and check satisfiability of the
459 : : * input formula under these assumptions.
460 : : */
461 : : class CVC5_EXPORT CheckSatAssumingCommand : public Cmd
462 : : {
463 : : public:
464 : : CheckSatAssumingCommand(cvc5::Term term);
465 : : CheckSatAssumingCommand(const std::vector<cvc5::Term>& terms);
466 : :
467 : : const std::vector<cvc5::Term>& getTerms() const;
468 : : cvc5::Result getResult() const;
469 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
470 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
471 : : std::string getCommandName() const override;
472 : : void toStream(std::ostream& out) const override;
473 : :
474 : : private:
475 : : std::vector<cvc5::Term> d_terms;
476 : : cvc5::Result d_result;
477 : : }; /* class CheckSatAssumingCommand */
478 : :
479 : : /* ------------------- sygus commands ------------------ */
480 : :
481 : : /** Declares a sygus universal variable */
482 : : class CVC5_EXPORT DeclareSygusVarCommand : public DeclarationDefinitionCommand
483 : : {
484 : : public:
485 : : DeclareSygusVarCommand(const std::string& id,
486 : : cvc5::Sort sort);
487 : : /** returns the declared variable */
488 : : cvc5::Term getVar() const;
489 : : /** returns the declared variable's sort */
490 : : cvc5::Sort getSort() const;
491 : : /** invokes this command
492 : : *
493 : : * The declared sygus variable is communicated to the SMT engine in case a
494 : : * synthesis conjecture is built later on.
495 : : */
496 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
497 : : /** returns this command's name */
498 : : std::string getCommandName() const override;
499 : : /** prints this command */
500 : : void toStream(std::ostream& out) const override;
501 : :
502 : : protected:
503 : : /** the declared variable's sort */
504 : : cvc5::Sort d_sort;
505 : : };
506 : :
507 : : /** Declares a sygus function-to-synthesize
508 : : *
509 : : * This command is also used for the special case in which we are declaring an
510 : : * invariant-to-synthesize
511 : : */
512 : : class CVC5_EXPORT SynthFunCommand : public DeclarationDefinitionCommand
513 : : {
514 : : public:
515 : : SynthFunCommand(const std::string& id,
516 : : const std::vector<cvc5::Term>& vars,
517 : : cvc5::Sort sort,
518 : : cvc5::Grammar* g);
519 : : /** returns the input variables of the function-to-synthesize */
520 : : const std::vector<cvc5::Term>& getVars() const;
521 : : /** returns the sygus sort of the function-to-synthesize */
522 : : cvc5::Sort getSort() const;
523 : : /** Get the sygus grammar given for the synth fun command */
524 : : const cvc5::Grammar* getGrammar() const;
525 : :
526 : : /** invokes this command
527 : : *
528 : : * The declared function-to-synthesize is communicated to the SMT engine in
529 : : * case a synthesis conjecture is built later on.
530 : : */
531 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
532 : : /** returns this command's name */
533 : : std::string getCommandName() const override;
534 : : /** prints this command */
535 : : void toStream(std::ostream& out) const override;
536 : :
537 : : protected:
538 : : /** the input variables of the function-to-synthesize */
539 : : std::vector<cvc5::Term> d_vars;
540 : : /** sort of the function-to-synthesize */
541 : : cvc5::Sort d_sort;
542 : : /** optional grammar for the possible values of the function-to-sytnhesize */
543 : : cvc5::Grammar* d_grammar;
544 : : };
545 : :
546 : : /** Declares a sygus constraint */
547 : : class CVC5_EXPORT SygusConstraintCommand : public Cmd
548 : : {
549 : : public:
550 : : SygusConstraintCommand(const cvc5::Term& t, bool isAssume = false);
551 : : /** returns the declared constraint */
552 : : cvc5::Term getTerm() const;
553 : : /** invokes this command
554 : : *
555 : : * The declared constraint is communicated to the SMT engine in case a
556 : : * synthesis conjecture is built later on.
557 : : */
558 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
559 : : /** returns this command's name */
560 : : std::string getCommandName() const override;
561 : : /** prints this command */
562 : : void toStream(std::ostream& out) const override;
563 : :
564 : : protected:
565 : : /** the declared constraint */
566 : : cvc5::Term d_term;
567 : : /** true if this is a sygus assumption */
568 : : bool d_isAssume;
569 : : };
570 : :
571 : : /** Declares a sygus invariant constraint
572 : : *
573 : : * Invarint constraints are declared in a somewhat implicit manner in the SyGuS
574 : : * language: they are declared in terms of the previously declared
575 : : * invariant-to-synthesize, precondition, transition relation and condition.
576 : : *
577 : : * The actual constraint must be built such that the invariant is not stronger
578 : : * than the precondition, not weaker than the postcondition and inductive
579 : : * w.r.t. the transition relation.
580 : : */
581 : : class CVC5_EXPORT SygusInvConstraintCommand : public Cmd
582 : : {
583 : : public:
584 : : SygusInvConstraintCommand(const std::vector<cvc5::Term>& predicates);
585 : : SygusInvConstraintCommand(const cvc5::Term& inv,
586 : : const cvc5::Term& pre,
587 : : const cvc5::Term& trans,
588 : : const cvc5::Term& post);
589 : : /** returns the place holder predicates */
590 : : const std::vector<cvc5::Term>& getPredicates() const;
591 : : /** invokes this command
592 : : *
593 : : * The place holders are communicated to the SMT engine and the actual
594 : : * invariant constraint is built, in case an actual synthesis conjecture is
595 : : * built later on.
596 : : */
597 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
598 : : /** returns this command's name */
599 : : std::string getCommandName() const override;
600 : : /** prints this command */
601 : : void toStream(std::ostream& out) const override;
602 : :
603 : : protected:
604 : : /** the place holder predicates with which to build the actual constraint
605 : : * (i.e. the invariant, precondition, transition relation and postcondition)
606 : : */
607 : : std::vector<cvc5::Term> d_predicates;
608 : : };
609 : :
610 : : /** Declares a synthesis conjecture */
611 : : class CVC5_EXPORT CheckSynthCommand : public Cmd
612 : : {
613 : : public:
614 : 952 : CheckSynthCommand(bool isNext = false) : d_isNext(isNext){};
615 : : /** returns the result of the check-synth call */
616 : : cvc5::SynthResult getResult() const;
617 : : /** prints the result of the check-synth-call */
618 : : void printResult(cvc5::Solver* solver, std::ostream& out) const override;
619 : : /** invokes this command
620 : : *
621 : : * This invocation makes the SMT engine build a synthesis conjecture based on
622 : : * previously declared information (such as universal variables,
623 : : * functions-to-synthesize and so on), set up attributes to guide the solving,
624 : : * and then perform a satisfiability check, whose result is stored in
625 : : * d_result.
626 : : */
627 : : void invoke(cvc5::Solver* solver, parser::SymManager* sm) override;
628 : : /** returns this command's name */
629 : : std::string getCommandName() const override;
630 : : /** prints this command */
631 : : void toStream(std::ostream& out) const override;
632 : :
633 : : protected:
634 : : /** Whether this is a check-synth-next call */
635 : : bool d_isNext;
636 : : /** result of the check-synth call */
637 : : cvc5::SynthResult d_result;
638 : : /** string stream that stores the output of the solution */
639 : : std::stringstream d_solution;
640 : : };
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 : 3032 : 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 */
|
