From 0d5cfe9292d9d9b60a6567c48bb48d5a2aa246a9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 26 Aug 2017 09:23:15 -0700
Subject: [PATCH] separate out, add copy constructor

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast.h                  | 35 -----------------------
 src/ast/justified_expr.h       | 52 ++++++++++++++++++++++++++++++++++
 src/ast/macros/macro_manager.h |  1 +
 src/ast/macros/quasi_macros.h  |  1 +
 src/smt/elim_term_ite.h        |  2 ++
 5 files changed, 56 insertions(+), 35 deletions(-)
 create mode 100644 src/ast/justified_expr.h

diff --git a/src/ast/ast.h b/src/ast/ast.h
index 34ea96653..699268bd0 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -2470,41 +2470,6 @@ public:
     void operator()(AST * n) { m_manager.inc_ref(n); }
 };
 
-class justified_expr {
-    ast_manager& m;
-    expr*        m_fml;
-    proof*       m_proof;
-public:
-    justified_expr(ast_manager& m, expr* fml, proof* p):
-        m(m),
-        m_fml(fml),
-        m_proof(p) {
-        m.inc_ref(fml);
-        m.inc_ref(p);
-    }
-    
-    justified_expr& operator=(justified_expr& other) {
-        SASSERT(&m == &other.m);
-        if (this != &other) {
-            m.dec_ref(m_fml);
-            m.dec_ref(m_proof);
-            m_fml = other.get_fml();
-            m_proof = other.get_proof();
-            m.inc_ref(m_fml);
-            m.inc_ref(m_proof);
-        }
-        return *this;
-    }
-    
-    ~justified_expr() {
-        m.dec_ref(m_fml);
-        m.dec_ref(m_proof);
-    }
-    
-    expr* get_fml() const { return m_fml; }
-    proof* get_proof() const { return m_proof; }        
-};
-
 
 #endif /* AST_H_ */
 
diff --git a/src/ast/justified_expr.h b/src/ast/justified_expr.h
new file mode 100644
index 000000000..49362940d
--- /dev/null
+++ b/src/ast/justified_expr.h
@@ -0,0 +1,52 @@
+
+#ifndef JUSTIFIED_EXPR_H_
+#define JUSTIFIED_EXPR_H_
+
+#include "ast/ast.h"
+
+class justified_expr {
+    ast_manager& m;
+    expr*        m_fml;
+    proof*       m_proof;
+public:
+    justified_expr(ast_manager& m, expr* fml, proof* p):
+        m(m),
+        m_fml(fml),
+        m_proof(p) {
+        SASSERT(fml);
+        m.inc_ref(fml);
+        m.inc_ref(p);
+    }
+    
+    justified_expr& operator=(justified_expr const& other) {
+        SASSERT(&m == &other.m);
+        if (this != &other) {
+            m.dec_ref(m_fml);
+            m.dec_ref(m_proof);
+            m_fml = other.get_fml();
+            m_proof = other.get_proof();
+            m.inc_ref(m_fml);
+            m.inc_ref(m_proof);
+        }
+        return *this;
+    }
+    
+    justified_expr(justified_expr const& other):
+        m(other.m),
+        m_fml(other.m_fml),
+        m_proof(other.m_proof)
+    {
+        m.inc_ref(m_fml);
+        m.inc_ref(m_proof);
+    }
+
+    ~justified_expr() {
+        m.dec_ref(m_fml);
+        m.dec_ref(m_proof);
+    }
+    
+    expr* get_fml() const { return m_fml; }
+    proof* get_proof() const { return m_proof; }        
+};
+
+#endif
diff --git a/src/ast/macros/macro_manager.h b/src/ast/macros/macro_manager.h
index 46dfa059d..0205fb891 100644
--- a/src/ast/macros/macro_manager.h
+++ b/src/ast/macros/macro_manager.h
@@ -21,6 +21,7 @@ Revision History:
 
 #include "util/obj_hashtable.h"
 #include "ast/ast_util.h"
+#include "ast/justified_expr.h"
 #include "ast/recurse_expr.h"
 #include "ast/func_decl_dependencies.h"
 #include "ast/macros/macro_util.h"
diff --git a/src/ast/macros/quasi_macros.h b/src/ast/macros/quasi_macros.h
index fc7287554..1b1483a90 100644
--- a/src/ast/macros/quasi_macros.h
+++ b/src/ast/macros/quasi_macros.h
@@ -20,6 +20,7 @@ Revision History:
 #define QUASI_MACROS_H_
 
 #include<sstream>
+#include "ast/justified_expr.h"
 #include "ast/macros/macro_manager.h"
 #include "ast/rewriter/th_rewriter.h"
 
diff --git a/src/smt/elim_term_ite.h b/src/smt/elim_term_ite.h
index 86b9a79e2..a57ea1dad 100644
--- a/src/smt/elim_term_ite.h
+++ b/src/smt/elim_term_ite.h
@@ -22,6 +22,8 @@ Revision History:
 #include "ast/normal_forms/defined_names.h"
 #include "ast/rewriter/rewriter.h"
 #include "ast/simplifier/simplifier.h"
+#include "ast/justified_expr.h"
+
 
 class elim_term_ite : public simplifier {
     defined_names &    m_defined_names;