summaryrefslogtreecommitdiff
path: root/src/expr/command.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/command.cpp')
-rw-r--r--src/expr/command.cpp135
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) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback