diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-03-09 21:10:17 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-03-09 21:10:17 +0000 |
commit | 84f26af22566f7c10dea45b399b944cb50b5e317 (patch) | |
tree | 68fbe22665cc09f46c321c6132e49dabbc15c337 /src/expr/command.cpp | |
parent | f29ea80fb3e238278a721d79077c9087bccbac0b (diff) |
Some work on the dump infrastructure to support portfolio work.
Dump("foo") << FooCommand(...);
now "dumps" the textual representation of the command (in the current
output language) to a file, IF dumping is on at configure-time, AND the
"muzzle" feature is off, AND the "foo" flag is turned on for the dump
stream during this run.
If it's a portfolio build, the above will also store the command in a
CommandSequence, IF the "foo" flag is turned on for the dump stream
during this run. This is done even if the muzzle is on.
This commit also cleans up some code that used the dump feature (in arrays,
particularly).
Diffstat (limited to 'src/expr/command.cpp')
-rw-r--r-- | src/expr/command.cpp | 166 |
1 files changed, 147 insertions, 19 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 3dac28e11..48b6940dd 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -27,6 +27,7 @@ #include "smt/smt_engine.h" #include "smt/bad_option_exception.h" #include "util/output.h" +#include "util/dump.h" #include "util/sexpr.h" #include "expr/node.h" #include "printer/printer.h" @@ -134,6 +135,10 @@ Command* EmptyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollecti return new EmptyCommand(d_name); } +Command* EmptyCommand::clone() const { + return new EmptyCommand(d_name); +} + /* class AssertCommand */ AssertCommand::AssertCommand(const BoolExpr& e) throw() : @@ -157,6 +162,10 @@ Command* AssertCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollect return new AssertCommand(d_expr.exportTo(exprManager, variableMap)); } +Command* AssertCommand::clone() const { + return new AssertCommand(d_expr); +} + /* class PushCommand */ void PushCommand::invoke(SmtEngine* smtEngine) throw() { @@ -169,7 +178,11 @@ void PushCommand::invoke(SmtEngine* smtEngine) throw() { } Command* PushCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new PushCommand; + return new PushCommand(); +} + +Command* PushCommand::clone() const { + return new PushCommand(); } /* class PopCommand */ @@ -193,6 +206,10 @@ Command* PopCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection return new PopCommand(); } +Command* PopCommand::clone() const { + return new PopCommand(); +} + /* class CheckSatCommand */ CheckSatCommand::CheckSatCommand(const BoolExpr& expr) throw() : @@ -230,6 +247,12 @@ Command* CheckSatCommand::exportTo(ExprManager* exprManager, ExprManagerMapColle return c; } +Command* CheckSatCommand::clone() const { + CheckSatCommand* c = new CheckSatCommand(d_expr); + c->d_result = d_result; + return c; +} + /* class QueryCommand */ QueryCommand::QueryCommand(const BoolExpr& e) throw() : @@ -267,6 +290,12 @@ Command* QueryCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollecti return c; } +Command* QueryCommand::clone() const { + QueryCommand* c = new QueryCommand(d_expr); + c->d_result = d_result; + return c; +} + /* class QuitCommand */ QuitCommand::QuitCommand() throw() { @@ -281,6 +310,10 @@ Command* QuitCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollectio return new QuitCommand(); } +Command* QuitCommand::clone() const { + return new QuitCommand(); +} + /* class CommentCommand */ CommentCommand::CommentCommand(std::string comment) throw() : d_comment(comment) { @@ -299,6 +332,10 @@ Command* CommentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollec return new CommentCommand(d_comment); } +Command* CommentCommand::clone() const { + return new CommentCommand(d_comment); +} + /* class CommandSequence */ CommandSequence::CommandSequence() throw() : @@ -315,6 +352,10 @@ 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); @@ -350,6 +391,15 @@ Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapColle 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::end() const throw() { return d_commandSequence.end(); } @@ -386,7 +436,7 @@ Type DeclareFunctionCommand::getType() const throw() { } void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() { - Dump("declarations") << *this << endl; + Dump("declarations") << *this; } Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager, @@ -395,6 +445,10 @@ Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager, d_type.exportTo(exprManager, variableMap)); } +Command* DeclareFunctionCommand::clone() const { + return new DeclareFunctionCommand(d_symbol, d_type); +} + /* class DeclareTypeCommand */ DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw() : @@ -412,7 +466,7 @@ Type DeclareTypeCommand::getType() const throw() { } void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() { - Dump("declarations") << *this << endl; + Dump("declarations") << *this; } Command* DeclareTypeCommand::exportTo(ExprManager* exprManager, @@ -421,6 +475,10 @@ Command* DeclareTypeCommand::exportTo(ExprManager* exprManager, d_type.exportTo(exprManager, variableMap)); } +Command* DeclareTypeCommand::clone() const { + return new DeclareTypeCommand(d_symbol, d_arity, d_type); +} + /* class DefineTypeCommand */ DefineTypeCommand::DefineTypeCommand(const std::string& id, @@ -447,7 +505,7 @@ Type DefineTypeCommand::getType() const throw() { } void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() { - Dump("declarations") << *this << endl; + Dump("declarations") << *this; d_commandStatus = CommandSuccess::instance(); } @@ -459,6 +517,10 @@ Command* DefineTypeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCol return new DefineTypeCommand(d_symbol, params, type); } +Command* DefineTypeCommand::clone() const { + return new DefineTypeCommand(d_symbol, d_params, d_type); +} + /* class DefineFunctionCommand */ DefineFunctionCommand::DefineFunctionCommand(const std::string& id, @@ -493,7 +555,7 @@ Expr DefineFunctionCommand::getFormula() const throw() { } void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() { - //Dump("declarations") << *this << endl; -- done by SmtEngine + //Dump("declarations") << *this; -- done by SmtEngine try { if(!d_func.isNull()) { smtEngine->defineFunction(d_func, d_formals, d_formula); @@ -513,6 +575,10 @@ Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMa return new DefineFunctionCommand(d_symbol, func, formals, formula); } +Command* DefineFunctionCommand::clone() const { + return new DefineFunctionCommand(d_symbol, d_func, d_formals, d_formula); +} + /* class DefineNamedFunctionCommand */ DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id, @@ -539,6 +605,10 @@ Command* DefineNamedFunctionCommand::exportTo(ExprManager* exprManager, ExprMana return new DefineNamedFunctionCommand(d_symbol, func, formals, formula); } +Command* DefineNamedFunctionCommand::clone() const { + return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula); +} + /* class Simplify */ SimplifyCommand::SimplifyCommand(Expr term) throw() : @@ -572,6 +642,12 @@ Command* SimplifyCommand::exportTo(ExprManager* exprManager, ExprManagerMapColle return c; } +Command* SimplifyCommand::clone() const { + SimplifyCommand* c = new SimplifyCommand(d_term); + c->d_result = d_result; + return c; +} + /* class GetValueCommand */ GetValueCommand::GetValueCommand(Expr term) throw() : @@ -610,6 +686,12 @@ Command* GetValueCommand::exportTo(ExprManager* exprManager, ExprManagerMapColle return c; } +Command* GetValueCommand::clone() const { + GetValueCommand* c = new GetValueCommand(d_term); + c->d_result = d_result; + return c; +} + /* class GetAssignmentCommand */ GetAssignmentCommand::GetAssignmentCommand() throw() { @@ -637,7 +719,13 @@ void GetAssignmentCommand::printResult(std::ostream& out) const throw() { } Command* GetAssignmentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetAssignmentCommand* c = new GetAssignmentCommand; + 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; } @@ -669,7 +757,13 @@ void GetProofCommand::printResult(std::ostream& out) const throw() { } Command* GetProofCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetProofCommand* c = new GetProofCommand; + 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; } @@ -704,7 +798,13 @@ void GetAssertionsCommand::printResult(std::ostream& out) const throw() { } Command* GetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetAssertionsCommand* c = new GetAssertionsCommand; + 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; } @@ -732,8 +832,11 @@ void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() { } Command* SetBenchmarkStatusCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - SetBenchmarkStatusCommand* c = new SetBenchmarkStatusCommand(d_status); - return c; + return new SetBenchmarkStatusCommand(d_status); +} + +Command* SetBenchmarkStatusCommand::clone() const { + return new SetBenchmarkStatusCommand(d_status); } /* class SetBenchmarkLogicCommand */ @@ -756,8 +859,11 @@ void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) throw() { } Command* SetBenchmarkLogicCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - SetBenchmarkLogicCommand* c = new SetBenchmarkLogicCommand(d_logic); - return c; + return new SetBenchmarkLogicCommand(d_logic); +} + +Command* SetBenchmarkLogicCommand::clone() const { + return new SetBenchmarkLogicCommand(d_logic); } /* class SetInfoCommand */ @@ -787,8 +893,11 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() { } Command* SetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - SetInfoCommand* c = new SetInfoCommand(d_flag, d_sexpr); - return c; + return new SetInfoCommand(d_flag, d_sexpr); +} + +Command* SetInfoCommand::clone() const { + return new SetInfoCommand(d_flag, d_sexpr); } /* class GetInfoCommand */ @@ -832,6 +941,12 @@ Command* GetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollec return c; } +Command* GetInfoCommand::clone() const { + GetInfoCommand* c = new GetInfoCommand(d_flag); + c->d_result = d_result; + return c; +} + /* class SetOptionCommand */ SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) throw() : @@ -859,8 +974,11 @@ void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() { } Command* SetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - SetOptionCommand* c = new SetOptionCommand(d_flag, d_sexpr); - return c; + return new SetOptionCommand(d_flag, d_sexpr); +} + +Command* SetOptionCommand::clone() const { + return new SetOptionCommand(d_flag, d_sexpr); } /* class GetOptionCommand */ @@ -902,6 +1020,12 @@ Command* GetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapColl return c; } +Command* GetOptionCommand::clone() const { + GetOptionCommand* c = new GetOptionCommand(d_flag); + c->d_result = d_result; + return c; +} + /* class DatatypeDeclarationCommand */ DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() : @@ -919,15 +1043,19 @@ DatatypeDeclarationCommand::getDatatypes() const throw() { } void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() { - Dump("declarations") << *this << endl; + Dump("declarations") << *this; 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); + Warning() << "We currently do not support exportTo with Datatypes" << std::endl; return NULL; } + +Command* DatatypeDeclarationCommand::clone() const { + return new DatatypeDeclarationCommand(d_datatypes); +} + /* output stream insertion operator for benchmark statuses */ std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) throw() { |