std::vector<Expr> ExportTo(ExprManager* exprManager,
ExprManagerMapCollection& variableMap,
- const std::vector<Expr>& exprs) {
+ const std::vector<Expr>& exprs)
+{
std::vector<Expr> exported;
exported.reserve(exprs.size());
- for (const Expr& expr : exprs) {
+ for (const Expr& expr : exprs)
+ {
exported.push_back(expr.exportTo(exprManager, variableMap));
}
return exported;
const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc();
const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess();
-const CommandInterrupted* CommandInterrupted::s_instance = new CommandInterrupted();
+const CommandInterrupted* CommandInterrupted::s_instance =
+ new CommandInterrupted();
-std::ostream& operator<<(std::ostream& out, const Command& c) throw() {
+std::ostream& operator<<(std::ostream& out, const Command& c)
+{
c.toStream(out,
Node::setdepth::getDepth(out),
Node::printtypes::getPrintTypes(out),
return out;
}
-ostream& operator<<(ostream& out, const Command* c) throw() {
- if(c == NULL) {
+ostream& operator<<(ostream& out, const Command* c)
+{
+ if (c == NULL)
+ {
out << "null";
- } else {
+ }
+ else
+ {
out << *c;
}
return out;
}
-std::ostream& operator<<(std::ostream& out, const CommandStatus& s) throw() {
+std::ostream& operator<<(std::ostream& out, const CommandStatus& s)
+{
s.toStream(out, Node::setlanguage::getLanguage(out));
return out;
}
-ostream& operator<<(ostream& out, const CommandStatus* s) throw() {
- if(s == NULL) {
+ostream& operator<<(ostream& out, const CommandStatus* s)
+{
+ if (s == NULL)
+ {
out << "null";
- } else {
+ }
+ else
+ {
out << *s;
}
return out;
}
-/* class Command */
+/* class CommandPrintSuccess */
-Command::Command() throw() : d_commandStatus(NULL), d_muted(false) {
+void CommandPrintSuccess::applyPrintSuccess(std::ostream& out)
+{
+ out.iword(s_iosIndex) = d_printSuccess;
}
-Command::Command(const Command& cmd) {
- d_commandStatus = (cmd.d_commandStatus == NULL) ? NULL : &cmd.d_commandStatus->clone();
+bool CommandPrintSuccess::getPrintSuccess(std::ostream& out)
+{
+ return out.iword(s_iosIndex);
+}
+
+void CommandPrintSuccess::setPrintSuccess(std::ostream& out, bool printSuccess)
+{
+ out.iword(s_iosIndex) = printSuccess;
+}
+
+std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps)
+{
+ cps.applyPrintSuccess(out);
+ return out;
+}
+
+/* class Command */
+
+Command::Command() : d_commandStatus(NULL), d_muted(false) {}
+Command::Command(const Command& cmd)
+{
+ d_commandStatus =
+ (cmd.d_commandStatus == NULL) ? NULL : &cmd.d_commandStatus->clone();
d_muted = cmd.d_muted;
}
-Command::~Command() throw() {
- if(d_commandStatus != NULL && d_commandStatus != CommandSuccess::instance()) {
+Command::~Command()
+{
+ if (d_commandStatus != NULL && d_commandStatus != CommandSuccess::instance())
+ {
delete d_commandStatus;
}
}
-bool Command::ok() const throw() {
+bool Command::ok() const
+{
// either we haven't run the command yet, or it ran successfully
- return d_commandStatus == NULL || dynamic_cast<const CommandSuccess*>(d_commandStatus) != NULL;
+ return d_commandStatus == NULL
+ || dynamic_cast<const CommandSuccess*>(d_commandStatus) != NULL;
}
-bool Command::fail() const throw() {
- return d_commandStatus != NULL && dynamic_cast<const CommandFailure*>(d_commandStatus) != NULL;
+bool Command::fail() const
+{
+ return d_commandStatus != NULL
+ && dynamic_cast<const CommandFailure*>(d_commandStatus) != NULL;
}
-bool Command::interrupted() const throw() {
- return d_commandStatus != NULL && dynamic_cast<const CommandInterrupted*>(d_commandStatus) != NULL;
+bool Command::interrupted() const
+{
+ return d_commandStatus != NULL
+ && dynamic_cast<const CommandInterrupted*>(d_commandStatus) != NULL;
}
-void Command::invoke(SmtEngine* smtEngine, std::ostream& out) {
+void Command::invoke(SmtEngine* smtEngine, std::ostream& out)
+{
invoke(smtEngine);
- if(!(isMuted() && ok())) {
- printResult(out, smtEngine->getOption("command-verbosity:" + getCommandName()).getIntegerValue().toUnsignedInt());
+ if (!(isMuted() && ok()))
+ {
+ printResult(out,
+ smtEngine->getOption("command-verbosity:" + getCommandName())
+ .getIntegerValue()
+ .toUnsignedInt());
}
}
-std::string Command::toString() const throw() {
+std::string Command::toString() const
+{
std::stringstream ss;
toStream(ss);
return ss.str();
}
-void Command::toStream(std::ostream& out, int toDepth, bool types, size_t dag,
- OutputLanguage language) const throw() {
+void Command::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
Printer::getPrinter(language)->toStream(out, this, toDepth, types, dag);
}
-void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const throw() {
+void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const
+{
Printer::getPrinter(language)->toStream(out, this);
}
-void Command::printResult(std::ostream& out, uint32_t verbosity) const {
- if(d_commandStatus != NULL) {
- if((!ok() && verbosity >= 1) || verbosity >= 2) {
+void Command::printResult(std::ostream& out, uint32_t verbosity) const
+{
+ if (d_commandStatus != NULL)
+ {
+ if ((!ok() && verbosity >= 1) || verbosity >= 2)
+ {
out << *d_commandStatus;
}
}
/* class EmptyCommand */
-EmptyCommand::EmptyCommand(std::string name) throw() :
- d_name(name) {
-}
-
-std::string EmptyCommand::getName() const throw() {
- return d_name;
-}
-
-void EmptyCommand::invoke(SmtEngine* smtEngine) {
+EmptyCommand::EmptyCommand(std::string name) : d_name(name) {}
+std::string EmptyCommand::getName() const { return d_name; }
+void EmptyCommand::invoke(SmtEngine* smtEngine)
+{
/* empty commands have no implementation */
d_commandStatus = CommandSuccess::instance();
}
-Command* EmptyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new EmptyCommand(d_name);
-}
-
-Command* EmptyCommand::clone() const {
+Command* EmptyCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
return new EmptyCommand(d_name);
}
-std::string EmptyCommand::getCommandName() const throw() {
- return "empty";
-}
-
+Command* EmptyCommand::clone() const { return new EmptyCommand(d_name); }
+std::string EmptyCommand::getCommandName() const { return "empty"; }
/* class EchoCommand */
-EchoCommand::EchoCommand(std::string output) throw() :
- d_output(output) {
-}
-
-std::string EchoCommand::getOutput() const throw() {
- return d_output;
-}
-
-void EchoCommand::invoke(SmtEngine* smtEngine) {
+EchoCommand::EchoCommand(std::string output) : d_output(output) {}
+std::string EchoCommand::getOutput() const { return d_output; }
+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) {
+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());
+ printResult(out,
+ smtEngine->getOption("command-verbosity:" + getCommandName())
+ .getIntegerValue()
+ .toUnsignedInt());
}
-Command* EchoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new EchoCommand(d_output);
-}
-
-Command* EchoCommand::clone() const {
+Command* EchoCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
return new EchoCommand(d_output);
}
-std::string EchoCommand::getCommandName() const throw() {
- return "echo";
-}
-
+Command* EchoCommand::clone() const { return new EchoCommand(d_output); }
+std::string EchoCommand::getCommandName() const { return "echo"; }
/* class AssertCommand */
-AssertCommand::AssertCommand(const Expr& e, bool inUnsatCore) throw() :
- d_expr(e), d_inUnsatCore(inUnsatCore) {
-}
-
-Expr AssertCommand::getExpr() const throw() {
- return d_expr;
+AssertCommand::AssertCommand(const Expr& e, bool inUnsatCore)
+ : d_expr(e), d_inUnsatCore(inUnsatCore)
+{
}
-void AssertCommand::invoke(SmtEngine* smtEngine) {
- try {
+Expr AssertCommand::getExpr() const { return d_expr; }
+void AssertCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
smtEngine->assertFormula(d_expr, d_inUnsatCore);
d_commandStatus = CommandSuccess::instance();
- } catch(UnsafeInterruptException& e) {
+ }
+ catch (UnsafeInterruptException& e)
+ {
d_commandStatus = new CommandInterrupted();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Command* AssertCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new AssertCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore);
+Command* AssertCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
+ return new AssertCommand(d_expr.exportTo(exprManager, variableMap),
+ d_inUnsatCore);
}
-Command* AssertCommand::clone() const {
+Command* AssertCommand::clone() const
+{
return new AssertCommand(d_expr, d_inUnsatCore);
}
-std::string AssertCommand::getCommandName() const throw() {
- return "assert";
-}
-
+std::string AssertCommand::getCommandName() const { return "assert"; }
/* class PushCommand */
-void PushCommand::invoke(SmtEngine* smtEngine) {
- try {
+void PushCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
smtEngine->push();
d_commandStatus = CommandSuccess::instance();
- } catch(UnsafeInterruptException& e) {
+ }
+ catch (UnsafeInterruptException& e)
+ {
d_commandStatus = new CommandInterrupted();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Command* PushCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new PushCommand();
-}
-
-Command* PushCommand::clone() const {
+Command* PushCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
return new PushCommand();
}
-std::string PushCommand::getCommandName() const throw() {
- return "push";
-}
-
+Command* PushCommand::clone() const { return new PushCommand(); }
+std::string PushCommand::getCommandName() const { return "push"; }
/* class PopCommand */
-void PopCommand::invoke(SmtEngine* smtEngine) {
- try {
+void PopCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
smtEngine->pop();
d_commandStatus = CommandSuccess::instance();
- } catch(UnsafeInterruptException& e) {
+ }
+ catch (UnsafeInterruptException& e)
+ {
d_commandStatus = new CommandInterrupted();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Command* PopCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new PopCommand();
-}
-
-Command* PopCommand::clone() const {
+Command* PopCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
return new PopCommand();
}
-std::string PopCommand::getCommandName() const throw() {
- return "pop";
-}
-
+Command* PopCommand::clone() const { return new PopCommand(); }
+std::string PopCommand::getCommandName() const { return "pop"; }
/* class CheckSatCommand */
-CheckSatCommand::CheckSatCommand() throw() :
- d_expr() {
-}
-
-CheckSatCommand::CheckSatCommand(const Expr& expr, bool inUnsatCore) throw() :
- d_expr(expr), d_inUnsatCore(inUnsatCore) {
-}
-
-Expr CheckSatCommand::getExpr() const throw() {
- return d_expr;
+CheckSatCommand::CheckSatCommand() : d_expr() {}
+CheckSatCommand::CheckSatCommand(const Expr& expr, bool inUnsatCore)
+ : d_expr(expr), d_inUnsatCore(inUnsatCore)
+{
}
-void CheckSatCommand::invoke(SmtEngine* smtEngine) {
- try {
+Expr CheckSatCommand::getExpr() const { return d_expr; }
+void CheckSatCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
d_result = smtEngine->checkSat(d_expr);
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Result CheckSatCommand::getResult() const throw() {
- return d_result;
-}
-
-void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+Result CheckSatCommand::getResult() const { return d_result; }
+void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
+ }
+ else
+ {
out << d_result << endl;
}
}
-Command* CheckSatCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- CheckSatCommand* c = new CheckSatCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore);
+Command* CheckSatCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
+ CheckSatCommand* c = new CheckSatCommand(
+ d_expr.exportTo(exprManager, variableMap), d_inUnsatCore);
c->d_result = d_result;
return c;
}
-Command* CheckSatCommand::clone() const {
+Command* CheckSatCommand::clone() const
+{
CheckSatCommand* c = new CheckSatCommand(d_expr, d_inUnsatCore);
c->d_result = d_result;
return c;
}
-std::string CheckSatCommand::getCommandName() const throw() {
- return "check-sat";
-}
-
+std::string CheckSatCommand::getCommandName() const { return "check-sat"; }
/* class QueryCommand */
-QueryCommand::QueryCommand(const Expr& e, bool inUnsatCore) throw() :
- d_expr(e), d_inUnsatCore(inUnsatCore) {
-}
-
-Expr QueryCommand::getExpr() const throw() {
- return d_expr;
+QueryCommand::QueryCommand(const Expr& e, bool inUnsatCore)
+ : d_expr(e), d_inUnsatCore(inUnsatCore)
+{
}
-void QueryCommand::invoke(SmtEngine* smtEngine) {
- try {
+Expr QueryCommand::getExpr() const { return d_expr; }
+void QueryCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
d_result = smtEngine->query(d_expr);
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Result QueryCommand::getResult() const throw() {
- return d_result;
-}
-
-void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+Result QueryCommand::getResult() const { return d_result; }
+void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
+ }
+ else
+ {
out << d_result << endl;
}
}
-Command* QueryCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- QueryCommand* c = new QueryCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore);
+Command* QueryCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
+ QueryCommand* c = new QueryCommand(d_expr.exportTo(exprManager, variableMap),
+ d_inUnsatCore);
c->d_result = d_result;
return c;
}
-Command* QueryCommand::clone() const {
+Command* QueryCommand::clone() const
+{
QueryCommand* c = new QueryCommand(d_expr, d_inUnsatCore);
c->d_result = d_result;
return c;
}
-std::string QueryCommand::getCommandName() const throw() {
- return "query";
-}
-
-
+std::string QueryCommand::getCommandName() const { return "query"; }
/* class CheckSynthCommand */
-CheckSynthCommand::CheckSynthCommand() throw() :
- d_expr() {
-}
-
-CheckSynthCommand::CheckSynthCommand(const Expr& expr) throw() :
- d_expr(expr) {
-}
-
-Expr CheckSynthCommand::getExpr() const throw() {
- return d_expr;
-}
-
-void CheckSynthCommand::invoke(SmtEngine* smtEngine) {
- try {
+CheckSynthCommand::CheckSynthCommand() : d_expr() {}
+CheckSynthCommand::CheckSynthCommand(const Expr& expr) : d_expr(expr) {}
+Expr CheckSynthCommand::getExpr() const { return d_expr; }
+void CheckSynthCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
d_result = smtEngine->checkSynth(d_expr);
d_commandStatus = CommandSuccess::instance();
smt::SmtScope scope(smtEngine);
// instead of during printResult.
smtEngine->printSynthSolution(d_solution);
}
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Result CheckSynthCommand::getResult() const throw() {
- return d_result;
-}
-
-void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+Result CheckSynthCommand::getResult() const { return d_result; }
+void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
+ }
+ else
+ {
out << d_solution.str();
}
}
-Command* CheckSynthCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- CheckSynthCommand* c = new CheckSynthCommand(d_expr.exportTo(exprManager, variableMap));
+Command* CheckSynthCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
+ CheckSynthCommand* c =
+ new CheckSynthCommand(d_expr.exportTo(exprManager, variableMap));
c->d_result = d_result;
return c;
}
-Command* CheckSynthCommand::clone() const {
+Command* CheckSynthCommand::clone() const
+{
CheckSynthCommand* c = new CheckSynthCommand(d_expr);
c->d_result = d_result;
return c;
}
-std::string CheckSynthCommand::getCommandName() const throw() {
- return "check-synth";
-}
-
-
+std::string CheckSynthCommand::getCommandName() const { return "check-synth"; }
/* class ResetCommand */
-void ResetCommand::invoke(SmtEngine* smtEngine) {
- try {
+void ResetCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
smtEngine->reset();
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Command* ResetCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new ResetCommand();
-}
-
-Command* ResetCommand::clone() const {
+Command* ResetCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
return new ResetCommand();
}
-std::string ResetCommand::getCommandName() const throw() {
- return "reset";
-}
-
+Command* ResetCommand::clone() const { return new ResetCommand(); }
+std::string ResetCommand::getCommandName() const { return "reset"; }
/* class ResetAssertionsCommand */
-void ResetAssertionsCommand::invoke(SmtEngine* smtEngine) {
- try {
+void ResetAssertionsCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
smtEngine->resetAssertions();
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Command* ResetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* ResetAssertionsCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
return new ResetAssertionsCommand();
}
-Command* ResetAssertionsCommand::clone() const {
+Command* ResetAssertionsCommand::clone() const
+{
return new ResetAssertionsCommand();
}
-std::string ResetAssertionsCommand::getCommandName() const throw() {
+std::string ResetAssertionsCommand::getCommandName() const
+{
return "reset-assertions";
}
/* class QuitCommand */
-void QuitCommand::invoke(SmtEngine* smtEngine) {
+void QuitCommand::invoke(SmtEngine* smtEngine)
+{
Dump("benchmark") << *this;
d_commandStatus = CommandSuccess::instance();
}
-Command* QuitCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new QuitCommand();
-}
-
-Command* QuitCommand::clone() const {
+Command* QuitCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
return new QuitCommand();
}
-std::string QuitCommand::getCommandName() const throw() {
- return "exit";
-}
-
+Command* QuitCommand::clone() const { return new QuitCommand(); }
+std::string QuitCommand::getCommandName() const { return "exit"; }
/* class CommentCommand */
-CommentCommand::CommentCommand(std::string comment) throw() : d_comment(comment) {
-}
-
-std::string CommentCommand::getComment() const throw() {
- return d_comment;
-}
-
-void CommentCommand::invoke(SmtEngine* smtEngine) {
+CommentCommand::CommentCommand(std::string comment) : d_comment(comment) {}
+std::string CommentCommand::getComment() const { return d_comment; }
+void CommentCommand::invoke(SmtEngine* smtEngine)
+{
Dump("benchmark") << *this;
d_commandStatus = CommandSuccess::instance();
}
-Command* CommentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- return new CommentCommand(d_comment);
-}
-
-Command* CommentCommand::clone() const {
+Command* CommentCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
return new CommentCommand(d_comment);
}
-std::string CommentCommand::getCommandName() const throw() {
- return "comment";
-}
-
+Command* CommentCommand::clone() const { return new CommentCommand(d_comment); }
+std::string CommentCommand::getCommandName() const { return "comment"; }
/* class CommandSequence */
-CommandSequence::CommandSequence() throw() :
- d_index(0) {
-}
-
-CommandSequence::~CommandSequence() throw() {
- for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
+CommandSequence::CommandSequence() : d_index(0) {}
+CommandSequence::~CommandSequence()
+{
+ for (unsigned i = d_index; i < d_commandSequence.size(); ++i)
+ {
delete d_commandSequence[i];
}
}
-void CommandSequence::addCommand(Command* cmd) throw() {
+void CommandSequence::addCommand(Command* cmd)
+{
d_commandSequence.push_back(cmd);
}
-void CommandSequence::clear() throw() {
- d_commandSequence.clear();
-}
-
-void CommandSequence::invoke(SmtEngine* smtEngine) {
- for(; d_index < d_commandSequence.size(); ++d_index) {
+void CommandSequence::clear() { d_commandSequence.clear(); }
+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()) {
+ if (!d_commandSequence[d_index]->ok())
+ {
// abort execution
d_commandStatus = d_commandSequence[d_index]->getCommandStatus();
return;
d_commandStatus = CommandSuccess::instance();
}
-void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) {
- for(; d_index < d_commandSequence.size(); ++d_index) {
+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()) {
+ if (!d_commandSequence[d_index]->ok())
+ {
// abort execution
d_commandStatus = d_commandSequence[d_index]->getCommandStatus();
return;
d_commandStatus = CommandSuccess::instance();
}
-Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* CommandSequence::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
CommandSequence* seq = new CommandSequence();
- for(iterator i = begin(); i != end(); ++i) {
+ for (iterator i = begin(); i != end(); ++i)
+ {
Command* cmd_to_export = *i;
Command* cmd = cmd_to_export->exportTo(exprManager, variableMap);
seq->addCommand(cmd);
return seq;
}
-Command* CommandSequence::clone() const {
+Command* CommandSequence::clone() const
+{
CommandSequence* seq = new CommandSequence();
- for(const_iterator i = begin(); i != end(); ++i) {
+ for (const_iterator i = begin(); i != end(); ++i)
+ {
seq->addCommand((*i)->clone());
}
seq->d_index = d_index;
return seq;
}
-CommandSequence::const_iterator CommandSequence::begin() const throw() {
+CommandSequence::const_iterator CommandSequence::begin() const
+{
return d_commandSequence.begin();
}
-CommandSequence::const_iterator CommandSequence::end() const throw() {
+CommandSequence::const_iterator CommandSequence::end() const
+{
return d_commandSequence.end();
}
-CommandSequence::iterator CommandSequence::begin() throw() {
+CommandSequence::iterator CommandSequence::begin()
+{
return d_commandSequence.begin();
}
-CommandSequence::iterator CommandSequence::end() throw() {
+CommandSequence::iterator CommandSequence::end()
+{
return d_commandSequence.end();
}
-std::string CommandSequence::getCommandName() const throw() {
- return "sequence";
-}
-
+std::string CommandSequence::getCommandName() const { return "sequence"; }
/* class DeclarationSequenceCommand */
/* class DeclarationDefinitionCommand */
-DeclarationDefinitionCommand::DeclarationDefinitionCommand(const std::string& id) throw() :
- d_symbol(id) {
-}
-
-std::string DeclarationDefinitionCommand::getSymbol() const throw() {
- return d_symbol;
+DeclarationDefinitionCommand::DeclarationDefinitionCommand(
+ const std::string& id)
+ : d_symbol(id)
+{
}
+std::string DeclarationDefinitionCommand::getSymbol() const { return d_symbol; }
/* class DeclareFunctionCommand */
-DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Expr func, Type t) throw() :
- DeclarationDefinitionCommand(id),
- d_func(func),
- d_type(t),
- d_printInModel(true),
- d_printInModelSetByUser(false){
-}
-
-Expr DeclareFunctionCommand::getFunction() const throw() {
- return d_func;
-}
-
-Type DeclareFunctionCommand::getType() const throw() {
- return d_type;
-}
-
-bool DeclareFunctionCommand::getPrintInModel() const throw() {
- return d_printInModel;
+DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id,
+ Expr func,
+ Type t)
+ : DeclarationDefinitionCommand(id),
+ d_func(func),
+ d_type(t),
+ d_printInModel(true),
+ d_printInModelSetByUser(false)
+{
}
-bool DeclareFunctionCommand::getPrintInModelSetByUser() const throw() {
+Expr DeclareFunctionCommand::getFunction() const { return d_func; }
+Type DeclareFunctionCommand::getType() const { return d_type; }
+bool DeclareFunctionCommand::getPrintInModel() const { return d_printInModel; }
+bool DeclareFunctionCommand::getPrintInModelSetByUser() const
+{
return d_printInModelSetByUser;
}
-void DeclareFunctionCommand::setPrintInModel( bool p ) {
+void DeclareFunctionCommand::setPrintInModel(bool p)
+{
d_printInModel = p;
d_printInModelSetByUser = true;
}
-void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) {
+void DeclareFunctionCommand::invoke(SmtEngine* smtEngine)
+{
d_commandStatus = CommandSuccess::instance();
}
Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) {
- DeclareFunctionCommand * dfc = new DeclareFunctionCommand(d_symbol, d_func.exportTo(exprManager, variableMap),
- d_type.exportTo(exprManager, variableMap));
+ ExprManagerMapCollection& variableMap)
+{
+ DeclareFunctionCommand* dfc =
+ new DeclareFunctionCommand(d_symbol,
+ d_func.exportTo(exprManager, variableMap),
+ d_type.exportTo(exprManager, variableMap));
dfc->d_printInModel = d_printInModel;
dfc->d_printInModelSetByUser = d_printInModelSetByUser;
return dfc;
}
-Command* DeclareFunctionCommand::clone() const {
- DeclareFunctionCommand * dfc = new DeclareFunctionCommand(d_symbol, d_func, d_type);
+Command* DeclareFunctionCommand::clone() const
+{
+ DeclareFunctionCommand* dfc =
+ new DeclareFunctionCommand(d_symbol, d_func, d_type);
dfc->d_printInModel = d_printInModel;
dfc->d_printInModelSetByUser = d_printInModelSetByUser;
return dfc;
}
-std::string DeclareFunctionCommand::getCommandName() const throw() {
+std::string DeclareFunctionCommand::getCommandName() const
+{
return "declare-fun";
}
/* class DeclareTypeCommand */
-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 throw() {
- return d_arity;
-}
-
-Type DeclareTypeCommand::getType() const throw() {
- return d_type;
+DeclareTypeCommand::DeclareTypeCommand(const std::string& id,
+ size_t arity,
+ Type t)
+ : DeclarationDefinitionCommand(id), d_arity(arity), d_type(t)
+{
}
-void DeclareTypeCommand::invoke(SmtEngine* smtEngine) {
+size_t DeclareTypeCommand::getArity() const { return d_arity; }
+Type DeclareTypeCommand::getType() const { return d_type; }
+void DeclareTypeCommand::invoke(SmtEngine* smtEngine)
+{
d_commandStatus = CommandSuccess::instance();
}
Command* DeclareTypeCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) {
- return new DeclareTypeCommand(d_symbol, d_arity,
- d_type.exportTo(exprManager, variableMap));
+ ExprManagerMapCollection& variableMap)
+{
+ return new DeclareTypeCommand(
+ d_symbol, d_arity, d_type.exportTo(exprManager, variableMap));
}
-Command* DeclareTypeCommand::clone() const {
+Command* DeclareTypeCommand::clone() const
+{
return new DeclareTypeCommand(d_symbol, d_arity, d_type);
}
-std::string DeclareTypeCommand::getCommandName() const throw() {
+std::string DeclareTypeCommand::getCommandName() const
+{
return "declare-sort";
}
/* class DefineTypeCommand */
-DefineTypeCommand::DefineTypeCommand(const std::string& id,
- Type t) throw() :
- DeclarationDefinitionCommand(id),
- d_params(),
- d_type(t) {
+DefineTypeCommand::DefineTypeCommand(const std::string& id, Type t)
+ : DeclarationDefinitionCommand(id), d_params(), d_type(t)
+{
}
DefineTypeCommand::DefineTypeCommand(const std::string& id,
const std::vector<Type>& params,
- Type t) throw() :
- DeclarationDefinitionCommand(id),
- d_params(params),
- d_type(t) {
+ Type t)
+ : DeclarationDefinitionCommand(id), d_params(params), d_type(t)
+{
}
-const std::vector<Type>& DefineTypeCommand::getParameters() const throw() {
+const std::vector<Type>& DefineTypeCommand::getParameters() const
+{
return d_params;
}
-Type DefineTypeCommand::getType() const throw() {
- return d_type;
-}
-
-void DefineTypeCommand::invoke(SmtEngine* smtEngine) {
+Type DefineTypeCommand::getType() const { return d_type; }
+void DefineTypeCommand::invoke(SmtEngine* smtEngine)
+{
d_commandStatus = CommandSuccess::instance();
}
-Command* DefineTypeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* DefineTypeCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
vector<Type> params;
- transform(d_params.begin(), d_params.end(), back_inserter(params),
+ transform(d_params.begin(),
+ d_params.end(),
+ back_inserter(params),
ExportTransformer(exprManager, variableMap));
Type type = d_type.exportTo(exprManager, variableMap);
return new DefineTypeCommand(d_symbol, params, type);
}
-Command* DefineTypeCommand::clone() const {
+Command* DefineTypeCommand::clone() const
+{
return new DefineTypeCommand(d_symbol, d_params, d_type);
}
-std::string DefineTypeCommand::getCommandName() const throw() {
- return "define-sort";
-}
-
+std::string DefineTypeCommand::getCommandName() const { return "define-sort"; }
/* class DefineFunctionCommand */
DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
Expr func,
- Expr formula) throw() :
- DeclarationDefinitionCommand(id),
- d_func(func),
- d_formals(),
- d_formula(formula) {
+ Expr formula)
+ : DeclarationDefinitionCommand(id),
+ d_func(func),
+ d_formals(),
+ d_formula(formula)
+{
}
DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
Expr func,
const std::vector<Expr>& formals,
- Expr formula) throw() :
- DeclarationDefinitionCommand(id),
- d_func(func),
- d_formals(formals),
- d_formula(formula) {
-}
-
-Expr DefineFunctionCommand::getFunction() const throw() {
- return d_func;
+ Expr formula)
+ : DeclarationDefinitionCommand(id),
+ d_func(func),
+ d_formals(formals),
+ d_formula(formula)
+{
}
-const std::vector<Expr>& DefineFunctionCommand::getFormals() const throw() {
+Expr DefineFunctionCommand::getFunction() const { return d_func; }
+const std::vector<Expr>& DefineFunctionCommand::getFormals() const
+{
return d_formals;
}
-Expr DefineFunctionCommand::getFormula() const throw() {
- return d_formula;
-}
-
-void DefineFunctionCommand::invoke(SmtEngine* smtEngine) {
- try {
- if(!d_func.isNull()) {
+Expr DefineFunctionCommand::getFormula() const { return d_formula; }
+void DefineFunctionCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
+ if (!d_func.isNull())
+ {
smtEngine->defineFunction(d_func, d_formals, d_formula);
}
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- Expr func = d_func.exportTo(exprManager, variableMap, /* flags = */ ExprManager::VAR_FLAG_DEFINED);
+Command* DefineFunctionCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
+ Expr func = d_func.exportTo(
+ exprManager, variableMap, /* flags = */ ExprManager::VAR_FLAG_DEFINED);
vector<Expr> formals;
- transform(d_formals.begin(), d_formals.end(), back_inserter(formals),
+ transform(d_formals.begin(),
+ d_formals.end(),
+ back_inserter(formals),
ExportTransformer(exprManager, variableMap));
Expr formula = d_formula.exportTo(exprManager, variableMap);
return new DefineFunctionCommand(d_symbol, func, formals, formula);
}
-Command* DefineFunctionCommand::clone() const {
+Command* DefineFunctionCommand::clone() const
+{
return new DefineFunctionCommand(d_symbol, d_func, d_formals, d_formula);
}
-std::string DefineFunctionCommand::getCommandName() const throw() {
+std::string DefineFunctionCommand::getCommandName() const
+{
return "define-fun";
}
/* class DefineNamedFunctionCommand */
-DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id,
- Expr func,
- const std::vector<Expr>& formals,
- Expr formula) throw() :
- DefineFunctionCommand(id, func, formals, formula) {
+DefineNamedFunctionCommand::DefineNamedFunctionCommand(
+ const std::string& id,
+ Expr func,
+ const std::vector<Expr>& formals,
+ Expr formula)
+ : DefineFunctionCommand(id, func, formals, formula)
+{
}
-void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) {
+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));
+ if (!d_func.isNull() && d_func.getType().isBoolean())
+ {
+ smtEngine->addToAssignment(
+ d_func.getExprManager()->mkExpr(kind::APPLY, d_func));
}
d_commandStatus = CommandSuccess::instance();
}
-Command* DefineNamedFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* DefineNamedFunctionCommand::exportTo(
+ ExprManager* exprManager, ExprManagerMapCollection& variableMap)
+{
Expr func = d_func.exportTo(exprManager, variableMap);
vector<Expr> formals;
- transform(d_formals.begin(), d_formals.end(), back_inserter(formals),
+ transform(d_formals.begin(),
+ d_formals.end(),
+ back_inserter(formals),
ExportTransformer(exprManager, variableMap));
Expr formula = d_formula.exportTo(exprManager, variableMap);
return new DefineNamedFunctionCommand(d_symbol, func, formals, formula);
}
-Command* DefineNamedFunctionCommand::clone() const {
+Command* DefineNamedFunctionCommand::clone() const
+{
return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula);
}
/* class DefineFunctionRecCommand */
DefineFunctionRecCommand::DefineFunctionRecCommand(
- Expr func, const std::vector<Expr>& formals, Expr formula) throw()
+ Expr func, const std::vector<Expr>& formals, Expr formula)
{
d_funcs.push_back(func);
d_formals.push_back(formals);
DefineFunctionRecCommand::DefineFunctionRecCommand(
const std::vector<Expr>& funcs,
const std::vector<std::vector<Expr> >& formals,
- const std::vector<Expr>& formulas) throw()
+ const std::vector<Expr>& formulas)
{
d_funcs.insert(d_funcs.end(), funcs.begin(), funcs.end());
d_formals.insert(d_formals.end(), formals.begin(), formals.end());
d_formulas.insert(d_formulas.end(), formulas.begin(), formulas.end());
}
-const std::vector<Expr>& DefineFunctionRecCommand::getFunctions() const throw()
+const std::vector<Expr>& DefineFunctionRecCommand::getFunctions() const
{
return d_funcs;
}
const std::vector<std::vector<Expr> >& DefineFunctionRecCommand::getFormals()
- const throw()
+ const
{
return d_formals;
}
-const std::vector<Expr>& DefineFunctionRecCommand::getFormulas() const throw()
+const std::vector<Expr>& DefineFunctionRecCommand::getFormulas() const
{
return d_formulas;
}
return new DefineFunctionRecCommand(d_funcs, d_formals, d_formulas);
}
-std::string DefineFunctionRecCommand::getCommandName() const throw()
+std::string DefineFunctionRecCommand::getCommandName() const
{
return "define-fun-rec";
}
/* class SetUserAttribute */
SetUserAttributeCommand::SetUserAttributeCommand(
- const std::string& attr, Expr expr, const std::vector<Expr>& expr_values,
- const std::string& str_value) throw()
+ const std::string& attr,
+ Expr expr,
+ const std::vector<Expr>& expr_values,
+ const std::string& str_value)
: d_attr(attr),
d_expr(expr),
d_expr_values(expr_values),
- d_str_value(str_value) {}
+ d_str_value(str_value)
+{
+}
SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr,
- Expr expr) throw()
- : SetUserAttributeCommand(attr, expr, {}, "") {}
+ Expr expr)
+ : SetUserAttributeCommand(attr, expr, {}, "")
+{
+}
SetUserAttributeCommand::SetUserAttributeCommand(
- const std::string& attr, Expr expr, const std::vector<Expr>& values) throw()
- : SetUserAttributeCommand(attr, expr, values, "") {}
+ const std::string& attr, Expr expr, const std::vector<Expr>& values)
+ : SetUserAttributeCommand(attr, expr, values, "")
+{
+}
-SetUserAttributeCommand::SetUserAttributeCommand(
- const std::string& attr, Expr expr, const std::string& value) throw()
- : SetUserAttributeCommand(attr, expr, {}, value) {}
+SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr,
+ Expr expr,
+ const std::string& value)
+ : SetUserAttributeCommand(attr, expr, {}, value)
+{
+}
-void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) {
- try {
- if (!d_expr.isNull()) {
+void SetUserAttributeCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
+ if (!d_expr.isNull())
+ {
smtEngine->setUserAttribute(d_attr, d_expr, d_expr_values, d_str_value);
}
d_commandStatus = CommandSuccess::instance();
- } catch (exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
Command* SetUserAttributeCommand::exportTo(
- ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+ ExprManager* exprManager, ExprManagerMapCollection& variableMap)
+{
Expr expr = d_expr.exportTo(exprManager, variableMap);
return new SetUserAttributeCommand(d_attr, expr, d_expr_values, d_str_value);
}
-Command* SetUserAttributeCommand::clone() const {
- return new SetUserAttributeCommand(d_attr, d_expr, d_expr_values,
- d_str_value);
+Command* SetUserAttributeCommand::clone() const
+{
+ return new SetUserAttributeCommand(
+ d_attr, d_expr, d_expr_values, d_str_value);
}
-std::string SetUserAttributeCommand::getCommandName() const throw() {
+std::string SetUserAttributeCommand::getCommandName() const
+{
return "set-user-attribute";
}
/* class SimplifyCommand */
-SimplifyCommand::SimplifyCommand(Expr term) throw() :
- d_term(term) {
-}
-
-Expr SimplifyCommand::getTerm() const throw() {
- return d_term;
-}
-
-void SimplifyCommand::invoke(SmtEngine* smtEngine) {
- try {
+SimplifyCommand::SimplifyCommand(Expr term) : d_term(term) {}
+Expr SimplifyCommand::getTerm() const { return d_term; }
+void SimplifyCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
d_result = smtEngine->simplify(d_term);
d_commandStatus = CommandSuccess::instance();
- } catch(UnsafeInterruptException& e) {
+ }
+ catch (UnsafeInterruptException& e)
+ {
d_commandStatus = new CommandInterrupted();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Expr SimplifyCommand::getResult() const throw() {
- return d_result;
-}
-
-void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+Expr SimplifyCommand::getResult() const { return d_result; }
+void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
+ }
+ else
+ {
out << d_result << endl;
}
}
-Command* SimplifyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- SimplifyCommand* c = new SimplifyCommand(d_term.exportTo(exprManager, variableMap));
+Command* SimplifyCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
+ SimplifyCommand* c =
+ new SimplifyCommand(d_term.exportTo(exprManager, variableMap));
c->d_result = d_result.exportTo(exprManager, variableMap);
return c;
}
-Command* SimplifyCommand::clone() const {
+Command* SimplifyCommand::clone() const
+{
SimplifyCommand* c = new SimplifyCommand(d_term);
c->d_result = d_result;
return c;
}
-std::string SimplifyCommand::getCommandName() const throw() {
- return "simplify";
-}
-
+std::string SimplifyCommand::getCommandName() const { return "simplify"; }
/* class ExpandDefinitionsCommand */
-ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term) throw() :
- d_term(term) {
-}
-
-Expr ExpandDefinitionsCommand::getTerm() const throw() {
- return d_term;
-}
-
-void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine) {
+ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term) : d_term(term) {}
+Expr ExpandDefinitionsCommand::getTerm() const { return d_term; }
+void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine)
+{
d_result = smtEngine->expandDefinitions(d_term);
d_commandStatus = CommandSuccess::instance();
}
-Expr ExpandDefinitionsCommand::getResult() const throw() {
- return d_result;
-}
-
-void ExpandDefinitionsCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+Expr ExpandDefinitionsCommand::getResult() const { return d_result; }
+void ExpandDefinitionsCommand::printResult(std::ostream& out,
+ uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
+ }
+ else
+ {
out << d_result << endl;
}
}
-Command* ExpandDefinitionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term.exportTo(exprManager, variableMap));
+Command* ExpandDefinitionsCommand::exportTo(
+ ExprManager* exprManager, ExprManagerMapCollection& variableMap)
+{
+ ExpandDefinitionsCommand* c =
+ new ExpandDefinitionsCommand(d_term.exportTo(exprManager, variableMap));
c->d_result = d_result.exportTo(exprManager, variableMap);
return c;
}
-Command* ExpandDefinitionsCommand::clone() const {
+Command* ExpandDefinitionsCommand::clone() const
+{
ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term);
c->d_result = d_result;
return c;
}
-std::string ExpandDefinitionsCommand::getCommandName() const throw() {
+std::string ExpandDefinitionsCommand::getCommandName() const
+{
return "expand-definitions";
}
/* class GetValueCommand */
-GetValueCommand::GetValueCommand(Expr term) throw() :
- d_terms() {
+GetValueCommand::GetValueCommand(Expr term) : d_terms()
+{
d_terms.push_back(term);
}
-GetValueCommand::GetValueCommand(const std::vector<Expr>& terms) throw() :
- d_terms(terms) {
- PrettyCheckArgument(terms.size() >= 1, terms,
- "cannot get-value of an empty set of terms");
-}
-
-const std::vector<Expr>& GetValueCommand::getTerms() const throw() {
- return d_terms;
+GetValueCommand::GetValueCommand(const std::vector<Expr>& terms)
+ : d_terms(terms)
+{
+ PrettyCheckArgument(
+ terms.size() >= 1, terms, "cannot get-value of an empty set of terms");
}
-void GetValueCommand::invoke(SmtEngine* smtEngine) {
- try {
+const std::vector<Expr>& GetValueCommand::getTerms() const { return d_terms; }
+void GetValueCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
vector<Expr> result;
ExprManager* em = smtEngine->getExprManager();
NodeManager* nm = NodeManager::fromExprManager(em);
- for(std::vector<Expr>::const_iterator i = d_terms.begin(); i != d_terms.end(); ++i) {
+ for (std::vector<Expr>::const_iterator i = d_terms.begin();
+ i != d_terms.end();
+ ++i)
+ {
Assert(nm == NodeManager::fromExprManager((*i).getExprManager()));
smt::SmtScope scope(smtEngine);
- Node request = Node::fromExpr(options::expandDefinitions() ? smtEngine->expandDefinitions(*i) : *i);
+ Node request = Node::fromExpr(
+ options::expandDefinitions() ? smtEngine->expandDefinitions(*i) : *i);
Node value = Node::fromExpr(smtEngine->getValue(*i));
- if(value.getType().isInteger() && request.getType() == nm->realType()) {
+ if (value.getType().isInteger() && request.getType() == nm->realType())
+ {
// Need to wrap in special marker so that output printers know this
// is an integer-looking constant that really should be output as
// a rational. Necessary for SMT-LIB standards compliance, but ugly.
value = nm->mkNode(kind::APPLY_TYPE_ASCRIPTION,
- nm->mkConst(AscriptionType(em->realType())), value);
+ nm->mkConst(AscriptionType(em->realType())),
+ value);
}
result.push_back(nm->mkNode(kind::SEXPR, request, value).toExpr());
}
d_result = em->mkExpr(kind::SEXPR, result);
d_commandStatus = CommandSuccess::instance();
- } catch (RecoverableModalException& e) {
+ }
+ catch (RecoverableModalException& e)
+ {
d_commandStatus = new CommandRecoverableFailure(e.what());
- } catch(UnsafeInterruptException& e) {
+ }
+ catch (UnsafeInterruptException& e)
+ {
d_commandStatus = new CommandInterrupted();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Expr GetValueCommand::getResult() const throw() {
- return d_result;
-}
-
-void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+Expr GetValueCommand::getResult() const { return d_result; }
+void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
+ }
+ else
+ {
expr::ExprDag::Scope scope(out, false);
out << d_result << endl;
}
}
-Command* GetValueCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* GetValueCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
vector<Expr> exportedTerms;
- for(std::vector<Expr>::const_iterator i = d_terms.begin(); i != d_terms.end(); ++i) {
+ for (std::vector<Expr>::const_iterator i = d_terms.begin();
+ i != d_terms.end();
+ ++i)
+ {
exportedTerms.push_back((*i).exportTo(exprManager, variableMap));
}
GetValueCommand* c = new GetValueCommand(exportedTerms);
return c;
}
-Command* GetValueCommand::clone() const {
+Command* GetValueCommand::clone() const
+{
GetValueCommand* c = new GetValueCommand(d_terms);
c->d_result = d_result;
return c;
}
-std::string GetValueCommand::getCommandName() const throw() {
- return "get-value";
-}
-
+std::string GetValueCommand::getCommandName() const { return "get-value"; }
/* class GetAssignmentCommand */
-GetAssignmentCommand::GetAssignmentCommand() throw() {
-}
-
-void GetAssignmentCommand::invoke(SmtEngine* smtEngine) {
- try {
+GetAssignmentCommand::GetAssignmentCommand() {}
+void GetAssignmentCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
d_result = smtEngine->getAssignment();
d_commandStatus = CommandSuccess::instance();
- } catch (RecoverableModalException& e) {
+ }
+ catch (RecoverableModalException& e)
+ {
d_commandStatus = new CommandRecoverableFailure(e.what());
- } catch(UnsafeInterruptException& e) {
+ }
+ catch (UnsafeInterruptException& e)
+ {
d_commandStatus = new CommandInterrupted();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-SExpr GetAssignmentCommand::getResult() const throw() {
- return d_result;
-}
-
-void GetAssignmentCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+SExpr GetAssignmentCommand::getResult() const { return d_result; }
+void GetAssignmentCommand::printResult(std::ostream& out,
+ uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
+ }
+ else
+ {
out << d_result << endl;
}
}
-Command* GetAssignmentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* GetAssignmentCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
GetAssignmentCommand* c = new GetAssignmentCommand();
c->d_result = d_result;
return c;
}
-Command* GetAssignmentCommand::clone() const {
+Command* GetAssignmentCommand::clone() const
+{
GetAssignmentCommand* c = new GetAssignmentCommand();
c->d_result = d_result;
return c;
}
-std::string GetAssignmentCommand::getCommandName() const throw() {
+std::string GetAssignmentCommand::getCommandName() const
+{
return "get-assignment";
}
/* class GetModelCommand */
-GetModelCommand::GetModelCommand() throw()
- : d_result(nullptr), d_smtEngine(nullptr) {}
-
-void GetModelCommand::invoke(SmtEngine* smtEngine) {
- try {
+GetModelCommand::GetModelCommand() : d_result(nullptr), d_smtEngine(nullptr) {}
+void GetModelCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
d_result = smtEngine->getModel();
d_smtEngine = smtEngine;
d_commandStatus = CommandSuccess::instance();
- } catch (RecoverableModalException& e) {
+ }
+ catch (RecoverableModalException& e)
+ {
d_commandStatus = new CommandRecoverableFailure(e.what());
- } catch(UnsafeInterruptException& e) {
+ }
+ catch (UnsafeInterruptException& e)
+ {
d_commandStatus = new CommandInterrupted();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
/* Model is private to the library -- for now
-Model* GetModelCommand::getResult() const throw() {
+Model* GetModelCommand::getResult() const {
return d_result;
}
*/
-void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
+ }
+ else
+ {
out << *d_result;
}
}
-Command* GetModelCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* GetModelCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
GetModelCommand* c = new GetModelCommand();
c->d_result = d_result;
c->d_smtEngine = d_smtEngine;
return c;
}
-Command* GetModelCommand::clone() const {
+Command* GetModelCommand::clone() const
+{
GetModelCommand* c = new GetModelCommand();
c->d_result = d_result;
c->d_smtEngine = d_smtEngine;
return c;
}
-std::string GetModelCommand::getCommandName() const throw() {
- return "get-model";
-}
-
+std::string GetModelCommand::getCommandName() const { return "get-model"; }
/* class GetProofCommand */
-GetProofCommand::GetProofCommand() throw()
- : d_smtEngine(nullptr), d_result(nullptr) {}
-
-void GetProofCommand::invoke(SmtEngine* smtEngine) {
- try {
+GetProofCommand::GetProofCommand() : d_smtEngine(nullptr), d_result(nullptr) {}
+void GetProofCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
d_smtEngine = smtEngine;
d_result = &smtEngine->getProof();
d_commandStatus = CommandSuccess::instance();
- } catch (RecoverableModalException& e) {
+ }
+ catch (RecoverableModalException& e)
+ {
d_commandStatus = new CommandRecoverableFailure(e.what());
- } catch(UnsafeInterruptException& e) {
+ }
+ catch (UnsafeInterruptException& e)
+ {
d_commandStatus = new CommandInterrupted();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-const Proof& GetProofCommand::getResult() const throw() { return *d_result; }
-void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+const Proof& GetProofCommand::getResult() const { return *d_result; }
+void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
+ }
+ else
+ {
smt::SmtScope scope(d_smtEngine);
d_result->toStream(out);
}
}
-Command* GetProofCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* GetProofCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
GetProofCommand* c = new GetProofCommand();
c->d_result = d_result;
c->d_smtEngine = d_smtEngine;
return c;
}
-Command* GetProofCommand::clone() const {
+Command* GetProofCommand::clone() const
+{
GetProofCommand* c = new GetProofCommand();
c->d_result = d_result;
c->d_smtEngine = d_smtEngine;
return c;
}
-std::string GetProofCommand::getCommandName() const throw() {
- return "get-proof";
-}
-
+std::string GetProofCommand::getCommandName() const { return "get-proof"; }
/* class GetInstantiationsCommand */
-GetInstantiationsCommand::GetInstantiationsCommand() throw()
- : d_smtEngine(nullptr) {}
-
-void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) {
- try {
+GetInstantiationsCommand::GetInstantiationsCommand() : d_smtEngine(nullptr) {}
+void GetInstantiationsCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
d_smtEngine = smtEngine;
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-//Instantiations* GetInstantiationsCommand::getResult() const throw() {
-// return d_result;
-//}
-
-void GetInstantiationsCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+void GetInstantiationsCommand::printResult(std::ostream& out,
+ uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
+ }
+ else
+ {
d_smtEngine->printInstantiations(out);
}
}
-Command* GetInstantiationsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* GetInstantiationsCommand::exportTo(
+ ExprManager* exprManager, ExprManagerMapCollection& variableMap)
+{
GetInstantiationsCommand* c = new GetInstantiationsCommand();
- //c->d_result = d_result;
+ // c->d_result = d_result;
c->d_smtEngine = d_smtEngine;
return c;
}
-Command* GetInstantiationsCommand::clone() const {
+Command* GetInstantiationsCommand::clone() const
+{
GetInstantiationsCommand* c = new GetInstantiationsCommand();
- //c->d_result = d_result;
+ // c->d_result = d_result;
c->d_smtEngine = d_smtEngine;
return c;
}
-std::string GetInstantiationsCommand::getCommandName() const throw() {
+std::string GetInstantiationsCommand::getCommandName() const
+{
return "get-instantiations";
}
/* class GetSynthSolutionCommand */
-GetSynthSolutionCommand::GetSynthSolutionCommand() throw()
- : d_smtEngine(nullptr) {}
-
-void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) {
- try {
+GetSynthSolutionCommand::GetSynthSolutionCommand() : d_smtEngine(nullptr) {}
+void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
d_smtEngine = smtEngine;
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-void GetSynthSolutionCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+void GetSynthSolutionCommand::printResult(std::ostream& out,
+ uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
+ }
+ else
+ {
d_smtEngine->printSynthSolution(out);
}
}
-Command* GetSynthSolutionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* GetSynthSolutionCommand::exportTo(
+ ExprManager* exprManager, ExprManagerMapCollection& variableMap)
+{
GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
c->d_smtEngine = d_smtEngine;
return c;
}
-Command* GetSynthSolutionCommand::clone() const {
+Command* GetSynthSolutionCommand::clone() const
+{
GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
c->d_smtEngine = d_smtEngine;
return c;
}
-std::string GetSynthSolutionCommand::getCommandName() const throw() {
+std::string GetSynthSolutionCommand::getCommandName() const
+{
return "get-instantiations";
}
/* class GetQuantifierEliminationCommand */
-GetQuantifierEliminationCommand::GetQuantifierEliminationCommand() throw() :
- d_expr() {
-}
-
-GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(const Expr& expr, bool doFull) throw() :
- d_expr(expr), d_doFull(doFull) {
-}
-
-Expr GetQuantifierEliminationCommand::getExpr() const throw() {
- return d_expr;
-}
-bool GetQuantifierEliminationCommand::getDoFull() const throw() {
- return d_doFull;
+GetQuantifierEliminationCommand::GetQuantifierEliminationCommand() : d_expr() {}
+GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(
+ const Expr& expr, bool doFull)
+ : d_expr(expr), d_doFull(doFull)
+{
}
-void GetQuantifierEliminationCommand::invoke(SmtEngine* smtEngine) {
- try {
+Expr GetQuantifierEliminationCommand::getExpr() const { return d_expr; }
+bool GetQuantifierEliminationCommand::getDoFull() const { return d_doFull; }
+void GetQuantifierEliminationCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
d_result = smtEngine->doQuantifierElimination(d_expr, d_doFull);
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Expr GetQuantifierEliminationCommand::getResult() const throw() {
- return d_result;
-}
-
-void GetQuantifierEliminationCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+Expr GetQuantifierEliminationCommand::getResult() const { return d_result; }
+void GetQuantifierEliminationCommand::printResult(std::ostream& out,
+ uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
+ }
+ else
+ {
out << d_result << endl;
}
}
-Command* GetQuantifierEliminationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- GetQuantifierEliminationCommand* c = new GetQuantifierEliminationCommand(d_expr.exportTo(exprManager, variableMap), d_doFull);
+Command* GetQuantifierEliminationCommand::exportTo(
+ ExprManager* exprManager, ExprManagerMapCollection& variableMap)
+{
+ GetQuantifierEliminationCommand* c = new GetQuantifierEliminationCommand(
+ d_expr.exportTo(exprManager, variableMap), d_doFull);
c->d_result = d_result;
return c;
}
-Command* GetQuantifierEliminationCommand::clone() const {
- GetQuantifierEliminationCommand* c = new GetQuantifierEliminationCommand(d_expr, d_doFull);
+Command* GetQuantifierEliminationCommand::clone() const
+{
+ GetQuantifierEliminationCommand* c =
+ new GetQuantifierEliminationCommand(d_expr, d_doFull);
c->d_result = d_result;
return c;
}
-std::string GetQuantifierEliminationCommand::getCommandName() const throw() {
+std::string GetQuantifierEliminationCommand::getCommandName() const
+{
return d_doFull ? "get-qe" : "get-qe-disjunct";
}
/* class GetUnsatCoreCommand */
-GetUnsatCoreCommand::GetUnsatCoreCommand() throw() {
-}
-
-void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) {
- try {
+GetUnsatCoreCommand::GetUnsatCoreCommand() {}
+void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
d_result = smtEngine->getUnsatCore();
d_commandStatus = CommandSuccess::instance();
- } catch (RecoverableModalException& e) {
+ }
+ catch (RecoverableModalException& e)
+ {
d_commandStatus = new CommandRecoverableFailure(e.what());
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+void GetUnsatCoreCommand::printResult(std::ostream& out,
+ uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
+ }
+ else
+ {
d_result.toStream(out);
}
}
-const UnsatCore& GetUnsatCoreCommand::getUnsatCore() const throw() {
+const UnsatCore& GetUnsatCoreCommand::getUnsatCore() const
+{
// of course, this will be empty if the command hasn't been invoked yet
return d_result;
}
-Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
GetUnsatCoreCommand* c = new GetUnsatCoreCommand;
c->d_result = d_result;
return c;
}
-Command* GetUnsatCoreCommand::clone() const {
+Command* GetUnsatCoreCommand::clone() const
+{
GetUnsatCoreCommand* c = new GetUnsatCoreCommand;
c->d_result = d_result;
return c;
}
-std::string GetUnsatCoreCommand::getCommandName() const throw() {
+std::string GetUnsatCoreCommand::getCommandName() const
+{
return "get-unsat-core";
}
/* class GetAssertionsCommand */
-GetAssertionsCommand::GetAssertionsCommand() throw() {
-}
-
-void GetAssertionsCommand::invoke(SmtEngine* smtEngine) {
- try {
+GetAssertionsCommand::GetAssertionsCommand() {}
+void GetAssertionsCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
stringstream ss;
const vector<Expr> v = smtEngine->getAssertions();
ss << "(\n";
- copy( v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n") );
+ copy(v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n"));
ss << ")\n";
d_result = ss.str();
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-std::string GetAssertionsCommand::getResult() const throw() {
- return d_result;
-}
-
-void GetAssertionsCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+std::string GetAssertionsCommand::getResult() const { return d_result; }
+void GetAssertionsCommand::printResult(std::ostream& out,
+ uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else {
+ }
+ else
+ {
out << d_result;
}
}
-Command* GetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* GetAssertionsCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
GetAssertionsCommand* c = new GetAssertionsCommand();
c->d_result = d_result;
return c;
}
-Command* GetAssertionsCommand::clone() const {
+Command* GetAssertionsCommand::clone() const
+{
GetAssertionsCommand* c = new GetAssertionsCommand();
c->d_result = d_result;
return c;
}
-std::string GetAssertionsCommand::getCommandName() const throw() {
+std::string GetAssertionsCommand::getCommandName() const
+{
return "get-assertions";
}
/* class SetBenchmarkStatusCommand */
-SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) throw() :
- d_status(status) {
+SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status)
+ : d_status(status)
+{
}
-BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const throw() {
+BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const
+{
return d_status;
}
-void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) {
- try {
+void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
stringstream ss;
ss << d_status;
SExpr status = SExpr(ss.str());
smtEngine->setInfo("status", status);
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Command* SetBenchmarkStatusCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* SetBenchmarkStatusCommand::exportTo(
+ ExprManager* exprManager, ExprManagerMapCollection& variableMap)
+{
return new SetBenchmarkStatusCommand(d_status);
}
-Command* SetBenchmarkStatusCommand::clone() const {
+Command* SetBenchmarkStatusCommand::clone() const
+{
return new SetBenchmarkStatusCommand(d_status);
}
-std::string SetBenchmarkStatusCommand::getCommandName() const throw() {
+std::string SetBenchmarkStatusCommand::getCommandName() const
+{
return "set-info";
}
/* class SetBenchmarkLogicCommand */
-SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) throw() :
- d_logic(logic) {
-}
-
-std::string SetBenchmarkLogicCommand::getLogic() const throw() {
- return d_logic;
+SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic)
+ : d_logic(logic)
+{
}
-void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) {
- try {
+std::string SetBenchmarkLogicCommand::getLogic() const { return d_logic; }
+void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
smtEngine->setLogic(d_logic);
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Command* SetBenchmarkLogicCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* SetBenchmarkLogicCommand::exportTo(
+ ExprManager* exprManager, ExprManagerMapCollection& variableMap)
+{
return new SetBenchmarkLogicCommand(d_logic);
}
-Command* SetBenchmarkLogicCommand::clone() const {
+Command* SetBenchmarkLogicCommand::clone() const
+{
return new SetBenchmarkLogicCommand(d_logic);
}
-std::string SetBenchmarkLogicCommand::getCommandName() const throw() {
+std::string SetBenchmarkLogicCommand::getCommandName() const
+{
return "set-logic";
}
/* class SetInfoCommand */
-SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) throw() :
- d_flag(flag),
- d_sexpr(sexpr) {
-}
-
-std::string SetInfoCommand::getFlag() const throw() {
- return d_flag;
-}
-
-SExpr SetInfoCommand::getSExpr() const throw() {
- return d_sexpr;
+SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr)
+ : d_flag(flag), d_sexpr(sexpr)
+{
}
-void SetInfoCommand::invoke(SmtEngine* smtEngine) {
- try {
+std::string SetInfoCommand::getFlag() const { return d_flag; }
+SExpr SetInfoCommand::getSExpr() const { return d_sexpr; }
+void SetInfoCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
smtEngine->setInfo(d_flag, d_sexpr);
d_commandStatus = CommandSuccess::instance();
- } catch(UnrecognizedOptionException&) {
+ }
+ catch (UnrecognizedOptionException&)
+ {
// As per SMT-LIB spec, silently accept unknown set-info keys
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Command* SetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* SetInfoCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
return new SetInfoCommand(d_flag, d_sexpr);
}
-Command* SetInfoCommand::clone() const {
+Command* SetInfoCommand::clone() const
+{
return new SetInfoCommand(d_flag, d_sexpr);
}
-std::string SetInfoCommand::getCommandName() const throw() {
- return "set-info";
-}
-
+std::string SetInfoCommand::getCommandName() const { return "set-info"; }
/* class GetInfoCommand */
-GetInfoCommand::GetInfoCommand(std::string flag) throw() :
- d_flag(flag) {
-}
-
-std::string GetInfoCommand::getFlag() const throw() {
- return d_flag;
-}
-
-void GetInfoCommand::invoke(SmtEngine* smtEngine) {
- try {
+GetInfoCommand::GetInfoCommand(std::string flag) : d_flag(flag) {}
+std::string GetInfoCommand::getFlag() const { return d_flag; }
+void GetInfoCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
vector<SExpr> v;
v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
v.push_back(smtEngine->getInfo(d_flag));
stringstream ss;
- if(d_flag == "all-options" || d_flag == "all-statistics") {
+ if (d_flag == "all-options" || d_flag == "all-statistics")
+ {
ss << PrettySExprs(true);
}
ss << SExpr(v);
d_result = ss.str();
d_commandStatus = CommandSuccess::instance();
- } catch(UnrecognizedOptionException&) {
+ }
+ catch (UnrecognizedOptionException&)
+ {
d_commandStatus = new CommandUnsupported();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-std::string GetInfoCommand::getResult() const throw() {
- return d_result;
-}
-
-void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+std::string GetInfoCommand::getResult() const { return d_result; }
+void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else if(d_result != "") {
+ }
+ else if (d_result != "")
+ {
out << d_result << endl;
}
}
-Command* GetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* GetInfoCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
GetInfoCommand* c = new GetInfoCommand(d_flag);
c->d_result = d_result;
return c;
}
-Command* GetInfoCommand::clone() const {
+Command* GetInfoCommand::clone() const
+{
GetInfoCommand* c = new GetInfoCommand(d_flag);
c->d_result = d_result;
return c;
}
-std::string GetInfoCommand::getCommandName() const throw() {
- return "get-info";
-}
-
+std::string GetInfoCommand::getCommandName() const { return "get-info"; }
/* class SetOptionCommand */
-SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) throw() :
- d_flag(flag),
- d_sexpr(sexpr) {
-}
-
-std::string SetOptionCommand::getFlag() const throw() {
- return d_flag;
-}
-
-SExpr SetOptionCommand::getSExpr() const throw() {
- return d_sexpr;
+SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr)
+ : d_flag(flag), d_sexpr(sexpr)
+{
}
-void SetOptionCommand::invoke(SmtEngine* smtEngine) {
- try {
+std::string SetOptionCommand::getFlag() const { return d_flag; }
+SExpr SetOptionCommand::getSExpr() const { return d_sexpr; }
+void SetOptionCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
smtEngine->setOption(d_flag, d_sexpr);
d_commandStatus = CommandSuccess::instance();
- } catch(UnrecognizedOptionException&) {
+ }
+ catch (UnrecognizedOptionException&)
+ {
d_commandStatus = new CommandUnsupported();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Command* SetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* SetOptionCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
return new SetOptionCommand(d_flag, d_sexpr);
}
-Command* SetOptionCommand::clone() const {
+Command* SetOptionCommand::clone() const
+{
return new SetOptionCommand(d_flag, d_sexpr);
}
-std::string SetOptionCommand::getCommandName() const throw() {
- return "set-option";
-}
-
+std::string SetOptionCommand::getCommandName() const { return "set-option"; }
/* class GetOptionCommand */
-GetOptionCommand::GetOptionCommand(std::string flag) throw() :
- d_flag(flag) {
-}
-
-std::string GetOptionCommand::getFlag() const throw() {
- return d_flag;
-}
-
-void GetOptionCommand::invoke(SmtEngine* smtEngine) {
- try {
+GetOptionCommand::GetOptionCommand(std::string flag) : d_flag(flag) {}
+std::string GetOptionCommand::getFlag() const { return d_flag; }
+void GetOptionCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
SExpr res = smtEngine->getOption(d_flag);
d_result = res.toString();
d_commandStatus = CommandSuccess::instance();
- } catch(UnrecognizedOptionException&) {
+ }
+ catch (UnrecognizedOptionException&)
+ {
d_commandStatus = new CommandUnsupported();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-std::string GetOptionCommand::getResult() const throw() {
- return d_result;
-}
-
-void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const {
- if(! ok()) {
+std::string GetOptionCommand::getResult() const { return d_result; }
+void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const
+{
+ if (!ok())
+ {
this->Command::printResult(out, verbosity);
- } else if(d_result != "") {
+ }
+ else if (d_result != "")
+ {
out << d_result << endl;
}
}
-Command* GetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* GetOptionCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
GetOptionCommand* c = new GetOptionCommand(d_flag);
c->d_result = d_result;
return c;
}
-Command* GetOptionCommand::clone() const {
+Command* GetOptionCommand::clone() const
+{
GetOptionCommand* c = new GetOptionCommand(d_flag);
c->d_result = d_result;
return c;
}
-std::string GetOptionCommand::getCommandName() const throw() {
- return "get-option";
-}
-
-
+std::string GetOptionCommand::getCommandName() const { return "get-option"; }
/* class SetExpressionNameCommand */
-SetExpressionNameCommand::SetExpressionNameCommand(Expr expr, std::string name) throw() :
-d_expr(expr), d_name(name) {
-
+SetExpressionNameCommand::SetExpressionNameCommand(Expr expr, std::string name)
+ : d_expr(expr), d_name(name)
+{
}
-void SetExpressionNameCommand::invoke(SmtEngine* smtEngine) {
+void SetExpressionNameCommand::invoke(SmtEngine* smtEngine)
+{
smtEngine->setExpressionName(d_expr, d_name);
d_commandStatus = CommandSuccess::instance();
}
-Command* SetExpressionNameCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- SetExpressionNameCommand* c = new SetExpressionNameCommand(d_expr.exportTo(exprManager, variableMap), d_name);
+Command* SetExpressionNameCommand::exportTo(
+ ExprManager* exprManager, ExprManagerMapCollection& variableMap)
+{
+ SetExpressionNameCommand* c = new SetExpressionNameCommand(
+ d_expr.exportTo(exprManager, variableMap), d_name);
return c;
}
-Command* SetExpressionNameCommand::clone() const {
+Command* SetExpressionNameCommand::clone() const
+{
SetExpressionNameCommand* c = new SetExpressionNameCommand(d_expr, d_name);
return c;
}
-std::string SetExpressionNameCommand::getCommandName() const throw() {
+std::string SetExpressionNameCommand::getCommandName() const
+{
return "set-expr-name";
}
/* class DatatypeDeclarationCommand */
-DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() :
- d_datatypes() {
+DatatypeDeclarationCommand::DatatypeDeclarationCommand(
+ const DatatypeType& datatype)
+ : d_datatypes()
+{
d_datatypes.push_back(datatype);
}
-DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw() :
- d_datatypes(datatypes) {
+DatatypeDeclarationCommand::DatatypeDeclarationCommand(
+ const std::vector<DatatypeType>& datatypes)
+ : d_datatypes(datatypes)
+{
}
-const std::vector<DatatypeType>&
-DatatypeDeclarationCommand::getDatatypes() const throw() {
+const std::vector<DatatypeType>& DatatypeDeclarationCommand::getDatatypes()
+ const
+{
return d_datatypes;
}
-void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) {
+void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine)
+{
d_commandStatus = CommandSuccess::instance();
}
-Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- throw ExportUnsupportedException
- ("export of DatatypeDeclarationCommand unsupported");
+Command* DatatypeDeclarationCommand::exportTo(
+ ExprManager* exprManager, ExprManagerMapCollection& variableMap)
+{
+ throw ExportUnsupportedException(
+ "export of DatatypeDeclarationCommand unsupported");
}
-Command* DatatypeDeclarationCommand::clone() const {
+Command* DatatypeDeclarationCommand::clone() const
+{
return new DatatypeDeclarationCommand(d_datatypes);
}
-std::string DatatypeDeclarationCommand::getCommandName() const throw() {
+std::string DatatypeDeclarationCommand::getCommandName() const
+{
return "declare-datatypes";
}
RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars,
const std::vector<Expr>& guards,
- Expr head, Expr body,
- const Triggers& triggers) throw() :
- d_vars(vars), d_guards(guards), d_head(head), d_body(body), d_triggers(triggers) {
+ Expr head,
+ Expr body,
+ const Triggers& triggers)
+ : d_vars(vars),
+ d_guards(guards),
+ d_head(head),
+ d_body(body),
+ d_triggers(triggers)
+{
}
RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars,
- Expr head, Expr body) throw() :
- d_vars(vars), d_head(head), d_body(body) {
-}
-
-const std::vector<Expr>& RewriteRuleCommand::getVars() const throw() {
- return d_vars;
+ Expr head,
+ Expr body)
+ : d_vars(vars), d_head(head), d_body(body)
+{
}
-const std::vector<Expr>& RewriteRuleCommand::getGuards() const throw() {
+const std::vector<Expr>& RewriteRuleCommand::getVars() const { return d_vars; }
+const std::vector<Expr>& RewriteRuleCommand::getGuards() const
+{
return d_guards;
}
-Expr RewriteRuleCommand::getHead() const throw() {
- return d_head;
-}
-
-Expr RewriteRuleCommand::getBody() const throw() {
- return d_body;
-}
-
-const RewriteRuleCommand::Triggers& RewriteRuleCommand::getTriggers() const throw() {
+Expr RewriteRuleCommand::getHead() const { return d_head; }
+Expr RewriteRuleCommand::getBody() const { return d_body; }
+const RewriteRuleCommand::Triggers& RewriteRuleCommand::getTriggers() const
+{
return d_triggers;
}
-void RewriteRuleCommand::invoke(SmtEngine* smtEngine) {
- try {
+void RewriteRuleCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
ExprManager* em = smtEngine->getExprManager();
/** build vars list */
Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars);
/** build guards list */
Expr guards;
- if(d_guards.size() == 0) guards = em->mkConst<bool>(true);
- else if(d_guards.size() == 1) guards = d_guards[0];
- else guards = em->mkExpr(kind::AND,d_guards);
+ if (d_guards.size() == 0)
+ guards = em->mkConst<bool>(true);
+ else if (d_guards.size() == 1)
+ guards = d_guards[0];
+ else
+ guards = em->mkExpr(kind::AND, d_guards);
/** build expression */
Expr expr;
- if( d_triggers.empty() ){
- expr = em->mkExpr(kind::RR_REWRITE,vars,guards,d_head,d_body);
- } else {
+ if (d_triggers.empty())
+ {
+ expr = em->mkExpr(kind::RR_REWRITE, vars, guards, d_head, d_body);
+ }
+ else
+ {
/** build triggers list */
std::vector<Expr> vtriggers;
vtriggers.reserve(d_triggers.size());
- for(Triggers::const_iterator i = d_triggers.begin(),
- end = d_triggers.end(); i != end; ++i){
- vtriggers.push_back(em->mkExpr(kind::INST_PATTERN,*i));
+ for (Triggers::const_iterator i = d_triggers.begin(),
+ end = d_triggers.end();
+ i != end;
+ ++i)
+ {
+ vtriggers.push_back(em->mkExpr(kind::INST_PATTERN, *i));
}
- Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST,vtriggers);
- expr = em->mkExpr(kind::RR_REWRITE,vars,guards,d_head,d_body,triggers);
+ Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST, vtriggers);
+ expr =
+ em->mkExpr(kind::RR_REWRITE, vars, guards, d_head, d_body, triggers);
}
smtEngine->assertFormula(expr);
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Command* RewriteRuleCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* RewriteRuleCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
/** Convert variables */
VExpr vars = ExportTo(exprManager, variableMap, d_vars);
/** Convert guards */
/** Convert triggers */
Triggers triggers;
triggers.reserve(d_triggers.size());
- for (const std::vector<Expr>& trigger_list : d_triggers) {
+ for (const std::vector<Expr>& trigger_list : d_triggers)
+ {
triggers.push_back(ExportTo(exprManager, variableMap, trigger_list));
}
/** Convert head and body */
return new RewriteRuleCommand(vars, guards, head, body, triggers);
}
-Command* RewriteRuleCommand::clone() const {
+Command* RewriteRuleCommand::clone() const
+{
return new RewriteRuleCommand(d_vars, d_guards, d_head, d_body, d_triggers);
}
-std::string RewriteRuleCommand::getCommandName() const throw() {
+std::string RewriteRuleCommand::getCommandName() const
+{
return "rewrite-rule";
}
const std::vector<Expr>& heads,
Expr body,
const Triggers& triggers,
- bool deduction) throw() :
- d_vars(vars), d_guards(guards), d_heads(heads), d_body(body), d_triggers(triggers), d_deduction(deduction) {
+ bool deduction)
+ : d_vars(vars),
+ d_guards(guards),
+ d_heads(heads),
+ d_body(body),
+ d_triggers(triggers),
+ d_deduction(deduction)
+{
}
PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars,
const std::vector<Expr>& heads,
Expr body,
- bool deduction) throw() :
- d_vars(vars), d_heads(heads), d_body(body), d_deduction(deduction) {
+ bool deduction)
+ : d_vars(vars), d_heads(heads), d_body(body), d_deduction(deduction)
+{
}
-const std::vector<Expr>& PropagateRuleCommand::getVars() const throw() {
+const std::vector<Expr>& PropagateRuleCommand::getVars() const
+{
return d_vars;
}
-const std::vector<Expr>& PropagateRuleCommand::getGuards() const throw() {
+const std::vector<Expr>& PropagateRuleCommand::getGuards() const
+{
return d_guards;
}
-const std::vector<Expr>& PropagateRuleCommand::getHeads() const throw() {
+const std::vector<Expr>& PropagateRuleCommand::getHeads() const
+{
return d_heads;
}
-Expr PropagateRuleCommand::getBody() const throw() {
- return d_body;
-}
-
-const PropagateRuleCommand::Triggers& PropagateRuleCommand::getTriggers() const throw() {
+Expr PropagateRuleCommand::getBody() const { return d_body; }
+const PropagateRuleCommand::Triggers& PropagateRuleCommand::getTriggers() const
+{
return d_triggers;
}
-bool PropagateRuleCommand::isDeduction() const throw() {
- return d_deduction;
-}
-
-void PropagateRuleCommand::invoke(SmtEngine* smtEngine) {
- try {
+bool PropagateRuleCommand::isDeduction() const { return d_deduction; }
+void PropagateRuleCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
ExprManager* em = smtEngine->getExprManager();
/** build vars list */
Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars);
/** build guards list */
Expr guards;
- if(d_guards.size() == 0) guards = em->mkConst<bool>(true);
- else if(d_guards.size() == 1) guards = d_guards[0];
- else guards = em->mkExpr(kind::AND,d_guards);
+ if (d_guards.size() == 0)
+ guards = em->mkConst<bool>(true);
+ else if (d_guards.size() == 1)
+ guards = d_guards[0];
+ else
+ guards = em->mkExpr(kind::AND, d_guards);
/** build heads list */
Expr heads;
- if(d_heads.size() == 1) heads = d_heads[0];
- else heads = em->mkExpr(kind::AND,d_heads);
+ if (d_heads.size() == 1)
+ heads = d_heads[0];
+ else
+ heads = em->mkExpr(kind::AND, d_heads);
/** build expression */
Expr expr;
- if( d_triggers.empty() ){
- expr = em->mkExpr(kind::RR_REWRITE,vars,guards,heads,d_body);
- } else {
+ if (d_triggers.empty())
+ {
+ expr = em->mkExpr(kind::RR_REWRITE, vars, guards, heads, d_body);
+ }
+ else
+ {
/** build triggers list */
std::vector<Expr> vtriggers;
vtriggers.reserve(d_triggers.size());
- for(Triggers::const_iterator i = d_triggers.begin(),
- end = d_triggers.end(); i != end; ++i){
- vtriggers.push_back(em->mkExpr(kind::INST_PATTERN,*i));
+ for (Triggers::const_iterator i = d_triggers.begin(),
+ end = d_triggers.end();
+ i != end;
+ ++i)
+ {
+ vtriggers.push_back(em->mkExpr(kind::INST_PATTERN, *i));
}
- Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST,vtriggers);
- expr = em->mkExpr(kind::RR_REWRITE,vars,guards,heads,d_body,triggers);
+ Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST, vtriggers);
+ expr =
+ em->mkExpr(kind::RR_REWRITE, vars, guards, heads, d_body, triggers);
}
smtEngine->assertFormula(expr);
d_commandStatus = CommandSuccess::instance();
- } catch(exception& e) {
+ }
+ catch (exception& e)
+ {
d_commandStatus = new CommandFailure(e.what());
}
}
-Command* PropagateRuleCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+Command* PropagateRuleCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
/** Convert variables */
VExpr vars = ExportTo(exprManager, variableMap, d_vars);
/** Convert guards */
/** Convert triggers */
Triggers triggers;
triggers.reserve(d_triggers.size());
- for (const std::vector<Expr>& trigger_list : d_triggers) {
+ for (const std::vector<Expr>& trigger_list : d_triggers)
+ {
triggers.push_back(ExportTo(exprManager, variableMap, trigger_list));
}
/** Convert head and body */
return new PropagateRuleCommand(vars, guards, heads, body, triggers);
}
-Command* PropagateRuleCommand::clone() const {
- return new PropagateRuleCommand(d_vars, d_guards, d_heads, d_body, d_triggers);
+Command* PropagateRuleCommand::clone() const
+{
+ return new PropagateRuleCommand(
+ d_vars, d_guards, d_heads, d_body, d_triggers);
}
-std::string PropagateRuleCommand::getCommandName() const throw() {
+std::string PropagateRuleCommand::getCommandName() const
+{
return "propagate-rule";
}
/* output stream insertion operator for benchmark statuses */
-std::ostream& operator<<(std::ostream& out,
- BenchmarkStatus status) throw() {
- switch(status) {
-
- case SMT_SATISFIABLE:
- return out << "sat";
+std::ostream& operator<<(std::ostream& out, BenchmarkStatus status)
+{
+ switch (status)
+ {
+ case SMT_SATISFIABLE: return out << "sat";
- case SMT_UNSATISFIABLE:
- return out << "unsat";
+ case SMT_UNSATISFIABLE: return out << "unsat";
- case SMT_UNKNOWN:
- return out << "unknown";
+ case SMT_UNKNOWN: return out << "unknown";
- default:
- return out << "BenchmarkStatus::[UNKNOWNSTATUS!]";
+ default: return out << "BenchmarkStatus::[UNKNOWNSTATUS!]";
}
}
-}/* CVC4 namespace */
+} /* CVC4 namespace */
class CommandStatus;
class Model;
-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;
+std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, const CommandStatus&) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, const CommandStatus*) CVC4_PUBLIC;
/** The status an SMT benchmark can have */
-enum BenchmarkStatus {
+enum BenchmarkStatus
+{
/** Benchmark is satisfiable */
SMT_SATISFIABLE,
/** Benchmark is unsatisfiable */
SMT_UNSATISFIABLE,
/** The status of the benchmark is unknown */
SMT_UNKNOWN
-};/* enum BenchmarkStatus */
+}; /* enum BenchmarkStatus */
-std::ostream& operator<<(std::ostream& out,
- BenchmarkStatus status) throw() CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) CVC4_PUBLIC;
/**
* IOStream manipulator to print success messages or not.
* 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.
- */
+class CVC4_PUBLIC CommandPrintSuccess
+{
+ public:
+ /** Construct a CommandPrintSuccess with the given setting. */
+ CommandPrintSuccess(bool printSuccess) : d_printSuccess(printSuccess) {}
+ void applyPrintSuccess(std::ostream& out);
+ static bool getPrintSuccess(std::ostream& out);
+ static void setPrintSuccess(std::ostream& out, bool printSuccess);
+
+ private:
+ /** 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.
+ * 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.
- */
+ /** 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 */
+}; /* class CommandPrintSuccess */
/**
* Sets the default print-success setting when pretty-printing an Expr
*
* 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:
+std::ostream& operator<<(std::ostream& out,
+ CommandPrintSuccess cps) CVC4_PUBLIC;
+
+class CVC4_PUBLIC CommandStatus
+{
+ protected:
// shouldn't construct a CommandStatus (use a derived class)
- CommandStatus() throw() {}
-public:
- virtual ~CommandStatus() throw() {}
+ CommandStatus() {}
+ public:
+ virtual ~CommandStatus() {}
void toStream(std::ostream& out,
- OutputLanguage language = language::output::LANG_AUTO) const throw();
+ OutputLanguage language = language::output::LANG_AUTO) const;
virtual CommandStatus& clone() const = 0;
-};/* class CommandStatus */
+}; /* class CommandStatus */
-class CVC4_PUBLIC CommandSuccess : public CommandStatus {
+class CVC4_PUBLIC CommandSuccess : public CommandStatus
+{
static const CommandSuccess* s_instance;
-public:
- static const CommandSuccess* instance() throw() { return s_instance; }
- CommandStatus& clone() const { return const_cast<CommandSuccess&>(*this); }
-};/* class CommandSuccess */
-class CVC4_PUBLIC CommandInterrupted : public CommandStatus {
+ public:
+ static const CommandSuccess* instance() { return s_instance; }
+ CommandStatus& clone() const override
+ {
+ return const_cast<CommandSuccess&>(*this);
+ }
+}; /* class CommandSuccess */
+
+class CVC4_PUBLIC CommandInterrupted : public CommandStatus
+{
static const CommandInterrupted* s_instance;
-public:
- static const CommandInterrupted* instance() throw() { return s_instance; }
- CommandStatus& clone() const { return const_cast<CommandInterrupted&>(*this); }
-};/* class CommandInterrupted */
-class CVC4_PUBLIC CommandUnsupported : public CommandStatus {
-public:
- CommandStatus& clone() const { return *new CommandUnsupported(*this); }
-};/* class CommandSuccess */
+ public:
+ static const CommandInterrupted* instance() { return s_instance; }
+ CommandStatus& clone() const override
+ {
+ return const_cast<CommandInterrupted&>(*this);
+ }
+}; /* class CommandInterrupted */
-class CVC4_PUBLIC CommandFailure : public CommandStatus {
+class CVC4_PUBLIC CommandUnsupported : public CommandStatus
+{
+ public:
+ CommandStatus& clone() const override
+ {
+ return *new CommandUnsupported(*this);
+ }
+}; /* class CommandSuccess */
+
+class CVC4_PUBLIC CommandFailure : public CommandStatus
+{
std::string d_message;
-public:
- CommandFailure(std::string message) throw() : d_message(message) {}
- CommandFailure& clone() const { return *new CommandFailure(*this); }
- ~CommandFailure() throw() {}
- std::string getMessage() const throw() { return d_message; }
-};/* class CommandFailure */
+
+ public:
+ CommandFailure(std::string message) : d_message(message) {}
+ CommandFailure& clone() const override { return *new CommandFailure(*this); }
+ std::string getMessage() const { return d_message; }
+}; /* class CommandFailure */
/**
* The execution of the command resulted in a non-fatal error and further
* for an unsat core in a place that is not immediately preceded by an
* unsat/valid response.
*/
-class CVC4_PUBLIC CommandRecoverableFailure : public CommandStatus {
+class CVC4_PUBLIC CommandRecoverableFailure : public CommandStatus
+{
std::string d_message;
public:
- CommandRecoverableFailure(std::string message) throw() : d_message(message) {}
- CommandRecoverableFailure& clone() const {
+ CommandRecoverableFailure(std::string message) : d_message(message) {}
+ CommandRecoverableFailure& clone() const override
+ {
return *new CommandRecoverableFailure(*this);
}
- ~CommandRecoverableFailure() throw() {}
- std::string getMessage() const throw() { return d_message; }
+ std::string getMessage() const { return d_message; }
}; /* class CommandRecoverableFailure */
-class CVC4_PUBLIC Command {
-protected:
+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
*/
bool d_muted;
-public:
+ public:
typedef CommandPrintSuccess printsuccess;
- Command() throw();
+ Command();
Command(const Command& cmd);
- virtual ~Command() throw();
+ virtual ~Command();
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();
+ void toStream(std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const;
- std::string toString() const throw();
+ std::string toString() const;
- virtual std::string getCommandName() const throw() = 0;
+ virtual std::string getCommandName() const = 0;
/**
* If false, instruct this Command not to print a success message.
*/
- void setMuted(bool muted) throw() { d_muted = muted; }
-
+ void setMuted(bool muted) { d_muted = muted; }
/**
* Determine whether this Command will print a success message.
*/
- bool isMuted() throw() { return d_muted; }
-
+ bool isMuted() { return d_muted; }
/**
* Either the command hasn't run yet, or it completed successfully
* (CommandSuccess, not CommandUnsupported or CommandFailure).
*/
- bool ok() const throw();
+ bool ok() const;
/**
* The command completed in a failure state (CommandFailure, not
* CommandSuccess or CommandUnsupported).
*/
- bool fail() const throw();
+ bool fail() const;
/**
* The command was ran but was interrupted due to resource limiting.
*/
- bool interrupted() const throw();
+ bool interrupted() const;
/** Get the command status (it's NULL if we haven't run yet). */
- const CommandStatus* getCommandStatus() const throw() { return d_commandStatus; }
-
+ const CommandStatus* getCommandStatus() const { return d_commandStatus; }
virtual void printResult(std::ostream& out, uint32_t verbosity = 2) const;
/**
*/
virtual Command* clone() const = 0;
-protected:
- class ExportTransformer {
+ protected:
+ class ExportTransformer
+ {
ExprManager* d_exprManager;
ExprManagerMapCollection& d_variableMap;
- public:
- ExportTransformer(ExprManager* exprManager, ExprManagerMapCollection& variableMap) :
- d_exprManager(exprManager),
- d_variableMap(variableMap) {
- }
- Expr operator()(Expr e) {
- return e.exportTo(d_exprManager, d_variableMap);
- }
- Type operator()(Type t) {
- return t.exportTo(d_exprManager, d_variableMap);
+
+ public:
+ ExportTransformer(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+ : d_exprManager(exprManager), d_variableMap(variableMap)
+ {
}
- };/* class Command::ExportTransformer */
-};/* class Command */
+ Expr operator()(Expr e) { return e.exportTo(d_exprManager, d_variableMap); }
+ Type operator()(Type t) { return t.exportTo(d_exprManager, d_variableMap); }
+ }; /* class Command::ExportTransformer */
+}; /* class Command */
/**
* EmptyCommands are the residue of a command after the parser handles
* them (and there's nothing left to do).
*/
-class CVC4_PUBLIC EmptyCommand : public Command {
-protected:
+class CVC4_PUBLIC EmptyCommand : public Command
+{
+ public:
+ EmptyCommand(std::string name = "");
+ std::string getName() const;
+ void invoke(SmtEngine* smtEngine) override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+
+ protected:
std::string d_name;
-public:
- EmptyCommand(std::string name = "") throw();
- ~EmptyCommand() throw() {}
- std::string getName() const throw();
- void invoke(SmtEngine* smtEngine);
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class EmptyCommand */
-
-class CVC4_PUBLIC EchoCommand : public Command {
-protected:
+}; /* class EmptyCommand */
+
+class CVC4_PUBLIC EchoCommand : public Command
+{
+ public:
+ EchoCommand(std::string output = "");
+
+ std::string getOutput() const;
+
+ void invoke(SmtEngine* smtEngine) override;
+ void invoke(SmtEngine* smtEngine, std::ostream& out) override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+
+ protected:
std::string d_output;
-public:
- EchoCommand(std::string output = "") throw();
- ~EchoCommand() throw() {}
- std::string getOutput() const 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();
-};/* class EchoCommand */
-
-class CVC4_PUBLIC AssertCommand : public Command {
-protected:
+}; /* class EchoCommand */
+
+class CVC4_PUBLIC AssertCommand : public Command
+{
+ protected:
Expr d_expr;
bool d_inUnsatCore;
-public:
- AssertCommand(const Expr& e, bool inUnsatCore = true) throw();
- ~AssertCommand() throw() {}
- Expr getExpr() const throw();
- void invoke(SmtEngine* smtEngine);
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class AssertCommand */
-
-class CVC4_PUBLIC PushCommand : public Command {
-public:
- ~PushCommand() throw() {}
- void invoke(SmtEngine* smtEngine);
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class PushCommand */
-
-class CVC4_PUBLIC PopCommand : public Command {
-public:
- ~PopCommand() throw() {}
- void invoke(SmtEngine* smtEngine);
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class PopCommand */
-
-class CVC4_PUBLIC DeclarationDefinitionCommand : public Command {
-protected:
+
+ public:
+ AssertCommand(const Expr& e, bool inUnsatCore = true);
+
+ Expr getExpr() const;
+
+ void invoke(SmtEngine* smtEngine) override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class AssertCommand */
+
+class CVC4_PUBLIC PushCommand : public Command
+{
+ public:
+ void invoke(SmtEngine* smtEngine) override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class PushCommand */
+
+class CVC4_PUBLIC PopCommand : public Command
+{
+ public:
+ void invoke(SmtEngine* smtEngine) override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class PopCommand */
+
+class CVC4_PUBLIC DeclarationDefinitionCommand : public Command
+{
+ protected:
std::string d_symbol;
-public:
- DeclarationDefinitionCommand(const std::string& id) throw();
- ~DeclarationDefinitionCommand() throw() {}
- virtual void invoke(SmtEngine* smtEngine) = 0;
- std::string getSymbol() const throw();
-};/* class DeclarationDefinitionCommand */
-class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand {
-protected:
+ public:
+ DeclarationDefinitionCommand(const std::string& id);
+
+ void invoke(SmtEngine* smtEngine) override = 0;
+ std::string getSymbol() const;
+}; /* class DeclarationDefinitionCommand */
+
+class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand
+{
+ protected:
Expr d_func;
Type d_type;
bool d_printInModel;
bool d_printInModelSetByUser;
-public:
- DeclareFunctionCommand(const std::string& id, Expr func, Type type) throw();
- ~DeclareFunctionCommand() throw() {}
- Expr getFunction() const throw();
- Type getType() const throw();
- bool getPrintInModel() const throw();
- bool getPrintInModelSetByUser() const throw();
- void setPrintInModel( bool p );
- void invoke(SmtEngine* smtEngine);
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class DeclareFunctionCommand */
-
-class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand {
-protected:
+
+ public:
+ DeclareFunctionCommand(const std::string& id, Expr func, Type type);
+ Expr getFunction() const;
+ Type getType() const;
+ bool getPrintInModel() const;
+ bool getPrintInModelSetByUser() const;
+ void setPrintInModel(bool p);
+
+ void invoke(SmtEngine* smtEngine) override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class DeclareFunctionCommand */
+
+class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand
+{
+ protected:
size_t d_arity;
Type d_type;
-public:
- 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);
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class DeclareTypeCommand */
-
-class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand {
-protected:
+
+ public:
+ DeclareTypeCommand(const std::string& id, size_t arity, Type t);
+
+ size_t getArity() const;
+ Type getType() const;
+
+ void invoke(SmtEngine* smtEngine) override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class DeclareTypeCommand */
+
+class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand
+{
+ protected:
std::vector<Type> d_params;
Type d_type;
-public:
- 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);
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class DefineTypeCommand */
-
-class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand {
-protected:
+
+ 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) override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class DefineTypeCommand */
+
+class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand
+{
+ protected:
Expr d_func;
std::vector<Expr> d_formals;
Expr d_formula;
-public:
- DefineFunctionCommand(const std::string& id, Expr func, Expr formula) throw();
- DefineFunctionCommand(const std::string& id, Expr func,
- 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);
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class DefineFunctionCommand */
+
+ public:
+ DefineFunctionCommand(const std::string& id, Expr func, Expr formula);
+ 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) override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class DefineFunctionCommand */
/**
* This differs from DefineFunctionCommand only in that it instructs
* the SmtEngine to "remember" this function for later retrieval with
* getAssignment(). Used for :named attributes in SMT-LIBv2.
*/
-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);
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
-};/* class DefineNamedFunctionCommand */
+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) override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+}; /* class DefineNamedFunctionCommand */
/**
* The command when parsing define-fun-rec or define-funs-rec.
public:
DefineFunctionRecCommand(Expr func,
const std::vector<Expr>& formals,
- Expr formula) throw();
+ Expr formula);
DefineFunctionRecCommand(const std::vector<Expr>& funcs,
const std::vector<std::vector<Expr> >& formals,
- const std::vector<Expr>& formula) throw();
- ~DefineFunctionRecCommand() throw() {}
- const std::vector<Expr>& getFunctions() const throw();
- const std::vector<std::vector<Expr> >& getFormals() const throw();
- const std::vector<Expr>& getFormulas() const throw();
+ const std::vector<Expr>& formula);
+
+ const std::vector<Expr>& getFunctions() const;
+ const std::vector<std::vector<Expr> >& getFormals() const;
+ const std::vector<Expr>& getFormulas() const;
+
void invoke(SmtEngine* smtEngine) override;
Command* exportTo(ExprManager* exprManager,
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
- std::string getCommandName() const throw() override;
+ std::string getCommandName() const override;
protected:
/** functions we are defining */
* The command when an attribute is set by a user. In SMT-LIBv2 this is done
* via the syntax (! expr :attr)
*/
-class CVC4_PUBLIC SetUserAttributeCommand : public Command {
+class CVC4_PUBLIC SetUserAttributeCommand : public Command
+{
public:
- SetUserAttributeCommand(const std::string& attr, Expr expr) throw();
- SetUserAttributeCommand(const std::string& attr, Expr expr,
- const std::vector<Expr>& values) throw();
- SetUserAttributeCommand(const std::string& attr, Expr expr,
- const std::string& value) throw();
- ~SetUserAttributeCommand() throw() override {}
+ SetUserAttributeCommand(const std::string& attr, Expr expr);
+ SetUserAttributeCommand(const std::string& attr,
+ Expr expr,
+ const std::vector<Expr>& values);
+ SetUserAttributeCommand(const std::string& attr,
+ Expr expr,
+ const std::string& value);
void invoke(SmtEngine* smtEngine) override;
Command* exportTo(ExprManager* exprManager,
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
- std::string getCommandName() const throw() override;
+ std::string getCommandName() const override;
private:
- SetUserAttributeCommand(const std::string& attr, Expr expr,
+ SetUserAttributeCommand(const std::string& attr,
+ Expr expr,
const std::vector<Expr>& expr_values,
- const std::string& str_value) throw();
+ const std::string& str_value);
const std::string d_attr;
const Expr d_expr;
const std::string d_str_value;
}; /* class SetUserAttributeCommand */
-class CVC4_PUBLIC CheckSatCommand : public Command {
-protected:
+class CVC4_PUBLIC CheckSatCommand : public Command
+{
+ protected:
Expr d_expr;
Result d_result;
bool d_inUnsatCore;
-public:
- CheckSatCommand() throw();
- CheckSatCommand(const Expr& expr, bool inUnsatCore = true) throw();
- ~CheckSatCommand() throw() {}
- Expr getExpr() const throw();
- void invoke(SmtEngine* smtEngine);
- Result getResult() 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();
-};/* class CheckSatCommand */
-
-class CVC4_PUBLIC QueryCommand : public Command {
-protected:
+
+ public:
+ CheckSatCommand();
+ CheckSatCommand(const Expr& expr, bool inUnsatCore = true);
+
+ Expr getExpr() const;
+ Result getResult() const;
+ void invoke(SmtEngine* smtEngine) override;
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class CheckSatCommand */
+
+class CVC4_PUBLIC QueryCommand : public Command
+{
+ protected:
Expr d_expr;
Result d_result;
bool d_inUnsatCore;
-public:
- QueryCommand(const Expr& e, bool inUnsatCore = true) throw();
- ~QueryCommand() throw() {}
- Expr getExpr() const throw();
- void invoke(SmtEngine* smtEngine);
- Result getResult() 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();
-};/* class QueryCommand */
-
-class CVC4_PUBLIC CheckSynthCommand : public Command {
-public:
- CheckSynthCommand() throw();
- CheckSynthCommand(const Expr& expr) throw();
- ~CheckSynthCommand() throw() {}
- Expr getExpr() const throw();
- void invoke(SmtEngine* smtEngine);
- Result getResult() 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();
+
+ public:
+ QueryCommand(const Expr& e, bool inUnsatCore = true);
+
+ Expr getExpr() const;
+ Result getResult() const;
+ void invoke(SmtEngine* smtEngine) override;
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class QueryCommand */
+
+class CVC4_PUBLIC CheckSynthCommand : public Command
+{
+ public:
+ CheckSynthCommand();
+ CheckSynthCommand(const Expr& expr);
+
+ Expr getExpr() const;
+ Result getResult() const;
+ void invoke(SmtEngine* smtEngine) override;
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
protected:
/** the assertion of check-synth */
Result d_result;
/** string stream that stores the output of the solution */
std::stringstream d_solution;
-};/* class CheckSynthCommand */
+}; /* class CheckSynthCommand */
// this is TRANSFORM in the CVC presentation language
-class CVC4_PUBLIC SimplifyCommand : public Command {
-protected:
+class CVC4_PUBLIC SimplifyCommand : public Command
+{
+ protected:
Expr d_term;
Expr d_result;
-public:
- SimplifyCommand(Expr term) throw();
- ~SimplifyCommand() throw() {}
- Expr getTerm() const throw();
- void invoke(SmtEngine* smtEngine);
- Expr getResult() 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();
-};/* class SimplifyCommand */
-
-class CVC4_PUBLIC ExpandDefinitionsCommand : public Command {
-protected:
+
+ public:
+ SimplifyCommand(Expr term);
+
+ Expr getTerm() const;
+ Expr getResult() const;
+ void invoke(SmtEngine* smtEngine) override;
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class SimplifyCommand */
+
+class CVC4_PUBLIC ExpandDefinitionsCommand : public Command
+{
+ protected:
Expr d_term;
Expr d_result;
-public:
- ExpandDefinitionsCommand(Expr term) throw();
- ~ExpandDefinitionsCommand() throw() {}
- Expr getTerm() const throw();
- void invoke(SmtEngine* smtEngine);
- Expr getResult() 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();
-};/* class ExpandDefinitionsCommand */
-
-class CVC4_PUBLIC GetValueCommand : public Command {
-protected:
+
+ public:
+ ExpandDefinitionsCommand(Expr term);
+
+ Expr getTerm() const;
+ Expr getResult() const;
+ void invoke(SmtEngine* smtEngine) override;
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class ExpandDefinitionsCommand */
+
+class CVC4_PUBLIC GetValueCommand : public Command
+{
+ protected:
std::vector<Expr> d_terms;
Expr d_result;
-public:
- GetValueCommand(Expr term) throw();
- GetValueCommand(const std::vector<Expr>& terms) throw();
- ~GetValueCommand() throw() {}
- const std::vector<Expr>& getTerms() const throw();
- void invoke(SmtEngine* smtEngine);
- Expr getResult() 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();
-};/* class GetValueCommand */
-
-class CVC4_PUBLIC GetAssignmentCommand : public Command {
-protected:
+
+ public:
+ GetValueCommand(Expr term);
+ GetValueCommand(const std::vector<Expr>& terms);
+
+ const std::vector<Expr>& getTerms() const;
+ Expr getResult() const;
+ void invoke(SmtEngine* smtEngine) override;
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class GetValueCommand */
+
+class CVC4_PUBLIC GetAssignmentCommand : public Command
+{
+ protected:
SExpr d_result;
-public:
- GetAssignmentCommand() throw();
- ~GetAssignmentCommand() throw() {}
- void invoke(SmtEngine* smtEngine);
- SExpr getResult() 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();
-};/* class GetAssignmentCommand */
-
-class CVC4_PUBLIC GetModelCommand : public Command {
+
+ public:
+ GetAssignmentCommand();
+
+ SExpr getResult() const;
+ void invoke(SmtEngine* smtEngine) override;
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class GetAssignmentCommand */
+
+class CVC4_PUBLIC GetModelCommand : public Command
+{
public:
- GetModelCommand() throw();
- ~GetModelCommand() throw() {}
- void invoke(SmtEngine* smtEngine);
+ GetModelCommand();
+
// Model is private to the library -- for now
- // Model* getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const;
+ // Model* getResult() const ;
+ void invoke(SmtEngine* smtEngine) override;
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
protected:
Model* d_result;
SmtEngine* d_smtEngine;
}; /* class GetModelCommand */
-class CVC4_PUBLIC GetProofCommand : public Command {
+class CVC4_PUBLIC GetProofCommand : public Command
+{
public:
- GetProofCommand() throw();
- ~GetProofCommand() throw() {}
- void invoke(SmtEngine* smtEngine);
- const Proof& getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const;
+ GetProofCommand();
+
+ const Proof& getResult() const;
+ void invoke(SmtEngine* smtEngine) override;
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
protected:
SmtEngine* d_smtEngine;
const Proof* d_result;
}; /* class GetProofCommand */
-class CVC4_PUBLIC GetInstantiationsCommand : public Command {
+class CVC4_PUBLIC GetInstantiationsCommand : public Command
+{
public:
- GetInstantiationsCommand() throw();
- ~GetInstantiationsCommand() throw() {}
- void invoke(SmtEngine* smtEngine);
- // Instantiations* getResult() const throw();
- void printResult(std::ostream& out, uint32_t verbosity = 2) const;
+ GetInstantiationsCommand();
+
+ void invoke(SmtEngine* smtEngine) override;
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
protected:
SmtEngine* d_smtEngine;
}; /* class GetInstantiationsCommand */
-class CVC4_PUBLIC GetSynthSolutionCommand : public Command {
+class CVC4_PUBLIC GetSynthSolutionCommand : public Command
+{
public:
- GetSynthSolutionCommand() throw();
- ~GetSynthSolutionCommand() throw() {}
- void invoke(SmtEngine* smtEngine);
- void printResult(std::ostream& out, uint32_t verbosity = 2) const;
+ GetSynthSolutionCommand();
+
+ void invoke(SmtEngine* smtEngine) override;
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
protected:
SmtEngine* d_smtEngine;
}; /* class GetSynthSolutionCommand */
-class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command {
-protected:
+class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command
+{
+ protected:
Expr d_expr;
bool d_doFull;
Expr d_result;
-public:
- GetQuantifierEliminationCommand() throw();
- GetQuantifierEliminationCommand(const Expr& expr, bool doFull) throw();
- ~GetQuantifierEliminationCommand() throw() {}
- Expr getExpr() const throw();
- bool getDoFull() const throw();
- void invoke(SmtEngine* smtEngine);
- Expr getResult() 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();
-};/* class GetQuantifierEliminationCommand */
-
-class CVC4_PUBLIC GetUnsatCoreCommand : public Command {
-public:
- GetUnsatCoreCommand() throw();
- ~GetUnsatCoreCommand() 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;
- std::string getCommandName() const throw();
-
-protected:
+
+ public:
+ GetQuantifierEliminationCommand();
+ GetQuantifierEliminationCommand(const Expr& expr, bool doFull);
+
+ Expr getExpr() const;
+ bool getDoFull() const;
+ void invoke(SmtEngine* smtEngine) override;
+ Expr getResult() const;
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class GetQuantifierEliminationCommand */
+
+class CVC4_PUBLIC GetUnsatCoreCommand : public Command
+{
+ public:
+ GetUnsatCoreCommand();
+ const UnsatCore& getUnsatCore() const;
+
+ void invoke(SmtEngine* smtEngine) override;
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+
+ protected:
// the result of the unsat core call
UnsatCore d_result;
-};/* class GetUnsatCoreCommand */
+}; /* class GetUnsatCoreCommand */
-class CVC4_PUBLIC GetAssertionsCommand : public Command {
-protected:
+class CVC4_PUBLIC GetAssertionsCommand : public Command
+{
+ protected:
std::string d_result;
-public:
- GetAssertionsCommand() throw();
- ~GetAssertionsCommand() throw() {}
- void invoke(SmtEngine* smtEngine);
- std::string getResult() 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();
-};/* class GetAssertionsCommand */
-
-class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
-protected:
+
+ public:
+ GetAssertionsCommand();
+
+ void invoke(SmtEngine* smtEngine) override;
+ std::string getResult() const;
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class GetAssertionsCommand */
+
+class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command
+{
+ protected:
BenchmarkStatus d_status;
-public:
- SetBenchmarkStatusCommand(BenchmarkStatus status) throw();
- ~SetBenchmarkStatusCommand() throw() {}
- BenchmarkStatus getStatus() const throw();
- void invoke(SmtEngine* smtEngine);
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class SetBenchmarkStatusCommand */
-
-class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
-protected:
+
+ public:
+ SetBenchmarkStatusCommand(BenchmarkStatus status);
+
+ BenchmarkStatus getStatus() const;
+
+ void invoke(SmtEngine* smtEngine) override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class SetBenchmarkStatusCommand */
+
+class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command
+{
+ protected:
std::string d_logic;
-public:
- SetBenchmarkLogicCommand(std::string logic) throw();
- ~SetBenchmarkLogicCommand() throw() {}
- std::string getLogic() const throw();
- void invoke(SmtEngine* smtEngine);
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class SetBenchmarkLogicCommand */
-
-class CVC4_PUBLIC SetInfoCommand : public Command {
-protected:
+
+ public:
+ SetBenchmarkLogicCommand(std::string logic);
+
+ std::string getLogic() const;
+ void invoke(SmtEngine* smtEngine) override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class SetBenchmarkLogicCommand */
+
+class CVC4_PUBLIC SetInfoCommand : public Command
+{
+ protected:
std::string d_flag;
SExpr d_sexpr;
-public:
- SetInfoCommand(std::string flag, const SExpr& sexpr) throw();
- ~SetInfoCommand() throw() {}
- std::string getFlag() const throw();
- SExpr getSExpr() const throw();
- void invoke(SmtEngine* smtEngine);
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class SetInfoCommand */
-
-class CVC4_PUBLIC GetInfoCommand : public Command {
-protected:
+
+ public:
+ SetInfoCommand(std::string flag, const SExpr& sexpr);
+
+ std::string getFlag() const;
+ SExpr getSExpr() const;
+
+ void invoke(SmtEngine* smtEngine) override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class SetInfoCommand */
+
+class CVC4_PUBLIC GetInfoCommand : public Command
+{
+ protected:
std::string d_flag;
std::string d_result;
-public:
- GetInfoCommand(std::string flag) throw();
- ~GetInfoCommand() throw() {}
- std::string getFlag() const throw();
- void invoke(SmtEngine* smtEngine);
- std::string getResult() 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();
-};/* class GetInfoCommand */
-
-class CVC4_PUBLIC SetOptionCommand : public Command {
-protected:
+
+ public:
+ GetInfoCommand(std::string flag);
+
+ std::string getFlag() const;
+ std::string getResult() const;
+
+ void invoke(SmtEngine* smtEngine) override;
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class GetInfoCommand */
+
+class CVC4_PUBLIC SetOptionCommand : public Command
+{
+ protected:
std::string d_flag;
SExpr d_sexpr;
-public:
- SetOptionCommand(std::string flag, const SExpr& sexpr) throw();
- ~SetOptionCommand() throw() {}
- std::string getFlag() const throw();
- SExpr getSExpr() const throw();
- void invoke(SmtEngine* smtEngine);
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class SetOptionCommand */
-
-class CVC4_PUBLIC GetOptionCommand : public Command {
-protected:
+
+ public:
+ SetOptionCommand(std::string flag, const SExpr& sexpr);
+
+ std::string getFlag() const;
+ SExpr getSExpr() const;
+
+ void invoke(SmtEngine* smtEngine) override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class SetOptionCommand */
+
+class CVC4_PUBLIC GetOptionCommand : public Command
+{
+ protected:
std::string d_flag;
std::string d_result;
-public:
- GetOptionCommand(std::string flag) throw();
- ~GetOptionCommand() throw() {}
- std::string getFlag() const throw();
- void invoke(SmtEngine* smtEngine);
- std::string getResult() 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();
-};/* class GetOptionCommand */
+
+ public:
+ GetOptionCommand(std::string flag);
+
+ std::string getFlag() const;
+ std::string getResult() const;
+
+ void invoke(SmtEngine* smtEngine) override;
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class GetOptionCommand */
// Set expression name command
// Note this is not an official smt2 command
// is converted to
// (assert expr)
// (set-expr-name expr name)
-class CVC4_PUBLIC SetExpressionNameCommand : public Command {
-protected:
+class CVC4_PUBLIC SetExpressionNameCommand : public Command
+{
+ protected:
Expr d_expr;
std::string d_name;
-public:
- SetExpressionNameCommand(Expr expr, std::string name) throw();
- ~SetExpressionNameCommand() throw() {}
- void invoke(SmtEngine* smtEngine);
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class SetExpressionNameCommand */
-
-
-class CVC4_PUBLIC DatatypeDeclarationCommand : public Command {
-private:
+
+ public:
+ SetExpressionNameCommand(Expr expr, std::string name);
+
+ void invoke(SmtEngine* smtEngine) override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class SetExpressionNameCommand */
+
+class CVC4_PUBLIC DatatypeDeclarationCommand : public Command
+{
+ private:
std::vector<DatatypeType> d_datatypes;
-public:
- 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);
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class DatatypeDeclarationCommand */
-
-class CVC4_PUBLIC RewriteRuleCommand : public Command {
-public:
- typedef std::vector< std::vector< Expr > > Triggers;
-protected:
- typedef std::vector< Expr > VExpr;
+
+ public:
+ DatatypeDeclarationCommand(const DatatypeType& datatype);
+
+ DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes);
+ const std::vector<DatatypeType>& getDatatypes() const;
+ void invoke(SmtEngine* smtEngine) override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class DatatypeDeclarationCommand */
+
+class CVC4_PUBLIC RewriteRuleCommand : public Command
+{
+ public:
+ typedef std::vector<std::vector<Expr> > Triggers;
+
+ protected:
+ typedef std::vector<Expr> VExpr;
VExpr d_vars;
VExpr d_guards;
Expr d_head;
Expr d_body;
Triggers d_triggers;
-public:
+
+ public:
RewriteRuleCommand(const std::vector<Expr>& vars,
const std::vector<Expr>& guards,
Expr head,
Expr body,
- const Triggers& d_triggers) throw();
- RewriteRuleCommand(const std::vector<Expr>& vars,
- Expr head,
- Expr body) throw();
- ~RewriteRuleCommand() throw() {}
- const std::vector<Expr>& getVars() const throw();
- const std::vector<Expr>& getGuards() const throw();
- Expr getHead() const throw();
- Expr getBody() const throw();
- const Triggers& getTriggers() const throw();
- void invoke(SmtEngine* smtEngine);
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class RewriteRuleCommand */
-
-class CVC4_PUBLIC PropagateRuleCommand : public Command {
-public:
- typedef std::vector< std::vector< Expr > > Triggers;
-protected:
- typedef std::vector< Expr > VExpr;
+ const Triggers& d_triggers);
+ RewriteRuleCommand(const std::vector<Expr>& vars, Expr head, Expr body);
+
+ const std::vector<Expr>& getVars() const;
+ const std::vector<Expr>& getGuards() const;
+ Expr getHead() const;
+ Expr getBody() const;
+ const Triggers& getTriggers() const;
+
+ void invoke(SmtEngine* smtEngine) override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class RewriteRuleCommand */
+
+class CVC4_PUBLIC PropagateRuleCommand : public Command
+{
+ public:
+ typedef std::vector<std::vector<Expr> > Triggers;
+
+ protected:
+ typedef std::vector<Expr> VExpr;
VExpr d_vars;
VExpr d_guards;
VExpr d_heads;
Expr d_body;
Triggers d_triggers;
bool d_deduction;
-public:
+
+ public:
PropagateRuleCommand(const std::vector<Expr>& vars,
const std::vector<Expr>& guards,
const std::vector<Expr>& heads,
Expr body,
const Triggers& d_triggers,
/* true if we want a deduction rule */
- bool d_deduction = false) throw();
+ bool d_deduction = false);
PropagateRuleCommand(const std::vector<Expr>& vars,
const std::vector<Expr>& heads,
Expr body,
- bool d_deduction = false) throw();
- ~PropagateRuleCommand() throw() {}
- const std::vector<Expr>& getVars() const throw();
- const std::vector<Expr>& getGuards() const throw();
- const std::vector<Expr>& getHeads() const throw();
- Expr getBody() const throw();
- const Triggers& getTriggers() const throw();
- bool isDeduction() const throw();
- void invoke(SmtEngine* smtEngine);
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class PropagateRuleCommand */
-
-class CVC4_PUBLIC ResetCommand : public Command {
-public:
- ResetCommand() throw() {}
- ~ResetCommand() throw() {}
- void invoke(SmtEngine* smtEngine);
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class ResetCommand */
-
-class CVC4_PUBLIC ResetAssertionsCommand : public Command {
-public:
- ResetAssertionsCommand() throw() {}
- ~ResetAssertionsCommand() throw() {}
- void invoke(SmtEngine* smtEngine);
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class ResetAssertionsCommand */
-
-class CVC4_PUBLIC QuitCommand : public Command {
-public:
- QuitCommand() throw() {}
- ~QuitCommand() throw() {}
- void invoke(SmtEngine* smtEngine);
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class QuitCommand */
-
-class CVC4_PUBLIC CommentCommand : public Command {
+ bool d_deduction = false);
+
+ const std::vector<Expr>& getVars() const;
+ const std::vector<Expr>& getGuards() const;
+ const std::vector<Expr>& getHeads() const;
+ Expr getBody() const;
+ const Triggers& getTriggers() const;
+ bool isDeduction() const;
+ void invoke(SmtEngine* smtEngine) override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class PropagateRuleCommand */
+
+class CVC4_PUBLIC ResetCommand : public Command
+{
+ public:
+ ResetCommand() {}
+ void invoke(SmtEngine* smtEngine) override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class ResetCommand */
+
+class CVC4_PUBLIC ResetAssertionsCommand : public Command
+{
+ public:
+ ResetAssertionsCommand() {}
+ void invoke(SmtEngine* smtEngine) override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class ResetAssertionsCommand */
+
+class CVC4_PUBLIC QuitCommand : public Command
+{
+ public:
+ QuitCommand() {}
+ void invoke(SmtEngine* smtEngine) override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class QuitCommand */
+
+class CVC4_PUBLIC CommentCommand : public Command
+{
std::string d_comment;
-public:
- CommentCommand(std::string comment) throw();
- ~CommentCommand() throw() {}
- std::string getComment() const throw();
- void invoke(SmtEngine* smtEngine);
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class CommentCommand */
-
-class CVC4_PUBLIC CommandSequence : public Command {
-private:
+
+ public:
+ CommentCommand(std::string comment);
+
+ std::string getComment() const;
+
+ void invoke(SmtEngine* smtEngine) override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class CommentCommand */
+
+class CVC4_PUBLIC CommandSequence : public Command
+{
+ private:
/** All the commands to be executed (in sequence) */
std::vector<Command*> d_commandSequence;
/** Next command to be executed */
unsigned int d_index;
-public:
- CommandSequence() throw();
- ~CommandSequence() throw();
- void addCommand(Command* cmd) throw();
- void clear() throw();
+ public:
+ CommandSequence();
+ ~CommandSequence();
- void invoke(SmtEngine* smtEngine);
- void invoke(SmtEngine* smtEngine, std::ostream& out);
+ void addCommand(Command* cmd);
+ void clear();
+
+ void invoke(SmtEngine* smtEngine) override;
+ void invoke(SmtEngine* smtEngine, std::ostream& out) override;
typedef std::vector<Command*>::iterator iterator;
typedef std::vector<Command*>::const_iterator const_iterator;
- const_iterator begin() const throw();
- const_iterator end() const throw();
+ const_iterator begin() const;
+ const_iterator end() const;
- iterator begin() throw();
- iterator end() throw();
+ iterator begin();
+ iterator end();
- Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
- Command* clone() const;
- std::string getCommandName() const throw();
-};/* class CommandSequence */
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+}; /* class CommandSequence */
-class CVC4_PUBLIC DeclarationSequence : public CommandSequence {
-public:
- ~DeclarationSequence() throw() {}
-};/* class DeclarationSequence */
+class CVC4_PUBLIC DeclarationSequence : public CommandSequence
+{
+};
-}/* CVC4 namespace */
+} /* CVC4 namespace */
#endif /* __CVC4__COMMAND_H */
projects / cvc5.git / commitdiff