summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/command.cpp462
-rw-r--r--src/expr/command.h400
-rw-r--r--src/expr/command.i10
-rw-r--r--src/expr/expr_template.cpp23
-rw-r--r--src/expr/expr_template.h22
-rw-r--r--src/expr/node.cpp6
-rw-r--r--src/expr/node.h8
-rw-r--r--src/expr/type.i1
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback