diff options
Diffstat (limited to 'src/printer/tptp/tptp_printer.h')
| -rw-r--r-- | src/printer/tptp/tptp_printer.h | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/src/printer/tptp/tptp_printer.h b/src/printer/tptp/tptp_printer.h index 449fe409c..38a56bcb5 100644 --- a/src/printer/tptp/tptp_printer.h +++ b/src/printer/tptp/tptp_printer.h @@ -44,9 +44,21 @@ class TptpPrinter : public CVC4::Printer void toStream(std::ostream& out, const UnsatCore& core) const override; private: - void toStream(std::ostream& out, - const smt::Model& m, - const NodeCommand* c) const override; + /** + * To stream model sort. This prints the appropriate output for type + * tn declared via declare-sort or declare-datatype. + */ + void toStreamModelSort(std::ostream& out, + const smt::Model& m, + TypeNode tn) const override; + + /** + * To stream model term. This prints the appropriate output for term + * n declared via declare-fun. + */ + void toStreamModelTerm(std::ostream& out, + const smt::Model& m, + Node n) const override; }; /* class TptpPrinter */ |