diff options
Diffstat (limited to 'src/printer/printer.cpp')
| -rw-r--r-- | src/printer/printer.cpp | 30 |
1 files changed, 22 insertions, 8 deletions
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index b24025124..7225721c0 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -74,18 +74,34 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang) void Printer::toStream(std::ostream& out, const smt::Model& m) const { - for(size_t i = 0; i < m.getNumCommands(); ++i) { - const NodeCommand* cmd = m.getCommand(i); - const DeclareFunctionNodeCommand* dfc = - dynamic_cast<const DeclareFunctionNodeCommand*>(cmd); - if (dfc != NULL && !m.isModelCoreSymbol(dfc->getFunction())) + // print the declared sorts + const std::vector<TypeNode>& dsorts = m.getDeclaredSorts(); + for (const TypeNode& tn : dsorts) + { + toStreamModelSort(out, m, tn); + } + + // print the declared terms + const std::vector<Node>& dterms = m.getDeclaredTerms(); + for (const Node& n : dterms) + { + // take into account model core, independently of the format + if (!m.isModelCoreSymbol(n)) { continue; } - toStream(out, m, cmd); + toStreamModelTerm(out, m, n); } + }/* Printer::toStream(Model) */ +void Printer::toStreamUsing(OutputLanguage lang, + std::ostream& out, + const smt::Model& m) const +{ + getPrinter(lang)->toStream(out, m); +} + void Printer::toStream(std::ostream& out, const UnsatCore& core) const { for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) { @@ -160,8 +176,6 @@ void Printer::toStreamCmdDeclareFunction(std::ostream& out, } void Printer::toStreamCmdDeclareType(std::ostream& out, - const std::string& id, - size_t arity, TypeNode type) const { printUnknownCommand(out, "declare-sort"); |