1 /********************* */
4 ** Top contributors (to current version):
5 ** Morgan Deters, Andrew Reynolds, Andres Noetzli
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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
&) throw() CVC4_PUBLIC
;
48 std::ostream
& operator<<(std::ostream
&, const Command
*) throw() CVC4_PUBLIC
;
49 std::ostream
& operator<<(std::ostream
&, const CommandStatus
&) throw() CVC4_PUBLIC
;
50 std::ostream
& operator<<(std::ostream
&, const CommandStatus
*) throw() CVC4_PUBLIC
;
52 /** The status an SMT benchmark can have */
53 enum BenchmarkStatus
{
54 /** Benchmark is satisfiable */
56 /** Benchmark is unsatisfiable */
58 /** The status of the benchmark is unknown */
60 };/* enum BenchmarkStatus */
62 std::ostream
& operator<<(std::ostream
& out
,
63 BenchmarkStatus status
) throw() 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
{
79 * The allocated index in ios_base for our depth setting.
81 static const int s_iosIndex
;
84 * The default setting, for ostreams that haven't yet had a
85 * setdepth() applied to them.
87 static const int s_defaultPrintSuccess
= false;
90 * When this manipulator is used, the setting is stored here.
96 * Construct a CommandPrintSuccess with the given setting.
98 CommandPrintSuccess(bool printSuccess
) throw() : d_printSuccess(printSuccess
) {}
100 inline void applyPrintSuccess(std::ostream
& out
) throw() {
101 out
.iword(s_iosIndex
) = d_printSuccess
;
104 static inline bool getPrintSuccess(std::ostream
& out
) throw() {
105 return out
.iword(s_iosIndex
);
108 static inline void setPrintSuccess(std::ostream
& out
, bool printSuccess
) throw() {
109 out
.iword(s_iosIndex
) = printSuccess
;
113 * Set the print-success state on the output stream for the current
114 * stack scope. This makes sure the old state is reset on the
115 * stream after normal OR exceptional exit from the scope, using the
120 bool d_oldPrintSuccess
;
124 inline Scope(std::ostream
& out
, bool printSuccess
) throw() :
126 d_oldPrintSuccess(CommandPrintSuccess::getPrintSuccess(out
)) {
127 CommandPrintSuccess::setPrintSuccess(out
, printSuccess
);
130 inline ~Scope() throw() {
131 CommandPrintSuccess::setPrintSuccess(d_out
, d_oldPrintSuccess
);
134 };/* class CommandPrintSuccess::Scope */
136 };/* class CommandPrintSuccess */
139 * Sets the default print-success setting when pretty-printing an Expr
140 * to an ostream. Use like this:
142 * // let out be an ostream, e an Expr
143 * out << Expr::setdepth(n) << e << endl;
145 * The depth stays permanently (until set again) with the stream.
147 inline std::ostream
& operator<<(std::ostream
& out
, CommandPrintSuccess cps
) throw() CVC4_PUBLIC
;
148 inline std::ostream
& operator<<(std::ostream
& out
, CommandPrintSuccess cps
) throw() {
149 cps
.applyPrintSuccess(out
);
153 class CVC4_PUBLIC CommandStatus
{
155 // shouldn't construct a CommandStatus (use a derived class)
156 CommandStatus() throw() {}
158 virtual ~CommandStatus() throw() {}
159 void toStream(std::ostream
& out
,
160 OutputLanguage language
= language::output::LANG_AUTO
) const throw();
161 virtual CommandStatus
& clone() const = 0;
162 };/* class CommandStatus */
164 class CVC4_PUBLIC CommandSuccess
: public CommandStatus
{
165 static const CommandSuccess
* s_instance
;
167 static const CommandSuccess
* instance() throw() { return s_instance
; }
168 CommandStatus
& clone() const { return const_cast<CommandSuccess
&>(*this); }
169 };/* class CommandSuccess */
171 class CVC4_PUBLIC CommandInterrupted
: public CommandStatus
{
172 static const CommandInterrupted
* s_instance
;
174 static const CommandInterrupted
* instance() throw() { return s_instance
; }
175 CommandStatus
& clone() const { return const_cast<CommandInterrupted
&>(*this); }
176 };/* class CommandInterrupted */
178 class CVC4_PUBLIC CommandUnsupported
: public CommandStatus
{
180 CommandStatus
& clone() const { return *new CommandUnsupported(*this); }
181 };/* class CommandSuccess */
183 class CVC4_PUBLIC CommandFailure
: public CommandStatus
{
184 std::string d_message
;
186 CommandFailure(std::string message
) throw() : d_message(message
) {}
187 CommandFailure
& clone() const { return *new CommandFailure(*this); }
188 ~CommandFailure() throw() {}
189 std::string
getMessage() const throw() { return d_message
; }
190 };/* class CommandFailure */
193 * The execution of the command resulted in a non-fatal error and further
194 * commands can be processed. This status is for example used when a user asks
195 * for an unsat core in a place that is not immediately preceded by an
196 * unsat/valid response.
198 class CVC4_PUBLIC CommandRecoverableFailure
: public CommandStatus
{
199 std::string d_message
;
202 CommandRecoverableFailure(std::string message
) throw() : d_message(message
) {}
203 CommandRecoverableFailure
& clone() const {
204 return *new CommandRecoverableFailure(*this);
206 ~CommandRecoverableFailure() throw() {}
207 std::string
getMessage() const throw() { return d_message
; }
208 }; /* class CommandRecoverableFailure */
210 class CVC4_PUBLIC Command
{
213 * This field contains a command status if the command has been
214 * invoked, or NULL if it has not. This field is either a
215 * dynamically-allocated pointer, or it's a pointer to the singleton
216 * CommandSuccess instance. Doing so is somewhat asymmetric, but
217 * it avoids the need to dynamically allocate memory in the common
218 * case of a successful command.
220 const CommandStatus
* d_commandStatus
;
223 * True if this command is "muted"---i.e., don't print "success" on
224 * successful execution.
229 typedef CommandPrintSuccess printsuccess
;
232 Command(const Command
& cmd
);
234 virtual ~Command() throw();
236 virtual void invoke(SmtEngine
* smtEngine
) = 0;
237 virtual void invoke(SmtEngine
* smtEngine
, std::ostream
& out
);
239 virtual void toStream(std::ostream
& out
, int toDepth
= -1, bool types
= false, size_t dag
= 1,
240 OutputLanguage language
= language::output::LANG_AUTO
) const throw();
242 std::string
toString() const throw();
244 virtual std::string
getCommandName() const throw() = 0;
247 * If false, instruct this Command not to print a success message.
249 void setMuted(bool muted
) throw() { d_muted
= muted
; }
252 * Determine whether this Command will print a success message.
254 bool isMuted() throw() { return d_muted
; }
257 * Either the command hasn't run yet, or it completed successfully
258 * (CommandSuccess, not CommandUnsupported or CommandFailure).
260 bool ok() const throw();
263 * The command completed in a failure state (CommandFailure, not
264 * CommandSuccess or CommandUnsupported).
266 bool fail() const throw();
269 * The command was ran but was interrupted due to resource limiting.
271 bool interrupted() const throw();
273 /** Get the command status (it's NULL if we haven't run yet). */
274 const CommandStatus
* getCommandStatus() const throw() { return d_commandStatus
; }
276 virtual void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
279 * Maps this Command into one for a different ExprManager, using
280 * variableMap for the translation and extending it with any new
283 virtual Command
* exportTo(ExprManager
* exprManager
,
284 ExprManagerMapCollection
& variableMap
) = 0;
287 * Clone this Command (make a shallow copy).
289 virtual Command
* clone() const = 0;
292 class ExportTransformer
{
293 ExprManager
* d_exprManager
;
294 ExprManagerMapCollection
& d_variableMap
;
296 ExportTransformer(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
) :
297 d_exprManager(exprManager
),
298 d_variableMap(variableMap
) {
300 Expr
operator()(Expr e
) {
301 return e
.exportTo(d_exprManager
, d_variableMap
);
303 Type
operator()(Type t
) {
304 return t
.exportTo(d_exprManager
, d_variableMap
);
306 };/* class Command::ExportTransformer */
307 };/* class Command */
310 * EmptyCommands are the residue of a command after the parser handles
311 * them (and there's nothing left to do).
313 class CVC4_PUBLIC EmptyCommand
: public Command
{
317 EmptyCommand(std::string name
= "") throw();
318 ~EmptyCommand() throw() {}
319 std::string
getName() const throw();
320 void invoke(SmtEngine
* smtEngine
);
321 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
322 Command
* clone() const;
323 std::string
getCommandName() const throw();
324 };/* class EmptyCommand */
326 class CVC4_PUBLIC EchoCommand
: public Command
{
328 std::string d_output
;
330 EchoCommand(std::string output
= "") throw();
331 ~EchoCommand() throw() {}
332 std::string
getOutput() const throw();
333 void invoke(SmtEngine
* smtEngine
);
334 void invoke(SmtEngine
* smtEngine
, std::ostream
& out
);
335 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
336 Command
* clone() const;
337 std::string
getCommandName() const throw();
338 };/* class EchoCommand */
340 class CVC4_PUBLIC AssertCommand
: public Command
{
345 AssertCommand(const Expr
& e
, bool inUnsatCore
= true) throw();
346 ~AssertCommand() throw() {}
347 Expr
getExpr() const throw();
348 void invoke(SmtEngine
* smtEngine
);
349 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
350 Command
* clone() const;
351 std::string
getCommandName() const throw();
352 };/* class AssertCommand */
354 class CVC4_PUBLIC PushCommand
: public Command
{
356 ~PushCommand() throw() {}
357 void invoke(SmtEngine
* smtEngine
);
358 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
359 Command
* clone() const;
360 std::string
getCommandName() const throw();
361 };/* class PushCommand */
363 class CVC4_PUBLIC PopCommand
: public Command
{
365 ~PopCommand() throw() {}
366 void invoke(SmtEngine
* smtEngine
);
367 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
368 Command
* clone() const;
369 std::string
getCommandName() const throw();
370 };/* class PopCommand */
372 class CVC4_PUBLIC DeclarationDefinitionCommand
: public Command
{
374 std::string d_symbol
;
376 DeclarationDefinitionCommand(const std::string
& id
) throw();
377 ~DeclarationDefinitionCommand() throw() {}
378 virtual void invoke(SmtEngine
* smtEngine
) = 0;
379 std::string
getSymbol() const throw();
380 };/* class DeclarationDefinitionCommand */
382 class CVC4_PUBLIC DeclareFunctionCommand
: public DeclarationDefinitionCommand
{
387 bool d_printInModelSetByUser
;
389 DeclareFunctionCommand(const std::string
& id
, Expr func
, Type type
) throw();
390 ~DeclareFunctionCommand() throw() {}
391 Expr
getFunction() const throw();
392 Type
getType() const throw();
393 bool getPrintInModel() const throw();
394 bool getPrintInModelSetByUser() const throw();
395 void setPrintInModel( bool p
);
396 void invoke(SmtEngine
* smtEngine
);
397 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
398 Command
* clone() const;
399 std::string
getCommandName() const throw();
400 };/* class DeclareFunctionCommand */
402 class CVC4_PUBLIC DeclareTypeCommand
: public DeclarationDefinitionCommand
{
407 DeclareTypeCommand(const std::string
& id
, size_t arity
, Type t
) throw();
408 ~DeclareTypeCommand() throw() {}
409 size_t getArity() const throw();
410 Type
getType() const throw();
411 void invoke(SmtEngine
* smtEngine
);
412 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
413 Command
* clone() const;
414 std::string
getCommandName() const throw();
415 };/* class DeclareTypeCommand */
417 class CVC4_PUBLIC DefineTypeCommand
: public DeclarationDefinitionCommand
{
419 std::vector
<Type
> d_params
;
422 DefineTypeCommand(const std::string
& id
, Type t
) throw();
423 DefineTypeCommand(const std::string
& id
, const std::vector
<Type
>& params
, Type t
) throw();
424 ~DefineTypeCommand() throw() {}
425 const std::vector
<Type
>& getParameters() const throw();
426 Type
getType() const throw();
427 void invoke(SmtEngine
* smtEngine
);
428 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
429 Command
* clone() const;
430 std::string
getCommandName() const throw();
431 };/* class DefineTypeCommand */
433 class CVC4_PUBLIC DefineFunctionCommand
: public DeclarationDefinitionCommand
{
436 std::vector
<Expr
> d_formals
;
439 DefineFunctionCommand(const std::string
& id
, Expr func
, Expr formula
) throw();
440 DefineFunctionCommand(const std::string
& id
, Expr func
,
441 const std::vector
<Expr
>& formals
, Expr formula
) throw();
442 ~DefineFunctionCommand() throw() {}
443 Expr
getFunction() const throw();
444 const std::vector
<Expr
>& getFormals() const throw();
445 Expr
getFormula() const throw();
446 void invoke(SmtEngine
* smtEngine
);
447 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
448 Command
* clone() const;
449 std::string
getCommandName() const throw();
450 };/* class DefineFunctionCommand */
453 * This differs from DefineFunctionCommand only in that it instructs
454 * the SmtEngine to "remember" this function for later retrieval with
455 * getAssignment(). Used for :named attributes in SMT-LIBv2.
457 class CVC4_PUBLIC DefineNamedFunctionCommand
: public DefineFunctionCommand
{
459 DefineNamedFunctionCommand(const std::string
& id
, Expr func
,
460 const std::vector
<Expr
>& formals
, Expr formula
) throw();
461 void invoke(SmtEngine
* smtEngine
);
462 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
463 Command
* clone() const;
464 };/* class DefineNamedFunctionCommand */
467 * The command when an attribute is set by a user. In SMT-LIBv2 this is done
468 * via the syntax (! expr :attr)
470 class CVC4_PUBLIC SetUserAttributeCommand
: public Command
{
474 std::vector
<Expr
> d_expr_values
;
475 std::string d_str_value
;
477 SetUserAttributeCommand( const std::string
& attr
, Expr expr
) throw();
478 SetUserAttributeCommand( const std::string
& attr
, Expr expr
, std::vector
<Expr
>& values
) throw();
479 SetUserAttributeCommand( const std::string
& attr
, Expr expr
, const std::string
& value
) throw();
480 ~SetUserAttributeCommand() throw() {}
481 void invoke(SmtEngine
* smtEngine
);
482 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
483 Command
* clone() const;
484 std::string
getCommandName() const throw();
485 };/* class SetUserAttributeCommand */
487 class CVC4_PUBLIC CheckSatCommand
: public Command
{
493 CheckSatCommand() throw();
494 CheckSatCommand(const Expr
& expr
, bool inUnsatCore
= true) throw();
495 ~CheckSatCommand() throw() {}
496 Expr
getExpr() const throw();
497 void invoke(SmtEngine
* smtEngine
);
498 Result
getResult() const throw();
499 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
500 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
501 Command
* clone() const;
502 std::string
getCommandName() const throw();
503 };/* class CheckSatCommand */
505 class CVC4_PUBLIC QueryCommand
: public Command
{
511 QueryCommand(const Expr
& e
, bool inUnsatCore
= true) throw();
512 ~QueryCommand() throw() {}
513 Expr
getExpr() const throw();
514 void invoke(SmtEngine
* smtEngine
);
515 Result
getResult() const throw();
516 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
517 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
518 Command
* clone() const;
519 std::string
getCommandName() const throw();
520 };/* class QueryCommand */
522 class CVC4_PUBLIC CheckSynthCommand
: public Command
{
528 CheckSynthCommand() throw();
529 CheckSynthCommand(const Expr
& expr
, bool inUnsatCore
= true) throw();
530 ~CheckSynthCommand() throw() {}
531 Expr
getExpr() const throw();
532 void invoke(SmtEngine
* smtEngine
);
533 Result
getResult() const throw();
534 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
535 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
536 Command
* clone() const;
537 std::string
getCommandName() const throw();
538 };/* class CheckSynthCommand */
540 // this is TRANSFORM in the CVC presentation language
541 class CVC4_PUBLIC SimplifyCommand
: public Command
{
546 SimplifyCommand(Expr term
) throw();
547 ~SimplifyCommand() throw() {}
548 Expr
getTerm() const throw();
549 void invoke(SmtEngine
* smtEngine
);
550 Expr
getResult() const throw();
551 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
552 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
553 Command
* clone() const;
554 std::string
getCommandName() const throw();
555 };/* class SimplifyCommand */
557 class CVC4_PUBLIC ExpandDefinitionsCommand
: public Command
{
562 ExpandDefinitionsCommand(Expr term
) throw();
563 ~ExpandDefinitionsCommand() throw() {}
564 Expr
getTerm() const throw();
565 void invoke(SmtEngine
* smtEngine
);
566 Expr
getResult() const throw();
567 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
568 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
569 Command
* clone() const;
570 std::string
getCommandName() const throw();
571 };/* class ExpandDefinitionsCommand */
573 class CVC4_PUBLIC GetValueCommand
: public Command
{
575 std::vector
<Expr
> d_terms
;
578 GetValueCommand(Expr term
) throw();
579 GetValueCommand(const std::vector
<Expr
>& terms
) throw();
580 ~GetValueCommand() throw() {}
581 const std::vector
<Expr
>& getTerms() const throw();
582 void invoke(SmtEngine
* smtEngine
);
583 Expr
getResult() const throw();
584 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
585 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
586 Command
* clone() const;
587 std::string
getCommandName() const throw();
588 };/* class GetValueCommand */
590 class CVC4_PUBLIC GetAssignmentCommand
: public Command
{
594 GetAssignmentCommand() throw();
595 ~GetAssignmentCommand() throw() {}
596 void invoke(SmtEngine
* smtEngine
);
597 SExpr
getResult() const throw();
598 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
599 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
600 Command
* clone() const;
601 std::string
getCommandName() const throw();
602 };/* class GetAssignmentCommand */
604 class CVC4_PUBLIC GetModelCommand
: public Command
{
607 SmtEngine
* d_smtEngine
;
609 GetModelCommand() throw();
610 ~GetModelCommand() throw() {}
611 void invoke(SmtEngine
* smtEngine
);
612 // Model is private to the library -- for now
613 //Model* getResult() const throw();
614 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
615 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
616 Command
* clone() const;
617 std::string
getCommandName() const throw();
618 };/* class GetModelCommand */
620 class CVC4_PUBLIC GetProofCommand
: public Command
{
623 SmtEngine
* d_smtEngine
;
625 GetProofCommand() throw();
626 ~GetProofCommand() throw() {}
627 void invoke(SmtEngine
* smtEngine
);
628 Proof
* getResult() const throw();
629 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
630 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
631 Command
* clone() const;
632 std::string
getCommandName() const throw();
633 };/* class GetProofCommand */
635 class CVC4_PUBLIC GetInstantiationsCommand
: public Command
{
637 //Instantiations* d_result;
638 SmtEngine
* d_smtEngine
;
640 GetInstantiationsCommand() throw();
641 ~GetInstantiationsCommand() throw() {}
642 void invoke(SmtEngine
* smtEngine
);
643 //Instantiations* getResult() const throw();
644 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
645 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
646 Command
* clone() const;
647 std::string
getCommandName() const throw();
648 };/* class GetInstantiationsCommand */
650 class CVC4_PUBLIC GetSynthSolutionCommand
: public Command
{
652 SmtEngine
* d_smtEngine
;
654 GetSynthSolutionCommand() throw();
655 ~GetSynthSolutionCommand() throw() {}
656 void invoke(SmtEngine
* smtEngine
);
657 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
658 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
659 Command
* clone() const;
660 std::string
getCommandName() const throw();
661 };/* class GetSynthSolutionCommand */
663 class CVC4_PUBLIC GetQuantifierEliminationCommand
: public Command
{
669 GetQuantifierEliminationCommand() throw();
670 GetQuantifierEliminationCommand(const Expr
& expr
, bool doFull
) throw();
671 ~GetQuantifierEliminationCommand() throw() {}
672 Expr
getExpr() const throw();
673 bool getDoFull() const throw();
674 void invoke(SmtEngine
* smtEngine
);
675 Expr
getResult() const throw();
676 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
677 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
678 Command
* clone() const;
679 std::string
getCommandName() const throw();
680 };/* class GetQuantifierEliminationCommand */
682 class CVC4_PUBLIC GetUnsatCoreCommand
: public Command
{
685 std::map
<Expr
, std::string
> d_names
;
687 GetUnsatCoreCommand() throw();
688 GetUnsatCoreCommand(const std::map
<Expr
, std::string
>& names
) throw();
689 ~GetUnsatCoreCommand() throw() {}
690 void invoke(SmtEngine
* smtEngine
);
691 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
692 const UnsatCore
& getUnsatCore() const throw();
693 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
694 Command
* clone() const;
695 std::string
getCommandName() const throw();
696 };/* class GetUnsatCoreCommand */
698 class CVC4_PUBLIC GetAssertionsCommand
: public Command
{
700 std::string d_result
;
702 GetAssertionsCommand() throw();
703 ~GetAssertionsCommand() throw() {}
704 void invoke(SmtEngine
* smtEngine
);
705 std::string
getResult() const throw();
706 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
707 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
708 Command
* clone() const;
709 std::string
getCommandName() const throw();
710 };/* class GetAssertionsCommand */
712 class CVC4_PUBLIC SetBenchmarkStatusCommand
: public Command
{
714 BenchmarkStatus d_status
;
716 SetBenchmarkStatusCommand(BenchmarkStatus status
) throw();
717 ~SetBenchmarkStatusCommand() throw() {}
718 BenchmarkStatus
getStatus() const throw();
719 void invoke(SmtEngine
* smtEngine
);
720 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
721 Command
* clone() const;
722 std::string
getCommandName() const throw();
723 };/* class SetBenchmarkStatusCommand */
725 class CVC4_PUBLIC SetBenchmarkLogicCommand
: public Command
{
729 SetBenchmarkLogicCommand(std::string logic
) throw();
730 ~SetBenchmarkLogicCommand() throw() {}
731 std::string
getLogic() const throw();
732 void invoke(SmtEngine
* smtEngine
);
733 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
734 Command
* clone() const;
735 std::string
getCommandName() const throw();
736 };/* class SetBenchmarkLogicCommand */
738 class CVC4_PUBLIC SetInfoCommand
: public Command
{
743 SetInfoCommand(std::string flag
, const SExpr
& sexpr
) throw();
744 ~SetInfoCommand() throw() {}
745 std::string
getFlag() const throw();
746 SExpr
getSExpr() const throw();
747 void invoke(SmtEngine
* smtEngine
);
748 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
749 Command
* clone() const;
750 std::string
getCommandName() const throw();
751 };/* class SetInfoCommand */
753 class CVC4_PUBLIC GetInfoCommand
: public Command
{
756 std::string d_result
;
758 GetInfoCommand(std::string flag
) throw();
759 ~GetInfoCommand() throw() {}
760 std::string
getFlag() const throw();
761 void invoke(SmtEngine
* smtEngine
);
762 std::string
getResult() const throw();
763 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
764 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
765 Command
* clone() const;
766 std::string
getCommandName() const throw();
767 };/* class GetInfoCommand */
769 class CVC4_PUBLIC SetOptionCommand
: public Command
{
774 SetOptionCommand(std::string flag
, const SExpr
& sexpr
) throw();
775 ~SetOptionCommand() throw() {}
776 std::string
getFlag() const throw();
777 SExpr
getSExpr() const throw();
778 void invoke(SmtEngine
* smtEngine
);
779 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
780 Command
* clone() const;
781 std::string
getCommandName() const throw();
782 };/* class SetOptionCommand */
784 class CVC4_PUBLIC GetOptionCommand
: public Command
{
787 std::string d_result
;
789 GetOptionCommand(std::string flag
) throw();
790 ~GetOptionCommand() throw() {}
791 std::string
getFlag() const throw();
792 void invoke(SmtEngine
* smtEngine
);
793 std::string
getResult() const throw();
794 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
795 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
796 Command
* clone() const;
797 std::string
getCommandName() const throw();
798 };/* class GetOptionCommand */
800 class CVC4_PUBLIC DatatypeDeclarationCommand
: public Command
{
802 std::vector
<DatatypeType
> d_datatypes
;
804 DatatypeDeclarationCommand(const DatatypeType
& datatype
) throw();
805 ~DatatypeDeclarationCommand() throw() {}
806 DatatypeDeclarationCommand(const std::vector
<DatatypeType
>& datatypes
) throw();
807 const std::vector
<DatatypeType
>& getDatatypes() const throw();
808 void invoke(SmtEngine
* smtEngine
);
809 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
810 Command
* clone() const;
811 std::string
getCommandName() const throw();
812 };/* class DatatypeDeclarationCommand */
814 class CVC4_PUBLIC RewriteRuleCommand
: public Command
{
816 typedef std::vector
< std::vector
< Expr
> > Triggers
;
818 typedef std::vector
< Expr
> VExpr
;
825 RewriteRuleCommand(const std::vector
<Expr
>& vars
,
826 const std::vector
<Expr
>& guards
,
829 const Triggers
& d_triggers
) throw();
830 RewriteRuleCommand(const std::vector
<Expr
>& vars
,
833 ~RewriteRuleCommand() throw() {}
834 const std::vector
<Expr
>& getVars() const throw();
835 const std::vector
<Expr
>& getGuards() const throw();
836 Expr
getHead() const throw();
837 Expr
getBody() const throw();
838 const Triggers
& getTriggers() const throw();
839 void invoke(SmtEngine
* smtEngine
);
840 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
841 Command
* clone() const;
842 std::string
getCommandName() const throw();
843 };/* class RewriteRuleCommand */
845 class CVC4_PUBLIC PropagateRuleCommand
: public Command
{
847 typedef std::vector
< std::vector
< Expr
> > Triggers
;
849 typedef std::vector
< Expr
> VExpr
;
857 PropagateRuleCommand(const std::vector
<Expr
>& vars
,
858 const std::vector
<Expr
>& guards
,
859 const std::vector
<Expr
>& heads
,
861 const Triggers
& d_triggers
,
862 /* true if we want a deduction rule */
863 bool d_deduction
= false) throw();
864 PropagateRuleCommand(const std::vector
<Expr
>& vars
,
865 const std::vector
<Expr
>& heads
,
867 bool d_deduction
= false) throw();
868 ~PropagateRuleCommand() throw() {}
869 const std::vector
<Expr
>& getVars() const throw();
870 const std::vector
<Expr
>& getGuards() const throw();
871 const std::vector
<Expr
>& getHeads() const throw();
872 Expr
getBody() const throw();
873 const Triggers
& getTriggers() const throw();
874 bool isDeduction() const throw();
875 void invoke(SmtEngine
* smtEngine
);
876 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
877 Command
* clone() const;
878 std::string
getCommandName() const throw();
879 };/* class PropagateRuleCommand */
881 class CVC4_PUBLIC ResetCommand
: public Command
{
883 ResetCommand() throw() {}
884 ~ResetCommand() throw() {}
885 void invoke(SmtEngine
* smtEngine
);
886 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
887 Command
* clone() const;
888 std::string
getCommandName() const throw();
889 };/* class ResetCommand */
891 class CVC4_PUBLIC ResetAssertionsCommand
: public Command
{
893 ResetAssertionsCommand() throw() {}
894 ~ResetAssertionsCommand() throw() {}
895 void invoke(SmtEngine
* smtEngine
);
896 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
897 Command
* clone() const;
898 std::string
getCommandName() const throw();
899 };/* class ResetAssertionsCommand */
901 class CVC4_PUBLIC QuitCommand
: public Command
{
903 QuitCommand() throw() {}
904 ~QuitCommand() throw() {}
905 void invoke(SmtEngine
* smtEngine
);
906 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
907 Command
* clone() const;
908 std::string
getCommandName() const throw();
909 };/* class QuitCommand */
911 class CVC4_PUBLIC CommentCommand
: public Command
{
912 std::string d_comment
;
914 CommentCommand(std::string comment
) throw();
915 ~CommentCommand() throw() {}
916 std::string
getComment() const throw();
917 void invoke(SmtEngine
* smtEngine
);
918 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
919 Command
* clone() const;
920 std::string
getCommandName() const throw();
921 };/* class CommentCommand */
923 class CVC4_PUBLIC CommandSequence
: public Command
{
925 /** All the commands to be executed (in sequence) */
926 std::vector
<Command
*> d_commandSequence
;
927 /** Next command to be executed */
928 unsigned int d_index
;
930 CommandSequence() throw();
931 ~CommandSequence() throw();
933 void addCommand(Command
* cmd
) throw();
934 void clear() throw();
936 void invoke(SmtEngine
* smtEngine
);
937 void invoke(SmtEngine
* smtEngine
, std::ostream
& out
);
939 typedef std::vector
<Command
*>::iterator iterator
;
940 typedef std::vector
<Command
*>::const_iterator const_iterator
;
942 const_iterator
begin() const throw();
943 const_iterator
end() const throw();
945 iterator
begin() throw();
946 iterator
end() throw();
948 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
949 Command
* clone() const;
950 std::string
getCommandName() const throw();
951 };/* class CommandSequence */
953 class CVC4_PUBLIC DeclarationSequence
: public CommandSequence
{
955 ~DeclarationSequence() throw() {}
956 };/* class DeclarationSequence */
958 }/* CVC4 namespace */
960 #endif /* __CVC4__COMMAND_H */