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
{
472 SetUserAttributeCommand(const std::string
& attr
, Expr expr
) throw();
473 SetUserAttributeCommand(const std::string
& attr
, Expr expr
,
474 const std::vector
<Expr
>& values
) throw();
475 SetUserAttributeCommand(const std::string
& attr
, Expr expr
,
476 const std::string
& value
) throw();
477 ~SetUserAttributeCommand() throw() override
{}
479 void invoke(SmtEngine
* smtEngine
) override
;
480 Command
* exportTo(ExprManager
* exprManager
,
481 ExprManagerMapCollection
& variableMap
) override
;
482 Command
* clone() const override
;
483 std::string
getCommandName() const throw() override
;
486 SetUserAttributeCommand(const std::string
& attr
, Expr expr
,
487 const std::vector
<Expr
>& expr_values
,
488 const std::string
& str_value
) throw();
490 const std::string d_attr
;
492 const std::vector
<Expr
> d_expr_values
;
493 const std::string d_str_value
;
494 }; /* class SetUserAttributeCommand */
496 class CVC4_PUBLIC CheckSatCommand
: public Command
{
502 CheckSatCommand() throw();
503 CheckSatCommand(const Expr
& expr
, bool inUnsatCore
= true) throw();
504 ~CheckSatCommand() throw() {}
505 Expr
getExpr() const throw();
506 void invoke(SmtEngine
* smtEngine
);
507 Result
getResult() const throw();
508 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
509 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
510 Command
* clone() const;
511 std::string
getCommandName() const throw();
512 };/* class CheckSatCommand */
514 class CVC4_PUBLIC QueryCommand
: public Command
{
520 QueryCommand(const Expr
& e
, bool inUnsatCore
= true) throw();
521 ~QueryCommand() throw() {}
522 Expr
getExpr() const throw();
523 void invoke(SmtEngine
* smtEngine
);
524 Result
getResult() const throw();
525 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
526 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
527 Command
* clone() const;
528 std::string
getCommandName() const throw();
529 };/* class QueryCommand */
531 class CVC4_PUBLIC CheckSynthCommand
: public Command
{
533 CheckSynthCommand() throw();
534 CheckSynthCommand(const Expr
& expr
) throw();
535 ~CheckSynthCommand() throw() {}
536 Expr
getExpr() const throw();
537 void invoke(SmtEngine
* smtEngine
);
538 Result
getResult() const throw();
539 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
540 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
541 Command
* clone() const;
542 std::string
getCommandName() const throw();
545 /** the assertion of check-synth */
547 /** result of the check-synth call */
549 /** string stream that stores the output of the solution */
550 std::stringstream d_solution
;
551 };/* class CheckSynthCommand */
553 // this is TRANSFORM in the CVC presentation language
554 class CVC4_PUBLIC SimplifyCommand
: public Command
{
559 SimplifyCommand(Expr term
) throw();
560 ~SimplifyCommand() throw() {}
561 Expr
getTerm() const throw();
562 void invoke(SmtEngine
* smtEngine
);
563 Expr
getResult() const throw();
564 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
565 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
566 Command
* clone() const;
567 std::string
getCommandName() const throw();
568 };/* class SimplifyCommand */
570 class CVC4_PUBLIC ExpandDefinitionsCommand
: public Command
{
575 ExpandDefinitionsCommand(Expr term
) throw();
576 ~ExpandDefinitionsCommand() throw() {}
577 Expr
getTerm() const throw();
578 void invoke(SmtEngine
* smtEngine
);
579 Expr
getResult() const throw();
580 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
581 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
582 Command
* clone() const;
583 std::string
getCommandName() const throw();
584 };/* class ExpandDefinitionsCommand */
586 class CVC4_PUBLIC GetValueCommand
: public Command
{
588 std::vector
<Expr
> d_terms
;
591 GetValueCommand(Expr term
) throw();
592 GetValueCommand(const std::vector
<Expr
>& terms
) throw();
593 ~GetValueCommand() throw() {}
594 const std::vector
<Expr
>& getTerms() const throw();
595 void invoke(SmtEngine
* smtEngine
);
596 Expr
getResult() const throw();
597 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
598 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
599 Command
* clone() const;
600 std::string
getCommandName() const throw();
601 };/* class GetValueCommand */
603 class CVC4_PUBLIC GetAssignmentCommand
: public Command
{
607 GetAssignmentCommand() throw();
608 ~GetAssignmentCommand() throw() {}
609 void invoke(SmtEngine
* smtEngine
);
610 SExpr
getResult() const throw();
611 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
612 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
613 Command
* clone() const;
614 std::string
getCommandName() const throw();
615 };/* class GetAssignmentCommand */
617 class CVC4_PUBLIC GetModelCommand
: public Command
{
619 GetModelCommand() throw();
620 ~GetModelCommand() throw() {}
621 void invoke(SmtEngine
* smtEngine
);
622 // Model is private to the library -- for now
623 // Model* getResult() const throw();
624 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
625 Command
* exportTo(ExprManager
* exprManager
,
626 ExprManagerMapCollection
& variableMap
);
627 Command
* clone() const;
628 std::string
getCommandName() const throw();
632 SmtEngine
* d_smtEngine
;
633 }; /* class GetModelCommand */
635 class CVC4_PUBLIC GetProofCommand
: public Command
{
637 GetProofCommand() throw();
638 ~GetProofCommand() throw() {}
639 void invoke(SmtEngine
* smtEngine
);
640 const Proof
& getResult() const throw();
641 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
642 Command
* exportTo(ExprManager
* exprManager
,
643 ExprManagerMapCollection
& variableMap
);
644 Command
* clone() const;
645 std::string
getCommandName() const throw();
648 SmtEngine
* d_smtEngine
;
649 // d_result is owned by d_smtEngine.
650 const Proof
* d_result
;
651 }; /* class GetProofCommand */
653 class CVC4_PUBLIC GetInstantiationsCommand
: public Command
{
655 GetInstantiationsCommand() throw();
656 ~GetInstantiationsCommand() throw() {}
657 void invoke(SmtEngine
* smtEngine
);
658 // Instantiations* getResult() const throw();
659 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
660 Command
* exportTo(ExprManager
* exprManager
,
661 ExprManagerMapCollection
& variableMap
);
662 Command
* clone() const;
663 std::string
getCommandName() const throw();
666 SmtEngine
* d_smtEngine
;
667 }; /* class GetInstantiationsCommand */
669 class CVC4_PUBLIC GetSynthSolutionCommand
: public Command
{
671 GetSynthSolutionCommand() throw();
672 ~GetSynthSolutionCommand() throw() {}
673 void invoke(SmtEngine
* smtEngine
);
674 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
675 Command
* exportTo(ExprManager
* exprManager
,
676 ExprManagerMapCollection
& variableMap
);
677 Command
* clone() const;
678 std::string
getCommandName() const throw();
681 SmtEngine
* d_smtEngine
;
682 }; /* class GetSynthSolutionCommand */
684 class CVC4_PUBLIC GetQuantifierEliminationCommand
: public Command
{
690 GetQuantifierEliminationCommand() throw();
691 GetQuantifierEliminationCommand(const Expr
& expr
, bool doFull
) throw();
692 ~GetQuantifierEliminationCommand() throw() {}
693 Expr
getExpr() const throw();
694 bool getDoFull() const throw();
695 void invoke(SmtEngine
* smtEngine
);
696 Expr
getResult() const throw();
697 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
698 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
699 Command
* clone() const;
700 std::string
getCommandName() const throw();
701 };/* class GetQuantifierEliminationCommand */
703 class CVC4_PUBLIC GetUnsatCoreCommand
: public Command
{
705 GetUnsatCoreCommand() throw();
706 ~GetUnsatCoreCommand() throw() {}
707 void invoke(SmtEngine
* smtEngine
);
708 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
709 const UnsatCore
& getUnsatCore() const throw();
710 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
711 Command
* clone() const;
712 std::string
getCommandName() const throw();
715 // the result of the unsat core call
717 };/* class GetUnsatCoreCommand */
719 class CVC4_PUBLIC GetAssertionsCommand
: public Command
{
721 std::string d_result
;
723 GetAssertionsCommand() throw();
724 ~GetAssertionsCommand() throw() {}
725 void invoke(SmtEngine
* smtEngine
);
726 std::string
getResult() const throw();
727 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
728 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
729 Command
* clone() const;
730 std::string
getCommandName() const throw();
731 };/* class GetAssertionsCommand */
733 class CVC4_PUBLIC SetBenchmarkStatusCommand
: public Command
{
735 BenchmarkStatus d_status
;
737 SetBenchmarkStatusCommand(BenchmarkStatus status
) throw();
738 ~SetBenchmarkStatusCommand() throw() {}
739 BenchmarkStatus
getStatus() const throw();
740 void invoke(SmtEngine
* smtEngine
);
741 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
742 Command
* clone() const;
743 std::string
getCommandName() const throw();
744 };/* class SetBenchmarkStatusCommand */
746 class CVC4_PUBLIC SetBenchmarkLogicCommand
: public Command
{
750 SetBenchmarkLogicCommand(std::string logic
) throw();
751 ~SetBenchmarkLogicCommand() throw() {}
752 std::string
getLogic() const throw();
753 void invoke(SmtEngine
* smtEngine
);
754 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
755 Command
* clone() const;
756 std::string
getCommandName() const throw();
757 };/* class SetBenchmarkLogicCommand */
759 class CVC4_PUBLIC SetInfoCommand
: public Command
{
764 SetInfoCommand(std::string flag
, const SExpr
& sexpr
) throw();
765 ~SetInfoCommand() throw() {}
766 std::string
getFlag() const throw();
767 SExpr
getSExpr() const throw();
768 void invoke(SmtEngine
* smtEngine
);
769 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
770 Command
* clone() const;
771 std::string
getCommandName() const throw();
772 };/* class SetInfoCommand */
774 class CVC4_PUBLIC GetInfoCommand
: public Command
{
777 std::string d_result
;
779 GetInfoCommand(std::string flag
) throw();
780 ~GetInfoCommand() throw() {}
781 std::string
getFlag() const throw();
782 void invoke(SmtEngine
* smtEngine
);
783 std::string
getResult() const throw();
784 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
785 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
786 Command
* clone() const;
787 std::string
getCommandName() const throw();
788 };/* class GetInfoCommand */
790 class CVC4_PUBLIC SetOptionCommand
: public Command
{
795 SetOptionCommand(std::string flag
, const SExpr
& sexpr
) throw();
796 ~SetOptionCommand() throw() {}
797 std::string
getFlag() const throw();
798 SExpr
getSExpr() const throw();
799 void invoke(SmtEngine
* smtEngine
);
800 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
801 Command
* clone() const;
802 std::string
getCommandName() const throw();
803 };/* class SetOptionCommand */
805 class CVC4_PUBLIC GetOptionCommand
: public Command
{
808 std::string d_result
;
810 GetOptionCommand(std::string flag
) throw();
811 ~GetOptionCommand() throw() {}
812 std::string
getFlag() const throw();
813 void invoke(SmtEngine
* smtEngine
);
814 std::string
getResult() const throw();
815 void printResult(std::ostream
& out
, uint32_t verbosity
= 2) const;
816 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
817 Command
* clone() const;
818 std::string
getCommandName() const throw();
819 };/* class GetOptionCommand */
821 // Set expression name command
822 // Note this is not an official smt2 command
824 // (assert (! expr :named name))
827 // (set-expr-name expr name)
828 class CVC4_PUBLIC SetExpressionNameCommand
: public Command
{
833 SetExpressionNameCommand(Expr expr
, std::string name
) throw();
834 ~SetExpressionNameCommand() throw() {}
835 void invoke(SmtEngine
* smtEngine
);
836 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
837 Command
* clone() const;
838 std::string
getCommandName() const throw();
839 };/* class SetExpressionNameCommand */
842 class CVC4_PUBLIC DatatypeDeclarationCommand
: public Command
{
844 std::vector
<DatatypeType
> d_datatypes
;
846 DatatypeDeclarationCommand(const DatatypeType
& datatype
) throw();
847 ~DatatypeDeclarationCommand() throw() {}
848 DatatypeDeclarationCommand(const std::vector
<DatatypeType
>& datatypes
) throw();
849 const std::vector
<DatatypeType
>& getDatatypes() const throw();
850 void invoke(SmtEngine
* smtEngine
);
851 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
852 Command
* clone() const;
853 std::string
getCommandName() const throw();
854 };/* class DatatypeDeclarationCommand */
856 class CVC4_PUBLIC RewriteRuleCommand
: public Command
{
858 typedef std::vector
< std::vector
< Expr
> > Triggers
;
860 typedef std::vector
< Expr
> VExpr
;
867 RewriteRuleCommand(const std::vector
<Expr
>& vars
,
868 const std::vector
<Expr
>& guards
,
871 const Triggers
& d_triggers
) throw();
872 RewriteRuleCommand(const std::vector
<Expr
>& vars
,
875 ~RewriteRuleCommand() throw() {}
876 const std::vector
<Expr
>& getVars() const throw();
877 const std::vector
<Expr
>& getGuards() const throw();
878 Expr
getHead() const throw();
879 Expr
getBody() const throw();
880 const Triggers
& getTriggers() const throw();
881 void invoke(SmtEngine
* smtEngine
);
882 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
883 Command
* clone() const;
884 std::string
getCommandName() const throw();
885 };/* class RewriteRuleCommand */
887 class CVC4_PUBLIC PropagateRuleCommand
: public Command
{
889 typedef std::vector
< std::vector
< Expr
> > Triggers
;
891 typedef std::vector
< Expr
> VExpr
;
899 PropagateRuleCommand(const std::vector
<Expr
>& vars
,
900 const std::vector
<Expr
>& guards
,
901 const std::vector
<Expr
>& heads
,
903 const Triggers
& d_triggers
,
904 /* true if we want a deduction rule */
905 bool d_deduction
= false) throw();
906 PropagateRuleCommand(const std::vector
<Expr
>& vars
,
907 const std::vector
<Expr
>& heads
,
909 bool d_deduction
= false) throw();
910 ~PropagateRuleCommand() throw() {}
911 const std::vector
<Expr
>& getVars() const throw();
912 const std::vector
<Expr
>& getGuards() const throw();
913 const std::vector
<Expr
>& getHeads() const throw();
914 Expr
getBody() const throw();
915 const Triggers
& getTriggers() const throw();
916 bool isDeduction() 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 PropagateRuleCommand */
923 class CVC4_PUBLIC ResetCommand
: public Command
{
925 ResetCommand() throw() {}
926 ~ResetCommand() throw() {}
927 void invoke(SmtEngine
* smtEngine
);
928 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
929 Command
* clone() const;
930 std::string
getCommandName() const throw();
931 };/* class ResetCommand */
933 class CVC4_PUBLIC ResetAssertionsCommand
: public Command
{
935 ResetAssertionsCommand() throw() {}
936 ~ResetAssertionsCommand() throw() {}
937 void invoke(SmtEngine
* smtEngine
);
938 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
939 Command
* clone() const;
940 std::string
getCommandName() const throw();
941 };/* class ResetAssertionsCommand */
943 class CVC4_PUBLIC QuitCommand
: public Command
{
945 QuitCommand() throw() {}
946 ~QuitCommand() throw() {}
947 void invoke(SmtEngine
* smtEngine
);
948 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
949 Command
* clone() const;
950 std::string
getCommandName() const throw();
951 };/* class QuitCommand */
953 class CVC4_PUBLIC CommentCommand
: public Command
{
954 std::string d_comment
;
956 CommentCommand(std::string comment
) throw();
957 ~CommentCommand() throw() {}
958 std::string
getComment() const throw();
959 void invoke(SmtEngine
* smtEngine
);
960 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
961 Command
* clone() const;
962 std::string
getCommandName() const throw();
963 };/* class CommentCommand */
965 class CVC4_PUBLIC CommandSequence
: public Command
{
967 /** All the commands to be executed (in sequence) */
968 std::vector
<Command
*> d_commandSequence
;
969 /** Next command to be executed */
970 unsigned int d_index
;
972 CommandSequence() throw();
973 ~CommandSequence() throw();
975 void addCommand(Command
* cmd
) throw();
976 void clear() throw();
978 void invoke(SmtEngine
* smtEngine
);
979 void invoke(SmtEngine
* smtEngine
, std::ostream
& out
);
981 typedef std::vector
<Command
*>::iterator iterator
;
982 typedef std::vector
<Command
*>::const_iterator const_iterator
;
984 const_iterator
begin() const throw();
985 const_iterator
end() const throw();
987 iterator
begin() throw();
988 iterator
end() throw();
990 Command
* exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
);
991 Command
* clone() const;
992 std::string
getCommandName() const throw();
993 };/* class CommandSequence */
995 class CVC4_PUBLIC DeclarationSequence
: public CommandSequence
{
997 ~DeclarationSequence() throw() {}
998 };/* class DeclarationSequence */
1000 }/* CVC4 namespace */
1002 #endif /* __CVC4__COMMAND_H */