diff options
Diffstat (limited to 'src/smt_util/command.cpp')
-rw-r--r-- | src/smt_util/command.cpp | 1848 |
1 files changed, 1848 insertions, 0 deletions
diff --git a/src/smt_util/command.cpp b/src/smt_util/command.cpp new file mode 100644 index 000000000..464a2e0aa --- /dev/null +++ b/src/smt_util/command.cpp @@ -0,0 +1,1848 @@ +/********************* */ +/*! \file command.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): Kshitij Bansal, Dejan Jovanovic, Andrew Reynolds, Francois Bobot + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of command objects. + ** + ** Implementation of command objects. + **/ + +#include "smt_util/command.h" + +#include <exception> +#include <iostream> +#include <iterator> +#include <sstream> +#include <utility> +#include <vector> + +#include "base/output.h" +#include "expr/node.h" +#include "expr/sexpr.h" +#include "options/options.h" +#include "options/smt_options.h" +#include "printer/printer.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "smt_util/dump.h" +#include "smt_util/model.h" + +using namespace std; + +namespace CVC4 { + +const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc(); +const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess(); +const CommandInterrupted* CommandInterrupted::s_instance = new CommandInterrupted(); + +std::ostream& operator<<(std::ostream& out, const Command& c) throw() { + c.toStream(out, + Node::setdepth::getDepth(out), + Node::printtypes::getPrintTypes(out), + Node::dag::getDag(out), + Node::setlanguage::getLanguage(out)); + return out; +} + +ostream& operator<<(ostream& out, const Command* c) throw() { + if(c == NULL) { + out << "null"; + } else { + out << *c; + } + return out; +} + +std::ostream& operator<<(std::ostream& out, const CommandStatus& s) throw() { + s.toStream(out, Node::setlanguage::getLanguage(out)); + return out; +} + +ostream& operator<<(ostream& out, const CommandStatus* s) throw() { + if(s == NULL) { + out << "null"; + } else { + out << *s; + } + return out; +} + +/* class Command */ + +Command::Command() throw() : 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()) { + delete d_commandStatus; + } +} + +bool Command::ok() const throw() { + // either we haven't run the command yet, or it ran successfully + return d_commandStatus == NULL || dynamic_cast<const CommandSuccess*>(d_commandStatus) != NULL; +} + +bool Command::fail() const throw() { + 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; +} + +void Command::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { + invoke(smtEngine); + if(!(isMuted() && ok())) { + printResult(out, smtEngine->getOption("command-verbosity:" + getCommandName()).getIntegerValue().toUnsignedInt()); + } +} + +std::string Command::toString() const throw() { + 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() { + Printer::getPrinter(language)->toStream(out, this, toDepth, types, dag); +} + +void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const throw() { + Printer::getPrinter(language)->toStream(out, this); +} + +void Command::printResult(std::ostream& out, uint32_t verbosity) const throw() { + 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) throw() { + /* 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 { + return new EmptyCommand(d_name); +} + +std::string EmptyCommand::getCommandName() const throw() { + 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) throw() { + /* we don't have an output stream here, nothing to do */ + d_commandStatus = CommandSuccess::instance(); +} + +void EchoCommand::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { + out << d_output << std::endl; + d_commandStatus = CommandSuccess::instance(); + 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 { + return new EchoCommand(d_output); +} + +std::string EchoCommand::getCommandName() const throw() { + 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; +} + +void AssertCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->assertFormula(d_expr, d_inUnsatCore); + d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); + } 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::clone() const { + return new AssertCommand(d_expr, d_inUnsatCore); +} + +std::string AssertCommand::getCommandName() const throw() { + return "assert"; +} + +/* class PushCommand */ + +void PushCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->push(); + d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* PushCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new PushCommand(); +} + +Command* PushCommand::clone() const { + return new PushCommand(); +} + +std::string PushCommand::getCommandName() const throw() { + return "push"; +} + +/* class PopCommand */ + +void PopCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->pop(); + d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* PopCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new PopCommand(); +} + +Command* PopCommand::clone() const { + return new PopCommand(); +} + +std::string PopCommand::getCommandName() const throw() { + 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; +} + +void CheckSatCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->checkSat(d_expr); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Result CheckSatCommand::getResult() const throw() { + return d_result; +} + +void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + out << d_result << endl; + } +} + +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 { + CheckSatCommand* c = new CheckSatCommand(d_expr, d_inUnsatCore); + c->d_result = d_result; + return c; +} + +std::string CheckSatCommand::getCommandName() const throw() { + 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; +} + +void QueryCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->query(d_expr); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Result QueryCommand::getResult() const throw() { + return d_result; +} + +void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + out << d_result << endl; + } +} + +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 { + QueryCommand* c = new QueryCommand(d_expr, d_inUnsatCore); + c->d_result = d_result; + return c; +} + +std::string QueryCommand::getCommandName() const throw() { + return "query"; +} + +/* class ResetCommand */ + +void ResetCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->reset(); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* ResetCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new ResetCommand(); +} + +Command* ResetCommand::clone() const { + return new ResetCommand(); +} + +std::string ResetCommand::getCommandName() const throw() { + return "reset"; +} + +/* class ResetAssertionsCommand */ + +void ResetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->resetAssertions(); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* ResetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new ResetAssertionsCommand(); +} + +Command* ResetAssertionsCommand::clone() const { + return new ResetAssertionsCommand(); +} + +std::string ResetAssertionsCommand::getCommandName() const throw() { + return "reset-assertions"; +} + +/* class QuitCommand */ + +void QuitCommand::invoke(SmtEngine* smtEngine) throw() { + Dump("benchmark") << *this; + d_commandStatus = CommandSuccess::instance(); +} + +Command* QuitCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new QuitCommand(); +} + +Command* QuitCommand::clone() const { + return new QuitCommand(); +} + +std::string QuitCommand::getCommandName() const throw() { + 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) throw() { + Dump("benchmark") << *this; + d_commandStatus = CommandSuccess::instance(); +} + +Command* CommentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new CommentCommand(d_comment); +} + +Command* CommentCommand::clone() const { + return new CommentCommand(d_comment); +} + +std::string CommentCommand::getCommandName() const throw() { + return "comment"; +} + +/* class CommandSequence */ + +CommandSequence::CommandSequence() throw() : + d_index(0) { +} + +CommandSequence::~CommandSequence() throw() { + for(unsigned i = d_index; i < d_commandSequence.size(); ++i) { + delete d_commandSequence[i]; + } +} + +void CommandSequence::addCommand(Command* cmd) throw() { + d_commandSequence.push_back(cmd); +} + +void CommandSequence::clear() throw() { + d_commandSequence.clear(); +} + +void CommandSequence::invoke(SmtEngine* smtEngine) throw() { + for(; d_index < d_commandSequence.size(); ++d_index) { + d_commandSequence[d_index]->invoke(smtEngine); + if(! d_commandSequence[d_index]->ok()) { + // abort execution + d_commandStatus = d_commandSequence[d_index]->getCommandStatus(); + return; + } + delete d_commandSequence[d_index]; + } + + AlwaysAssert(d_commandStatus == NULL); + d_commandStatus = CommandSuccess::instance(); +} + +void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { + for(; d_index < d_commandSequence.size(); ++d_index) { + d_commandSequence[d_index]->invoke(smtEngine, out); + if(! d_commandSequence[d_index]->ok()) { + // abort execution + d_commandStatus = d_commandSequence[d_index]->getCommandStatus(); + return; + } + delete d_commandSequence[d_index]; + } + + AlwaysAssert(d_commandStatus == NULL); + d_commandStatus = CommandSuccess::instance(); +} + +Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + CommandSequence* seq = new CommandSequence(); + for(iterator i = begin(); i != end(); ++i) { + Command* cmd_to_export = *i; + Command* cmd = cmd_to_export->exportTo(exprManager, variableMap); + seq->addCommand(cmd); + Debug("export") << "[export] so far converted: " << seq << endl; + } + seq->d_index = d_index; + return seq; +} + +Command* CommandSequence::clone() const { + CommandSequence* seq = new CommandSequence(); + 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() { + return d_commandSequence.begin(); +} + +CommandSequence::const_iterator CommandSequence::end() const throw() { + return d_commandSequence.end(); +} + +CommandSequence::iterator CommandSequence::begin() throw() { + return d_commandSequence.begin(); +} + +CommandSequence::iterator CommandSequence::end() throw() { + return d_commandSequence.end(); +} + +std::string CommandSequence::getCommandName() const throw() { + 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; +} + +/* 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; +} + +bool DeclareFunctionCommand::getPrintInModelSetByUser() const throw() { + return d_printInModelSetByUser; +} + +void DeclareFunctionCommand::setPrintInModel( bool p ) { + d_printInModel = p; + d_printInModelSetByUser = true; +} + +void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() { + 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)); + 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); + dfc->d_printInModel = d_printInModel; + dfc->d_printInModelSetByUser = d_printInModelSetByUser; + return dfc; +} + +std::string DeclareFunctionCommand::getCommandName() const throw() { + 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; +} + +void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() { + d_commandStatus = CommandSuccess::instance(); +} + +Command* DeclareTypeCommand::exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) { + return new DeclareTypeCommand(d_symbol, d_arity, + d_type.exportTo(exprManager, variableMap)); +} + +Command* DeclareTypeCommand::clone() const { + return new DeclareTypeCommand(d_symbol, d_arity, d_type); +} + +std::string DeclareTypeCommand::getCommandName() const throw() { + 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, + const std::vector<Type>& params, + Type t) throw() : + DeclarationDefinitionCommand(id), + d_params(params), + d_type(t) { +} + +const std::vector<Type>& DefineTypeCommand::getParameters() const throw() { + return d_params; +} + +Type DefineTypeCommand::getType() const throw() { + return d_type; +} + +void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() { + d_commandStatus = CommandSuccess::instance(); +} + +Command* DefineTypeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + vector<Type> 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 { + return new DefineTypeCommand(d_symbol, d_params, d_type); +} + +std::string DefineTypeCommand::getCommandName() const throw() { + 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) { +} + +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; +} + +const std::vector<Expr>& DefineFunctionCommand::getFormals() const throw() { + return d_formals; +} + +Expr DefineFunctionCommand::getFormula() const throw() { + return d_formula; +} + +void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() { + try { + if(!d_func.isNull()) { + smtEngine->defineFunction(d_func, d_formals, d_formula); + } + d_commandStatus = CommandSuccess::instance(); + } 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); + vector<Expr> 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 { + return new DefineFunctionCommand(d_symbol, d_func, d_formals, d_formula); +} + +std::string DefineFunctionCommand::getCommandName() const throw() { + 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) { +} + +void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) throw() { + this->DefineFunctionCommand::invoke(smtEngine); + if(!d_func.isNull() && d_func.getType().isBoolean()) { + smtEngine->addToAssignment(d_func.getExprManager()->mkExpr(kind::APPLY, d_func)); + } + d_commandStatus = CommandSuccess::instance(); +} + +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), + ExportTransformer(exprManager, variableMap)); + Expr formula = d_formula.exportTo(exprManager, variableMap); + return new DefineNamedFunctionCommand(d_symbol, func, formals, formula); +} + +Command* DefineNamedFunctionCommand::clone() const { + return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula); +} + +/* class SetUserAttribute */ + +SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr ) throw() : + d_attr( attr ), d_expr( expr ){ +} + +SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr, + std::vector<Expr>& values ) throw() : + d_attr( attr ), d_expr( expr ){ + d_expr_values.insert( d_expr_values.begin(), values.begin(), values.end() ); +} + +SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr, + const std::string& value ) throw() : + d_attr( attr ), d_expr( expr ), d_str_value( value ){ +} + +void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) throw(){ + try { + if(!d_expr.isNull()) { + smtEngine->setUserAttribute( d_attr, d_expr, d_expr_values, d_str_value ); + } + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* SetUserAttributeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap){ + Expr expr = d_expr.exportTo(exprManager, variableMap); + SetUserAttributeCommand * c = new SetUserAttributeCommand( d_attr, expr, d_str_value ); + c->d_expr_values.insert( c->d_expr_values.end(), d_expr_values.begin(), d_expr_values.end() ); + return c; +} + +Command* SetUserAttributeCommand::clone() const{ + SetUserAttributeCommand * c = new SetUserAttributeCommand( d_attr, d_expr, d_str_value ); + c->d_expr_values.insert( c->d_expr_values.end(), d_expr_values.begin(), d_expr_values.end() ); + return c; +} + +std::string SetUserAttributeCommand::getCommandName() const throw() { + 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) throw() { + try { + d_result = smtEngine->simplify(d_term); + d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); + } 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 throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + out << d_result << endl; + } +} + +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 { + SimplifyCommand* c = new SimplifyCommand(d_term); + c->d_result = d_result; + return c; +} + +std::string SimplifyCommand::getCommandName() const throw() { + 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) throw() { + 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 throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + out << d_result << endl; + } +} + +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 { + ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term); + c->d_result = d_result; + return c; +} + +std::string ExpandDefinitionsCommand::getCommandName() const throw() { + return "expand-definitions"; +} + +/* class GetValueCommand */ + +GetValueCommand::GetValueCommand(Expr term) throw() : + d_terms() { + d_terms.push_back(term); +} + +GetValueCommand::GetValueCommand(const std::vector<Expr>& terms) throw() : + d_terms(terms) { + CheckArgument(terms.size() >= 1, terms, "cannot get-value of an empty set of terms"); +} + +const std::vector<Expr>& GetValueCommand::getTerms() const throw() { + return d_terms; +} + +void GetValueCommand::invoke(SmtEngine* smtEngine) throw() { + 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) { + Assert(nm == NodeManager::fromExprManager((*i).getExprManager())); + smt::SmtScope scope(smtEngine); + 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()) { + // 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); + } + result.push_back(nm->mkNode(kind::SEXPR, request, value).toExpr()); + } + d_result = em->mkExpr(kind::SEXPR, result); + d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); + } 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 throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + Expr::dag::Scope scope(out, false); + out << d_result << endl; + } +} + +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) { + exportedTerms.push_back((*i).exportTo(exprManager, variableMap)); + } + GetValueCommand* c = new GetValueCommand(exportedTerms); + c->d_result = d_result.exportTo(exprManager, variableMap); + return c; +} + +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"; +} + +/* class GetAssignmentCommand */ + +GetAssignmentCommand::GetAssignmentCommand() throw() { +} + +void GetAssignmentCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->getAssignment(); + d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); + } 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 throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + out << d_result << endl; + } +} + +Command* GetAssignmentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetAssignmentCommand* c = new GetAssignmentCommand(); + c->d_result = d_result; + return c; +} + +Command* GetAssignmentCommand::clone() const { + GetAssignmentCommand* c = new GetAssignmentCommand(); + c->d_result = d_result; + return c; +} + +std::string GetAssignmentCommand::getCommandName() const throw() { + return "get-assignment"; +} + +/* class GetModelCommand */ + +GetModelCommand::GetModelCommand() throw() { +} + +void GetModelCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->getModel(); + d_smtEngine = smtEngine; + d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +/* Model is private to the library -- for now +Model* GetModelCommand::getResult() const throw() { + return d_result; +} +*/ + +void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + out << *d_result; + } +} + +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 { + 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"; +} + +/* class GetProofCommand */ + +GetProofCommand::GetProofCommand() throw() { +} + +void GetProofCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->getProof(); + d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Proof* GetProofCommand::getResult() const throw() { + return d_result; +} + +void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + d_result->toStream(out); + } +} + +Command* GetProofCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetProofCommand* c = new GetProofCommand(); + c->d_result = d_result; + return c; +} + +Command* GetProofCommand::clone() const { + GetProofCommand* c = new GetProofCommand(); + c->d_result = d_result; + return c; +} + +std::string GetProofCommand::getCommandName() const throw() { + return "get-proof"; +} + +/* class GetInstantiationsCommand */ + +GetInstantiationsCommand::GetInstantiationsCommand() throw() { +} + +void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_smtEngine = smtEngine; + d_commandStatus = CommandSuccess::instance(); + } 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 throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + d_smtEngine->printInstantiations(out); + } +} + +Command* GetInstantiationsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetInstantiationsCommand* c = new GetInstantiationsCommand(); + //c->d_result = d_result; + c->d_smtEngine = d_smtEngine; + return c; +} + +Command* GetInstantiationsCommand::clone() const { + GetInstantiationsCommand* c = new GetInstantiationsCommand(); + //c->d_result = d_result; + c->d_smtEngine = d_smtEngine; + return c; +} + +std::string GetInstantiationsCommand::getCommandName() const throw() { + return "get-instantiations"; +} + +/* class GetSynthSolutionCommand */ + +GetSynthSolutionCommand::GetSynthSolutionCommand() throw() { +} + +void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_smtEngine = smtEngine; + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +void GetSynthSolutionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + d_smtEngine->printSynthSolution(out); + } +} + +Command* GetSynthSolutionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetSynthSolutionCommand* c = new GetSynthSolutionCommand(); + c->d_smtEngine = d_smtEngine; + return c; +} + +Command* GetSynthSolutionCommand::clone() const { + GetSynthSolutionCommand* c = new GetSynthSolutionCommand(); + c->d_smtEngine = d_smtEngine; + return c; +} + +std::string GetSynthSolutionCommand::getCommandName() const throw() { + return "get-instantiations"; +} + +/* class GetUnsatCoreCommand */ + +GetUnsatCoreCommand::GetUnsatCoreCommand() throw() { +} + +GetUnsatCoreCommand::GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw() : d_names(names) { +} + +void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->getUnsatCore(); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + d_result.toStream(out, d_names); + } +} + +const UnsatCore& GetUnsatCoreCommand::getUnsatCore() const throw() { + // of course, this will be empty if the command hasn't been invoked yet + return d_result; +} + +Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names); + c->d_result = d_result; + return c; +} + +Command* GetUnsatCoreCommand::clone() const { + GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names); + c->d_result = d_result; + return c; +} + +std::string GetUnsatCoreCommand::getCommandName() const throw() { + return "get-unsat-core"; +} + +/* class GetAssertionsCommand */ + +GetAssertionsCommand::GetAssertionsCommand() throw() { +} + +void GetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() { + try { + stringstream ss; + const vector<Expr> v = smtEngine->getAssertions(); + 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) { + 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 throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + out << d_result; + } +} + +Command* GetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetAssertionsCommand* c = new GetAssertionsCommand(); + c->d_result = d_result; + return c; +} + +Command* GetAssertionsCommand::clone() const { + GetAssertionsCommand* c = new GetAssertionsCommand(); + c->d_result = d_result; + return c; +} + +std::string GetAssertionsCommand::getCommandName() const throw() { + return "get-assertions"; +} + +/* class SetBenchmarkStatusCommand */ + +SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) throw() : + d_status(status) { +} + +BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const throw() { + return d_status; +} + +void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() { + try { + stringstream ss; + ss << d_status; + SExpr status = SExpr(ss.str()); + smtEngine->setInfo("status", status); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* SetBenchmarkStatusCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new SetBenchmarkStatusCommand(d_status); +} + +Command* SetBenchmarkStatusCommand::clone() const { + return new SetBenchmarkStatusCommand(d_status); +} + +std::string SetBenchmarkStatusCommand::getCommandName() const throw() { + return "set-info"; +} + +/* class SetBenchmarkLogicCommand */ + +SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) throw() : + d_logic(logic) { +} + +std::string SetBenchmarkLogicCommand::getLogic() const throw() { + return d_logic; +} + +void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->setLogic(d_logic); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* SetBenchmarkLogicCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new SetBenchmarkLogicCommand(d_logic); +} + +Command* SetBenchmarkLogicCommand::clone() const { + return new SetBenchmarkLogicCommand(d_logic); +} + +std::string SetBenchmarkLogicCommand::getCommandName() const throw() { + 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; +} + +void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->setInfo(d_flag, d_sexpr); + d_commandStatus = CommandSuccess::instance(); + } catch(UnrecognizedOptionException&) { + // As per SMT-LIB spec, silently accept unknown set-info keys + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* SetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new SetInfoCommand(d_flag, d_sexpr); +} + +Command* SetInfoCommand::clone() const { + return new SetInfoCommand(d_flag, d_sexpr); +} + +std::string SetInfoCommand::getCommandName() const throw() { + 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) throw() { + 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") { + ss << PrettySExprs(true); + } + ss << SExpr(v); + d_result = ss.str(); + d_commandStatus = CommandSuccess::instance(); + } catch(UnrecognizedOptionException&) { + d_commandStatus = new CommandUnsupported(); + } 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 throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else if(d_result != "") { + out << d_result << endl; + } +} + +Command* GetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetInfoCommand* c = new GetInfoCommand(d_flag); + c->d_result = d_result; + return c; +} + +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"; +} + +/* 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; +} + +void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->setOption(d_flag, d_sexpr); + d_commandStatus = CommandSuccess::instance(); + } catch(UnrecognizedOptionException&) { + d_commandStatus = new CommandUnsupported(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* SetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new SetOptionCommand(d_flag, d_sexpr); +} + +Command* SetOptionCommand::clone() const { + return new SetOptionCommand(d_flag, d_sexpr); +} + +std::string SetOptionCommand::getCommandName() const throw() { + 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) throw() { + try { + SExpr res = smtEngine->getOption(d_flag); + d_result = res.toString(); + d_commandStatus = CommandSuccess::instance(); + } catch(UnrecognizedOptionException&) { + d_commandStatus = new CommandUnsupported(); + } 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 throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else if(d_result != "") { + out << d_result << endl; + } +} + +Command* GetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetOptionCommand* c = new GetOptionCommand(d_flag); + c->d_result = d_result; + return c; +} + +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"; +} + +/* class DatatypeDeclarationCommand */ + +DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() : + d_datatypes() { + d_datatypes.push_back(datatype); +} + +DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw() : + d_datatypes(datatypes) { +} + +const std::vector<DatatypeType>& +DatatypeDeclarationCommand::getDatatypes() const throw() { + return d_datatypes; +} + +void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() { + d_commandStatus = CommandSuccess::instance(); +} + +Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + throw ExportUnsupportedException + ("export of DatatypeDeclarationCommand unsupported"); +} + +Command* DatatypeDeclarationCommand::clone() const { + return new DatatypeDeclarationCommand(d_datatypes); +} + +std::string DatatypeDeclarationCommand::getCommandName() const throw() { + return "declare-datatypes"; +} + +/* class RewriteRuleCommand */ + +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) { +} + +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; +} + +const std::vector<Expr>& RewriteRuleCommand::getGuards() const throw() { + 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() { + return d_triggers; +} + +void RewriteRuleCommand::invoke(SmtEngine* smtEngine) throw() { + 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); + /** build expression */ + Expr expr; + 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)); + } + 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) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* RewriteRuleCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + /** Convert variables */ + VExpr vars; vars.reserve(d_vars.size()); + for(VExpr::iterator i = d_vars.begin(), end = d_vars.end(); + i == end; ++i){ + vars.push_back(i->exportTo(exprManager, variableMap)); + }; + /** Convert guards */ + VExpr guards; guards.reserve(d_guards.size()); + for(VExpr::iterator i = d_guards.begin(), end = d_guards.end(); + i == end; ++i){ + guards.push_back(i->exportTo(exprManager, variableMap)); + }; + /** Convert triggers */ + Triggers triggers; triggers.resize(d_triggers.size()); + for(size_t i = 0, end = d_triggers.size(); + i < end; ++i){ + triggers[i].reserve(d_triggers[i].size()); + for(VExpr::iterator j = d_triggers[i].begin(), jend = d_triggers[i].end(); + j == jend; ++i){ + triggers[i].push_back(j->exportTo(exprManager, variableMap)); + }; + }; + /** Convert head and body */ + Expr head = d_head.exportTo(exprManager, variableMap); + Expr body = d_body.exportTo(exprManager, variableMap); + /** Create the converted rules */ + return new RewriteRuleCommand(vars, guards, head, body, triggers); +} + +Command* RewriteRuleCommand::clone() const { + return new RewriteRuleCommand(d_vars, d_guards, d_head, d_body, d_triggers); +} + +std::string RewriteRuleCommand::getCommandName() const throw() { + return "rewrite-rule"; +} + +/* class PropagateRuleCommand */ + +PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars, + const std::vector<Expr>& guards, + 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) { +} + +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) { +} + +const std::vector<Expr>& PropagateRuleCommand::getVars() const throw() { + return d_vars; +} + +const std::vector<Expr>& PropagateRuleCommand::getGuards() const throw() { + return d_guards; +} + +const std::vector<Expr>& PropagateRuleCommand::getHeads() const throw() { + return d_heads; +} + +Expr PropagateRuleCommand::getBody() const throw() { + return d_body; +} + +const PropagateRuleCommand::Triggers& PropagateRuleCommand::getTriggers() const throw() { + return d_triggers; +} + +bool PropagateRuleCommand::isDeduction() const throw() { + return d_deduction; +} + +void PropagateRuleCommand::invoke(SmtEngine* smtEngine) throw() { + 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); + /** build heads list */ + Expr 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 { + /** 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)); + } + 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) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* PropagateRuleCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + /** Convert variables */ + VExpr vars; vars.reserve(d_vars.size()); + for(VExpr::iterator i = d_vars.begin(), end = d_vars.end(); + i == end; ++i){ + vars.push_back(i->exportTo(exprManager, variableMap)); + }; + /** Convert guards */ + VExpr guards; guards.reserve(d_guards.size()); + for(VExpr::iterator i = d_guards.begin(), end = d_guards.end(); + i == end; ++i){ + guards.push_back(i->exportTo(exprManager, variableMap)); + }; + /** Convert heads */ + VExpr heads; heads.reserve(d_heads.size()); + for(VExpr::iterator i = d_heads.begin(), end = d_heads.end(); + i == end; ++i){ + heads.push_back(i->exportTo(exprManager, variableMap)); + }; + /** Convert triggers */ + Triggers triggers; triggers.resize(d_triggers.size()); + for(size_t i = 0, end = d_triggers.size(); + i < end; ++i){ + triggers[i].reserve(d_triggers[i].size()); + for(VExpr::iterator j = d_triggers[i].begin(), jend = d_triggers[i].end(); + j == jend; ++i){ + triggers[i].push_back(j->exportTo(exprManager, variableMap)); + }; + }; + /** Convert head and body */ + Expr body = d_body.exportTo(exprManager, variableMap); + /** Create the converted rules */ + 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); +} + +std::string PropagateRuleCommand::getCommandName() const throw() { + 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"; + + case SMT_UNSATISFIABLE: + return out << "unsat"; + + case SMT_UNKNOWN: + return out << "unknown"; + + default: + return out << "BenchmarkStatus::[UNKNOWNSTATUS!]"; + } +} + +}/* CVC4 namespace */ |