[Coverity] Remove throw qualifiers in src/smt

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

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index bd514e2a89e7864d981c3a3ea725d483782b33a7..9c6a143c571d0307c7c6cb861c42580b61e2af1f 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -105,7 +105,7 @@ bool Command::interrupted() const throw() {
   return d_commandStatus != NULL && dynamic_cast<const CommandInterrupted*>(d_commandStatus) != NULL;
 }
 
-void Command::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
+void Command::invoke(SmtEngine* smtEngine, std::ostream& out) {
   invoke(smtEngine);
   if(!(isMuted() && ok())) {
     printResult(out, smtEngine->getOption("command-verbosity:" + getCommandName()).getIntegerValue().toUnsignedInt());
@@ -127,7 +127,7 @@ void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const t
   Printer::getPrinter(language)->toStream(out, this);
 }
 
-void Command::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void Command::printResult(std::ostream& out, uint32_t verbosity) const {
   if(d_commandStatus != NULL) {
     if((!ok() && verbosity >= 1) || verbosity >= 2) {
       out << *d_commandStatus;
@@ -145,7 +145,7 @@ std::string EmptyCommand::getName() const throw() {
   return d_name;
 }
 
-void EmptyCommand::invoke(SmtEngine* smtEngine) throw() {
+void EmptyCommand::invoke(SmtEngine* smtEngine) {
   /* empty commands have no implementation */
   d_commandStatus = CommandSuccess::instance();
 }
@@ -172,12 +172,12 @@ std::string EchoCommand::getOutput() const throw() {
   return d_output;
 }
 
-void EchoCommand::invoke(SmtEngine* smtEngine) throw() {
+void EchoCommand::invoke(SmtEngine* smtEngine) {
   /* we don't have an output stream here, nothing to do */
   d_commandStatus = CommandSuccess::instance();
 }
 
-void EchoCommand::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
+void EchoCommand::invoke(SmtEngine* smtEngine, std::ostream& out) {
   out << d_output << std::endl;
   d_commandStatus = CommandSuccess::instance();
   printResult(out, smtEngine->getOption("command-verbosity:" + getCommandName()).getIntegerValue().toUnsignedInt());
@@ -205,7 +205,7 @@ Expr AssertCommand::getExpr() const throw() {
   return d_expr;
 }
 
-void AssertCommand::invoke(SmtEngine* smtEngine) throw() {
+void AssertCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->assertFormula(d_expr, d_inUnsatCore);
     d_commandStatus = CommandSuccess::instance();
@@ -230,7 +230,7 @@ std::string AssertCommand::getCommandName() const throw() {
 
 /* class PushCommand */
 
-void PushCommand::invoke(SmtEngine* smtEngine) throw() {
+void PushCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->push();
     d_commandStatus = CommandSuccess::instance();
@@ -255,7 +255,7 @@ std::string PushCommand::getCommandName() const throw() {
 
 /* class PopCommand */
 
-void PopCommand::invoke(SmtEngine* smtEngine) throw() {
+void PopCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->pop();
     d_commandStatus = CommandSuccess::instance();
@@ -292,7 +292,7 @@ Expr CheckSatCommand::getExpr() const throw() {
   return d_expr;
 }
 
-void CheckSatCommand::invoke(SmtEngine* smtEngine) throw() {
+void CheckSatCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->checkSat(d_expr);
     d_commandStatus = CommandSuccess::instance();
@@ -305,7 +305,7 @@ Result CheckSatCommand::getResult() const throw() {
   return d_result;
 }
 
-void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -339,7 +339,7 @@ Expr QueryCommand::getExpr() const throw() {
   return d_expr;
 }
 
-void QueryCommand::invoke(SmtEngine* smtEngine) throw() {
+void QueryCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->query(d_expr);
     d_commandStatus = CommandSuccess::instance();
@@ -352,7 +352,7 @@ Result QueryCommand::getResult() const throw() {
   return d_result;
 }
 
-void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -391,7 +391,7 @@ Expr CheckSynthCommand::getExpr() const throw() {
   return d_expr;
 }
 
-void CheckSynthCommand::invoke(SmtEngine* smtEngine) throw() {
+void CheckSynthCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->checkSynth(d_expr);
     d_commandStatus = CommandSuccess::instance();
@@ -404,7 +404,7 @@ Result CheckSynthCommand::getResult() const throw() {
   return d_result;
 }
 
-void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -431,7 +431,7 @@ std::string CheckSynthCommand::getCommandName() const throw() {
 
 /* class ResetCommand */
 
-void ResetCommand::invoke(SmtEngine* smtEngine) throw() {
+void ResetCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->reset();
     d_commandStatus = CommandSuccess::instance();
@@ -454,7 +454,7 @@ std::string ResetCommand::getCommandName() const throw() {
 
 /* class ResetAssertionsCommand */
 
-void ResetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() {
+void ResetAssertionsCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->resetAssertions();
     d_commandStatus = CommandSuccess::instance();
@@ -477,7 +477,7 @@ std::string ResetAssertionsCommand::getCommandName() const throw() {
 
 /* class QuitCommand */
 
-void QuitCommand::invoke(SmtEngine* smtEngine) throw() {
+void QuitCommand::invoke(SmtEngine* smtEngine) {
   Dump("benchmark") << *this;
   d_commandStatus = CommandSuccess::instance();
 }
@@ -503,7 +503,7 @@ std::string CommentCommand::getComment() const throw() {
   return d_comment;
 }
 
-void CommentCommand::invoke(SmtEngine* smtEngine) throw() {
+void CommentCommand::invoke(SmtEngine* smtEngine) {
   Dump("benchmark") << *this;
   d_commandStatus = CommandSuccess::instance();
 }
@@ -540,7 +540,7 @@ void CommandSequence::clear() throw() {
   d_commandSequence.clear();
 }
 
-void CommandSequence::invoke(SmtEngine* smtEngine) throw() {
+void CommandSequence::invoke(SmtEngine* smtEngine) {
   for(; d_index < d_commandSequence.size(); ++d_index) {
     d_commandSequence[d_index]->invoke(smtEngine);
     if(! d_commandSequence[d_index]->ok()) {
@@ -555,7 +555,7 @@ void CommandSequence::invoke(SmtEngine* smtEngine) throw() {
   d_commandStatus = CommandSuccess::instance();
 }
 
-void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
+void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) {
   for(; d_index < d_commandSequence.size(); ++d_index) {
     d_commandSequence[d_index]->invoke(smtEngine, out);
     if(! d_commandSequence[d_index]->ok()) {
@@ -654,7 +654,7 @@ void DeclareFunctionCommand::setPrintInModel( bool p ) {
   d_printInModelSetByUser = true;
 }
 
-void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
+void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) {
   d_commandStatus = CommandSuccess::instance();
 }
 
@@ -694,7 +694,7 @@ Type DeclareTypeCommand::getType() const throw() {
   return d_type;
 }
 
-void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() {
+void DeclareTypeCommand::invoke(SmtEngine* smtEngine) {
   d_commandStatus = CommandSuccess::instance();
 }
 
@@ -737,7 +737,7 @@ Type DefineTypeCommand::getType() const throw() {
   return d_type;
 }
 
-void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() {
+void DefineTypeCommand::invoke(SmtEngine* smtEngine) {
   d_commandStatus = CommandSuccess::instance();
 }
 
@@ -790,7 +790,7 @@ Expr DefineFunctionCommand::getFormula() const throw() {
   return d_formula;
 }
 
-void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
+void DefineFunctionCommand::invoke(SmtEngine* smtEngine) {
   try {
     if(!d_func.isNull()) {
       smtEngine->defineFunction(d_func, d_formals, d_formula);
@@ -827,7 +827,7 @@ DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id,
   DefineFunctionCommand(id, func, formals, formula) {
 }
 
-void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
+void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) {
   this->DefineFunctionCommand::invoke(smtEngine);
   if(!d_func.isNull() && d_func.getType().isBoolean()) {
     smtEngine->addToAssignment(d_func.getExprManager()->mkExpr(kind::APPLY, d_func));
@@ -865,7 +865,7 @@ SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr
   d_attr( attr ), d_expr( expr ), d_str_value( value ){
 }
 
-void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) throw(){
+void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) {
   try {
     if(!d_expr.isNull()) {
       smtEngine->setUserAttribute( d_attr, d_expr, d_expr_values, d_str_value );
@@ -903,7 +903,7 @@ Expr SimplifyCommand::getTerm() const throw() {
   return d_term;
 }
 
-void SimplifyCommand::invoke(SmtEngine* smtEngine) throw() {
+void SimplifyCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->simplify(d_term);
     d_commandStatus = CommandSuccess::instance();
@@ -918,7 +918,7 @@ Expr SimplifyCommand::getResult() const throw() {
   return d_result;
 }
 
-void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -952,7 +952,7 @@ Expr ExpandDefinitionsCommand::getTerm() const throw() {
   return d_term;
 }
 
-void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine) throw() {
+void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine) {
   d_result = smtEngine->expandDefinitions(d_term);
   d_commandStatus = CommandSuccess::instance();
 }
@@ -961,7 +961,7 @@ Expr ExpandDefinitionsCommand::getResult() const throw() {
   return d_result;
 }
 
-void ExpandDefinitionsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void ExpandDefinitionsCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -1002,7 +1002,7 @@ const std::vector<Expr>& GetValueCommand::getTerms() const throw() {
   return d_terms;
 }
 
-void GetValueCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetValueCommand::invoke(SmtEngine* smtEngine) {
   try {
     vector<Expr> result;
     ExprManager* em = smtEngine->getExprManager();
@@ -1034,7 +1034,7 @@ Expr GetValueCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -1068,7 +1068,7 @@ std::string GetValueCommand::getCommandName() const throw() {
 GetAssignmentCommand::GetAssignmentCommand() throw() {
 }
 
-void GetAssignmentCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetAssignmentCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->getAssignment();
     d_commandStatus = CommandSuccess::instance();
@@ -1083,7 +1083,7 @@ SExpr GetAssignmentCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetAssignmentCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetAssignmentCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -1112,7 +1112,7 @@ std::string GetAssignmentCommand::getCommandName() const throw() {
 GetModelCommand::GetModelCommand() throw() {
 }
 
-void GetModelCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetModelCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->getModel();
     d_smtEngine = smtEngine;
@@ -1130,7 +1130,7 @@ Model* GetModelCommand::getResult() const throw() {
 }
 */
 
-void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -1161,7 +1161,7 @@ std::string GetModelCommand::getCommandName() const throw() {
 GetProofCommand::GetProofCommand() throw() {
 }
 
-void GetProofCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetProofCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_smtEngine = smtEngine;
     d_result = smtEngine->getProof();
@@ -1177,7 +1177,7 @@ Proof* GetProofCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -1209,7 +1209,7 @@ std::string GetProofCommand::getCommandName() const throw() {
 GetInstantiationsCommand::GetInstantiationsCommand() throw() {
 }
 
-void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_smtEngine = smtEngine;
     d_commandStatus = CommandSuccess::instance();
@@ -1222,7 +1222,7 @@ void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) throw() {
 //  return d_result;
 //}
 
-void GetInstantiationsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetInstantiationsCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -1253,7 +1253,7 @@ std::string GetInstantiationsCommand::getCommandName() const throw() {
 GetSynthSolutionCommand::GetSynthSolutionCommand() throw() {
 }
 
-void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_smtEngine = smtEngine;
     d_commandStatus = CommandSuccess::instance();
@@ -1262,7 +1262,7 @@ void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) throw() {
   }
 }
 
-void GetSynthSolutionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetSynthSolutionCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -1303,7 +1303,7 @@ bool GetQuantifierEliminationCommand::getDoFull() const throw() {
   return d_doFull;
 }
 
-void GetQuantifierEliminationCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetQuantifierEliminationCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->doQuantifierElimination(d_expr, d_doFull);
     d_commandStatus = CommandSuccess::instance();
@@ -1316,7 +1316,7 @@ Expr GetQuantifierEliminationCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetQuantifierEliminationCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetQuantifierEliminationCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -1348,7 +1348,7 @@ GetUnsatCoreCommand::GetUnsatCoreCommand() throw() {
 GetUnsatCoreCommand::GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw() : d_names(names) {
 }
 
-void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->getUnsatCore();
     d_commandStatus = CommandSuccess::instance();
@@ -1357,7 +1357,7 @@ void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() {
   }
 }
 
-void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -1391,7 +1391,7 @@ std::string GetUnsatCoreCommand::getCommandName() const throw() {
 GetAssertionsCommand::GetAssertionsCommand() throw() {
 }
 
-void GetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetAssertionsCommand::invoke(SmtEngine* smtEngine) {
   try {
     stringstream ss;
     const vector<Expr> v = smtEngine->getAssertions();
@@ -1409,7 +1409,7 @@ std::string GetAssertionsCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetAssertionsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetAssertionsCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
@@ -1443,7 +1443,7 @@ BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const throw() {
   return d_status;
 }
 
-void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() {
+void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) {
   try {
     stringstream ss;
     ss << d_status;
@@ -1477,7 +1477,7 @@ std::string SetBenchmarkLogicCommand::getLogic() const throw() {
   return d_logic;
 }
 
-void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) throw() {
+void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->setLogic(d_logic);
     d_commandStatus = CommandSuccess::instance();
@@ -1513,7 +1513,7 @@ SExpr SetInfoCommand::getSExpr() const throw() {
   return d_sexpr;
 }
 
-void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
+void SetInfoCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->setInfo(d_flag, d_sexpr);
     d_commandStatus = CommandSuccess::instance();
@@ -1547,7 +1547,7 @@ std::string GetInfoCommand::getFlag() const throw() {
   return d_flag;
 }
 
-void GetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetInfoCommand::invoke(SmtEngine* smtEngine) {
   try {
     vector<SExpr> v;
     v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
@@ -1570,7 +1570,7 @@ std::string GetInfoCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else if(d_result != "") {
@@ -1609,7 +1609,7 @@ SExpr SetOptionCommand::getSExpr() const throw() {
   return d_sexpr;
 }
 
-void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
+void SetOptionCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->setOption(d_flag, d_sexpr);
     d_commandStatus = CommandSuccess::instance();
@@ -1642,7 +1642,7 @@ std::string GetOptionCommand::getFlag() const throw() {
   return d_flag;
 }
 
-void GetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetOptionCommand::invoke(SmtEngine* smtEngine) {
   try {
     SExpr res = smtEngine->getOption(d_flag);
     d_result = res.toString();
@@ -1658,7 +1658,7 @@ std::string GetOptionCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else if(d_result != "") {
@@ -1698,7 +1698,7 @@ DatatypeDeclarationCommand::getDatatypes() const throw() {
   return d_datatypes;
 }
 
-void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() {
+void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) {
   d_commandStatus = CommandSuccess::instance();
 }
 
@@ -1749,7 +1749,7 @@ const RewriteRuleCommand::Triggers& RewriteRuleCommand::getTriggers() const thro
   return d_triggers;
 }
 
-void RewriteRuleCommand::invoke(SmtEngine* smtEngine) throw() {
+void RewriteRuleCommand::invoke(SmtEngine* smtEngine) {
   try {
     ExprManager* em = smtEngine->getExprManager();
     /** build vars list */
@@ -1861,7 +1861,7 @@ bool PropagateRuleCommand::isDeduction() const throw() {
   return d_deduction;
 }
 
-void PropagateRuleCommand::invoke(SmtEngine* smtEngine) throw() {
+void PropagateRuleCommand::invoke(SmtEngine* smtEngine) {
   try {
     ExprManager* em = smtEngine->getExprManager();
     /** build vars list */

diff --git a/src/smt/command.h b/src/smt/command.h
index db4efd8195bf28a4e8a071e4fdf56a7d7bac8728..c4db23e043558faa86a4aa2c02d02965463ad216 100644 (file)
--- 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;

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8e641aca1131155bad2b545e293100b4b8824a5a..20cd5e83e0f742caca413bce4fd6d113e75548e7 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2104,8 +2104,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
   throw UnrecognizedOptionException();
 }
 
-CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
-  throw(OptionException, ModalException) {
+CVC4::SExpr SmtEngine::getInfo(const std::string& key) const {
 
   SmtScope smts(this);
 
@@ -4649,7 +4648,7 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin
   return resultNode.toExpr();
 }
 
-bool SmtEngine::addToAssignment(const Expr& ex) throw() {
+bool SmtEngine::addToAssignment(const Expr& ex) {
   SmtScope smts(this);
   finalOptionsAreSet();
   doPendingPops();
@@ -4682,7 +4681,7 @@ bool SmtEngine::addToAssignment(const Expr& ex) throw() {
   return true;
 }
 
-CVC4::SExpr SmtEngine::getAssignment() throw(ModalException, UnsafeInterruptException) {
+CVC4::SExpr SmtEngine::getAssignment() {
   Trace("smt") << "SMT getAssignment()" << endl;
   SmtScope smts(this);
   finalOptionsAreSet();
@@ -4780,7 +4779,7 @@ void SmtEngine::addToModelCommandAndDump(const Command& c, uint32_t flags, bool
   }
 }
 
-Model* SmtEngine::getModel() throw(ModalException, UnsafeInterruptException) {
+Model* SmtEngine::getModel() {
   Trace("smt") << "SMT getModel()" << endl;
   SmtScope smts(this);
 
@@ -5042,7 +5041,7 @@ void SmtEngine::checkModel(bool hardFailure) {
   Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl;
 }
 
-UnsatCore SmtEngine::getUnsatCore() throw(ModalException, UnsafeInterruptException) {
+UnsatCore SmtEngine::getUnsatCore() {
   Trace("smt") << "SMT getUnsatCore()" << endl;
   SmtScope smts(this);
   finalOptionsAreSet();
@@ -5066,7 +5065,7 @@ UnsatCore SmtEngine::getUnsatCore() throw(ModalException, UnsafeInterruptExcepti
 #endif /* IS_PROOFS_BUILD */
 }
 
-Proof* SmtEngine::getProof() throw(ModalException, UnsafeInterruptException) {
+Proof* SmtEngine::getProof() {
   Trace("smt") << "SMT getProof()" << endl;
   SmtScope smts(this);
   finalOptionsAreSet();
@@ -5202,7 +5201,7 @@ void SmtEngine::getInstantiationTermVectors( Expr q, std::vector< std::vector< E
   }
 }
 
-vector<Expr> SmtEngine::getAssertions() throw(ModalException) {
+vector<Expr> SmtEngine::getAssertions() {
   SmtScope smts(this);
   finalOptionsAreSet();
   doPendingPops();
@@ -5250,7 +5249,7 @@ void SmtEngine::push() throw(ModalException, LogicException, UnsafeInterruptExce
                        << d_userContext->getLevel() << endl;
 }
 
-void SmtEngine::pop() throw(ModalException, UnsafeInterruptException) {
+void SmtEngine::pop() {
   SmtScope smts(this);
   finalOptionsAreSet();
   Trace("smt") << "SMT pop()" << endl;

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index f1ce2e0e980bc64807991de99e87973d60baf503..d17dd204bfc6128727b34c36779a8e954b0db4cf 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -394,7 +394,7 @@ class CVC4_PUBLIC SmtEngine {
    * or INVALID query).  Only permitted if CVC4 was built with model
    * support and produce-models is on.
    */
-  Model* getModel() throw(ModalException, UnsafeInterruptException);
+  Model* getModel();
 
   // disallow copy/assignment
   SmtEngine(const SmtEngine&) CVC4_UNDEFINED;
@@ -443,8 +443,7 @@ public:
   /**
    * Query information about the SMT environment.
    */
-  CVC4::SExpr getInfo(const std::string& key) const
-    throw(OptionException, ModalException);
+  CVC4::SExpr getInfo(const std::string& key) const;
 
   /**
    * Set an aspect of the current SMT execution environment.
@@ -533,21 +532,21 @@ public:
    * this function returns true if the expression was added and false
    * if this request was ignored.
    */
-  bool addToAssignment(const Expr& e) throw();
+  bool addToAssignment(const Expr& e);
 
   /**
    * Get the assignment (only if immediately preceded by a SAT or
    * INVALID query).  Only permitted if the SmtEngine is set to
    * operate interactively and produce-assignments is on.
    */
-  CVC4::SExpr getAssignment() throw(ModalException, UnsafeInterruptException);
+  CVC4::SExpr getAssignment();
 
   /**
    * Get the last proof (only if immediately preceded by an UNSAT
    * or VALID query).  Only permitted if CVC4 was built with proof
    * support and produce-proofs is on.
    */
-  Proof* getProof() throw(ModalException, UnsafeInterruptException);
+  Proof* getProof();
 
   /**
    * Print all instantiations made by the quantifiers module.
@@ -580,13 +579,13 @@ public:
    * UNSAT or VALID query).  Only permitted if CVC4 was built with
    * unsat-core support and produce-unsat-cores is on.
    */
-  UnsatCore getUnsatCore() throw(ModalException, UnsafeInterruptException);
+  UnsatCore getUnsatCore();
 
   /**
    * Get the current set of assertions.  Only permitted if the
    * SmtEngine is set to operate interactively.
    */
-  std::vector<Expr> getAssertions() throw(ModalException);
+  std::vector<Expr> getAssertions();
 
   /**
    * Push a user-level context.
@@ -596,7 +595,7 @@ public:
   /**
    * Pop a user-level context.  Throws an exception if nothing to pop.
    */
-  void pop() throw(ModalException, UnsafeInterruptException);
+  void pop();
 
   /**
    * Completely reset the state of the solver, as though destroyed and