diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/command.cpp | 462 | ||||
-rw-r--r-- | src/expr/command.h | 400 | ||||
-rw-r--r-- | src/expr/command.i | 10 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 23 | ||||
-rw-r--r-- | src/expr/expr_template.h | 22 | ||||
-rw-r--r-- | src/expr/node.cpp | 6 | ||||
-rw-r--r-- | src/expr/node.h | 8 | ||||
-rw-r--r-- | src/expr/type.i | 1 |
8 files changed, 600 insertions, 332 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 345d7f956..47c6d1eb5 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -21,6 +21,7 @@ #include <utility> #include <iterator> #include <sstream> +#include <exception> #include "expr/command.h" #include "smt/smt_engine.h" @@ -34,7 +35,10 @@ using namespace std; namespace CVC4 { -std::ostream& operator<<(std::ostream& out, const Command& c) { +const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc(); +const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess(); + +std::ostream& operator<<(std::ostream& out, const Command& c) throw() { c.toStream(out, Node::setdepth::getDepth(out), Node::printtypes::getPrintTypes(out), @@ -42,7 +46,7 @@ std::ostream& operator<<(std::ostream& out, const Command& c) { return out; } -ostream& operator<<(ostream& out, const Command* c) { +ostream& operator<<(ostream& out, const Command* c) throw() { if(c == NULL) { out << "null"; } else { @@ -51,180 +55,259 @@ ostream& operator<<(ostream& out, const Command* c) { return out; } +std::ostream& operator<<(std::ostream& out, const CommandStatus& s) throw() { + s.toStream(out, Node::setlanguage::getLanguage(out)); + return out; +} + +ostream& operator<<(ostream& out, const CommandStatus* s) throw() { + if(s == NULL) { + out << "null"; + } else { + out << *s; + } + return out; +} + /* class Command */ -void Command::invoke(SmtEngine* smtEngine, std::ostream& out) { +Command::Command() throw() : d_commandStatus(NULL) { +} + +Command::~Command() throw() { + if(d_commandStatus != NULL && d_commandStatus != CommandSuccess::instance()) { + delete d_commandStatus; + } +} + +bool Command::ok() const throw() { + // either we haven't run the command yet, or it ran successfully + return d_commandStatus == NULL || dynamic_cast<const CommandSuccess*>(d_commandStatus) != NULL; +} + +void Command::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { invoke(smtEngine); printResult(out); } -std::string Command::toString() const { +std::string Command::toString() const throw() { std::stringstream ss; toStream(ss); return ss.str(); } void Command::toStream(std::ostream& out, int toDepth, bool types, - OutputLanguage language) const { + OutputLanguage language) const throw() { Printer::getPrinter(language)->toStream(out, this, toDepth, types); } -void Command::printResult(std::ostream& out) const { +void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const throw() { + Printer::getPrinter(language)->toStream(out, this); +} + +void Command::printResult(std::ostream& out) const throw() { + if(d_commandStatus != NULL) { + out << *d_commandStatus; + } } /* class EmptyCommand */ -EmptyCommand::EmptyCommand(std::string name) : +EmptyCommand::EmptyCommand(std::string name) throw() : d_name(name) { } -std::string EmptyCommand::getName() const { +std::string EmptyCommand::getName() const throw() { return d_name; } -void EmptyCommand::invoke(SmtEngine* smtEngine) { +void EmptyCommand::invoke(SmtEngine* smtEngine) throw() { /* empty commands have no implementation */ + d_commandStatus = CommandSuccess::instance(); } /* class AssertCommand */ -AssertCommand::AssertCommand(const BoolExpr& e) : +AssertCommand::AssertCommand(const BoolExpr& e) throw() : d_expr(e) { } -BoolExpr AssertCommand::getExpr() const { +BoolExpr AssertCommand::getExpr() const throw() { return d_expr; } -void AssertCommand::invoke(SmtEngine* smtEngine) { - smtEngine->assertFormula(d_expr); +void AssertCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->assertFormula(d_expr); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } } /* class PushCommand */ -void PushCommand::invoke(SmtEngine* smtEngine) { - smtEngine->push(); +void PushCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->push(); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } } /* class PopCommand */ -void PopCommand::invoke(SmtEngine* smtEngine) { - smtEngine->pop(); +void PopCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->pop(); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } } /* class CheckSatCommand */ -CheckSatCommand::CheckSatCommand() : +CheckSatCommand::CheckSatCommand() throw() : d_expr() { } -CheckSatCommand::CheckSatCommand(const BoolExpr& expr) : +CheckSatCommand::CheckSatCommand(const BoolExpr& expr) throw() : d_expr(expr) { } -BoolExpr CheckSatCommand::getExpr() const { +BoolExpr CheckSatCommand::getExpr() const throw() { return d_expr; } -void CheckSatCommand::invoke(SmtEngine* smtEngine) { - d_result = smtEngine->checkSat(d_expr); +void CheckSatCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->checkSat(d_expr); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } } -Result CheckSatCommand::getResult() const { +Result CheckSatCommand::getResult() const throw() { return d_result; } -void CheckSatCommand::printResult(std::ostream& out) const { - out << d_result << endl; +void CheckSatCommand::printResult(std::ostream& out) const throw() { + if(! ok()) { + this->Command::printResult(out); + } else { + out << d_result << endl; + } } /* class QueryCommand */ -QueryCommand::QueryCommand(const BoolExpr& e) : +QueryCommand::QueryCommand(const BoolExpr& e) throw() : d_expr(e) { } -BoolExpr QueryCommand::getExpr() const { +BoolExpr QueryCommand::getExpr() const throw() { return d_expr; } -void QueryCommand::invoke(SmtEngine* smtEngine) { - d_result = smtEngine->query(d_expr); +void QueryCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->query(d_expr); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } } -Result QueryCommand::getResult() const { +Result QueryCommand::getResult() const throw() { return d_result; } -void QueryCommand::printResult(std::ostream& out) const { - out << d_result << endl; +void QueryCommand::printResult(std::ostream& out) const throw() { + if(! ok()) { + this->Command::printResult(out); + } else { + out << d_result << endl; + } } /* class QuitCommand */ -QuitCommand::QuitCommand() { +QuitCommand::QuitCommand() throw() { } -void QuitCommand::invoke(SmtEngine* smtEngine) { +void QuitCommand::invoke(SmtEngine* smtEngine) throw() { Dump("benchmark") << *this; + d_commandStatus = CommandSuccess::instance(); } /* class CommentCommand */ -CommentCommand::CommentCommand(std::string comment) : d_comment(comment) { +CommentCommand::CommentCommand(std::string comment) throw() : d_comment(comment) { } -std::string CommentCommand::getComment() const { +std::string CommentCommand::getComment() const throw() { return d_comment; } -void CommentCommand::invoke(SmtEngine* smtEngine) { +void CommentCommand::invoke(SmtEngine* smtEngine) throw() { Dump("benchmark") << *this; + d_commandStatus = CommandSuccess::instance(); } /* class CommandSequence */ -CommandSequence::CommandSequence() : +CommandSequence::CommandSequence() throw() : d_index(0) { } -CommandSequence::~CommandSequence() { +CommandSequence::~CommandSequence() throw() { for(unsigned i = d_index; i < d_commandSequence.size(); ++i) { delete d_commandSequence[i]; } } -void CommandSequence::addCommand(Command* cmd) { +void CommandSequence::addCommand(Command* cmd) throw() { d_commandSequence.push_back(cmd); } -void CommandSequence::invoke(SmtEngine* smtEngine) { +void CommandSequence::invoke(SmtEngine* smtEngine) throw() { for(; d_index < d_commandSequence.size(); ++d_index) { d_commandSequence[d_index]->invoke(smtEngine); + if(! d_commandSequence[d_index]->ok()) { + // abort execution + d_commandStatus = d_commandSequence[d_index]->getCommandStatus(); + return; + } delete d_commandSequence[d_index]; } + + AlwaysAssert(d_commandStatus == NULL); + d_commandStatus = CommandSuccess::instance(); } -void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) { +void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { for(; d_index < d_commandSequence.size(); ++d_index) { d_commandSequence[d_index]->invoke(smtEngine, out); delete d_commandSequence[d_index]; } } -CommandSequence::const_iterator CommandSequence::begin() const { +CommandSequence::const_iterator CommandSequence::begin() const throw() { return d_commandSequence.begin(); } -CommandSequence::const_iterator CommandSequence::end() const { +CommandSequence::const_iterator CommandSequence::end() const throw() { return d_commandSequence.end(); } -CommandSequence::iterator CommandSequence::begin() { +CommandSequence::iterator CommandSequence::begin() throw() { return d_commandSequence.begin(); } -CommandSequence::iterator CommandSequence::end() { +CommandSequence::iterator CommandSequence::end() throw() { return d_commandSequence.end(); } @@ -232,53 +315,53 @@ CommandSequence::iterator CommandSequence::end() { /* class DeclarationDefinitionCommand */ -DeclarationDefinitionCommand::DeclarationDefinitionCommand(const std::string& id) : +DeclarationDefinitionCommand::DeclarationDefinitionCommand(const std::string& id) throw() : d_symbol(id) { } -std::string DeclarationDefinitionCommand::getSymbol() const { +std::string DeclarationDefinitionCommand::getSymbol() const throw() { return d_symbol; } /* class DeclareFunctionCommand */ -DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Type t) : +DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Type t) throw() : DeclarationDefinitionCommand(id), d_type(t) { } -Type DeclareFunctionCommand::getType() const { +Type DeclareFunctionCommand::getType() const throw() { return d_type; } -void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) { +void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() { Dump("declarations") << *this << endl; } /* class DeclareTypeCommand */ -DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) : +DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw() : DeclarationDefinitionCommand(id), d_arity(arity), d_type(t) { } -size_t DeclareTypeCommand::getArity() const { +size_t DeclareTypeCommand::getArity() const throw() { return d_arity; } -Type DeclareTypeCommand::getType() const { +Type DeclareTypeCommand::getType() const throw() { return d_type; } -void DeclareTypeCommand::invoke(SmtEngine* smtEngine) { +void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() { Dump("declarations") << *this << endl; } /* class DefineTypeCommand */ DefineTypeCommand::DefineTypeCommand(const std::string& id, - Type t) : + Type t) throw() : DeclarationDefinitionCommand(id), d_params(), d_type(t) { @@ -286,29 +369,30 @@ DefineTypeCommand::DefineTypeCommand(const std::string& id, DefineTypeCommand::DefineTypeCommand(const std::string& id, const std::vector<Type>& params, - Type t) : + Type t) throw() : DeclarationDefinitionCommand(id), d_params(params), d_type(t) { } -const std::vector<Type>& DefineTypeCommand::getParameters() const { +const std::vector<Type>& DefineTypeCommand::getParameters() const throw() { return d_params; } -Type DefineTypeCommand::getType() const { +Type DefineTypeCommand::getType() const throw() { return d_type; } -void DefineTypeCommand::invoke(SmtEngine* smtEngine) { +void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() { Dump("declarations") << *this << endl; + d_commandStatus = CommandSuccess::instance(); } /* class DefineFunctionCommand */ DefineFunctionCommand::DefineFunctionCommand(const std::string& id, Expr func, - Expr formula) : + Expr formula) throw() : DeclarationDefinitionCommand(id), d_func(func), d_formals(), @@ -318,30 +402,31 @@ DefineFunctionCommand::DefineFunctionCommand(const std::string& id, DefineFunctionCommand::DefineFunctionCommand(const std::string& id, Expr func, const std::vector<Expr>& formals, - Expr formula) : + Expr formula) throw() : DeclarationDefinitionCommand(id), d_func(func), d_formals(formals), d_formula(formula) { } -Expr DefineFunctionCommand::getFunction() const { +Expr DefineFunctionCommand::getFunction() const throw() { return d_func; } -const std::vector<Expr>& DefineFunctionCommand::getFormals() const { +const std::vector<Expr>& DefineFunctionCommand::getFormals() const throw() { return d_formals; } -Expr DefineFunctionCommand::getFormula() const { +Expr DefineFunctionCommand::getFormula() const throw() { return d_formula; } -void DefineFunctionCommand::invoke(SmtEngine* smtEngine) { +void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() { //Dump("declarations") << *this << endl; -- done by SmtEngine if(!d_func.isNull()) { smtEngine->defineFunction(d_func, d_formals, d_formula); } + d_commandStatus = CommandSuccess::instance(); } /* class DefineNamedFunctionCommand */ @@ -349,314 +434,339 @@ void DefineFunctionCommand::invoke(SmtEngine* smtEngine) { DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id, Expr func, const std::vector<Expr>& formals, - Expr formula) : + Expr formula) throw() : DefineFunctionCommand(id, func, formals, formula) { } -void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) { +void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) throw() { this->DefineFunctionCommand::invoke(smtEngine); if(!d_func.isNull() && d_func.getType().isBoolean()) { - smtEngine->addToAssignment(d_func.getExprManager()->mkExpr(kind::APPLY, - d_func)); + smtEngine->addToAssignment(d_func.getExprManager()->mkExpr(kind::APPLY, d_func)); } + d_commandStatus = CommandSuccess::instance(); } /* class Simplify */ -SimplifyCommand::SimplifyCommand(Expr term) : +SimplifyCommand::SimplifyCommand(Expr term) throw() : d_term(term) { } -Expr SimplifyCommand::getTerm() const { +Expr SimplifyCommand::getTerm() const throw() { return d_term; } -void SimplifyCommand::invoke(SmtEngine* smtEngine) { +void SimplifyCommand::invoke(SmtEngine* smtEngine) throw() { d_result = smtEngine->simplify(d_term); + d_commandStatus = CommandSuccess::instance(); } -Expr SimplifyCommand::getResult() const { +Expr SimplifyCommand::getResult() const throw() { return d_result; } -void SimplifyCommand::printResult(std::ostream& out) const { - out << d_result << endl; +void SimplifyCommand::printResult(std::ostream& out) const throw() { + if(! ok()) { + this->Command::printResult(out); + } else { + out << d_result << endl; + } } /* class GetValueCommand */ -GetValueCommand::GetValueCommand(Expr term) : +GetValueCommand::GetValueCommand(Expr term) throw() : d_term(term) { } -Expr GetValueCommand::getTerm() const { +Expr GetValueCommand::getTerm() const throw() { return d_term; } -void GetValueCommand::invoke(SmtEngine* smtEngine) { +void GetValueCommand::invoke(SmtEngine* smtEngine) throw() { d_result = d_term.getExprManager()->mkExpr(kind::TUPLE, d_term, smtEngine->getValue(d_term)); + d_commandStatus = CommandSuccess::instance(); } -Expr GetValueCommand::getResult() const { +Expr GetValueCommand::getResult() const throw() { return d_result; } -void GetValueCommand::printResult(std::ostream& out) const { - out << d_result << endl; +void GetValueCommand::printResult(std::ostream& out) const throw() { + if(! ok()) { + this->Command::printResult(out); + } else { + out << d_result << endl; + } } /* class GetAssignmentCommand */ -GetAssignmentCommand::GetAssignmentCommand() { +GetAssignmentCommand::GetAssignmentCommand() throw() { } -void GetAssignmentCommand::invoke(SmtEngine* smtEngine) { - d_result = smtEngine->getAssignment(); +void GetAssignmentCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->getAssignment(); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } } -SExpr GetAssignmentCommand::getResult() const { +SExpr GetAssignmentCommand::getResult() const throw() { return d_result; } -void GetAssignmentCommand::printResult(std::ostream& out) const { - out << d_result << endl; +void GetAssignmentCommand::printResult(std::ostream& out) const throw() { + if(! ok()) { + this->Command::printResult(out); + } else { + out << d_result << endl; + } } /* class GetProofCommand */ -GetProofCommand::GetProofCommand() { +GetProofCommand::GetProofCommand() throw() { } -void GetProofCommand::invoke(SmtEngine* smtEngine) { - d_result = smtEngine->getProof(); +void GetProofCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->getProof(); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } } -Proof* GetProofCommand::getResult() const { +Proof* GetProofCommand::getResult() const throw() { return d_result; } -void GetProofCommand::printResult(std::ostream& out) const { - d_result->toStream(out); +void GetProofCommand::printResult(std::ostream& out) const throw() { + if(! ok()) { + this->Command::printResult(out); + } else { + d_result->toStream(out); + } } /* class GetAssertionsCommand */ -GetAssertionsCommand::GetAssertionsCommand() { +GetAssertionsCommand::GetAssertionsCommand() throw() { } -void GetAssertionsCommand::invoke(SmtEngine* smtEngine) { - stringstream ss; - const vector<Expr> v = smtEngine->getAssertions(); - copy( v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n") ); - d_result = ss.str(); +void GetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() { + try { + stringstream ss; + const vector<Expr> v = smtEngine->getAssertions(); + copy( v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n") ); + d_result = ss.str(); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } } -std::string GetAssertionsCommand::getResult() const { +std::string GetAssertionsCommand::getResult() const throw() { return d_result; } -void GetAssertionsCommand::printResult(std::ostream& out) const { - out << d_result; +void GetAssertionsCommand::printResult(std::ostream& out) const throw() { + if(! ok()) { + this->Command::printResult(out); + } else { + out << d_result; + } } /* class SetBenchmarkStatusCommand */ -SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) : +SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) throw() : d_status(status) { } -BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const { +BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const throw() { return d_status; } -void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) { - stringstream ss; - ss << d_status; - SExpr status = ss.str(); +void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() { try { + stringstream ss; + ss << d_status; + SExpr status = ss.str(); smtEngine->setInfo(":status", status); - //d_result = "success"; - } catch(ModalException&) { - d_result = "error"; - } catch(BadOptionException&) { - // should not happen - d_result = "error"; + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); } } /* class SetBenchmarkLogicCommand */ -SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) : +SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) throw() : d_logic(logic) { } -std::string SetBenchmarkLogicCommand::getLogic() const { +std::string SetBenchmarkLogicCommand::getLogic() const throw() { return d_logic; } -void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) { +void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) throw() { try { smtEngine->setLogic(d_logic); - //d_result = "success"; - } catch(ModalException&) { - d_result = "error"; + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); } } /* class SetInfoCommand */ -SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) : +SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) throw() : d_flag(flag), d_sexpr(sexpr) { } -std::string SetInfoCommand::getFlag() const { +std::string SetInfoCommand::getFlag() const throw() { return d_flag; } -SExpr SetInfoCommand::getSExpr() const { +SExpr SetInfoCommand::getSExpr() const throw() { return d_sexpr; } -void SetInfoCommand::invoke(SmtEngine* smtEngine) { +void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() { try { smtEngine->setInfo(d_flag, d_sexpr); - //d_result = "success"; - } catch(ModalException&) { - d_result = "error"; + d_commandStatus = CommandSuccess::instance(); } catch(BadOptionException&) { - d_result = "unsupported"; - } -} - -std::string SetInfoCommand::getResult() const { - return d_result; -} - -void SetInfoCommand::printResult(std::ostream& out) const { - if(d_result != "") { - out << d_result << endl; + d_commandStatus = new CommandUnsupported(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); } } /* class GetInfoCommand */ -GetInfoCommand::GetInfoCommand(std::string flag) : +GetInfoCommand::GetInfoCommand(std::string flag) throw() : d_flag(flag) { } -std::string GetInfoCommand::getFlag() const { +std::string GetInfoCommand::getFlag() const throw() { return d_flag; } -void GetInfoCommand::invoke(SmtEngine* smtEngine) { +void GetInfoCommand::invoke(SmtEngine* smtEngine) throw() { try { stringstream ss; ss << smtEngine->getInfo(d_flag); d_result = ss.str(); + d_commandStatus = CommandSuccess::instance(); } catch(BadOptionException&) { - d_result = "unsupported"; + d_commandStatus = new CommandUnsupported(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); } } -std::string GetInfoCommand::getResult() const { +std::string GetInfoCommand::getResult() const throw() { return d_result; } -void GetInfoCommand::printResult(std::ostream& out) const { - if(d_result != "") { +void GetInfoCommand::printResult(std::ostream& out) const throw() { + if(! ok()) { + this->Command::printResult(out); + } else if(d_result != "") { out << d_result << endl; } } /* class SetOptionCommand */ -SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) : +SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) throw() : d_flag(flag), d_sexpr(sexpr) { } -std::string SetOptionCommand::getFlag() const { +std::string SetOptionCommand::getFlag() const throw() { return d_flag; } -SExpr SetOptionCommand::getSExpr() const { +SExpr SetOptionCommand::getSExpr() const throw() { return d_sexpr; } -void SetOptionCommand::invoke(SmtEngine* smtEngine) { +void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() { try { smtEngine->setOption(d_flag, d_sexpr); - //d_result = "success"; - } catch(ModalException&) { - d_result = "error"; + d_commandStatus = CommandSuccess::instance(); } catch(BadOptionException&) { - d_result = "unsupported"; - } -} - -std::string SetOptionCommand::getResult() const { - return d_result; -} - -void SetOptionCommand::printResult(std::ostream& out) const { - if(d_result != "") { - out << d_result << endl; + d_commandStatus = new CommandUnsupported(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); } } /* class GetOptionCommand */ -GetOptionCommand::GetOptionCommand(std::string flag) : +GetOptionCommand::GetOptionCommand(std::string flag) throw() : d_flag(flag) { } -std::string GetOptionCommand::getFlag() const { +std::string GetOptionCommand::getFlag() const throw() { return d_flag; } -void GetOptionCommand::invoke(SmtEngine* smtEngine) { +void GetOptionCommand::invoke(SmtEngine* smtEngine) throw() { try { d_result = smtEngine->getOption(d_flag).getValue(); + d_commandStatus = CommandSuccess::instance(); } catch(BadOptionException&) { - d_result = "unsupported"; + d_commandStatus = new CommandUnsupported(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); } } -std::string GetOptionCommand::getResult() const { +std::string GetOptionCommand::getResult() const throw() { return d_result; } -void GetOptionCommand::printResult(std::ostream& out) const { - if(d_result != "") { +void GetOptionCommand::printResult(std::ostream& out) const throw() { + if(! ok()) { + this->Command::printResult(out); + } else if(d_result != "") { out << d_result << endl; } } /* class DatatypeDeclarationCommand */ -DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) : +DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() : d_datatypes() { d_datatypes.push_back(datatype); } -DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) : +DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw() : d_datatypes(datatypes) { } const std::vector<DatatypeType>& -DatatypeDeclarationCommand::getDatatypes() const { +DatatypeDeclarationCommand::getDatatypes() const throw() { return d_datatypes; } -void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) { +void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() { Dump("declarations") << *this << endl; + d_commandStatus = CommandSuccess::instance(); } /* output stream insertion operator for benchmark statuses */ std::ostream& operator<<(std::ostream& out, - BenchmarkStatus status) { + BenchmarkStatus status) throw() { switch(status) { case SMT_SATISFIABLE: diff --git a/src/expr/command.h b/src/expr/command.h index b686025fe..cf8c1b615 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -41,9 +41,12 @@ namespace CVC4 { class SmtEngine; class Command; +class CommandStatus; -std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC; -std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream&, const Command&) throw() CVC4_PUBLIC; +std::ostream& operator<<(std::ostream&, const Command*) throw() CVC4_PUBLIC; +std::ostream& operator<<(std::ostream&, const CommandStatus&) throw() CVC4_PUBLIC; +std::ostream& operator<<(std::ostream&, const CommandStatus*) throw() CVC4_PUBLIC; /** The status an SMT benchmark can have */ enum BenchmarkStatus { @@ -56,21 +59,156 @@ enum BenchmarkStatus { }; std::ostream& operator<<(std::ostream& out, - BenchmarkStatus status) CVC4_PUBLIC; + BenchmarkStatus status) throw() CVC4_PUBLIC; + +/** + * IOStream manipulator to print success messages or not. + * + * out << Command::printsuccess(false) << CommandSuccess(); + * + * prints nothing, but + * + * out << Command::printsuccess(true) << CommandSuccess(); + * + * prints a success message (in a manner appropriate for the current + * output language). + */ +class CVC4_PUBLIC CommandPrintSuccess { + /** + * The allocated index in ios_base for our depth setting. + */ + static const int s_iosIndex; + + /** + * The default setting, for ostreams that haven't yet had a + * setdepth() applied to them. + */ + static const int s_defaultPrintSuccess = false; + + /** + * When this manipulator is used, the setting is stored here. + */ + bool d_printSuccess; + +public: + /** + * Construct a CommandPrintSuccess with the given setting. + */ + CommandPrintSuccess(bool printSuccess) throw() : d_printSuccess(printSuccess) {} + + inline void applyPrintSuccess(std::ostream& out) throw() { + out.iword(s_iosIndex) = d_printSuccess; + } + + static inline bool getPrintSuccess(std::ostream& out) throw() { + return out.iword(s_iosIndex); + } + + static inline void setPrintSuccess(std::ostream& out, bool printSuccess) throw() { + out.iword(s_iosIndex) = printSuccess; + } + + /** + * Set the print-success state on the output stream for the current + * stack scope. This makes sure the old state is reset on the + * stream after normal OR exceptional exit from the scope, using the + * RAII C++ idiom. + */ + class Scope { + std::ostream& d_out; + bool d_oldPrintSuccess; + + public: + + inline Scope(std::ostream& out, bool printSuccess) throw() : + d_out(out), + d_oldPrintSuccess(CommandPrintSuccess::getPrintSuccess(out)) { + CommandPrintSuccess::setPrintSuccess(out, printSuccess); + } + + inline ~Scope() throw() { + CommandPrintSuccess::setPrintSuccess(d_out, d_oldPrintSuccess); + } + + };/* class CommandPrintSuccess::Scope */ + +};/* class CommandPrintSuccess */ + +/** + * Sets the default print-success setting when pretty-printing an Expr + * to an ostream. Use like this: + * + * // let out be an ostream, e an Expr + * out << Expr::setdepth(n) << e << endl; + * + * The depth stays permanently (until set again) with the stream. + */ +inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() { + cps.applyPrintSuccess(out); + return out; +} + +class CVC4_PUBLIC CommandStatus { +protected: + // shouldn't construct a CommandStatus (use a derived class) + CommandStatus() throw() {} +public: + virtual ~CommandStatus() throw() {} + void toStream(std::ostream& out, + OutputLanguage language = language::output::LANG_AST) const throw(); +};/* class CommandStatus */ + +class CVC4_PUBLIC CommandSuccess : public CommandStatus { + static const CommandSuccess* s_instance; +public: + static const CommandSuccess* instance() throw() { return s_instance; } +};/* class CommandSuccess */ + +class CVC4_PUBLIC CommandUnsupported : public CommandStatus { +};/* class CommandSuccess */ + +class CVC4_PUBLIC CommandFailure : public CommandStatus { + std::string d_message; +public: + CommandFailure(std::string message) throw() : d_message(message) {} + ~CommandFailure() throw() {} + std::string getMessage() const throw() { return d_message; } +};/* class CommandFailure */ class CVC4_PUBLIC Command { +protected: + /** + * This field contains a command status if the command has been + * invoked, or NULL if it has not. This field is either a + * dynamically-allocated pointer, or it's a pointer to the singleton + * CommandSuccess instance. Doing so is somewhat asymmetric, but + * it avoids the need to dynamically allocate memory in the common + * case of a successful command. + */ + const CommandStatus* d_commandStatus; + public: - virtual ~Command() {} + typedef CommandPrintSuccess printsuccess; + + Command() throw(); + virtual ~Command() throw(); - virtual void invoke(SmtEngine* smtEngine) = 0; - virtual void invoke(SmtEngine* smtEngine, std::ostream& out); + virtual void invoke(SmtEngine* smtEngine) throw() = 0; + virtual void invoke(SmtEngine* smtEngine, std::ostream& out) throw(); virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false, - OutputLanguage language = language::output::LANG_AST) const; + OutputLanguage language = language::output::LANG_AST) const throw(); + + std::string toString() const throw(); + + /** Either the command hasn't run yet, or it completed successfully. */ + bool ok() const throw(); - std::string toString() const; + /** 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) const; + virtual void printResult(std::ostream& out) const throw(); };/* class Command */ @@ -82,45 +220,51 @@ class CVC4_PUBLIC EmptyCommand : public Command { protected: std::string d_name; public: - EmptyCommand(std::string name = ""); - std::string getName() const; - void invoke(SmtEngine* smtEngine); + EmptyCommand(std::string name = "") throw(); + ~EmptyCommand() throw() {} + std::string getName() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class EmptyCommand */ class CVC4_PUBLIC AssertCommand : public Command { protected: BoolExpr d_expr; public: - AssertCommand(const BoolExpr& e); - BoolExpr getExpr() const; - void invoke(SmtEngine* smtEngine); + AssertCommand(const BoolExpr& e) throw(); + ~AssertCommand() throw() {} + BoolExpr getExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class AssertCommand */ class CVC4_PUBLIC PushCommand : public Command { public: - void invoke(SmtEngine* smtEngine); + ~PushCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); };/* class PushCommand */ class CVC4_PUBLIC PopCommand : public Command { public: - void invoke(SmtEngine* smtEngine); + ~PopCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); };/* class PopCommand */ class CVC4_PUBLIC DeclarationDefinitionCommand : public Command { protected: std::string d_symbol; public: - DeclarationDefinitionCommand(const std::string& id); - std::string getSymbol() const; + DeclarationDefinitionCommand(const std::string& id) throw(); + ~DeclarationDefinitionCommand() throw() {} + std::string getSymbol() const throw(); };/* class DeclarationDefinitionCommand */ class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand { protected: Type d_type; public: - DeclareFunctionCommand(const std::string& id, Type type); - Type getType() const; - void invoke(SmtEngine* smtEngine); + DeclareFunctionCommand(const std::string& id, Type type) throw(); + ~DeclareFunctionCommand() throw() {} + Type getType() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class DeclareFunctionCommand */ class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand { @@ -128,10 +272,11 @@ protected: size_t d_arity; Type d_type; public: - DeclareTypeCommand(const std::string& id, size_t arity, Type t); - size_t getArity() const; - Type getType() const; - void invoke(SmtEngine* smtEngine); + DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw(); + ~DeclareTypeCommand() throw() {} + size_t getArity() const throw(); + Type getType() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class DeclareTypeCommand */ class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand { @@ -139,11 +284,12 @@ protected: std::vector<Type> d_params; Type d_type; public: - DefineTypeCommand(const std::string& id, Type t); - DefineTypeCommand(const std::string& id, const std::vector<Type>& params, Type t); - const std::vector<Type>& getParameters() const; - Type getType() const; - void invoke(SmtEngine* smtEngine); + DefineTypeCommand(const std::string& id, Type t) throw(); + DefineTypeCommand(const std::string& id, const std::vector<Type>& params, Type t) throw(); + ~DefineTypeCommand() throw() {} + const std::vector<Type>& getParameters() const throw(); + Type getType() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class DefineTypeCommand */ class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand { @@ -152,13 +298,14 @@ protected: std::vector<Expr> d_formals; Expr d_formula; public: - DefineFunctionCommand(const std::string& id, Expr func, Expr formula); + DefineFunctionCommand(const std::string& id, Expr func, Expr formula) throw(); DefineFunctionCommand(const std::string& id, Expr func, - const std::vector<Expr>& formals, Expr formula); - Expr getFunction() const; - const std::vector<Expr>& getFormals() const; - Expr getFormula() const; - void invoke(SmtEngine* smtEngine); + const std::vector<Expr>& formals, Expr formula) throw(); + ~DefineFunctionCommand() throw() {} + Expr getFunction() const throw(); + const std::vector<Expr>& getFormals() const throw(); + Expr getFormula() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class DefineFunctionCommand */ /** @@ -169,8 +316,8 @@ public: class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand { public: DefineNamedFunctionCommand(const std::string& id, Expr func, - const std::vector<Expr>& formals, Expr formula); - void invoke(SmtEngine* smtEngine); + const std::vector<Expr>& formals, Expr formula) throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class DefineNamedFunctionCommand */ class CVC4_PUBLIC CheckSatCommand : public Command { @@ -178,12 +325,13 @@ protected: BoolExpr d_expr; Result d_result; public: - CheckSatCommand(); - CheckSatCommand(const BoolExpr& expr); - BoolExpr getExpr() const; - void invoke(SmtEngine* smtEngine); - Result getResult() const; - void printResult(std::ostream& out) const; + CheckSatCommand() throw(); + CheckSatCommand(const BoolExpr& expr) throw(); + ~CheckSatCommand() throw() {} + BoolExpr getExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Result getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class CheckSatCommand */ class CVC4_PUBLIC QueryCommand : public Command { @@ -191,11 +339,12 @@ protected: BoolExpr d_expr; Result d_result; public: - QueryCommand(const BoolExpr& e); - BoolExpr getExpr() const; - void invoke(SmtEngine* smtEngine); - Result getResult() const; - void printResult(std::ostream& out) const; + QueryCommand(const BoolExpr& e) throw(); + ~QueryCommand() throw() {} + BoolExpr getExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Result getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class QueryCommand */ // this is TRANSFORM in the CVC presentation language @@ -204,11 +353,12 @@ protected: Expr d_term; Expr d_result; public: - SimplifyCommand(Expr term); - Expr getTerm() const; - void invoke(SmtEngine* smtEngine); - Expr getResult() const; - void printResult(std::ostream& out) const; + SimplifyCommand(Expr term) throw(); + ~SimplifyCommand() throw() {} + Expr getTerm() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Expr getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class SimplifyCommand */ class CVC4_PUBLIC GetValueCommand : public Command { @@ -216,75 +366,77 @@ protected: Expr d_term; Expr d_result; public: - GetValueCommand(Expr term); - Expr getTerm() const; - void invoke(SmtEngine* smtEngine); - Expr getResult() const; - void printResult(std::ostream& out) const; + GetValueCommand(Expr term) throw(); + ~GetValueCommand() throw() {} + Expr getTerm() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Expr getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class GetValueCommand */ class CVC4_PUBLIC GetAssignmentCommand : public Command { protected: SExpr d_result; public: - GetAssignmentCommand(); - void invoke(SmtEngine* smtEngine); - SExpr getResult() const; - void printResult(std::ostream& out) const; + GetAssignmentCommand() throw(); + ~GetAssignmentCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + SExpr getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class GetAssignmentCommand */ class CVC4_PUBLIC GetProofCommand : public Command { protected: Proof* d_result; public: - GetProofCommand(); - void invoke(SmtEngine* smtEngine); - Proof* getResult() const; - void printResult(std::ostream& out) const; + GetProofCommand() throw(); + ~GetProofCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + Proof* getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class GetProofCommand */ class CVC4_PUBLIC GetAssertionsCommand : public Command { protected: std::string d_result; public: - GetAssertionsCommand(); - void invoke(SmtEngine* smtEngine); - std::string getResult() const; - void printResult(std::ostream& out) const; + GetAssertionsCommand() throw(); + ~GetAssertionsCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + std::string getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class GetAssertionsCommand */ class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command { protected: - std::string d_result; BenchmarkStatus d_status; public: - SetBenchmarkStatusCommand(BenchmarkStatus status); - BenchmarkStatus getStatus() const; - void invoke(SmtEngine* smtEngine); + SetBenchmarkStatusCommand(BenchmarkStatus status) throw(); + ~SetBenchmarkStatusCommand() throw() {} + BenchmarkStatus getStatus() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class SetBenchmarkStatusCommand */ class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command { protected: - std::string d_result; std::string d_logic; public: - SetBenchmarkLogicCommand(std::string logic); - std::string getLogic() const; - void invoke(SmtEngine* smtEngine); + SetBenchmarkLogicCommand(std::string logic) throw(); + ~SetBenchmarkLogicCommand() throw() {} + std::string getLogic() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class SetBenchmarkLogicCommand */ class CVC4_PUBLIC SetInfoCommand : public Command { protected: std::string d_flag; SExpr d_sexpr; - std::string d_result; public: - SetInfoCommand(std::string flag, const SExpr& sexpr); - std::string getFlag() const; - SExpr getSExpr() const; - void invoke(SmtEngine* smtEngine); - std::string getResult() const; - void printResult(std::ostream& out) const; + SetInfoCommand(std::string flag, const SExpr& sexpr) throw(); + ~SetInfoCommand() throw() {} + std::string getFlag() const throw(); + SExpr getSExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class SetInfoCommand */ class CVC4_PUBLIC GetInfoCommand : public Command { @@ -292,25 +444,24 @@ protected: std::string d_flag; std::string d_result; public: - GetInfoCommand(std::string flag); - std::string getFlag() const; - void invoke(SmtEngine* smtEngine); - std::string getResult() const; - void printResult(std::ostream& out) const; + GetInfoCommand(std::string flag) throw(); + ~GetInfoCommand() throw() {} + std::string getFlag() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + std::string getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class GetInfoCommand */ class CVC4_PUBLIC SetOptionCommand : public Command { protected: std::string d_flag; SExpr d_sexpr; - std::string d_result; public: - SetOptionCommand(std::string flag, const SExpr& sexpr); - std::string getFlag() const; - SExpr getSExpr() const; - void invoke(SmtEngine* smtEngine); - std::string getResult() const; - void printResult(std::ostream& out) const; + SetOptionCommand(std::string flag, const SExpr& sexpr) throw(); + ~SetOptionCommand() throw() {} + std::string getFlag() const throw(); + SExpr getSExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class SetOptionCommand */ class CVC4_PUBLIC GetOptionCommand : public Command { @@ -318,35 +469,39 @@ protected: std::string d_flag; std::string d_result; public: - GetOptionCommand(std::string flag); - std::string getFlag() const; - void invoke(SmtEngine* smtEngine); - std::string getResult() const; - void printResult(std::ostream& out) const; + GetOptionCommand(std::string flag) throw(); + ~GetOptionCommand() throw() {} + std::string getFlag() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + std::string getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class GetOptionCommand */ class CVC4_PUBLIC DatatypeDeclarationCommand : public Command { private: std::vector<DatatypeType> d_datatypes; public: - DatatypeDeclarationCommand(const DatatypeType& datatype); - DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes); - const std::vector<DatatypeType>& getDatatypes() const; - void invoke(SmtEngine* smtEngine); + DatatypeDeclarationCommand(const DatatypeType& datatype) throw(); + ~DatatypeDeclarationCommand() throw() {} + DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw(); + const std::vector<DatatypeType>& getDatatypes() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class DatatypeDeclarationCommand */ class CVC4_PUBLIC QuitCommand : public Command { public: - QuitCommand(); - void invoke(SmtEngine* smtEngine); + QuitCommand() throw(); + ~QuitCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); };/* class QuitCommand */ class CVC4_PUBLIC CommentCommand : public Command { std::string d_comment; public: - CommentCommand(std::string comment); - std::string getComment() const; - void invoke(SmtEngine* smtEngine); + CommentCommand(std::string comment) throw(); + ~CommentCommand() throw() {} + std::string getComment() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class CommentCommand */ class CVC4_PUBLIC CommandSequence : public Command { @@ -356,27 +511,28 @@ private: /** Next command to be executed */ unsigned int d_index; public: - CommandSequence(); - ~CommandSequence(); + CommandSequence() throw(); + ~CommandSequence() throw(); - void addCommand(Command* cmd); + void addCommand(Command* cmd) throw(); - void invoke(SmtEngine* smtEngine); - void invoke(SmtEngine* smtEngine, std::ostream& out); + void invoke(SmtEngine* smtEngine) throw(); + void invoke(SmtEngine* smtEngine, std::ostream& out) throw(); typedef std::vector<Command*>::iterator iterator; typedef std::vector<Command*>::const_iterator const_iterator; - const_iterator begin() const; - const_iterator end() const; + const_iterator begin() const throw(); + const_iterator end() const throw(); - iterator begin(); - iterator end(); + iterator begin() throw(); + iterator end() throw(); };/* class CommandSequence */ class CVC4_PUBLIC DeclarationSequence : public CommandSequence { public: + ~DeclarationSequence() throw() {} };/* class DeclarationSequence */ }/* CVC4 namespace */ diff --git a/src/expr/command.i b/src/expr/command.i index 3a029b785..a4bf5473e 100644 --- a/src/expr/command.i +++ b/src/expr/command.i @@ -2,11 +2,11 @@ #include "expr/command.h" %} -%ignore CVC4::operator<<(std::ostream&, const Command&); -%ignore CVC4::operator<<(std::ostream&, const Command*); -%ignore CVC4::operator<<(std::ostream&, BenchmarkStatus status); +%ignore CVC4::operator<<(std::ostream&, const Command&) throw(); +%ignore CVC4::operator<<(std::ostream&, const Command*) throw(); +%ignore CVC4::operator<<(std::ostream&, BenchmarkStatus status) throw(); -%rename(beginConst) CVC4::CommandSequence::begin() const; -%rename(endConst) CVC4::CommandSequence::end() const; +%rename(beginConst) CVC4::CommandSequence::begin() const throw(); +%rename(endConst) CVC4::CommandSequence::end() const throw(); %include "expr/command.h" diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 619fd5280..29aa1a737 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -56,31 +56,28 @@ std::ostream& operator<<(std::ostream& out, const Expr& e) { return out << e.getNode(); } -TypeCheckingException::TypeCheckingException(const TypeCheckingException& t) -: Exception(t.d_msg), d_expr(new Expr(t.getExpression())) - {} - +TypeCheckingException::TypeCheckingException(const TypeCheckingException& t) throw() : + Exception(t.d_msg), d_expr(new Expr(t.getExpression())) { +} -TypeCheckingException::TypeCheckingException(const Expr& expr, std::string message) -: Exception(message), d_expr(new Expr(expr)) -{ +TypeCheckingException::TypeCheckingException(const Expr& expr, std::string message) throw() : + Exception(message), d_expr(new Expr(expr)) { } TypeCheckingException::TypeCheckingException(ExprManager* em, - const TypeCheckingExceptionPrivate* exc) -: Exception(exc->getMessage()), d_expr(new Expr(em, new Node(exc->getNode()))) -{ + const TypeCheckingExceptionPrivate* exc) throw() : + Exception(exc->getMessage()), d_expr(new Expr(em, new Node(exc->getNode()))) { } -TypeCheckingException::~TypeCheckingException() throw () { +TypeCheckingException::~TypeCheckingException() throw() { delete d_expr; } -void TypeCheckingException::toStream(std::ostream& os) const { +void TypeCheckingException::toStream(std::ostream& os) const throw() { os << "Error type-checking " << d_expr << ": " << d_msg << endl << *d_expr; } -Expr TypeCheckingException::getExpression() const { +Expr TypeCheckingException::getExpression() const throw() { return *d_expr; } diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 616a7c8ff..b54ec20d4 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -81,32 +81,32 @@ private: protected: - TypeCheckingException() : Exception() {} - TypeCheckingException(const Expr& expr, std::string message); + TypeCheckingException() throw() : Exception() {} + TypeCheckingException(const Expr& expr, std::string message) throw(); TypeCheckingException(ExprManager* em, - const TypeCheckingExceptionPrivate* exc); + const TypeCheckingExceptionPrivate* exc) throw(); public: /** Copy constructor */ - TypeCheckingException(const TypeCheckingException& t); + TypeCheckingException(const TypeCheckingException& t) throw(); /** Destructor */ - ~TypeCheckingException() throw (); + ~TypeCheckingException() throw(); /** * Get the Expr that caused the type-checking to fail. * * @return the expr */ - Expr getExpression() const; + Expr getExpression() const throw(); /** * Returns the message corresponding to the type-checking failure. * We prefer toStream() to toString() because that keeps the expr-depth * and expr-language settings present in the stream. */ - void toStream(std::ostream& out) const; + void toStream(std::ostream& out) const throw(); friend class ExprManager; };/* class TypeCheckingException */ @@ -457,9 +457,13 @@ public: * * // let a, b, c, and d be variables of sort U * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d))) - * out << e; + * out << printtypes(true) << e; * * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but + * + * out << printtypes(false) << [same expr as above] + * + * gives "(OR a b (AND c (NOT d)))" */ typedef expr::ExprPrintTypes printtypes; @@ -824,7 +828,7 @@ public: ${getConst_instantiations} -#line 828 "${template}" +#line 832 "${template}" namespace expr { diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 586d0cb13..695e572ab 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -26,7 +26,7 @@ using namespace std; namespace CVC4 { TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node, - std::string message) : + std::string message) throw() : Exception(message), d_node(new Node(node)) { } @@ -35,11 +35,11 @@ TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() throw () { delete d_node; } -void TypeCheckingExceptionPrivate::toStream(std::ostream& os) const { +void TypeCheckingExceptionPrivate::toStream(std::ostream& os) const throw() { os << "Error type-checking " << d_node << ": " << d_msg << std::endl << *d_node; } -Node TypeCheckingExceptionPrivate::getNode() const { +NodeTemplate<true> TypeCheckingExceptionPrivate::getNode() const throw() { return *d_node; } diff --git a/src/expr/node.h b/src/expr/node.h index 2751c96a8..57b02b05b 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -65,7 +65,7 @@ private: protected: - TypeCheckingExceptionPrivate() : Exception() {} + TypeCheckingExceptionPrivate() throw() : Exception() {} public: @@ -74,7 +74,7 @@ public: * @param node the problematic node * @param message the message explaining the failure */ - TypeCheckingExceptionPrivate(NodeTemplate<false> node, std::string message); + TypeCheckingExceptionPrivate(NodeTemplate<false> node, std::string message) throw(); /** Destructor */ ~TypeCheckingExceptionPrivate() throw (); @@ -83,14 +83,14 @@ public: * Get the Node that caused the type-checking to fail. * @return the node */ - NodeTemplate<true> getNode() const; + NodeTemplate<true> getNode() const throw(); /** * Returns the message corresponding to the type-checking failure. * We prefer toStream() to toString() because that keeps the expr-depth * and expr-language settings present in the stream. */ - void toStream(std::ostream& out) const; + void toStream(std::ostream& out) const throw(); };/* class TypeCheckingExceptionPrivate */ diff --git a/src/expr/type.i b/src/expr/type.i index 314903342..acde96955 100644 --- a/src/expr/type.i +++ b/src/expr/type.i @@ -18,6 +18,7 @@ %rename(toIntegerType) CVC4::Type::operator IntegerType() const; %rename(toRealType) CVC4::Type::operator RealType() const; %rename(toPseudobooleanType) CVC4::Type::operator PseudobooleanType() const; +%rename(toStringType) CVC4::Type::operator StringType() const; %rename(toBitVectorType) CVC4::Type::operator BitVectorType() const; %rename(toFunctionType) CVC4::Type::operator FunctionType() const; %rename(toTupleType) CVC4::Type::operator TupleType() const; |