diff options
Diffstat (limited to 'src/smt/command.cpp')
-rw-r--r-- | src/smt/command.cpp | 118 |
1 files changed, 59 insertions, 59 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 */ |