From 446cba594a8b26c03aabb2385b18c2ccad637f2f Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sat, 6 Jul 2013 20:32:48 -0400 Subject: [PATCH] Model output is now const; this related to bug 519 --- src/printer/ast/ast_printer.cpp | 4 ++-- src/printer/ast/ast_printer.h | 4 ++-- src/printer/cvc/cvc_printer.cpp | 4 ++-- src/printer/cvc/cvc_printer.h | 2 +- src/printer/printer.cpp | 2 +- src/printer/printer.h | 4 ++-- src/printer/smt1/smt1_printer.cpp | 4 ++-- src/printer/smt1/smt1_printer.h | 4 ++-- src/printer/smt2/smt2_printer.cpp | 6 +++--- src/printer/smt2/smt2_printer.h | 4 ++-- src/smt/smt_engine.cpp | 13 ++++--------- src/smt/smt_engine.h | 4 ++-- src/util/util_model.cpp | 2 +- src/util/util_model.h | 6 ++++-- 14 files changed, 30 insertions(+), 33 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(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(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(); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index fbe442207..4ee00161f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3166,7 +3166,7 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log return quickCheck().asValidityResult(); } -Node SmtEngine::postprocess(TNode node, TypeNode expectedType) { +Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const { ModelPostprocessor mpost; NodeVisitor visitor; Node value = visitor.run(mpost, node); @@ -3221,7 +3221,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L return n.toExpr(); } -Expr SmtEngine::getValue(const Expr& ex) throw(ModalException, TypeCheckingException, LogicException) { +Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckingException, LogicException) { Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); @@ -3448,13 +3448,8 @@ void SmtEngine::checkModel(bool hardFailure) { // Check individual theory assertions d_theoryEngine->checkTheoryAssertionsWithModel(); - if(Notice.isOn()) { - // This operator<< routine is non-const (i.e., takes a non-const Model&). - // This confuses the Notice() output routines, so extract the ostream - // from it and output it "manually." Should be fixed by making Model - // accessors const. - Notice.getStream() << *m; - } + // Output the model + Notice() << *m; // We have a "fake context" for the substitution map (we don't need it // to be context-dependent) diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 1b5af415f..a45fe3383 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -249,7 +249,7 @@ class CVC4_PUBLIC SmtEngine { * like turning datatypes back into tuples, length-1-bitvectors back * into booleans, etc. */ - Node postprocess(TNode n, TypeNode expectedType); + Node postprocess(TNode n, TypeNode expectedType) const; /** * This is something of an "init" procedure, but is idempotent; call @@ -444,7 +444,7 @@ public: * by a SAT or INVALID query). Only permitted if the SmtEngine is * set to operate interactively and produce-models is on. */ - Expr getValue(const Expr& e) throw(ModalException, TypeCheckingException, LogicException); + Expr getValue(const Expr& e) const throw(ModalException, TypeCheckingException, LogicException); /** * Add a function to the set of expressions whose value is to be diff --git a/src/util/util_model.cpp b/src/util/util_model.cpp index ab4c95ea5..1c2dc2edf 100644 --- a/src/util/util_model.cpp +++ b/src/util/util_model.cpp @@ -24,7 +24,7 @@ using namespace std; namespace CVC4 { -std::ostream& operator<<(std::ostream& out, Model& m) { +std::ostream& operator<<(std::ostream& out, const Model& m) { smt::SmtScope smts(&m.d_smt); Expr::dag::Scope scope(out, false); Printer::getPrinter(options::outputLanguage())->toStream(out, m); diff --git a/src/util/util_model.h b/src/util/util_model.h index 535493a2d..365e7124d 100644 --- a/src/util/util_model.h +++ b/src/util/util_model.h @@ -29,10 +29,10 @@ class Command; class SmtEngine; class Model; -std::ostream& operator<<(std::ostream&, Model&); +std::ostream& operator<<(std::ostream&, const Model&); class Model { - friend std::ostream& operator<<(std::ostream&, Model&); + friend std::ostream& operator<<(std::ostream&, const Model&); protected: /** The SmtEngine we're associated with */ @@ -50,6 +50,8 @@ public: const Command* getCommand(size_t i) const; /** get the smt engine that this model is hooked up to */ SmtEngine* getSmtEngine() { return &d_smt; } + /** get the smt engine (as a pointer-to-const) that this model is hooked up to */ + const SmtEngine* getSmtEngine() const { return &d_smt; } public: /** get value for expression */ -- 2.30.2