[Coverity] Remove throw qualifiers in src/smtremove_throw

Addresses coverity issues:

1172167
1172174
1172176
1172183
1172185
1172186
1172188
1172189
1172191
1172192
1172193
1172194
1172197
1172197
1172198
1172434
1172437
1172438
1172443
1172445
1172446
1172447
1172448
1362695
1362700
1362717
1362736
1362768
1362786
1362811
1379599
1421404
1421405
1421406
1421407
1421408
1421409
1421410
1421411
1421412
1421413

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;