diff options
Diffstat (limited to 'src/printer/cvc/cvc_printer.h')
| -rw-r--r-- | src/printer/cvc/cvc_printer.h | 21 |
1 files changed, 20 insertions, 1 deletions
diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h index b0328bc3c..799bba8d2 100644 --- a/src/printer/cvc/cvc_printer.h +++ b/src/printer/cvc/cvc_printer.h @@ -24,6 +24,9 @@ #include "printer/printer.h" namespace CVC4 { + +class LetBinding; + namespace printer { namespace cvc { @@ -163,7 +166,14 @@ class CvcPrinter : public CVC4::Printer std::ostream& out, const std::vector<Command*>& sequence) const override; private: - void toStream(std::ostream& out, TNode n, int toDepth, bool bracket) const; + /** + * The main method for printing Nodes. + */ + void toStreamNode(std::ostream& out, + TNode n, + int toDepth, + bool bracket, + LetBinding* lbind) const; /** * To stream model sort. This prints the appropriate output for type * tn declared via declare-sort or declare-datatype. @@ -179,6 +189,15 @@ class CvcPrinter : public CVC4::Printer void toStreamModelTerm(std::ostream& out, const smt::Model& m, Node n) const override; + /** + * To stream with let binding. This prints n, possibly in the scope + * of letification generated by this method based on lbind. + */ + void toStreamNodeWithLetify(std::ostream& out, + Node n, + int toDepth, + bool bracket, + LetBinding* lbind) const; bool d_cvc3Mode; }; /* class CvcPrinter */ |