diff options
author | Clark Barrett <barrett@cs.stanford.edu> | 2017-03-30 12:49:38 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-03-30 12:49:38 -0700 |
commit | d5d727e65a27056030e88b58becc236f50e448df (patch) | |
tree | 067f9df357725c07ea7d04a5895801152b5f1a27 | |
parent | 100037d531ff1fd30ed3dd5bed91076c383ad55c (diff) | |
parent | faec717e89cfd657daaa370a061f4a8e282b0eff (diff) |
Merge pull request #139 from 4tXJ7f/remove_throw
[Coverity] Remove throw qualifiers in src/smt
-rw-r--r-- | src/smt/command.cpp | 118 | ||||
-rw-r--r-- | src/smt/command.h | 122 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 17 | ||||
-rw-r--r-- | 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<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 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; 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<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 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<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 |