22 #ifndef __CVC4__COMMAND_H 23 #define __CVC4__COMMAND_H 47 std::ostream& operator<<(
std::ostream&, const Command*) throw() CVC4_PUBLIC;
48 std::ostream& operator<<(
std::ostream&, const CommandStatus&) throw() CVC4_PUBLIC;
49 std::ostream& operator<<(
std::ostream&, const CommandStatus*) throw() CVC4_PUBLIC;
80 static const int s_iosIndex;
86 static const int s_defaultPrintSuccess =
false;
100 out.iword(s_iosIndex) = d_printSuccess;
104 return out.iword(s_iosIndex);
119 bool d_oldPrintSuccess;
158 void toStream(std::ostream& out,
176 std::string d_message;
210 virtual
void invoke(
SmtEngine* smtEngine) throw() = 0;
211 virtual
void invoke(
SmtEngine* smtEngine,
std::ostream& out) throw();
213 virtual
void toStream(
std::ostream& out,
int toDepth = -1,
bool types = false,
size_t dag = 1,
216 std::
string toString() const throw();
218 virtual
std::
string getCommandName() const throw() = 0;
223 void setMuted(
bool muted) throw() { d_muted = muted; }
234 bool ok()
const throw();
240 bool fail()
const throw();
245 virtual void printResult(std::ostream& out, uint32_t
verbosity = 2)
const throw();
258 virtual Command* clone()
const = 0;
266 d_exprManager(exprManager),
267 d_variableMap(variableMap) {
270 return e.
exportTo(d_exprManager, d_variableMap);
273 return t.
exportTo(d_exprManager, d_variableMap);
288 std::string getName()
const throw();
289 void invoke(
SmtEngine* smtEngine)
throw();
292 std::string getCommandName()
const throw();
301 std::string getOutput()
const throw();
302 void invoke(
SmtEngine* smtEngine)
throw();
303 void invoke(
SmtEngine* smtEngine, std::ostream& out)
throw();
306 std::string getCommandName()
const throw();
315 Expr getExpr()
const throw();
316 void invoke(
SmtEngine* smtEngine)
throw();
319 std::string getCommandName()
const throw();
325 void invoke(
SmtEngine* smtEngine)
throw();
328 std::string getCommandName()
const throw();
334 void invoke(
SmtEngine* smtEngine)
throw();
337 std::string getCommandName()
const throw();
346 virtual void invoke(
SmtEngine* smtEngine)
throw() = 0;
347 std::string getSymbol()
const throw();
359 Expr getFunction()
const throw();
360 Type getType()
const throw();
361 bool getPrintInModel()
const throw();
362 bool getPrintInModelSetByUser()
const throw();
363 void setPrintInModel(
bool p );
364 void invoke(
SmtEngine* smtEngine)
throw();
367 std::string getCommandName()
const throw();
377 size_t getArity()
const throw();
378 Type getType()
const throw();
379 void invoke(
SmtEngine* smtEngine)
throw();
382 std::string getCommandName()
const throw();
393 const std::vector<Type>& getParameters()
const throw();
394 Type getType()
const throw();
395 void invoke(
SmtEngine* smtEngine)
throw();
398 std::string getCommandName()
const throw();
409 const std::vector<Expr>& formals,
Expr formula)
throw();
411 Expr getFunction()
const throw();
412 const std::vector<Expr>& getFormals()
const throw();
413 Expr getFormula()
const throw();
414 void invoke(
SmtEngine* smtEngine)
throw();
417 std::string getCommandName()
const throw();
428 const std::vector<Expr>& formals,
Expr formula)
throw();
429 void invoke(
SmtEngine* smtEngine)
throw();
449 void invoke(
SmtEngine* smtEngine)
throw();
452 std::string getCommandName()
const throw();
464 Expr getExpr()
const throw();
465 void invoke(
SmtEngine* smtEngine)
throw();
466 Result getResult()
const throw();
467 void printResult(std::ostream& out, uint32_t
verbosity = 2)
const throw();
470 std::string getCommandName()
const throw();
480 Expr getExpr()
const throw();
481 void invoke(
SmtEngine* smtEngine)
throw();
482 Result getResult()
const throw();
483 void printResult(std::ostream& out, uint32_t
verbosity = 2)
const throw();
486 std::string getCommandName()
const throw();
497 Expr getTerm()
const throw();
498 void invoke(
SmtEngine* smtEngine)
throw();
499 Expr getResult()
const throw();
500 void printResult(std::ostream& out, uint32_t
verbosity = 2)
const throw();
503 std::string getCommandName()
const throw();
513 Expr getTerm()
const throw();
514 void invoke(
SmtEngine* smtEngine)
throw();
515 Expr getResult()
const throw();
516 void printResult(std::ostream& out, uint32_t
verbosity = 2)
const throw();
519 std::string getCommandName()
const throw();
530 const std::vector<Expr>& getTerms()
const throw();
531 void invoke(
SmtEngine* smtEngine)
throw();
532 Expr getResult()
const throw();
533 void printResult(std::ostream& out, uint32_t
verbosity = 2)
const throw();
536 std::string getCommandName()
const throw();
545 void invoke(
SmtEngine* smtEngine)
throw();
546 SExpr getResult()
const throw();
547 void printResult(std::ostream& out, uint32_t
verbosity = 2)
const throw();
550 std::string getCommandName()
const throw();
560 void invoke(
SmtEngine* smtEngine)
throw();
563 void printResult(std::ostream& out, uint32_t
verbosity = 2)
const throw();
566 std::string getCommandName()
const throw();
575 void invoke(
SmtEngine* smtEngine)
throw();
576 Proof* getResult()
const throw();
577 void printResult(std::ostream& out, uint32_t
verbosity = 2)
const throw();
580 std::string getCommandName()
const throw();
590 void invoke(
SmtEngine* smtEngine)
throw();
592 void printResult(std::ostream& out, uint32_t
verbosity = 2)
const throw();
595 std::string getCommandName()
const throw();
604 void invoke(
SmtEngine* smtEngine)
throw();
605 void printResult(std::ostream& out, uint32_t
verbosity = 2)
const throw();
608 std::string getCommandName()
const throw();
617 void invoke(
SmtEngine* smtEngine)
throw();
618 std::string getResult()
const throw();
619 void printResult(std::ostream& out, uint32_t
verbosity = 2)
const throw();
622 std::string getCommandName()
const throw();
632 void invoke(
SmtEngine* smtEngine)
throw();
635 std::string getCommandName()
const throw();
644 std::string getLogic()
const throw();
645 void invoke(
SmtEngine* smtEngine)
throw();
648 std::string getCommandName()
const throw();
658 std::string getFlag()
const throw();
659 SExpr getSExpr()
const throw();
660 void invoke(
SmtEngine* smtEngine)
throw();
663 std::string getCommandName()
const throw();
673 std::string getFlag()
const throw();
674 void invoke(
SmtEngine* smtEngine)
throw();
675 std::string getResult()
const throw();
676 void printResult(std::ostream& out, uint32_t
verbosity = 2)
const throw();
679 std::string getCommandName()
const throw();
689 std::string getFlag()
const throw();
690 SExpr getSExpr()
const throw();
691 void invoke(
SmtEngine* smtEngine)
throw();
694 std::string getCommandName()
const throw();
704 std::string getFlag()
const throw();
705 void invoke(
SmtEngine* smtEngine)
throw();
706 std::string getResult()
const throw();
707 void printResult(std::ostream& out, uint32_t
verbosity = 2)
const throw();
710 std::string getCommandName()
const throw();
715 std::vector<DatatypeType> d_datatypes;
720 const std::vector<DatatypeType>& getDatatypes()
const throw();
721 void invoke(
SmtEngine* smtEngine)
throw();
724 std::string getCommandName()
const throw();
729 typedef std::vector< std::vector< Expr > >
Triggers;
739 const std::vector<Expr>& guards,
742 const Triggers& d_triggers)
throw();
747 const std::vector<Expr>& getVars()
const throw();
748 const std::vector<Expr>& getGuards()
const throw();
749 Expr getHead()
const throw();
750 Expr getBody()
const throw();
751 const Triggers& getTriggers()
const throw();
752 void invoke(
SmtEngine* smtEngine)
throw();
755 std::string getCommandName()
const throw();
760 typedef std::vector< std::vector< Expr > >
Triggers;
771 const std::vector<Expr>& guards,
772 const std::vector<Expr>& heads,
774 const Triggers& d_triggers,
776 bool d_deduction =
false) throw();
778 const
std::vector<
Expr>& heads,
780 bool d_deduction = false) throw();
782 const std::vector<Expr>& getVars()
const throw();
783 const std::vector<Expr>& getGuards()
const throw();
784 const std::vector<Expr>& getHeads()
const throw();
785 Expr getBody()
const throw();
786 const Triggers& getTriggers()
const throw();
787 bool isDeduction()
const throw();
788 void invoke(
SmtEngine* smtEngine)
throw();
791 std::string getCommandName()
const throw();
799 void invoke(
SmtEngine* smtEngine)
throw();
802 std::string getCommandName()
const throw();
806 std::string d_comment;
810 std::string getComment()
const throw();
811 void invoke(
SmtEngine* smtEngine)
throw();
814 std::string getCommandName()
const throw();
820 std::vector<Command*> d_commandSequence;
822 unsigned int d_index;
827 void addCommand(
Command* cmd)
throw();
828 void clear()
throw();
830 void invoke(
SmtEngine* smtEngine)
throw();
831 void invoke(
SmtEngine* smtEngine, std::ostream& out)
throw();
836 const_iterator begin()
const throw();
837 const_iterator end() const throw();
839 iterator begin() throw();
840 iterator end() throw();
844 std::
string getCommandName() const throw();
std::vector< Expr > VExpr
A class representing a Datatype definition.
Expr exportTo(ExprManager *exprManager, ExprManagerMapCollection &variableMap, uint32_t flags=0) const
Maps this Expr into one for a different ExprManager, using variableMap for the translation and extend...
CommandStatus & clone() const
Scope(std::ostream &out, bool printSuccess)
Set the print-success state on the output stream for the current stack scope.
Class encapsulating CVC4 expressions and methods for constructing new expressions.
std::vector< Expr > d_formals
[[ Add one-line brief description here ]]
struct CVC4::options::printSuccess__option_t printSuccess
std::vector< Expr > d_terms
bool isMuted()
Determine whether this Command will print a success message.
~SetUserAttributeCommand()
std::vector< Expr > VExpr
~DeclarationDefinitionCommand()
Benchmark is satisfiable.
void applyPrintSuccess(std::ostream &out)
~DeclareFunctionCommand()
The command when an attribute is set by a user.
Class encapsulating CVC4 expression types.
Simple representation of S-expressions.
const CommandStatus * d_commandStatus
This field contains a command status if the command has been invoked, or NULL if it has not...
~SetBenchmarkLogicCommand()
std::vector< std::vector< Expr > > Triggers
struct CVC4::options::verbosity__option_t verbosity
Type exportTo(ExprManager *exprManager, ExprManagerMapCollection &vmap) const
Exports this type into a different ExprManager.
static const CommandSuccess * instance()
~SetBenchmarkStatusCommand()
std::vector< Command * >::iterator iterator
bool d_printInModelSetByUser
static bool getPrintSuccess(std::ostream &out)
Encapsulation of the result of a query.
Match the output language to the input language.
bool d_muted
True if this command is "muted"—i.e., don't print "success" on successful execution.
~ExpandDefinitionsCommand()
const CommandStatus * getCommandStatus() const
Get the command status (it's NULL if we haven't run yet).
CommandPrintSuccess printsuccess
IOStream manipulator to print success messages or not.
The status of the benchmark is unknown.
This differs from DefineFunctionCommand only in that it instructs the SmtEngine to "remember" this fu...
Class encapsulating the datatype type.
CommandPrintSuccess(bool printSuccess)
Construct a CommandPrintSuccess with the given setting.
Macros that should be defined everywhere during the building of the libraries and driver binary...
Three-valued SMT result, with optional explanation.
~DatatypeDeclarationCommand()
EmptyCommands are the residue of a command after the parser handles them (and there's nothing left to...
std::string getMessage() const
BenchmarkStatus
The status an SMT benchmark can have.
Benchmark is unsatisfiable.
std::ostream & operator<<(std::ostream &out, ModelFormatMode mode)
struct CVC4::options::out__option_t out
[[ Add one-line brief description here ]]
CommandFailure & clone() const
CommandFailure(std::string message)
std::vector< Type > d_params
CommandStatus & clone() const
std::vector< std::vector< Expr > > Triggers
static void setPrintSuccess(std::ostream &out, bool printSuccess)
Interface for expression types.
std::vector< Command * >::const_iterator const_iterator