diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-07-06 20:32:48 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-07-06 20:50:16 -0400 |
commit | 446cba594a8b26c03aabb2385b18c2ccad637f2f (patch) | |
tree | ae7cb8132f19562cdcd8340d579aaf1384a6d2d7 /src/printer | |
parent | 7e1aae3dc746f4b7df2f65fb373ffc26e1a0498a (diff) |
Model output is now const; this related to bug 519
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/ast/ast_printer.cpp | 4 | ||||
-rw-r--r-- | src/printer/ast/ast_printer.h | 4 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 4 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.h | 2 | ||||
-rw-r--r-- | src/printer/printer.cpp | 2 | ||||
-rw-r--r-- | src/printer/printer.h | 4 | ||||
-rw-r--r-- | src/printer/smt1/smt1_printer.cpp | 4 | ||||
-rw-r--r-- | src/printer/smt1/smt1_printer.h | 4 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 6 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 4 |
10 files changed, 19 insertions, 19 deletions
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 57462c9f7..88c769f26 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -185,11 +185,11 @@ void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw }/* AstPrinter::toStream(CommandStatus*) */ -void AstPrinter::toStream(std::ostream& out, Model& m) const throw() { +void AstPrinter::toStream(std::ostream& out, const Model& m) const throw() { out << "Model()"; } -void AstPrinter::toStream(std::ostream& out, Model& m, const Command* c) const throw() { +void AstPrinter::toStream(std::ostream& out, const Model& m, const Command* c) const throw() { // shouldn't be called; only the non-Command* version above should be Unreachable(); } diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h index c9ee6071d..f09de9d00 100644 --- a/src/printer/ast/ast_printer.h +++ b/src/printer/ast/ast_printer.h @@ -29,13 +29,13 @@ namespace ast { class AstPrinter : public CVC4::Printer { void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw(); - void toStream(std::ostream& out, Model& m, const Command* c) const throw(); + void toStream(std::ostream& out, const Model& m, const Command* c) const throw(); public: using CVC4::Printer::toStream; void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const CommandStatus* s) const throw(); - void toStream(std::ostream& out, Model& m) const throw(); + void toStream(std::ostream& out, const Model& m) const throw(); };/* class AstPrinter */ }/* CVC4::printer::ast namespace */ diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 23c4727f3..513ff7276 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -813,8 +813,8 @@ void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw }/* CvcPrinter::toStream(CommandStatus*) */ -void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const throw() { - theory::TheoryModel& tm = (theory::TheoryModel&) m; +void CvcPrinter::toStream(std::ostream& out, const Model& m, const Command* c) const throw() { + const theory::TheoryModel& tm = (const theory::TheoryModel&) m; if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) { TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() ); if( options::modelUninterpDtEnum() && tn.isSort() && diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h index 49b70b012..15b04488d 100644 --- a/src/printer/cvc/cvc_printer.h +++ b/src/printer/cvc/cvc_printer.h @@ -29,7 +29,7 @@ namespace cvc { class CvcPrinter : public CVC4::Printer { void toStream(std::ostream& out, TNode n, int toDepth, bool types, bool bracket) const throw(); - void toStream(std::ostream& out, Model& m, const Command* c) const throw(); + void toStream(std::ostream& out, const Model& m, const Command* c) const throw(); public: using CVC4::Printer::toStream; void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw(); diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 2a10ae451..344cbfe8c 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -125,7 +125,7 @@ void Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() { } }/* Printer::toStream(SExpr) */ -void Printer::toStream(std::ostream& out, Model& m) const throw() { +void Printer::toStream(std::ostream& out, const Model& m) const throw() { for(size_t i = 0; i < m.getNumCommands(); ++i) { toStream(out, m, m.getCommand(i)); } diff --git a/src/printer/printer.h b/src/printer/printer.h index 48a041d6a..5198a6ef1 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -43,7 +43,7 @@ protected: Printer() throw() {} /** write model response to command */ - virtual void toStream(std::ostream& out, Model& m, const Command* c) const throw() = 0; + virtual void toStream(std::ostream& out, const Model& m, const Command* c) const throw() = 0; public: /** Get the Printer for a given OutputLanguage */ @@ -79,7 +79,7 @@ public: virtual void toStream(std::ostream& out, const Result& r) const throw(); /** Write a Model out to a stream with this Printer. */ - virtual void toStream(std::ostream& out, Model& m) const throw(); + virtual void toStream(std::ostream& out, const Model& m) const throw(); };/* class Printer */ diff --git a/src/printer/smt1/smt1_printer.cpp b/src/printer/smt1/smt1_printer.cpp index f62709988..c5c491cc0 100644 --- a/src/printer/smt1/smt1_printer.cpp +++ b/src/printer/smt1/smt1_printer.cpp @@ -49,11 +49,11 @@ void Smt1Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr); }/* Smt1Printer::toStream() */ -void Smt1Printer::toStream(std::ostream& out, Model& m) const throw() { +void Smt1Printer::toStream(std::ostream& out, const Model& m) const throw() { Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, m); } -void Smt1Printer::toStream(std::ostream& out, Model& m, const Command* c) const throw() { +void Smt1Printer::toStream(std::ostream& out, const Model& m, const Command* c) const throw() { // shouldn't be called; only the non-Command* version above should be Unreachable(); } diff --git a/src/printer/smt1/smt1_printer.h b/src/printer/smt1/smt1_printer.h index 185d23699..9faf76cc0 100644 --- a/src/printer/smt1/smt1_printer.h +++ b/src/printer/smt1/smt1_printer.h @@ -28,14 +28,14 @@ namespace printer { namespace smt1 { class Smt1Printer : public CVC4::Printer { - void toStream(std::ostream& out, Model& m, const Command* c) const throw(); + void toStream(std::ostream& out, const Model& m, const Command* c) const throw(); public: using CVC4::Printer::toStream; void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const CommandStatus* s) const throw(); void toStream(std::ostream& out, const SExpr& sexpr) const throw(); - void toStream(std::ostream& out, Model& m) const throw(); + void toStream(std::ostream& out, const Model& m) const throw(); };/* class Smt1Printer */ }/* CVC4::printer::smt1 namespace */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index ae787f42f..1ab364f0c 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -606,15 +606,15 @@ void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const thro }/* Smt2Printer::toStream(CommandStatus*) */ -void Smt2Printer::toStream(std::ostream& out, Model& m) const throw() { +void Smt2Printer::toStream(std::ostream& out, const Model& m) const throw() { out << "(model" << std::endl; this->Printer::toStream(out, m); out << ")" << std::endl; } -void Smt2Printer::toStream(std::ostream& out, Model& m, const Command* c) const throw() { - theory::TheoryModel& tm = (theory::TheoryModel&) m; +void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c) const throw() { + const theory::TheoryModel& tm = (const theory::TheoryModel&) m; if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) { TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() ); if( options::modelUninterpDtEnum() && tn.isSort() && diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 76ec39258..871b3823a 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -29,8 +29,8 @@ namespace smt2 { class Smt2Printer : public CVC4::Printer { void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw(); - void toStream(std::ostream& out, Model& m, const Command* c) const throw(); - void toStream(std::ostream& out, Model& m) const throw(); + void toStream(std::ostream& out, const Model& m, const Command* c) const throw(); + void toStream(std::ostream& out, const Model& m) const throw(); public: using CVC4::Printer::toStream; void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw(); |