1 /********************* */
4 ** Top contributors (to current version):
5 ** Tim King, Morgan Deters, Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief Implementation of the command pattern on SmtEngines.
14 ** Implementation of the command pattern on SmtEngines. Command
15 ** objects are generated by the parser (typically) to implement the
16 ** commands in parsed input (see Parser::parseNextCommand()), or by
20 #include "cvc4_public.h"
22 #ifndef __CVC4__COMMAND_H
23 #define __CVC4__COMMAND_H
31 #include "expr/datatype.h"
32 #include "expr/expr.h"
33 #include "expr/type.h"
34 #include "expr/variable_type_map.h"
35 #include "proof/unsat_core.h"
36 #include "util/proof.h"
37 #include "util/result.h"
38 #include "util/sexpr.h"
47 std::ostream
& operator<<(std::ostream
&, const Command
&) CVC4_PUBLIC
;
48 std::ostream
& operator<<(std::ostream
&, const Command
*) CVC4_PUBLIC
;
49 std::ostream
& operator<<(std::ostream
&, const CommandStatus
&) CVC4_PUBLIC
;
50 std::ostream
& operator<<(std::ostream
&, const CommandStatus
*) CVC4_PUBLIC
;
52 /** The status an SMT benchmark can have */
55 /** Benchmark is satisfiable */
57 /** Benchmark is unsatisfiable */
59 /** The status of the benchmark is unknown */
61 }; /* enum BenchmarkStatus */
63 std::ostream
& operator<<(std::ostream
& out
, BenchmarkStatus status
) CVC4_PUBLIC
;
66 * IOStream manipulator to print success messages or not.
68 * out << Command::printsuccess(false) << CommandSuccess();
72 * out << Command::printsuccess(true) << CommandSuccess();
74 * prints a success message (in a manner appropriate for the current
77 class CVC4_PUBLIC CommandPrintSuccess
80 /** Construct a CommandPrintSuccess with the given setting. */
81 CommandPrintSuccess(bool printSuccess
) : d_printSuccess(printSuccess
) {}
82 void applyPrintSuccess(std::ostream
& out
);
83 static bool getPrintSuccess(std::ostream
& out
);
84 static void setPrintSuccess(std::ostream
& out
, bool printSuccess
);
87 /** The allocated index in ios_base for our depth setting. */
88 static const int s_iosIndex
;
91 * The default setting, for ostreams that haven't yet had a setdepth()
94 static const int s_defaultPrintSuccess
= false;
96 /** When this manipulator is used, the setting is stored here. */
99 }; /* class CommandPrintSuccess */
102 * Sets the default print-success setting when pretty-printing an Expr
103 * to an ostream. Use like this:
105 * // let out be an ostream, e an Expr
106 * out << Expr::setdepth(n) << e << endl;
108 * The depth stays permanently (until set again) with the stream.
110 std::ostream
& operator<<(std::ostream
& out
,
111 CommandPrintSuccess cps
) CVC4_PUBLIC
;
113 class CVC4_PUBLIC CommandStatus
116 // shouldn't construct a CommandStatus (use a derived class)
119 virtual ~CommandStatus() {}
120 void toStream(std::ostream
& out
,
121 OutputLanguage language
= language::output::LANG_AUTO
) const;
122 virtual CommandStatus
& clone() const = 0;
123 }; /* class CommandStatus */
125 class CVC4_PUBLIC CommandSuccess
: public CommandStatus
127 static const CommandSuccess
* s_instance
;
130 static const CommandSuccess
* instance() { return s_instance
; }
131 CommandStatus
& clone() const override
133 return const_cast<CommandSuccess
&>(*this);
135 }; /* class CommandSuccess */
137 class CVC4_PUBLIC CommandInterrupted
: public CommandStatus
139 static const CommandInterrupted
* s_instance
;
142 static const CommandInterrupted
* instance() { return s_instance
; }
143 CommandStatus
& clone() const override
145 return const_cast<CommandInterrupted
&>(*this);
147 }; /* class CommandInterrupted */
149 class CVC4_PUBLIC CommandUnsupported
: public CommandStatus
152 CommandStatus
& clone() const override
154 return *new CommandUnsupported(*this);
156 }; /* class CommandSuccess */
158 class CVC4_PUBLIC CommandFailure
: public CommandStatus
160 std::string d_message
;
163 CommandFailure(std::string message
) : d_message(message
) {}
164 CommandFailure
& clone() const override
{ return *new CommandFailure(*this); }
165 std::string
getMessage() const { return d_message
; }
166 }; /* class CommandFailure */
169 * The execution of the command resulted in a non-fatal error and further
170 * commands can be processed. This status is for example used when a user asks
171 * for an unsat core in a place that is not immediately preceded by an
172 * unsat/valid response.
174 class CVC4_PUBLIC CommandRecoverableFailure
: public CommandStatus
176 std::string d_message
;
179 CommandRecoverableFailure(std::string message
) : d_message(message
) {}
180 CommandRecoverableFailure
& clone() const override
182 return *new CommandRecoverableFailure(*this);
184 std::string
getMessage() const { return d_message
; }
185 }; /* class CommandRecoverableFailure */
187 class CVC4_PUBLIC Command
191 * This field contains a command status if the command has been
192 * invoked, or NULL if it has not. This field is either a
193 * dynamically-allocated pointer, or it's a pointer to the singleton
194 * CommandSuccess instance. Doing so is somewhat asymmetric, but
195 * it avoids the need to dynamically allocate memory in the common
196 * case of a successful command.
198 const CommandStatus
* d_commandStatus
;
201 * True if this command is "muted"---i.e., don't print "success" on
202 * successful execution.
207 typedef CommandPrintSuccess printsuccess
;
210 Command(const Command
& cmd
);
214 virtual void invoke(SmtEngine
* smtEngine
) = 0;
215 virtual void invoke(SmtEngine
* smtEngine
, std::ostream
& out
);
217 void toStream(std::ostream
& out
,
221 OutputLanguage language
= language::output::LANG_AUTO
) const;
223 std::string
toString() const;
225 virtual std::string
getCommandName() const = 0;
228 * If false, instruct this Command not to print a success message.
230 void setMuted(bool muted
) { d_muted
= muted
; }
232 * Determine whether this Command will print a success message.
234 bool isMuted() { return d_muted
; }
236 * Either the command hasn't run yet, or it completed successfully
237 * (CommandSuccess, not CommandUnsupported or CommandFailure).
242 * The command completed in a failure state (CommandFailure, not
243 * CommandSuccess or CommandUnsupported).
248 * The command was ran but was interrupted due to resource limiting.
250 bool interrupted() const;
252 /** Get the command status (it's NULL if we haven't run yet). */
253 const CommandStatus
* getCommandStatus() const { return d_commandStatus
; }
254 virtual void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
257 * Maps this Command into one for a different ExprManager, using
258 * variableMap for the translation and extending it with any new
261 virtual Command
* exportTo(ExprManager
* exprManager
,
262 ExprManagerMapCollection
& variableMap
) = 0;
265 * Clone this Command (make a shallow copy).
267 virtual Command
* clone() const = 0;
270 class ExportTransformer
272 ExprManager
* d_exprManager
;
273 ExprManagerMapCollection
& d_variableMap
;
276 ExportTransformer(ExprManager
* exprManager
,
277 ExprManagerMapCollection
& variableMap
)
278 : d_exprManager(exprManager
), d_variableMap(variableMap
)
281 Expr
operator()(Expr e
) { return e
.exportTo(d_exprManager
, d_variableMap
); }
282 Type
operator()(Type t
) { return t
.exportTo(d_exprManager
, d_variableMap
); }
283 }; /* class Command::ExportTransformer */
284 }; /* class Command */
287 * EmptyCommands are the residue of a command after the parser handles
288 * them (and there's nothing left to do).
290 class CVC4_PUBLIC EmptyCommand
: public Command
293 EmptyCommand(std::string name
= "");
294 std::string
getName() const;
295 void invoke(SmtEngine
* smtEngine
) override
;
296 Command
* exportTo(ExprManager
* exprManager
,
297 ExprManagerMapCollection
& variableMap
) override
;
298 Command
* clone() const override
;
299 std::string
getCommandName() const override
;
303 }; /* class EmptyCommand */
305 class CVC4_PUBLIC EchoCommand
: public Command
308 EchoCommand(std::string output
= "");
310 std::string
getOutput() const;
312 void invoke(SmtEngine
* smtEngine
) override
;
313 void invoke(SmtEngine
* smtEngine
, std::ostream
& out
) override
;
314 Command
* exportTo(ExprManager
* exprManager
,
315 ExprManagerMapCollection
& variableMap
) override
;
316 Command
* clone() const override
;
317 std::string
getCommandName() const override
;
320 std::string d_output
;
321 }; /* class EchoCommand */
323 class CVC4_PUBLIC AssertCommand
: public Command
330 AssertCommand(const Expr
& e
, bool inUnsatCore
= true);
332 Expr
getExpr() const;
334 void invoke(SmtEngine
* smtEngine
) override
;
335 Command
* exportTo(ExprManager
* exprManager
,
336 ExprManagerMapCollection
& variableMap
) override
;
337 Command
* clone() const override
;
338 std::string
getCommandName() const override
;
339 }; /* class AssertCommand */
341 class CVC4_PUBLIC PushCommand
: public Command
344 void invoke(SmtEngine
* smtEngine
) override
;
345 Command
* exportTo(ExprManager
* exprManager
,
346 ExprManagerMapCollection
& variableMap
) override
;
347 Command
* clone() const override
;
348 std::string
getCommandName() const override
;
349 }; /* class PushCommand */
351 class CVC4_PUBLIC PopCommand
: public Command
354 void invoke(SmtEngine
* smtEngine
) override
;
355 Command
* exportTo(ExprManager
* exprManager
,
356 ExprManagerMapCollection
& variableMap
) override
;
357 Command
* clone() const override
;
358 std::string
getCommandName() const override
;
359 }; /* class PopCommand */
361 class CVC4_PUBLIC DeclarationDefinitionCommand
: public Command
364 std::string d_symbol
;
367 DeclarationDefinitionCommand(const std::string
& id
);
369 void invoke(SmtEngine
* smtEngine
) override
= 0;
370 std::string
getSymbol() const;
371 }; /* class DeclarationDefinitionCommand */
373 class CVC4_PUBLIC DeclareFunctionCommand
: public DeclarationDefinitionCommand
379 bool d_printInModelSetByUser
;
382 DeclareFunctionCommand(const std::string
& id
, Expr func
, Type type
);
383 Expr
getFunction() const;
384 Type
getType() const;
385 bool getPrintInModel() const;
386 bool getPrintInModelSetByUser() const;
387 void setPrintInModel(bool p
);
389 void invoke(SmtEngine
* smtEngine
) override
;
390 Command
* exportTo(ExprManager
* exprManager
,
391 ExprManagerMapCollection
& variableMap
) override
;
392 Command
* clone() const override
;
393 std::string
getCommandName() const override
;
394 }; /* class DeclareFunctionCommand */
396 class CVC4_PUBLIC DeclareTypeCommand
: public DeclarationDefinitionCommand
403 DeclareTypeCommand(const std::string
& id
, size_t arity
, Type t
);
405 size_t getArity() const;
406 Type
getType() const;
408 void invoke(SmtEngine
* smtEngine
) override
;
409 Command
* exportTo(ExprManager
* exprManager
,
410 ExprManagerMapCollection
& variableMap
) override
;
411 Command
* clone() const override
;
412 std::string
getCommandName() const override
;
413 }; /* class DeclareTypeCommand */
415 class CVC4_PUBLIC DefineTypeCommand
: public DeclarationDefinitionCommand
418 std::vector
<Type
> d_params
;
422 DefineTypeCommand(const std::string
& id
, Type t
);
423 DefineTypeCommand(const std::string
& id
,
424 const std::vector
<Type
>& params
,
427 const std::vector
<Type
>& getParameters() const;
428 Type
getType() const;
430 void invoke(SmtEngine
* smtEngine
) override
;
431 Command
* exportTo(ExprManager
* exprManager
,
432 ExprManagerMapCollection
& variableMap
) override
;
433 Command
* clone() const override
;
434 std::string
getCommandName() const override
;
435 }; /* class DefineTypeCommand */
437 class CVC4_PUBLIC DefineFunctionCommand
: public DeclarationDefinitionCommand
441 std::vector
<Expr
> d_formals
;
445 DefineFunctionCommand(const std::string
& id
, Expr func
, Expr formula
);
446 DefineFunctionCommand(const std::string
& id
,
448 const std::vector
<Expr
>& formals
,
451 Expr
getFunction() const;
452 const std::vector
<Expr
>& getFormals() const;
453 Expr
getFormula() const;
455 void invoke(SmtEngine
* smtEngine
) override
;
456 Command
* exportTo(ExprManager
* exprManager
,
457 ExprManagerMapCollection
& variableMap
) override
;
458 Command
* clone() const override
;
459 std::string
getCommandName() const override
;
460 }; /* class DefineFunctionCommand */
463 * This differs from DefineFunctionCommand only in that it instructs
464 * the SmtEngine to "remember" this function for later retrieval with
465 * getAssignment(). Used for :named attributes in SMT-LIBv2.
467 class CVC4_PUBLIC DefineNamedFunctionCommand
: public DefineFunctionCommand
470 DefineNamedFunctionCommand(const std::string
& id
,
472 const std::vector
<Expr
>& formals
,
474 void invoke(SmtEngine
* smtEngine
) override
;
475 Command
* exportTo(ExprManager
* exprManager
,
476 ExprManagerMapCollection
& variableMap
) override
;
477 Command
* clone() const override
;
478 }; /* class DefineNamedFunctionCommand */
481 * The command when parsing define-fun-rec or define-funs-rec.
482 * This command will assert a set of quantified formulas that specify
483 * the (mutually recursive) function definitions provided to it.
485 class CVC4_PUBLIC DefineFunctionRecCommand
: public Command
488 DefineFunctionRecCommand(Expr func
,
489 const std::vector
<Expr
>& formals
,
491 DefineFunctionRecCommand(const std::vector
<Expr
>& funcs
,
492 const std::vector
<std::vector
<Expr
> >& formals
,
493 const std::vector
<Expr
>& formula
);
495 const std::vector
<Expr
>& getFunctions() const;
496 const std::vector
<std::vector
<Expr
> >& getFormals() const;
497 const std::vector
<Expr
>& getFormulas() const;
499 void invoke(SmtEngine
* smtEngine
) override
;
500 Command
* exportTo(ExprManager
* exprManager
,
501 ExprManagerMapCollection
& variableMap
) override
;
502 Command
* clone() const override
;
503 std::string
getCommandName() const override
;
506 /** functions we are defining */
507 std::vector
<Expr
> d_funcs
;
508 /** formal arguments for each of the functions we are defining */
509 std::vector
<std::vector
<Expr
> > d_formals
;
510 /** formulas corresponding to the bodies of the functions we are defining */
511 std::vector
<Expr
> d_formulas
;
512 }; /* class DefineFunctionRecCommand */
515 * The command when an attribute is set by a user. In SMT-LIBv2 this is done
516 * via the syntax (! expr :attr)
518 class CVC4_PUBLIC SetUserAttributeCommand
: public Command
521 SetUserAttributeCommand(const std::string
& attr
, Expr expr
);
522 SetUserAttributeCommand(const std::string
& attr
,
524 const std::vector
<Expr
>& values
);
525 SetUserAttributeCommand(const std::string
& attr
,
527 const std::string
& value
);
529 void invoke(SmtEngine
* smtEngine
) override
;
530 Command
* exportTo(ExprManager
* exprManager
,
531 ExprManagerMapCollection
& variableMap
) override
;
532 Command
* clone() const override
;
533 std::string
getCommandName() const override
;
536 SetUserAttributeCommand(const std::string
& attr
,
538 const std::vector
<Expr
>& expr_values
,
539 const std::string
& str_value
);
541 const std::string d_attr
;
543 const std::vector
<Expr
> d_expr_values
;
544 const std::string d_str_value
;
545 }; /* class SetUserAttributeCommand */
548 * The command when parsing check-sat.
549 * This command will check satisfiability of the input formula.
551 class CVC4_PUBLIC CheckSatCommand
: public Command
555 CheckSatCommand(const Expr
& expr
, bool inUnsatCore
= true);
557 Expr
getExpr() const;
558 Result
getResult() const;
559 void invoke(SmtEngine
* smtEngine
) override
;
560 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const override
;
561 Command
* exportTo(ExprManager
* exprManager
,
562 ExprManagerMapCollection
& variableMap
) override
;
563 Command
* clone() const override
;
564 std::string
getCommandName() const override
;
570 }; /* class CheckSatCommand */
573 * The command when parsing check-sat-assuming.
574 * This command will assume a set of formulas and check satisfiability of the
575 * input formula under these assumptions.
577 class CVC4_PUBLIC CheckSatAssumingCommand
: public Command
580 CheckSatAssumingCommand(Expr term
);
581 CheckSatAssumingCommand(const std::vector
<Expr
>& terms
,
582 bool inUnsatCore
= true);
584 const std::vector
<Expr
>& getTerms() const;
585 Result
getResult() const;
586 void invoke(SmtEngine
* smtEngine
) override
;
587 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const override
;
588 Command
* exportTo(ExprManager
* exprManager
,
589 ExprManagerMapCollection
& variableMap
) override
;
590 Command
* clone() const override
;
591 std::string
getCommandName() const override
;
594 std::vector
<Expr
> d_terms
;
597 }; /* class CheckSatAssumingCommand */
599 class CVC4_PUBLIC QueryCommand
: public Command
607 QueryCommand(const Expr
& e
, bool inUnsatCore
= true);
609 Expr
getExpr() const;
610 Result
getResult() const;
611 void invoke(SmtEngine
* smtEngine
) override
;
612 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const override
;
613 Command
* exportTo(ExprManager
* exprManager
,
614 ExprManagerMapCollection
& variableMap
) override
;
615 Command
* clone() const override
;
616 std::string
getCommandName() const override
;
617 }; /* class QueryCommand */
619 class CVC4_PUBLIC CheckSynthCommand
: public Command
623 CheckSynthCommand(const Expr
& expr
);
625 Expr
getExpr() const;
626 Result
getResult() const;
627 void invoke(SmtEngine
* smtEngine
) override
;
628 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const override
;
629 Command
* exportTo(ExprManager
* exprManager
,
630 ExprManagerMapCollection
& variableMap
) override
;
631 Command
* clone() const override
;
632 std::string
getCommandName() const override
;
635 /** the assertion of check-synth */
637 /** result of the check-synth call */
639 /** string stream that stores the output of the solution */
640 std::stringstream d_solution
;
641 }; /* class CheckSynthCommand */
643 // this is TRANSFORM in the CVC presentation language
644 class CVC4_PUBLIC SimplifyCommand
: public Command
651 SimplifyCommand(Expr term
);
653 Expr
getTerm() const;
654 Expr
getResult() const;
655 void invoke(SmtEngine
* smtEngine
) override
;
656 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const override
;
657 Command
* exportTo(ExprManager
* exprManager
,
658 ExprManagerMapCollection
& variableMap
) override
;
659 Command
* clone() const override
;
660 std::string
getCommandName() const override
;
661 }; /* class SimplifyCommand */
663 class CVC4_PUBLIC ExpandDefinitionsCommand
: public Command
670 ExpandDefinitionsCommand(Expr term
);
672 Expr
getTerm() const;
673 Expr
getResult() const;
674 void invoke(SmtEngine
* smtEngine
) override
;
675 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const override
;
676 Command
* exportTo(ExprManager
* exprManager
,
677 ExprManagerMapCollection
& variableMap
) override
;
678 Command
* clone() const override
;
679 std::string
getCommandName() const override
;
680 }; /* class ExpandDefinitionsCommand */
682 class CVC4_PUBLIC GetValueCommand
: public Command
685 std::vector
<Expr
> d_terms
;
689 GetValueCommand(Expr term
);
690 GetValueCommand(const std::vector
<Expr
>& terms
);
692 const std::vector
<Expr
>& getTerms() const;
693 Expr
getResult() const;
694 void invoke(SmtEngine
* smtEngine
) override
;
695 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const override
;
696 Command
* exportTo(ExprManager
* exprManager
,
697 ExprManagerMapCollection
& variableMap
) override
;
698 Command
* clone() const override
;
699 std::string
getCommandName() const override
;
700 }; /* class GetValueCommand */
702 class CVC4_PUBLIC GetAssignmentCommand
: public Command
708 GetAssignmentCommand();
710 SExpr
getResult() const;
711 void invoke(SmtEngine
* smtEngine
) override
;
712 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const override
;
713 Command
* exportTo(ExprManager
* exprManager
,
714 ExprManagerMapCollection
& variableMap
) override
;
715 Command
* clone() const override
;
716 std::string
getCommandName() const override
;
717 }; /* class GetAssignmentCommand */
719 class CVC4_PUBLIC GetModelCommand
: public Command
724 // Model is private to the library -- for now
725 // Model* getResult() const ;
726 void invoke(SmtEngine
* smtEngine
) override
;
727 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const override
;
728 Command
* exportTo(ExprManager
* exprManager
,
729 ExprManagerMapCollection
& variableMap
) override
;
730 Command
* clone() const override
;
731 std::string
getCommandName() const override
;
735 SmtEngine
* d_smtEngine
;
736 }; /* class GetModelCommand */
738 class CVC4_PUBLIC GetProofCommand
: public Command
743 const Proof
& getResult() const;
744 void invoke(SmtEngine
* smtEngine
) override
;
745 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const override
;
746 Command
* exportTo(ExprManager
* exprManager
,
747 ExprManagerMapCollection
& variableMap
) override
;
748 Command
* clone() const override
;
749 std::string
getCommandName() const override
;
752 SmtEngine
* d_smtEngine
;
753 // d_result is owned by d_smtEngine.
754 const Proof
* d_result
;
755 }; /* class GetProofCommand */
757 class CVC4_PUBLIC GetInstantiationsCommand
: public Command
760 GetInstantiationsCommand();
762 void invoke(SmtEngine
* smtEngine
) override
;
763 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const override
;
764 Command
* exportTo(ExprManager
* exprManager
,
765 ExprManagerMapCollection
& variableMap
) override
;
766 Command
* clone() const override
;
767 std::string
getCommandName() const override
;
770 SmtEngine
* d_smtEngine
;
771 }; /* class GetInstantiationsCommand */
773 class CVC4_PUBLIC GetSynthSolutionCommand
: public Command
776 GetSynthSolutionCommand();
778 void invoke(SmtEngine
* smtEngine
) override
;
779 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const override
;
780 Command
* exportTo(ExprManager
* exprManager
,
781 ExprManagerMapCollection
& variableMap
) override
;
782 Command
* clone() const override
;
783 std::string
getCommandName() const override
;
786 SmtEngine
* d_smtEngine
;
787 }; /* class GetSynthSolutionCommand */
789 class CVC4_PUBLIC GetQuantifierEliminationCommand
: public Command
797 GetQuantifierEliminationCommand();
798 GetQuantifierEliminationCommand(const Expr
& expr
, bool doFull
);
800 Expr
getExpr() const;
801 bool getDoFull() const;
802 void invoke(SmtEngine
* smtEngine
) override
;
803 Expr
getResult() const;
804 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const override
;
806 Command
* exportTo(ExprManager
* exprManager
,
807 ExprManagerMapCollection
& variableMap
) override
;
808 Command
* clone() const override
;
809 std::string
getCommandName() const override
;
810 }; /* class GetQuantifierEliminationCommand */
812 class CVC4_PUBLIC GetUnsatAssumptionsCommand
: public Command
815 GetUnsatAssumptionsCommand();
816 void invoke(SmtEngine
* smtEngine
) override
;
817 std::vector
<Expr
> getResult() const;
818 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const override
;
819 Command
* exportTo(ExprManager
* exprManager
,
820 ExprManagerMapCollection
& variableMap
) override
;
821 Command
* clone() const override
;
822 std::string
getCommandName() const override
;
824 std::vector
<Expr
> d_result
;
825 }; /* class GetUnsatAssumptionsCommand */
827 class CVC4_PUBLIC GetUnsatCoreCommand
: public Command
830 GetUnsatCoreCommand();
831 const UnsatCore
& getUnsatCore() const;
833 void invoke(SmtEngine
* smtEngine
) override
;
834 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const override
;
836 Command
* exportTo(ExprManager
* exprManager
,
837 ExprManagerMapCollection
& variableMap
) override
;
838 Command
* clone() const override
;
839 std::string
getCommandName() const override
;
842 // the result of the unsat core call
844 }; /* class GetUnsatCoreCommand */
846 class CVC4_PUBLIC GetAssertionsCommand
: public Command
849 std::string d_result
;
852 GetAssertionsCommand();
854 void invoke(SmtEngine
* smtEngine
) override
;
855 std::string
getResult() const;
856 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const override
;
857 Command
* exportTo(ExprManager
* exprManager
,
858 ExprManagerMapCollection
& variableMap
) override
;
859 Command
* clone() const override
;
860 std::string
getCommandName() const override
;
861 }; /* class GetAssertionsCommand */
863 class CVC4_PUBLIC SetBenchmarkStatusCommand
: public Command
866 BenchmarkStatus d_status
;
869 SetBenchmarkStatusCommand(BenchmarkStatus status
);
871 BenchmarkStatus
getStatus() const;
873 void invoke(SmtEngine
* smtEngine
) override
;
874 Command
* exportTo(ExprManager
* exprManager
,
875 ExprManagerMapCollection
& variableMap
) override
;
876 Command
* clone() const override
;
877 std::string
getCommandName() const override
;
878 }; /* class SetBenchmarkStatusCommand */
880 class CVC4_PUBLIC SetBenchmarkLogicCommand
: public Command
886 SetBenchmarkLogicCommand(std::string logic
);
888 std::string
getLogic() const;
889 void invoke(SmtEngine
* smtEngine
) override
;
890 Command
* exportTo(ExprManager
* exprManager
,
891 ExprManagerMapCollection
& variableMap
) override
;
892 Command
* clone() const override
;
893 std::string
getCommandName() const override
;
894 }; /* class SetBenchmarkLogicCommand */
896 class CVC4_PUBLIC SetInfoCommand
: public Command
903 SetInfoCommand(std::string flag
, const SExpr
& sexpr
);
905 std::string
getFlag() const;
906 SExpr
getSExpr() const;
908 void invoke(SmtEngine
* smtEngine
) override
;
909 Command
* exportTo(ExprManager
* exprManager
,
910 ExprManagerMapCollection
& variableMap
) override
;
911 Command
* clone() const override
;
912 std::string
getCommandName() const override
;
913 }; /* class SetInfoCommand */
915 class CVC4_PUBLIC GetInfoCommand
: public Command
919 std::string d_result
;
922 GetInfoCommand(std::string flag
);
924 std::string
getFlag() const;
925 std::string
getResult() const;
927 void invoke(SmtEngine
* smtEngine
) override
;
928 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const override
;
929 Command
* exportTo(ExprManager
* exprManager
,
930 ExprManagerMapCollection
& variableMap
) override
;
931 Command
* clone() const override
;
932 std::string
getCommandName() const override
;
933 }; /* class GetInfoCommand */
935 class CVC4_PUBLIC SetOptionCommand
: public Command
942 SetOptionCommand(std::string flag
, const SExpr
& sexpr
);
944 std::string
getFlag() const;
945 SExpr
getSExpr() const;
947 void invoke(SmtEngine
* smtEngine
) override
;
948 Command
* exportTo(ExprManager
* exprManager
,
949 ExprManagerMapCollection
& variableMap
) override
;
950 Command
* clone() const override
;
951 std::string
getCommandName() const override
;
952 }; /* class SetOptionCommand */
954 class CVC4_PUBLIC GetOptionCommand
: public Command
958 std::string d_result
;
961 GetOptionCommand(std::string flag
);
963 std::string
getFlag() const;
964 std::string
getResult() const;
966 void invoke(SmtEngine
* smtEngine
) override
;
967 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const override
;
968 Command
* exportTo(ExprManager
* exprManager
,
969 ExprManagerMapCollection
& variableMap
) override
;
970 Command
* clone() const override
;
971 std::string
getCommandName() const override
;
972 }; /* class GetOptionCommand */
974 // Set expression name command
975 // Note this is not an official smt2 command
977 // (assert (! expr :named name))
980 // (set-expr-name expr name)
981 class CVC4_PUBLIC SetExpressionNameCommand
: public Command
988 SetExpressionNameCommand(Expr expr
, std::string name
);
990 void invoke(SmtEngine
* smtEngine
) override
;
991 Command
* exportTo(ExprManager
* exprManager
,
992 ExprManagerMapCollection
& variableMap
) override
;
993 Command
* clone() const override
;
994 std::string
getCommandName() const override
;
995 }; /* class SetExpressionNameCommand */
997 class CVC4_PUBLIC DatatypeDeclarationCommand
: public Command
1000 std::vector
<DatatypeType
> d_datatypes
;
1003 DatatypeDeclarationCommand(const DatatypeType
& datatype
);
1005 DatatypeDeclarationCommand(const std::vector
<DatatypeType
>& datatypes
);
1006 const std::vector
<DatatypeType
>& getDatatypes() const;
1007 void invoke(SmtEngine
* smtEngine
) override
;
1008 Command
* exportTo(ExprManager
* exprManager
,
1009 ExprManagerMapCollection
& variableMap
) override
;
1010 Command
* clone() const override
;
1011 std::string
getCommandName() const override
;
1012 }; /* class DatatypeDeclarationCommand */
1014 class CVC4_PUBLIC RewriteRuleCommand
: public Command
1017 typedef std::vector
<std::vector
<Expr
> > Triggers
;
1020 typedef std::vector
<Expr
> VExpr
;
1025 Triggers d_triggers
;
1028 RewriteRuleCommand(const std::vector
<Expr
>& vars
,
1029 const std::vector
<Expr
>& guards
,
1032 const Triggers
& d_triggers
);
1033 RewriteRuleCommand(const std::vector
<Expr
>& vars
, Expr head
, Expr body
);
1035 const std::vector
<Expr
>& getVars() const;
1036 const std::vector
<Expr
>& getGuards() const;
1037 Expr
getHead() const;
1038 Expr
getBody() const;
1039 const Triggers
& getTriggers() const;
1041 void invoke(SmtEngine
* smtEngine
) override
;
1042 Command
* exportTo(ExprManager
* exprManager
,
1043 ExprManagerMapCollection
& variableMap
) override
;
1044 Command
* clone() const override
;
1045 std::string
getCommandName() const override
;
1046 }; /* class RewriteRuleCommand */
1048 class CVC4_PUBLIC PropagateRuleCommand
: public Command
1051 typedef std::vector
<std::vector
<Expr
> > Triggers
;
1054 typedef std::vector
<Expr
> VExpr
;
1059 Triggers d_triggers
;
1063 PropagateRuleCommand(const std::vector
<Expr
>& vars
,
1064 const std::vector
<Expr
>& guards
,
1065 const std::vector
<Expr
>& heads
,
1067 const Triggers
& d_triggers
,
1068 /* true if we want a deduction rule */
1069 bool d_deduction
= false);
1070 PropagateRuleCommand(const std::vector
<Expr
>& vars
,
1071 const std::vector
<Expr
>& heads
,
1073 bool d_deduction
= false);
1075 const std::vector
<Expr
>& getVars() const;
1076 const std::vector
<Expr
>& getGuards() const;
1077 const std::vector
<Expr
>& getHeads() const;
1078 Expr
getBody() const;
1079 const Triggers
& getTriggers() const;
1080 bool isDeduction() const;
1081 void invoke(SmtEngine
* smtEngine
) override
;
1082 Command
* exportTo(ExprManager
* exprManager
,
1083 ExprManagerMapCollection
& variableMap
) override
;
1084 Command
* clone() const override
;
1085 std::string
getCommandName() const override
;
1086 }; /* class PropagateRuleCommand */
1088 class CVC4_PUBLIC ResetCommand
: public Command
1092 void invoke(SmtEngine
* smtEngine
) override
;
1093 Command
* exportTo(ExprManager
* exprManager
,
1094 ExprManagerMapCollection
& variableMap
) override
;
1095 Command
* clone() const override
;
1096 std::string
getCommandName() const override
;
1097 }; /* class ResetCommand */
1099 class CVC4_PUBLIC ResetAssertionsCommand
: public Command
1102 ResetAssertionsCommand() {}
1103 void invoke(SmtEngine
* smtEngine
) override
;
1104 Command
* exportTo(ExprManager
* exprManager
,
1105 ExprManagerMapCollection
& variableMap
) override
;
1106 Command
* clone() const override
;
1107 std::string
getCommandName() const override
;
1108 }; /* class ResetAssertionsCommand */
1110 class CVC4_PUBLIC QuitCommand
: public Command
1114 void invoke(SmtEngine
* smtEngine
) override
;
1115 Command
* exportTo(ExprManager
* exprManager
,
1116 ExprManagerMapCollection
& variableMap
) override
;
1117 Command
* clone() const override
;
1118 std::string
getCommandName() const override
;
1119 }; /* class QuitCommand */
1121 class CVC4_PUBLIC CommentCommand
: public Command
1123 std::string d_comment
;
1126 CommentCommand(std::string comment
);
1128 std::string
getComment() const;
1130 void invoke(SmtEngine
* smtEngine
) override
;
1131 Command
* exportTo(ExprManager
* exprManager
,
1132 ExprManagerMapCollection
& variableMap
) override
;
1133 Command
* clone() const override
;
1134 std::string
getCommandName() const override
;
1135 }; /* class CommentCommand */
1137 class CVC4_PUBLIC CommandSequence
: public Command
1140 /** All the commands to be executed (in sequence) */
1141 std::vector
<Command
*> d_commandSequence
;
1142 /** Next command to be executed */
1143 unsigned int d_index
;
1149 void addCommand(Command
* cmd
);
1152 void invoke(SmtEngine
* smtEngine
) override
;
1153 void invoke(SmtEngine
* smtEngine
, std::ostream
& out
) override
;
1155 typedef std::vector
<Command
*>::iterator iterator
;
1156 typedef std::vector
<Command
*>::const_iterator const_iterator
;
1158 const_iterator
begin() const;
1159 const_iterator
end() const;
1164 Command
* exportTo(ExprManager
* exprManager
,
1165 ExprManagerMapCollection
& variableMap
) override
;
1166 Command
* clone() const override
;
1167 std::string
getCommandName() const override
;
1168 }; /* class CommandSequence */
1170 class CVC4_PUBLIC DeclarationSequence
: public CommandSequence
1174 } /* CVC4 namespace */
1176 #endif /* __CVC4__COMMAND_H */