summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/command.cpp118
-rw-r--r--src/smt/command.h122
-rw-r--r--src/smt/smt_engine.cpp17
-rw-r--r--src/smt/smt_engine.h17
4 files changed, 136 insertions, 138 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index bd514e2a8..9c6a143c5 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -105,7 +105,7 @@ bool Command::interrupted() const throw() {
return d_commandStatus != NULL && dynamic_cast<const CommandInterrupted*>(d_commandStatus) != NULL;
}
-void Command::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
+void Command::invoke(SmtEngine* smtEngine, std::ostream& out) {
invoke(smtEngine);
if(!(isMuted() && ok())) {
printResult(out, smtEngine->getOption("command-verbosity:" + getCommandName()).getIntegerValue().toUnsignedInt());
@@ -127,7 +127,7 @@ void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const t
Printer::getPrinter(language)->toStream(out, this);
}
-void Command::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void Command::printResult(std::ostream& out, uint32_t verbosity) const {
if(d_commandStatus != NULL) {
if((!ok() && verbosity >= 1) || verbosity >= 2) {
out << *d_commandStatus;
@@ -145,7 +145,7 @@ std::string EmptyCommand::getName() const throw() {
return d_name;
}
-void EmptyCommand::invoke(SmtEngine* smtEngine) throw() {
+void EmptyCommand::invoke(SmtEngine* smtEngine) {
/* empty commands have no implementation */
d_commandStatus = CommandSuccess::instance();
}
@@ -172,12 +172,12 @@ std::string EchoCommand::getOutput() const throw() {
return d_output;
}
-void EchoCommand::invoke(SmtEngine* smtEngine) throw() {
+void EchoCommand::invoke(SmtEngine* smtEngine) {
/* we don't have an output stream here, nothing to do */
d_commandStatus = CommandSuccess::instance();
}
-void EchoCommand::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
+void EchoCommand::invoke(SmtEngine* smtEngine, std::ostream& out) {
out << d_output << std::endl;
d_commandStatus = CommandSuccess::instance();
printResult(out, smtEngine->getOption("command-verbosity:" + getCommandName()).getIntegerValue().toUnsignedInt());
@@ -205,7 +205,7 @@ Expr AssertCommand::getExpr() const throw() {
return d_expr;
}
-void AssertCommand::invoke(SmtEngine* smtEngine) throw() {
+void AssertCommand::invoke(SmtEngine* smtEngine) {
try {
smtEngine->assertFormula(d_expr, d_inUnsatCore);
d_commandStatus = CommandSuccess::instance();
@@ -230,7 +230,7 @@ std::string AssertCommand::getCommandName() const throw() {
/* class PushCommand */
-void PushCommand::invoke(SmtEngine* smtEngine) throw() {
+void PushCommand::invoke(SmtEngine* smtEngine) {
try {
smtEngine->push();
d_commandStatus = CommandSuccess::instance();
@@ -255,7 +255,7 @@ std::string PushCommand::getCommandName() const throw() {
/* class PopCommand */
-void PopCommand::invoke(SmtEngine* smtEngine) throw() {
+void PopCommand::invoke(SmtEngine* smtEngine) {
try {
smtEngine->pop();
d_commandStatus = CommandSuccess::instance();
@@ -292,7 +292,7 @@ Expr CheckSatCommand::getExpr() const throw() {
return d_expr;
}
-void CheckSatCommand::invoke(SmtEngine* smtEngine) throw() {
+void CheckSatCommand::invoke(SmtEngine* smtEngine) {
try {
d_result = smtEngine->checkSat(d_expr);
d_commandStatus = CommandSuccess::instance();
@@ -305,7 +305,7 @@ Result CheckSatCommand::getResult() const throw() {
return d_result;
}
-void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const {
if(! ok()) {
this->Command::printResult(out, verbosity);
} else {
@@ -339,7 +339,7 @@ Expr QueryCommand::getExpr() const throw() {
return d_expr;
}
-void QueryCommand::invoke(SmtEngine* smtEngine) throw() {
+void QueryCommand::invoke(SmtEngine* smtEngine) {
try {
d_result = smtEngine->query(d_expr);
d_commandStatus = CommandSuccess::instance();
@@ -352,7 +352,7 @@ Result QueryCommand::getResult() const throw() {
return d_result;
}
-void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const {
if(! ok()) {
this->Command::printResult(out, verbosity);
} else {
@@ -391,7 +391,7 @@ Expr CheckSynthCommand::getExpr() const throw() {
return d_expr;
}
-void CheckSynthCommand::invoke(SmtEngine* smtEngine) throw() {
+void CheckSynthCommand::invoke(SmtEngine* smtEngine) {
try {
d_result = smtEngine->checkSynth(d_expr);
d_commandStatus = CommandSuccess::instance();
@@ -404,7 +404,7 @@ Result CheckSynthCommand::getResult() const throw() {
return d_result;
}
-void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const {
if(! ok()) {
this->Command::printResult(out, verbosity);
} else {
@@ -431,7 +431,7 @@ std::string CheckSynthCommand::getCommandName() const throw() {
/* class ResetCommand */
-void ResetCommand::invoke(SmtEngine* smtEngine) throw() {
+void ResetCommand::invoke(SmtEngine* smtEngine) {
try {
smtEngine->reset();
d_commandStatus = CommandSuccess::instance();
@@ -454,7 +454,7 @@ std::string ResetCommand::getCommandName() const throw() {
/* class ResetAssertionsCommand */
-void ResetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() {
+void ResetAssertionsCommand::invoke(SmtEngine* smtEngine) {
try {
smtEngine->resetAssertions();
d_commandStatus = CommandSuccess::instance();
@@ -477,7 +477,7 @@ std::string ResetAssertionsCommand::getCommandName() const throw() {
/* class QuitCommand */
-void QuitCommand::invoke(SmtEngine* smtEngine) throw() {
+void QuitCommand::invoke(SmtEngine* smtEngine) {
Dump("benchmark") << *this;
d_commandStatus = CommandSuccess::instance();
}
@@ -503,7 +503,7 @@ std::string CommentCommand::getComment() const throw() {
return d_comment;
}
-void CommentCommand::invoke(SmtEngine* smtEngine) throw() {
+void CommentCommand::invoke(SmtEngine* smtEngine) {
Dump("benchmark") << *this;
d_commandStatus = CommandSuccess::instance();
}
@@ -540,7 +540,7 @@ void CommandSequence::clear() throw() {
d_commandSequence.clear();
}
-void CommandSequence::invoke(SmtEngine* smtEngine) throw() {
+void CommandSequence::invoke(SmtEngine* smtEngine) {
for(; d_index < d_commandSequence.size(); ++d_index) {
d_commandSequence[d_index]->invoke(smtEngine);
if(! d_commandSequence[d_index]->ok()) {
@@ -555,7 +555,7 @@ void CommandSequence::invoke(SmtEngine* smtEngine) throw() {
d_commandStatus = CommandSuccess::instance();
}
-void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
+void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) {
for(; d_index < d_commandSequence.size(); ++d_index) {
d_commandSequence[d_index]->invoke(smtEngine, out);
if(! d_commandSequence[d_index]->ok()) {
@@ -654,7 +654,7 @@ void DeclareFunctionCommand::setPrintInModel( bool p ) {
d_printInModelSetByUser = true;
}
-void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
+void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) {
d_commandStatus = CommandSuccess::instance();
}
@@ -694,7 +694,7 @@ Type DeclareTypeCommand::getType() const throw() {
return d_type;
}
-void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() {
+void DeclareTypeCommand::invoke(SmtEngine* smtEngine) {
d_commandStatus = CommandSuccess::instance();
}
@@ -737,7 +737,7 @@ Type DefineTypeCommand::getType() const throw() {
return d_type;
}
-void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() {
+void DefineTypeCommand::invoke(SmtEngine* smtEngine) {
d_commandStatus = CommandSuccess::instance();
}
@@ -790,7 +790,7 @@ Expr DefineFunctionCommand::getFormula() const throw() {
return d_formula;
}
-void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
+void DefineFunctionCommand::invoke(SmtEngine* smtEngine) {
try {
if(!d_func.isNull()) {
smtEngine->defineFunction(d_func, d_formals, d_formula);
@@ -827,7 +827,7 @@ DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id,
DefineFunctionCommand(id, func, formals, formula) {
}
-void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
+void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) {
this->DefineFunctionCommand::invoke(smtEngine);
if(!d_func.isNull() && d_func.getType().isBoolean()) {
smtEngine->addToAssignment(d_func.getExprManager()->mkExpr(kind::APPLY, d_func));
@@ -865,7 +865,7 @@ SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr
d_attr( attr ), d_expr( expr ), d_str_value( value ){
}
-void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) throw(){
+void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) {
try {
if(!d_expr.isNull()) {
smtEngine->setUserAttribute( d_attr, d_expr, d_expr_values, d_str_value );
@@ -903,7 +903,7 @@ Expr SimplifyCommand::getTerm() const throw() {
return d_term;
}
-void SimplifyCommand::invoke(SmtEngine* smtEngine) throw() {
+void SimplifyCommand::invoke(SmtEngine* smtEngine) {
try {
d_result = smtEngine->simplify(d_term);
d_commandStatus = CommandSuccess::instance();
@@ -918,7 +918,7 @@ Expr SimplifyCommand::getResult() const throw() {
return d_result;
}
-void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const {
if(! ok()) {
this->Command::printResult(out, verbosity);
} else {
@@ -952,7 +952,7 @@ Expr ExpandDefinitionsCommand::getTerm() const throw() {
return d_term;
}
-void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine) throw() {
+void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine) {
d_result = smtEngine->expandDefinitions(d_term);
d_commandStatus = CommandSuccess::instance();
}
@@ -961,7 +961,7 @@ Expr ExpandDefinitionsCommand::getResult() const throw() {
return d_result;
}
-void ExpandDefinitionsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void ExpandDefinitionsCommand::printResult(std::ostream& out, uint32_t verbosity) const {
if(! ok()) {
this->Command::printResult(out, verbosity);
} else {
@@ -1002,7 +1002,7 @@ const std::vector<Expr>& GetValueCommand::getTerms() const throw() {
return d_terms;
}
-void GetValueCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetValueCommand::invoke(SmtEngine* smtEngine) {
try {
vector<Expr> result;
ExprManager* em = smtEngine->getExprManager();
@@ -1034,7 +1034,7 @@ Expr GetValueCommand::getResult() const throw() {
return d_result;
}
-void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const {
if(! ok()) {
this->Command::printResult(out, verbosity);
} else {
@@ -1068,7 +1068,7 @@ std::string GetValueCommand::getCommandName() const throw() {
GetAssignmentCommand::GetAssignmentCommand() throw() {
}
-void GetAssignmentCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetAssignmentCommand::invoke(SmtEngine* smtEngine) {
try {
d_result = smtEngine->getAssignment();
d_commandStatus = CommandSuccess::instance();
@@ -1083,7 +1083,7 @@ SExpr GetAssignmentCommand::getResult() const throw() {
return d_result;
}
-void GetAssignmentCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetAssignmentCommand::printResult(std::ostream& out, uint32_t verbosity) const {
if(! ok()) {
this->Command::printResult(out, verbosity);
} else {
@@ -1112,7 +1112,7 @@ std::string GetAssignmentCommand::getCommandName() const throw() {
GetModelCommand::GetModelCommand() throw() {
}
-void GetModelCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetModelCommand::invoke(SmtEngine* smtEngine) {
try {
d_result = smtEngine->getModel();
d_smtEngine = smtEngine;
@@ -1130,7 +1130,7 @@ Model* GetModelCommand::getResult() const throw() {
}
*/
-void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const {
if(! ok()) {
this->Command::printResult(out, verbosity);
} else {
@@ -1161,7 +1161,7 @@ std::string GetModelCommand::getCommandName() const throw() {
GetProofCommand::GetProofCommand() throw() {
}
-void GetProofCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetProofCommand::invoke(SmtEngine* smtEngine) {
try {
d_smtEngine = smtEngine;
d_result = smtEngine->getProof();
@@ -1177,7 +1177,7 @@ Proof* GetProofCommand::getResult() const throw() {
return d_result;
}
-void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const {
if(! ok()) {
this->Command::printResult(out, verbosity);
} else {
@@ -1209,7 +1209,7 @@ std::string GetProofCommand::getCommandName() const throw() {
GetInstantiationsCommand::GetInstantiationsCommand() throw() {
}
-void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) {
try {
d_smtEngine = smtEngine;
d_commandStatus = CommandSuccess::instance();
@@ -1222,7 +1222,7 @@ void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) throw() {
// return d_result;
//}
-void GetInstantiationsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetInstantiationsCommand::printResult(std::ostream& out, uint32_t verbosity) const {
if(! ok()) {
this->Command::printResult(out, verbosity);
} else {
@@ -1253,7 +1253,7 @@ std::string GetInstantiationsCommand::getCommandName() const throw() {
GetSynthSolutionCommand::GetSynthSolutionCommand() throw() {
}
-void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) {
try {
d_smtEngine = smtEngine;
d_commandStatus = CommandSuccess::instance();
@@ -1262,7 +1262,7 @@ void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) throw() {
}
}
-void GetSynthSolutionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetSynthSolutionCommand::printResult(std::ostream& out, uint32_t verbosity) const {
if(! ok()) {
this->Command::printResult(out, verbosity);
} else {
@@ -1303,7 +1303,7 @@ bool GetQuantifierEliminationCommand::getDoFull() const throw() {
return d_doFull;
}
-void GetQuantifierEliminationCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetQuantifierEliminationCommand::invoke(SmtEngine* smtEngine) {
try {
d_result = smtEngine->doQuantifierElimination(d_expr, d_doFull);
d_commandStatus = CommandSuccess::instance();
@@ -1316,7 +1316,7 @@ Expr GetQuantifierEliminationCommand::getResult() const throw() {
return d_result;
}
-void GetQuantifierEliminationCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetQuantifierEliminationCommand::printResult(std::ostream& out, uint32_t verbosity) const {
if(! ok()) {
this->Command::printResult(out, verbosity);
} else {
@@ -1348,7 +1348,7 @@ GetUnsatCoreCommand::GetUnsatCoreCommand() throw() {
GetUnsatCoreCommand::GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw() : d_names(names) {
}
-void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) {
try {
d_result = smtEngine->getUnsatCore();
d_commandStatus = CommandSuccess::instance();
@@ -1357,7 +1357,7 @@ void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() {
}
}
-void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) const {
if(! ok()) {
this->Command::printResult(out, verbosity);
} else {
@@ -1391,7 +1391,7 @@ std::string GetUnsatCoreCommand::getCommandName() const throw() {
GetAssertionsCommand::GetAssertionsCommand() throw() {
}
-void GetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetAssertionsCommand::invoke(SmtEngine* smtEngine) {
try {
stringstream ss;
const vector<Expr> v = smtEngine->getAssertions();
@@ -1409,7 +1409,7 @@ std::string GetAssertionsCommand::getResult() const throw() {
return d_result;
}
-void GetAssertionsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetAssertionsCommand::printResult(std::ostream& out, uint32_t verbosity) const {
if(! ok()) {
this->Command::printResult(out, verbosity);
} else {
@@ -1443,7 +1443,7 @@ BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const throw() {
return d_status;
}
-void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() {
+void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) {
try {
stringstream ss;
ss << d_status;
@@ -1477,7 +1477,7 @@ std::string SetBenchmarkLogicCommand::getLogic() const throw() {
return d_logic;
}
-void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) throw() {
+void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) {
try {
smtEngine->setLogic(d_logic);
d_commandStatus = CommandSuccess::instance();
@@ -1513,7 +1513,7 @@ SExpr SetInfoCommand::getSExpr() const throw() {
return d_sexpr;
}
-void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
+void SetInfoCommand::invoke(SmtEngine* smtEngine) {
try {
smtEngine->setInfo(d_flag, d_sexpr);
d_commandStatus = CommandSuccess::instance();
@@ -1547,7 +1547,7 @@ std::string GetInfoCommand::getFlag() const throw() {
return d_flag;
}
-void GetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetInfoCommand::invoke(SmtEngine* smtEngine) {
try {
vector<SExpr> v;
v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
@@ -1570,7 +1570,7 @@ std::string GetInfoCommand::getResult() const throw() {
return d_result;
}
-void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const {
if(! ok()) {
this->Command::printResult(out, verbosity);
} else if(d_result != "") {
@@ -1609,7 +1609,7 @@ SExpr SetOptionCommand::getSExpr() const throw() {
return d_sexpr;
}
-void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
+void SetOptionCommand::invoke(SmtEngine* smtEngine) {
try {
smtEngine->setOption(d_flag, d_sexpr);
d_commandStatus = CommandSuccess::instance();
@@ -1642,7 +1642,7 @@ std::string GetOptionCommand::getFlag() const throw() {
return d_flag;
}
-void GetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
+void GetOptionCommand::invoke(SmtEngine* smtEngine) {
try {
SExpr res = smtEngine->getOption(d_flag);
d_result = res.toString();
@@ -1658,7 +1658,7 @@ std::string GetOptionCommand::getResult() const throw() {
return d_result;
}
-void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const {
if(! ok()) {
this->Command::printResult(out, verbosity);
} else if(d_result != "") {
@@ -1698,7 +1698,7 @@ DatatypeDeclarationCommand::getDatatypes() const throw() {
return d_datatypes;
}
-void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() {
+void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) {
d_commandStatus = CommandSuccess::instance();
}
@@ -1749,7 +1749,7 @@ const RewriteRuleCommand::Triggers& RewriteRuleCommand::getTriggers() const thro
return d_triggers;
}
-void RewriteRuleCommand::invoke(SmtEngine* smtEngine) throw() {
+void RewriteRuleCommand::invoke(SmtEngine* smtEngine) {
try {
ExprManager* em = smtEngine->getExprManager();
/** build vars list */
@@ -1861,7 +1861,7 @@ bool PropagateRuleCommand::isDeduction() const throw() {
return d_deduction;
}
-void PropagateRuleCommand::invoke(SmtEngine* smtEngine) throw() {
+void PropagateRuleCommand::invoke(SmtEngine* smtEngine) {
try {
ExprManager* em = smtEngine->getExprManager();
/** build vars list */
diff --git a/src/smt/command.h b/src/smt/command.h
index db4efd819..c4db23e04 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -215,8 +215,8 @@ public:
virtual ~Command() throw();
- virtual void invoke(SmtEngine* smtEngine) throw() = 0;
- virtual void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
+ virtual void invoke(SmtEngine* smtEngine) = 0;
+ virtual void invoke(SmtEngine* smtEngine, std::ostream& out);
virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const throw();
@@ -255,7 +255,7 @@ public:
/** Get the command status (it's NULL if we haven't run yet). */
const CommandStatus* getCommandStatus() const throw() { return d_commandStatus; }
- virtual void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ virtual void printResult(std::ostream& out, uint32_t verbosity = 2) const;
/**
* Maps this Command into one for a different ExprManager, using
@@ -299,7 +299,7 @@ public:
EmptyCommand(std::string name = "") throw();
~EmptyCommand() throw() {}
std::string getName() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -312,8 +312,8 @@ public:
EchoCommand(std::string output = "") throw();
~EchoCommand() throw() {}
std::string getOutput() const throw();
- void invoke(SmtEngine* smtEngine) throw();
- void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
+ void invoke(SmtEngine* smtEngine);
+ void invoke(SmtEngine* smtEngine, std::ostream& out);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -327,7 +327,7 @@ public:
AssertCommand(const Expr& e, bool inUnsatCore = true) throw();
~AssertCommand() throw() {}
Expr getExpr() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -336,7 +336,7 @@ public:
class CVC4_PUBLIC PushCommand : public Command {
public:
~PushCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -345,7 +345,7 @@ public:
class CVC4_PUBLIC PopCommand : public Command {
public:
~PopCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -357,7 +357,7 @@ protected:
public:
DeclarationDefinitionCommand(const std::string& id) throw();
~DeclarationDefinitionCommand() throw() {}
- virtual void invoke(SmtEngine* smtEngine) throw() = 0;
+ virtual void invoke(SmtEngine* smtEngine) = 0;
std::string getSymbol() const throw();
};/* class DeclarationDefinitionCommand */
@@ -375,7 +375,7 @@ public:
bool getPrintInModel() const throw();
bool getPrintInModelSetByUser() const throw();
void setPrintInModel( bool p );
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -390,7 +390,7 @@ public:
~DeclareTypeCommand() throw() {}
size_t getArity() const throw();
Type getType() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -406,7 +406,7 @@ public:
~DefineTypeCommand() throw() {}
const std::vector<Type>& getParameters() const throw();
Type getType() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -425,7 +425,7 @@ public:
Expr getFunction() const throw();
const std::vector<Expr>& getFormals() const throw();
Expr getFormula() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -440,7 +440,7 @@ class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand {
public:
DefineNamedFunctionCommand(const std::string& id, Expr func,
const std::vector<Expr>& formals, Expr formula) throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
};/* class DefineNamedFunctionCommand */
@@ -460,7 +460,7 @@ public:
SetUserAttributeCommand( const std::string& attr, Expr expr, std::vector<Expr>& values ) throw();
SetUserAttributeCommand( const std::string& attr, Expr expr, const std::string& value ) throw();
~SetUserAttributeCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -476,9 +476,9 @@ public:
CheckSatCommand(const Expr& expr, bool inUnsatCore = true) throw();
~CheckSatCommand() throw() {}
Expr getExpr() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Result getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -493,9 +493,9 @@ public:
QueryCommand(const Expr& e, bool inUnsatCore = true) throw();
~QueryCommand() throw() {}
Expr getExpr() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Result getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -511,9 +511,9 @@ public:
CheckSynthCommand(const Expr& expr, bool inUnsatCore = true) throw();
~CheckSynthCommand() throw() {}
Expr getExpr() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Result getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -528,9 +528,9 @@ public:
SimplifyCommand(Expr term) throw();
~SimplifyCommand() throw() {}
Expr getTerm() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Expr getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -544,9 +544,9 @@ public:
ExpandDefinitionsCommand(Expr term) throw();
~ExpandDefinitionsCommand() throw() {}
Expr getTerm() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Expr getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -561,9 +561,9 @@ public:
GetValueCommand(const std::vector<Expr>& terms) throw();
~GetValueCommand() throw() {}
const std::vector<Expr>& getTerms() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Expr getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -575,9 +575,9 @@ protected:
public:
GetAssignmentCommand() throw();
~GetAssignmentCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
SExpr getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -590,10 +590,10 @@ protected:
public:
GetModelCommand() throw();
~GetModelCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
// Model is private to the library -- for now
//Model* getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -606,9 +606,9 @@ protected:
public:
GetProofCommand() throw();
~GetProofCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Proof* getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -621,9 +621,9 @@ protected:
public:
GetInstantiationsCommand() throw();
~GetInstantiationsCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
//Instantiations* getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -635,8 +635,8 @@ protected:
public:
GetSynthSolutionCommand() throw();
~GetSynthSolutionCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void invoke(SmtEngine* smtEngine);
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -653,9 +653,9 @@ public:
~GetQuantifierEliminationCommand() throw() {}
Expr getExpr() const throw();
bool getDoFull() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Expr getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -669,8 +669,8 @@ public:
GetUnsatCoreCommand() throw();
GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw();
~GetUnsatCoreCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void invoke(SmtEngine* smtEngine);
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
const UnsatCore& getUnsatCore() const throw();
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
@@ -683,9 +683,9 @@ protected:
public:
GetAssertionsCommand() throw();
~GetAssertionsCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
std::string getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -698,7 +698,7 @@ public:
SetBenchmarkStatusCommand(BenchmarkStatus status) throw();
~SetBenchmarkStatusCommand() throw() {}
BenchmarkStatus getStatus() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -711,7 +711,7 @@ public:
SetBenchmarkLogicCommand(std::string logic) throw();
~SetBenchmarkLogicCommand() throw() {}
std::string getLogic() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -726,7 +726,7 @@ public:
~SetInfoCommand() throw() {}
std::string getFlag() const throw();
SExpr getSExpr() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -740,9 +740,9 @@ public:
GetInfoCommand(std::string flag) throw();
~GetInfoCommand() throw() {}
std::string getFlag() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
std::string getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -757,7 +757,7 @@ public:
~SetOptionCommand() throw() {}
std::string getFlag() const throw();
SExpr getSExpr() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -771,9 +771,9 @@ public:
GetOptionCommand(std::string flag) throw();
~GetOptionCommand() throw() {}
std::string getFlag() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
std::string getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const;
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -787,7 +787,7 @@ public:
~DatatypeDeclarationCommand() throw() {}
DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw();
const std::vector<DatatypeType>& getDatatypes() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -818,7 +818,7 @@ public:
Expr getHead() const throw();
Expr getBody() const throw();
const Triggers& getTriggers() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -854,7 +854,7 @@ public:
Expr getBody() const throw();
const Triggers& getTriggers() const throw();
bool isDeduction() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -864,7 +864,7 @@ class CVC4_PUBLIC ResetCommand : public Command {
public:
ResetCommand() throw() {}
~ResetCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -874,7 +874,7 @@ class CVC4_PUBLIC ResetAssertionsCommand : public Command {
public:
ResetAssertionsCommand() throw() {}
~ResetAssertionsCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -884,7 +884,7 @@ class CVC4_PUBLIC QuitCommand : public Command {
public:
QuitCommand() throw() {}
~QuitCommand() throw() {}
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -896,7 +896,7 @@ public:
CommentCommand(std::string comment) throw();
~CommentCommand() throw() {}
std::string getComment() const throw();
- void invoke(SmtEngine* smtEngine) throw();
+ void invoke(SmtEngine* smtEngine);
Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
Command* clone() const;
std::string getCommandName() const throw();
@@ -915,8 +915,8 @@ public:
void addCommand(Command* cmd) throw();
void clear() throw();
- void invoke(SmtEngine* smtEngine) throw();
- void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
+ void invoke(SmtEngine* smtEngine);
+ void invoke(SmtEngine* smtEngine, std::ostream& out);
typedef std::vector<Command*>::iterator iterator;
typedef std::vector<Command*>::const_iterator const_iterator;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8e641aca1..20cd5e83e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2104,8 +2104,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
throw UnrecognizedOptionException();
}
-CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
- throw(OptionException, ModalException) {
+CVC4::SExpr SmtEngine::getInfo(const std::string& key) const {
SmtScope smts(this);
@@ -4649,7 +4648,7 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin
return resultNode.toExpr();
}
-bool SmtEngine::addToAssignment(const Expr& ex) throw() {
+bool SmtEngine::addToAssignment(const Expr& ex) {
SmtScope smts(this);
finalOptionsAreSet();
doPendingPops();
@@ -4682,7 +4681,7 @@ bool SmtEngine::addToAssignment(const Expr& ex) throw() {
return true;
}
-CVC4::SExpr SmtEngine::getAssignment() throw(ModalException, UnsafeInterruptException) {
+CVC4::SExpr SmtEngine::getAssignment() {
Trace("smt") << "SMT getAssignment()" << endl;
SmtScope smts(this);
finalOptionsAreSet();
@@ -4780,7 +4779,7 @@ void SmtEngine::addToModelCommandAndDump(const Command& c, uint32_t flags, bool
}
}
-Model* SmtEngine::getModel() throw(ModalException, UnsafeInterruptException) {
+Model* SmtEngine::getModel() {
Trace("smt") << "SMT getModel()" << endl;
SmtScope smts(this);
@@ -5042,7 +5041,7 @@ void SmtEngine::checkModel(bool hardFailure) {
Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl;
}
-UnsatCore SmtEngine::getUnsatCore() throw(ModalException, UnsafeInterruptException) {
+UnsatCore SmtEngine::getUnsatCore() {
Trace("smt") << "SMT getUnsatCore()" << endl;
SmtScope smts(this);
finalOptionsAreSet();
@@ -5066,7 +5065,7 @@ UnsatCore SmtEngine::getUnsatCore() throw(ModalException, UnsafeInterruptExcepti
#endif /* IS_PROOFS_BUILD */
}
-Proof* SmtEngine::getProof() throw(ModalException, UnsafeInterruptException) {
+Proof* SmtEngine::getProof() {
Trace("smt") << "SMT getProof()" << endl;
SmtScope smts(this);
finalOptionsAreSet();
@@ -5202,7 +5201,7 @@ void SmtEngine::getInstantiationTermVectors( Expr q, std::vector< std::vector< E
}
}
-vector<Expr> SmtEngine::getAssertions() throw(ModalException) {
+vector<Expr> SmtEngine::getAssertions() {
SmtScope smts(this);
finalOptionsAreSet();
doPendingPops();
@@ -5250,7 +5249,7 @@ void SmtEngine::push() throw(ModalException, LogicException, UnsafeInterruptExce
<< d_userContext->getLevel() << endl;
}
-void SmtEngine::pop() throw(ModalException, UnsafeInterruptException) {
+void SmtEngine::pop() {
SmtScope smts(this);
finalOptionsAreSet();
Trace("smt") << "SMT pop()" << endl;
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index f1ce2e0e9..d17dd204b 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -394,7 +394,7 @@ class CVC4_PUBLIC SmtEngine {
* or INVALID query). Only permitted if CVC4 was built with model
* support and produce-models is on.
*/
- Model* getModel() throw(ModalException, UnsafeInterruptException);
+ Model* getModel();
// disallow copy/assignment
SmtEngine(const SmtEngine&) CVC4_UNDEFINED;
@@ -443,8 +443,7 @@ public:
/**
* Query information about the SMT environment.
*/
- CVC4::SExpr getInfo(const std::string& key) const
- throw(OptionException, ModalException);
+ CVC4::SExpr getInfo(const std::string& key) const;
/**
* Set an aspect of the current SMT execution environment.
@@ -533,21 +532,21 @@ public:
* this function returns true if the expression was added and false
* if this request was ignored.
*/
- bool addToAssignment(const Expr& e) throw();
+ bool addToAssignment(const Expr& e);
/**
* Get the assignment (only if immediately preceded by a SAT or
* INVALID query). Only permitted if the SmtEngine is set to
* operate interactively and produce-assignments is on.
*/
- CVC4::SExpr getAssignment() throw(ModalException, UnsafeInterruptException);
+ CVC4::SExpr getAssignment();
/**
* Get the last proof (only if immediately preceded by an UNSAT
* or VALID query). Only permitted if CVC4 was built with proof
* support and produce-proofs is on.
*/
- Proof* getProof() throw(ModalException, UnsafeInterruptException);
+ Proof* getProof();
/**
* Print all instantiations made by the quantifiers module.
@@ -580,13 +579,13 @@ public:
* UNSAT or VALID query). Only permitted if CVC4 was built with
* unsat-core support and produce-unsat-cores is on.
*/
- UnsatCore getUnsatCore() throw(ModalException, UnsafeInterruptException);
+ UnsatCore getUnsatCore();
/**
* Get the current set of assertions. Only permitted if the
* SmtEngine is set to operate interactively.
*/
- std::vector<Expr> getAssertions() throw(ModalException);
+ std::vector<Expr> getAssertions();
/**
* Push a user-level context.
@@ -596,7 +595,7 @@ public:
/**
* Pop a user-level context. Throws an exception if nothing to pop.
*/
- void pop() throw(ModalException, UnsafeInterruptException);
+ void pop();
/**
* Completely reset the state of the solver, as though destroyed and
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback