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;
148 cps.applyPrintSuccess(
out);
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();
243 const
CommandStatus* getCommandStatus() const throw() {
return d_commandStatus; }
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();
305 Command* clone() const;
306 std::
string getCommandName() const throw();
315 Expr getExpr()
const throw();
316 void invoke(
SmtEngine* smtEngine) throw();
318 Command* clone() const;
319 std::
string getCommandName() const throw();
325 void invoke(
SmtEngine* smtEngine)
throw();
327 Command* clone()
const;
328 std::string getCommandName()
const throw();
334 void invoke(
SmtEngine* smtEngine)
throw();
336 Command* clone()
const;
337 std::string getCommandName()
const throw();
346 virtual void invoke(
SmtEngine* smtEngine)
throw() = 0;
347 std::string getSymbol()
const throw();
357 Expr getFunction()
const throw();
358 Type getType() const throw();
359 void invoke(
SmtEngine* smtEngine) throw();
361 Command* clone() const;
362 std::
string getCommandName() const throw();
372 size_t getArity()
const throw();
373 Type getType() const throw();
374 void invoke(
SmtEngine* smtEngine) throw();
376 Command* clone() const;
377 std::
string getCommandName() const throw();
388 const std::vector<Type>& getParameters()
const throw();
389 Type getType() const throw();
390 void invoke(
SmtEngine* smtEngine) throw();
392 Command* clone() const;
393 std::
string getCommandName() const throw();
404 const std::vector<Expr>& formals,
Expr formula)
throw();
406 Expr getFunction()
const throw();
407 const std::vector<
Expr>& getFormals() const throw();
408 Expr getFormula() const throw();
409 void invoke(
SmtEngine* smtEngine) throw();
411 Command* clone() const;
412 std::
string getCommandName() const throw();
423 const std::vector<Expr>& formals,
Expr formula)
throw();
424 void invoke(
SmtEngine* smtEngine)
throw();
426 Command* clone()
const;
444 void invoke(
SmtEngine* smtEngine)
throw();
446 Command* clone()
const;
447 std::string getCommandName()
const throw();
459 Expr getExpr()
const throw();
460 void invoke(
SmtEngine* smtEngine) throw();
461 Result getResult() const throw();
462 void printResult(std::ostream&
out, uint32_t
verbosity = 2) const throw();
464 Command* clone() const;
465 std::
string getCommandName() const throw();
475 Expr getExpr()
const throw();
476 void invoke(
SmtEngine* smtEngine) throw();
477 Result getResult() const throw();
478 void printResult(std::ostream& out, uint32_t
verbosity = 2) const throw();
480 Command* clone() const;
481 std::
string getCommandName() const throw();
492 Expr getTerm()
const throw();
493 void invoke(
SmtEngine* smtEngine) throw();
494 Expr getResult() const throw();
495 void printResult(std::ostream& out, uint32_t
verbosity = 2) const throw();
497 Command* clone() const;
498 std::
string getCommandName() const throw();
508 Expr getTerm()
const throw();
509 void invoke(
SmtEngine* smtEngine) throw();
510 Expr getResult() const throw();
511 void printResult(std::ostream& out, uint32_t
verbosity = 2) const throw();
513 Command* clone() const;
514 std::
string getCommandName() const throw();
525 const std::vector<Expr>& getTerms()
const throw();
526 void invoke(
SmtEngine* smtEngine) throw();
527 Expr getResult() const throw();
528 void printResult(std::ostream& out, uint32_t
verbosity = 2) const throw();
530 Command* clone() const;
531 std::
string getCommandName() const throw();
540 void invoke(
SmtEngine* smtEngine)
throw();
541 SExpr getResult()
const throw();
542 void printResult(std::ostream& out, uint32_t
verbosity = 2) const throw();
544 Command* clone() const;
545 std::
string getCommandName() const throw();
555 void invoke(
SmtEngine* smtEngine)
throw();
558 void printResult(std::ostream& out, uint32_t
verbosity = 2)
const throw();
560 Command* clone() const;
561 std::
string getCommandName() const throw();
570 void invoke(
SmtEngine* smtEngine)
throw();
571 Proof* getResult()
const throw();
572 void printResult(std::ostream& out, uint32_t
verbosity = 2) const throw();
574 Command* clone() const;
575 std::
string getCommandName() const throw();
584 void invoke(
SmtEngine* smtEngine)
throw();
585 void printResult(std::ostream& out, uint32_t
verbosity = 2)
const throw();
587 Command* clone() const;
588 std::
string getCommandName() const throw();
597 void invoke(
SmtEngine* smtEngine)
throw();
598 std::string getResult()
const throw();
599 void printResult(std::ostream& out, uint32_t
verbosity = 2) const throw();
601 Command* clone() const;
602 std::
string getCommandName() const throw();
612 void invoke(
SmtEngine* smtEngine) throw();
614 Command* clone() const;
615 std::
string getCommandName() const throw();
624 std::string getLogic()
const throw();
625 void invoke(
SmtEngine* smtEngine) throw();
627 Command* clone() const;
628 std::
string getCommandName() const throw();
638 std::string getFlag()
const throw();
639 SExpr getSExpr() const throw();
640 void invoke(
SmtEngine* smtEngine) throw();
642 Command* clone() const;
643 std::
string getCommandName() const throw();
653 std::string getFlag()
const throw();
654 void invoke(
SmtEngine* smtEngine) throw();
655 std::
string getResult() const throw();
656 void printResult(std::ostream& out, uint32_t
verbosity = 2) const throw();
658 Command* clone() const;
659 std::
string getCommandName() const throw();
669 std::string getFlag()
const throw();
670 SExpr getSExpr() const throw();
671 void invoke(
SmtEngine* smtEngine) throw();
673 Command* clone() const;
674 std::
string getCommandName() const throw();
684 std::string getFlag()
const throw();
685 void invoke(
SmtEngine* smtEngine) throw();
686 std::
string getResult() const throw();
687 void printResult(std::ostream& out, uint32_t
verbosity = 2) const throw();
689 Command* clone() const;
690 std::
string getCommandName() const throw();
695 std::vector<DatatypeType> d_datatypes;
700 const std::vector<DatatypeType>& getDatatypes()
const throw();
701 void invoke(
SmtEngine* smtEngine) throw();
703 Command* clone() const;
704 std::
string getCommandName() const throw();
709 typedef std::vector< std::vector< Expr > >
Triggers;
719 const std::vector<Expr>& guards,
722 const Triggers& d_triggers)
throw();
727 const std::vector<Expr>& getVars()
const throw();
728 const std::vector<
Expr>& getGuards() const throw();
729 Expr getHead() const throw();
730 Expr getBody() const throw();
731 const Triggers& getTriggers() const throw();
732 void invoke(
SmtEngine* smtEngine) throw();
734 Command* clone() const;
735 std::
string getCommandName() const throw();
740 typedef std::vector< std::vector< Expr > >
Triggers;
751 const std::vector<Expr>& guards,
752 const std::vector<Expr>& heads,
754 const Triggers& d_triggers,
756 bool d_deduction =
false) throw();
758 const std::vector<
Expr>& heads,
760 bool d_deduction = false) throw();
762 const std::vector<Expr>& getVars()
const throw();
763 const std::vector<
Expr>& getGuards() const throw();
764 const std::vector<
Expr>& getHeads() const throw();
765 Expr getBody() const throw();
766 const Triggers& getTriggers() const throw();
767 bool isDeduction() const throw();
768 void invoke(
SmtEngine* smtEngine) throw();
770 Command* clone() const;
771 std::
string getCommandName() const throw();
779 void invoke(
SmtEngine* smtEngine)
throw();
781 Command* clone()
const;
782 std::string getCommandName()
const throw();
786 std::string d_comment;
790 std::string getComment()
const throw();
791 void invoke(
SmtEngine* smtEngine) throw();
793 Command* clone() const;
794 std::
string getCommandName() const throw();
800 std::vector<Command*> d_commandSequence;
802 unsigned int d_index;
807 void addCommand(Command* cmd)
throw();
808 void clear()
throw();
810 void invoke(
SmtEngine* smtEngine)
throw();
811 void invoke(
SmtEngine* smtEngine, std::ostream& out)
throw();
816 const_iterator begin()
const throw();
817 const_iterator end() const throw();
819 iterator begin() throw();
820 iterator end() throw();
823 Command* clone() const;
824 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
static bool getPrintSuccess(std::ostream &out)
Encapsulation of the result of a query.
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
bool d_muted
True if this command is "muted"—i.e., don't print "success" on successful execution.
~ExpandDefinitionsCommand()
CommandPrintSuccess printsuccess
IOStream manipulator to print success messages or not.
std::ostream & operator<<(std::ostream &out, TypeConstant typeConstant)
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.
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