diff options
Diffstat (limited to 'src/expr/command.cpp')
-rw-r--r-- | src/expr/command.cpp | 135 |
1 files changed, 15 insertions, 120 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 8d6748e54..2783e8eaa 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -27,21 +27,26 @@ #include "smt/bad_option_exception.h" #include "util/output.h" #include "util/sexpr.h" +#include "expr/node.h" +#include "printer/printer.h" using namespace std; namespace CVC4 { std::ostream& operator<<(std::ostream& out, const Command& c) { - c.toStream(out); + c.toStream(out, + Node::setdepth::getDepth(out), + Node::printtypes::getPrintTypes(out), + Node::setlanguage::getLanguage(out)); return out; } -ostream& operator<<(ostream& out, const Command* command) { - if(command == NULL) { +ostream& operator<<(ostream& out, const Command* c) { + if(c == NULL) { out << "null"; } else { - command->toStream(out); + out << *c; } return out; } @@ -59,6 +64,11 @@ std::string Command::toString() const { return ss.str(); } +void Command::toStream(std::ostream& out, int toDepth, bool types, + OutputLanguage language) const { + Printer::getPrinter(language)->toStream(out, this, toDepth, types); +} + void Command::printResult(std::ostream& out) const { } @@ -72,10 +82,6 @@ void EmptyCommand::invoke(SmtEngine* smtEngine) { /* empty commands have no implementation */ } -void EmptyCommand::toStream(std::ostream& out) const { - out << "EmptyCommand(" << d_name << ")"; -} - /* class AssertCommand */ AssertCommand::AssertCommand(const BoolExpr& e) : @@ -86,30 +92,18 @@ void AssertCommand::invoke(SmtEngine* smtEngine) { smtEngine->assertFormula(d_expr); } -void AssertCommand::toStream(std::ostream& out) const { - out << "Assert(" << d_expr << ")"; -} - /* class PushCommand */ void PushCommand::invoke(SmtEngine* smtEngine) { smtEngine->push(); } -void PushCommand::toStream(std::ostream& out) const { - out << "Push()"; -} - /* class PopCommand */ void PopCommand::invoke(SmtEngine* smtEngine) { smtEngine->pop(); } -void PopCommand::toStream(std::ostream& out) const { - out << "Pop()"; -} - /* class CheckSatCommand */ CheckSatCommand::CheckSatCommand(const BoolExpr& expr) : @@ -120,14 +114,6 @@ void CheckSatCommand::invoke(SmtEngine* smtEngine) { d_result = smtEngine->checkSat(d_expr); } -void CheckSatCommand::toStream(std::ostream& out) const { - if(d_expr.isNull()) { - out << "CheckSat()"; - } else { - out << "CheckSat(" << d_expr << ")"; - } -} - Result CheckSatCommand::getResult() const { return d_result; } @@ -154,19 +140,11 @@ void QueryCommand::printResult(std::ostream& out) const { out << d_result << endl; } -void QueryCommand::toStream(std::ostream& out) const { - out << "Query(" << d_expr << ')'; -} - /* class QuitCommand */ QuitCommand::QuitCommand() { } -void QuitCommand::toStream(std::ostream& out) const { - out << "Quit()" << endl; -} - /* class CommandSequence */ CommandSequence::CommandSequence() : @@ -197,14 +175,6 @@ void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) { } } -void CommandSequence::toStream(std::ostream& out) const { - out << "CommandSequence[" << endl; - for(unsigned i = d_index; i < d_commandSequence.size(); ++i) { - out << *d_commandSequence[i] << endl; - } - out << "]"; -} - /* class DeclarationCommand */ DeclarationCommand::DeclarationCommand(const std::string& id, Type t) : @@ -225,14 +195,6 @@ Type DeclarationCommand::getDeclaredType() const { return d_type; } -void DeclarationCommand::toStream(std::ostream& out) const { - out << "Declare(["; - copy( d_declaredSymbols.begin(), d_declaredSymbols.end() - 1, - ostream_iterator<string>(out, ", ") ); - out << d_declaredSymbols.back(); - out << "])"; -} - /* class DefineFunctionCommand */ DefineFunctionCommand::DefineFunctionCommand(Expr func, @@ -247,16 +209,6 @@ void DefineFunctionCommand::invoke(SmtEngine* smtEngine) { smtEngine->defineFunction(d_func, d_formals, d_formula); } -void DefineFunctionCommand::toStream(std::ostream& out) const { - out << "DefineFunction( \"" << d_func << "\", ["; - if(d_formals.size() > 0) { - copy( d_formals.begin(), d_formals.end() - 1, - ostream_iterator<Expr>(out, ", ") ); - out << d_formals.back(); - } - out << "], << " << d_formula << " >> )"; -} - /* class DefineFunctionCommand */ DefineNamedFunctionCommand::DefineNamedFunctionCommand(Expr func, @@ -273,12 +225,6 @@ void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) { } } -void DefineNamedFunctionCommand::toStream(std::ostream& out) const { - out << "DefineNamedFunction( "; - this->DefineFunctionCommand::toStream(out); - out << " )"; -} - /* class Simplify */ SimplifyCommand::SimplifyCommand(Expr term) : @@ -286,7 +232,7 @@ SimplifyCommand::SimplifyCommand(Expr term) : } void SimplifyCommand::invoke(SmtEngine* smtEngine) { -#warning TODO: what is this + d_result = smtEngine->simplify(d_term); } Expr SimplifyCommand::getResult() const { @@ -297,10 +243,6 @@ void SimplifyCommand::printResult(std::ostream& out) const { out << d_result << endl; } -void SimplifyCommand::toStream(std::ostream& out) const { - out << "Simplify( << " << d_term << " >> )"; -} - /* class GetValueCommand */ GetValueCommand::GetValueCommand(Expr term) : @@ -320,10 +262,6 @@ void GetValueCommand::printResult(std::ostream& out) const { out << d_result << endl; } -void GetValueCommand::toStream(std::ostream& out) const { - out << "GetValue( << " << d_term << " >> )"; -} - /* class GetAssignmentCommand */ GetAssignmentCommand::GetAssignmentCommand() { @@ -341,10 +279,6 @@ void GetAssignmentCommand::printResult(std::ostream& out) const { out << d_result << endl; } -void GetAssignmentCommand::toStream(std::ostream& out) const { - out << "GetAssignment()"; -} - /* class GetAssertionsCommand */ GetAssertionsCommand::GetAssertionsCommand() { @@ -365,10 +299,6 @@ void GetAssertionsCommand::printResult(std::ostream& out) const { out << d_result; } -void GetAssertionsCommand::toStream(std::ostream& out) const { - out << "GetAssertions()"; -} - /* class SetBenchmarkStatusCommand */ SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) : @@ -390,10 +320,6 @@ void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) { } } -void SetBenchmarkStatusCommand::toStream(std::ostream& out) const { - out << "SetBenchmarkStatus(" << d_status << ")"; -} - /* class SetBenchmarkLogicCommand */ SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) : @@ -409,10 +335,6 @@ void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) { } } -void SetBenchmarkLogicCommand::toStream(std::ostream& out) const { - out << "SetBenchmarkLogic(" << d_logic << ")"; -} - /* class SetInfoCommand */ SetInfoCommand::SetInfoCommand(std::string flag, SExpr& sexpr) : @@ -441,10 +363,6 @@ void SetInfoCommand::printResult(std::ostream& out) const { } } -void SetInfoCommand::toStream(std::ostream& out) const { - out << "SetInfo(" << d_flag << ", " << d_sexpr << ")"; -} - /* class GetInfoCommand */ GetInfoCommand::GetInfoCommand(std::string flag) : @@ -471,10 +389,6 @@ void GetInfoCommand::printResult(std::ostream& out) const { } } -void GetInfoCommand::toStream(std::ostream& out) const { - out << "GetInfo(" << d_flag << ")"; -} - /* class SetOptionCommand */ SetOptionCommand::SetOptionCommand(std::string flag, SExpr& sexpr) : @@ -503,10 +417,6 @@ void SetOptionCommand::printResult(std::ostream& out) const { } } -void SetOptionCommand::toStream(std::ostream& out) const { - out << "SetOption(" << d_flag << ", " << d_sexpr << ")"; -} - /* class GetOptionCommand */ GetOptionCommand::GetOptionCommand(std::string flag) : @@ -531,10 +441,6 @@ void GetOptionCommand::printResult(std::ostream& out) const { } } -void GetOptionCommand::toStream(std::ostream& out) const { - out << "GetOption(" << d_flag << ")"; -} - /* class DatatypeDeclarationCommand */ DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) : @@ -553,17 +459,6 @@ void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) { //smtEngine->addDatatypeDefinitions(d_datatype); } -void DatatypeDeclarationCommand::toStream(std::ostream& out) const { - out << "DatatypeDeclarationCommand(["; - for(vector<DatatypeType>::const_iterator i = d_datatypes.begin(), - i_end = d_datatypes.end(); - i != i_end; - ++i) { - out << *i << ";" << endl; - } - out << "])"; -} - /* output stream insertion operator for benchmark statuses */ std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) { |