diff options
Diffstat (limited to 'src/expr/command.cpp')
| -rw-r--r-- | src/expr/command.cpp | 152 |
1 files changed, 152 insertions, 0 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 7d060186a..ba29b6c34 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -126,6 +126,10 @@ void EmptyCommand::invoke(SmtEngine* smtEngine) throw() { d_commandStatus = CommandSuccess::instance(); } +Command* EmptyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new EmptyCommand(d_name); +} + /* class AssertCommand */ AssertCommand::AssertCommand(const BoolExpr& e) throw() : @@ -145,6 +149,10 @@ void AssertCommand::invoke(SmtEngine* smtEngine) throw() { } } +Command* AssertCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new AssertCommand(d_expr.exportTo(exprManager, variableMap)); +} + /* class PushCommand */ void PushCommand::invoke(SmtEngine* smtEngine) throw() { @@ -156,6 +164,10 @@ void PushCommand::invoke(SmtEngine* smtEngine) throw() { } } +Command* PushCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new PushCommand; +} + /* class PopCommand */ void PopCommand::invoke(SmtEngine* smtEngine) throw() { @@ -173,6 +185,12 @@ CheckSatCommand::CheckSatCommand() throw() : d_expr() { } +Command* PopCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new PopCommand(); +} + +/* class CheckSatCommand */ + CheckSatCommand::CheckSatCommand(const BoolExpr& expr) throw() : d_expr(expr) { } @@ -202,6 +220,12 @@ void CheckSatCommand::printResult(std::ostream& out) const throw() { } } +Command* CheckSatCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + CheckSatCommand* c = new CheckSatCommand(d_expr.exportTo(exprManager, variableMap)); + c->d_result = d_result; + return c; +} + /* class QueryCommand */ QueryCommand::QueryCommand(const BoolExpr& e) throw() : @@ -233,6 +257,12 @@ void QueryCommand::printResult(std::ostream& out) const throw() { } } +Command* QueryCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + QueryCommand* c = new QueryCommand(d_expr.exportTo(exprManager, variableMap)); + c->d_result = d_result; + return c; +} + /* class QuitCommand */ QuitCommand::QuitCommand() throw() { @@ -243,6 +273,10 @@ void QuitCommand::invoke(SmtEngine* smtEngine) throw() { d_commandStatus = CommandSuccess::instance(); } +Command* QuitCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new QuitCommand(); +} + /* class CommentCommand */ CommentCommand::CommentCommand(std::string comment) throw() : d_comment(comment) { @@ -257,6 +291,10 @@ void CommentCommand::invoke(SmtEngine* smtEngine) throw() { d_commandStatus = CommandSuccess::instance(); } +Command* CommentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new CommentCommand(d_comment); +} + /* class CommandSequence */ CommandSequence::CommandSequence() throw() : @@ -299,6 +337,15 @@ CommandSequence::const_iterator CommandSequence::begin() const throw() { return d_commandSequence.begin(); } +Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + CommandSequence* seq = new CommandSequence(); + for(iterator i = begin(); i != end(); ++i) { + seq->addCommand((*i)->exportTo(exprManager, variableMap)); + } + seq->d_index = d_index; + return seq; +} + CommandSequence::const_iterator CommandSequence::end() const throw() { return d_commandSequence.end(); } @@ -338,6 +385,12 @@ void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() { Dump("declarations") << *this << endl; } +Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) { + return new DeclareFunctionCommand(d_symbol, + d_type.exportTo(exprManager, variableMap)); +} + /* class DeclareTypeCommand */ DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw() : @@ -358,6 +411,12 @@ void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() { Dump("declarations") << *this << endl; } +Command* DeclareTypeCommand::exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) { + return new DeclareTypeCommand(d_symbol, d_arity, + d_type.exportTo(exprManager, variableMap)); +} + /* class DefineTypeCommand */ DefineTypeCommand::DefineTypeCommand(const std::string& id, @@ -388,6 +447,14 @@ 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); +} + /* class DefineFunctionCommand */ DefineFunctionCommand::DefineFunctionCommand(const std::string& id, @@ -429,6 +496,15 @@ void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() { d_commandStatus = CommandSuccess::instance(); } +Command* DefineFunctionCommand::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 DefineFunctionCommand(d_symbol, func, formals, formula); +} + /* class DefineNamedFunctionCommand */ DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id, @@ -446,6 +522,15 @@ void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) throw() { 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); +} + /* class Simplify */ SimplifyCommand::SimplifyCommand(Expr term) throw() : @@ -473,6 +558,12 @@ void SimplifyCommand::printResult(std::ostream& out) const throw() { } } +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; +} + /* class GetValueCommand */ GetValueCommand::GetValueCommand(Expr term) throw() : @@ -505,6 +596,12 @@ void GetValueCommand::printResult(std::ostream& out) const throw() { } } +Command* GetValueCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetValueCommand* c = new GetValueCommand(d_term.exportTo(exprManager, variableMap)); + c->d_result = d_result.exportTo(exprManager, variableMap); + return c; +} + /* class GetAssignmentCommand */ GetAssignmentCommand::GetAssignmentCommand() throw() { @@ -531,6 +628,12 @@ void GetAssignmentCommand::printResult(std::ostream& out) const throw() { } } +Command* GetAssignmentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetAssignmentCommand* c = new GetAssignmentCommand; + c->d_result = d_result; + return c; +} + /* class GetProofCommand */ GetProofCommand::GetProofCommand() throw() { @@ -557,6 +660,12 @@ void GetProofCommand::printResult(std::ostream& out) const throw() { } } +Command* GetProofCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetProofCommand* c = new GetProofCommand; + c->d_result = d_result; + return c; +} + /* class GetAssertionsCommand */ GetAssertionsCommand::GetAssertionsCommand() throw() { @@ -586,6 +695,12 @@ void GetAssertionsCommand::printResult(std::ostream& out) const throw() { } } +Command* GetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetAssertionsCommand* c = new GetAssertionsCommand; + c->d_result = d_result; + return c; +} + /* class SetBenchmarkStatusCommand */ SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) throw() : @@ -608,6 +723,11 @@ void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() { } } +Command* SetBenchmarkStatusCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + SetBenchmarkStatusCommand* c = new SetBenchmarkStatusCommand(d_status); + return c; +} + /* class SetBenchmarkLogicCommand */ SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) throw() : @@ -627,6 +747,11 @@ void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) throw() { } } +Command* SetBenchmarkLogicCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + SetBenchmarkLogicCommand* c = new SetBenchmarkLogicCommand(d_logic); + return c; +} + /* class SetInfoCommand */ SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) throw() : @@ -653,6 +778,11 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() { } } +Command* SetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + SetInfoCommand* c = new SetInfoCommand(d_flag, d_sexpr); + return c; +} + /* class GetInfoCommand */ GetInfoCommand::GetInfoCommand(std::string flag) throw() : @@ -688,6 +818,12 @@ void GetInfoCommand::printResult(std::ostream& out) const throw() { } } +Command* GetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetInfoCommand* c = new GetInfoCommand(d_flag); + c->d_result = d_result; + return c; +} + /* class SetOptionCommand */ SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) throw() : @@ -714,6 +850,11 @@ void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() { } } +Command* SetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + SetOptionCommand* c = new SetOptionCommand(d_flag, d_sexpr); + return c; +} + /* class GetOptionCommand */ GetOptionCommand::GetOptionCommand(std::string flag) throw() : @@ -747,6 +888,12 @@ void GetOptionCommand::printResult(std::ostream& out) const throw() { } } +Command* GetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetOptionCommand* c = new GetOptionCommand(d_flag); + c->d_result = d_result; + return c; +} + /* class DatatypeDeclarationCommand */ DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() : @@ -768,6 +915,11 @@ void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() { d_commandStatus = CommandSuccess::instance(); } +Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + std::cout << "We currently do not support exportTo with Datatypes" << std::endl; + exit(1); + return NULL; +} /* output stream insertion operator for benchmark statuses */ std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) throw() { |