summaryrefslogtreecommitdiff
path: root/src/smt/command.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/command.h')
-rw-r--r--src/smt/command.h122
1 files changed, 61 insertions, 61 deletions
diff --git a/src/smt/command.h b/src/smt/command.h
index db4efd819..c4db23e04 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -215,8 +215,8 @@ public:
virtual ~Command() throw();
- virtual void invoke(SmtEngine* smtEngine) throw() = 0;
- virtual void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
+ virtual void invoke(SmtEngine* smtEngine) = 0;
+ virtual void invoke(SmtEngine* smtEngine, std::ostream& out);
virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const throw();
@@ -255,7 +255,7 @@ public:
/** Get the command status (it's NULL if we haven't run yet). */
const CommandStatus* getCommandStatus() const throw() { return d_commandStatus; }
- virtual void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ virtual void printResult(std::ostream& out, uint32_t verbosity = 2) const;
/**
* Maps this Command into one for a different ExprManager, using
@@ -299,7 +299,7 @@ public:
EmptyCommand(std::string name = "") throw();
~EmptyCommand() throw() {}
std::string getName() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -312,8 +312,8 @@ public:
EchoCommand(std::string output = "") throw();
~EchoCommand() throw() {}
std::string getOutput() const throw();
- void invoke(SmtEngine* smtEngine) throw();
- void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
+ void invoke(SmtEngine* smtEngine);
+ void invoke(SmtEngine* smtEngine, std::ostream& out);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -327,7 +327,7 @@ public:
AssertCommand(const Expr& e, bool inUnsatCore = true) throw();
~AssertCommand() throw() {}
Expr getExpr() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -336,7 +336,7 @@ public:
class CVC4_PUBLIC PushCommand : public Command {
public:
~PushCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -345,7 +345,7 @@ public:
class CVC4_PUBLIC PopCommand : public Command {
public:
~PopCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -357,7 +357,7 @@ protected:
public:
DeclarationDefinitionCommand(const std::string& id) throw();
~DeclarationDefinitionCommand() throw() {}
- virtual void invoke(SmtEngine* smtEngine) throw() = 0;
+ virtual void invoke(SmtEngine* smtEngine) = 0;
std::string getSymbol() const throw();
};/* class DeclarationDefinitionCommand */
@@ -375,7 +375,7 @@ public:
bool getPrintInModel() const throw();
bool getPrintInModelSetByUser() const throw();
void setPrintInModel( bool p );
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -390,7 +390,7 @@ public:
~DeclareTypeCommand() throw() {}
size_t getArity() const throw();
Type getType() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -406,7 +406,7 @@ public:
~DefineTypeCommand() throw() {}
const std::vector<Type>& getParameters() const throw();
Type getType() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -425,7 +425,7 @@ public:
Expr getFunction() const throw();
const std::vector<Expr>& getFormals() const throw();
Expr getFormula() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -440,7 +440,7 @@ class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand {
public:
DefineNamedFunctionCommand(const std::string& id, Expr func,
const std::vector<Expr>& formals, Expr formula) throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
};/* class DefineNamedFunctionCommand */
@@ -460,7 +460,7 @@ public:
SetUserAttributeCommand( const std::string& attr, Expr expr, std::vector<Expr>& values ) throw();
SetUserAttributeCommand( const std::string& attr, Expr expr, const std::string& value ) throw();
~SetUserAttributeCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -476,9 +476,9 @@ public:
CheckSatCommand(const Expr& expr, bool inUnsatCore = true) throw();
~CheckSatCommand() throw() {}
Expr getExpr() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Result getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -493,9 +493,9 @@ public:
QueryCommand(const Expr& e, bool inUnsatCore = true) throw();
~QueryCommand() throw() {}
Expr getExpr() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Result getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -511,9 +511,9 @@ public:
CheckSynthCommand(const Expr& expr, bool inUnsatCore = true) throw();
~CheckSynthCommand() throw() {}
Expr getExpr() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Result getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -528,9 +528,9 @@ public:
SimplifyCommand(Expr term) throw();
~SimplifyCommand() throw() {}
Expr getTerm() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Expr getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -544,9 +544,9 @@ public:
ExpandDefinitionsCommand(Expr term) throw();
~ExpandDefinitionsCommand() throw() {}
Expr getTerm() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Expr getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -561,9 +561,9 @@ public:
GetValueCommand(const std::vector<Expr>& terms) throw();
~GetValueCommand() throw() {}
const std::vector<Expr>& getTerms() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Expr getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -575,9 +575,9 @@ protected:
public:
GetAssignmentCommand() throw();
~GetAssignmentCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
SExpr getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -590,10 +590,10 @@ protected:
public:
GetModelCommand() throw();
~GetModelCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
// Model is private to the library -- for now
//Model* getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -606,9 +606,9 @@ protected:
public:
GetProofCommand() throw();
~GetProofCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Proof* getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -621,9 +621,9 @@ protected:
public:
GetInstantiationsCommand() throw();
~GetInstantiationsCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
//Instantiations* getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -635,8 +635,8 @@ protected:
public:
GetSynthSolutionCommand() throw();
~GetSynthSolutionCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void invoke(SmtEngine* smtEngine);
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -653,9 +653,9 @@ public:
~GetQuantifierEliminationCommand() throw() {}
Expr getExpr() const throw();
bool getDoFull() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Expr getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -669,8 +669,8 @@ public:
GetUnsatCoreCommand() throw();
GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw();
~GetUnsatCoreCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void invoke(SmtEngine* smtEngine);
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
const UnsatCore& getUnsatCore() const throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
@@ -683,9 +683,9 @@ protected:
public:
GetAssertionsCommand() throw();
~GetAssertionsCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
std::string getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -698,7 +698,7 @@ public:
SetBenchmarkStatusCommand(BenchmarkStatus status) throw();
~SetBenchmarkStatusCommand() throw() {}
BenchmarkStatus getStatus() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -711,7 +711,7 @@ public:
SetBenchmarkLogicCommand(std::string logic) throw();
~SetBenchmarkLogicCommand() throw() {}
std::string getLogic() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -726,7 +726,7 @@ public:
~SetInfoCommand() throw() {}
std::string getFlag() const throw();
SExpr getSExpr() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -740,9 +740,9 @@ public:
GetInfoCommand(std::string flag) throw();
~GetInfoCommand() throw() {}
std::string getFlag() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
std::string getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -757,7 +757,7 @@ public:
~SetOptionCommand() throw() {}
std::string getFlag() const throw();
SExpr getSExpr() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -771,9 +771,9 @@ public:
GetOptionCommand(std::string flag) throw();
~GetOptionCommand() throw() {}
std::string getFlag() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
std::string getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -787,7 +787,7 @@ public:
~DatatypeDeclarationCommand() throw() {}
DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw();
const std::vector<DatatypeType>& getDatatypes() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -818,7 +818,7 @@ public:
Expr getHead() const throw();
Expr getBody() const throw();
const Triggers& getTriggers() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -854,7 +854,7 @@ public:
Expr getBody() const throw();
const Triggers& getTriggers() const throw();
bool isDeduction() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -864,7 +864,7 @@ class CVC4_PUBLIC ResetCommand : public Command {
public:
ResetCommand() throw() {}
~ResetCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -874,7 +874,7 @@ class CVC4_PUBLIC ResetAssertionsCommand : public Command {
public:
ResetAssertionsCommand() throw() {}
~ResetAssertionsCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -884,7 +884,7 @@ class CVC4_PUBLIC QuitCommand : public Command {
public:
QuitCommand() throw() {}
~QuitCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -896,7 +896,7 @@ public:
CommentCommand(std::string comment) throw();
~CommentCommand() throw() {}
std::string getComment() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -915,8 +915,8 @@ public:
void addCommand(Command* cmd) throw();
void clear() throw();
- void invoke(SmtEngine* smtEngine) throw();
- void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
+ void invoke(SmtEngine* smtEngine);
+ void invoke(SmtEngine* smtEngine, std::ostream& out);
typedef std::vector<Command*>::iterator iterator;
typedef std::vector<Command*>::const_iterator const_iterator;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback