From 5ab1afe5c2e451f5d35f52867b1d58b69a4c85be Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 18 Nov 2023 09:53:20 -0800
Subject: [PATCH] expose enode pp convenciences

---
 src/smt/smt_context.h | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index f9560cb01..4feeae1b5 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -61,9 +61,16 @@ Revision History:
 namespace smt {
 
     class model_generator;
+    class context;
 
     struct cancel_exception {};
 
+    struct enode_pp {
+        context const& ctx;
+        enode*   n;
+        enode_pp(enode* n, context const& ctx): ctx(ctx), n(n) {}
+    };
+
     class context {
         friend class model_generator;
         friend class lookahead;
@@ -1368,6 +1375,8 @@ namespace smt {
 
         void display_asserted_formulas(std::ostream & out) const;
 
+        enode_pp pp(enode* n) { return enode_pp(n, *this); }
+
         std::ostream& display_literal(std::ostream & out, literal l) const;
 
         std::ostream& display_detailed_literal(std::ostream & out, literal l) const { return smt::display(out, l, m, m_bool_var2expr.data()); }
@@ -1844,11 +1853,6 @@ namespace smt {
 
     std::ostream& operator<<(std::ostream& out, enode_eq_pp const& p);
 
-    struct enode_pp {
-        context const& ctx;
-        enode*   n;
-        enode_pp(enode* n, context const& ctx): ctx(ctx), n(n) {}
-    };
 
     std::ostream& operator<<(std::ostream& out, enode_pp const& p);