summaryrefslogtreecommitdiff
path: root/src/printer/ast/ast_printer.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/printer/ast/ast_printer.h')
-rw-r--r--src/printer/ast/ast_printer.h16
1 files changed, 15 insertions, 1 deletions
diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h
index e4251eba0..e0bc7b6bf 100644
--- a/src/printer/ast/ast_printer.h
+++ b/src/printer/ast/ast_printer.h
@@ -24,6 +24,9 @@
#include "printer/printer.h"
namespace CVC4 {
+
+class LetBinding;
+
namespace printer {
namespace ast {
@@ -162,7 +165,10 @@ class AstPrinter : public CVC4::Printer
std::ostream& out, const std::vector<Command*>& sequence) const override;
private:
- void toStream(std::ostream& out, TNode n, int toDepth) const;
+ void toStream(std::ostream& out,
+ TNode n,
+ int toDepth,
+ LetBinding* lbind = nullptr) const;
/**
* To stream model sort. This prints the appropriate output for type
* tn declared via declare-sort or declare-datatype.
@@ -178,6 +184,14 @@ class AstPrinter : 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 toStreamWithLetify(std::ostream& out,
+ Node n,
+ int toDepth,
+ LetBinding* lbind) const;
}; /* class AstPrinter */
} // namespace ast
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback