diff options
Diffstat (limited to 'src/smt/command.cpp')
| -rw-r--r-- | src/smt/command.cpp | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 717d423fe..154166eb7 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1091,6 +1091,8 @@ void DeclareFunctionCommand::setPrintInModel(bool p) void DeclareFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm) { + // mark that it will be printed in the model + sm->addModelDeclarationTerm(d_func); d_commandStatus = CommandSuccess::instance(); } @@ -1132,6 +1134,8 @@ size_t DeclareSortCommand::getArity() const { return d_arity; } api::Sort DeclareSortCommand::getSort() const { return d_sort; } void DeclareSortCommand::invoke(api::Solver* solver, SymbolManager* sm) { + // mark that it will be printed in the model + sm->addModelDeclarationSort(d_sort); d_commandStatus = CommandSuccess::instance(); } @@ -1150,8 +1154,8 @@ void DeclareSortCommand::toStream(std::ostream& out, size_t dag, OutputLanguage language) const { - Printer::getPrinter(language)->toStreamCmdDeclareType( - out, d_sort.toString(), d_arity, d_sort.getTypeNode()); + Printer::getPrinter(language)->toStreamCmdDeclareType(out, + d_sort.getTypeNode()); } /* -------------------------------------------------------------------------- */ @@ -1693,6 +1697,18 @@ void GetModelCommand::invoke(api::Solver* solver, SymbolManager* sm) try { d_result = solver->getSmtEngine()->getModel(); + // set the model declarations, which determines what is printed in the model + d_result->clearModelDeclarations(); + std::vector<api::Sort> declareSorts = sm->getModelDeclareSorts(); + for (const api::Sort& s : declareSorts) + { + d_result->addDeclarationSort(s.getTypeNode()); + } + std::vector<api::Term> declareTerms = sm->getModelDeclareTerms(); + for (const api::Term& t : declareTerms) + { + d_result->addDeclarationTerm(t.getNode()); + } d_commandStatus = CommandSuccess::instance(); } catch (RecoverableModalException& e) |