From faec717e89cfd657daaa370a061f4a8e282b0eff Mon Sep 17 00:00:00 2001 From: Andres Notzli Date: Wed, 29 Mar 2017 23:27:56 +0200 Subject: [PATCH] [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 --- src/smt/command.cpp | 118 +++++++++++++++++++-------------------- src/smt/command.h | 122 ++++++++++++++++++++--------------------- src/smt/smt_engine.cpp | 17 +++--- src/smt/smt_engine.h | 17 +++--- 4 files changed, 136 insertions(+), 138 deletions(-) diff --git a/src/smt/command.cpp b/src/smt/command.cpp index bd514e2a8..9c6a143c5 100644 --- 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(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& GetValueCommand::getTerms() const throw() { return d_terms; } -void GetValueCommand::invoke(SmtEngine* smtEngine) throw() { +void GetValueCommand::invoke(SmtEngine* smtEngine) { try { vector 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& 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 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 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 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& 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& 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& 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& 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& terms) throw(); ~GetValueCommand() throw() {} const std::vector& 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& 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& datatypes) throw(); const std::vector& 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::iterator iterator; typedef std::vector::const_iterator const_iterator; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8e641aca1..20cd5e83e 100644 --- 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 SmtEngine::getAssertions() throw(ModalException) { +vector 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 f1ce2e0e9..d17dd204b 100644 --- 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 getAssertions() throw(ModalException); + std::vector 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 -- 2.30.2