1 files changed, 21 insertions, 3 deletions
diff --git a/src/include/cvc4_expr.h b/src/include/cvc4_expr.h
index 3d7a35fc8..1f5ac659d 100644
--- a/src/include/cvc4_expr.h
+++ b/src/include/cvc4_expr.h
@@ -15,10 +15,15 @@
 
 #include <vector>
 #include <stdint.h>
+#include "expr/kind.h"
 
 namespace CVC4 {
 
-class ExprValue;
+namespace expr {
+  class ExprValue;
+}/* CVC4::expr namespace */
+
+using CVC4::expr::ExprValue;
 
 /**
  * Encapsulation of an ExprValue pointer.  The reference count is
@@ -41,6 +46,8 @@ class Expr {
   typedef Expr* iterator;
   typedef Expr const* const_iterator;
 
+  friend class ExprBuilder;
+
 public:
   Expr(const Expr&);
 
@@ -69,11 +76,22 @@ public:
   Expr substExpr(const std::vector<Expr>& oldTerms,
                  const std::vector<Expr>& newTerms) const;
 
+  inline Kind getKind() const;
+
   static Expr null() { return s_null; }
 
-  friend class ExprBuilder;
 };/* class Expr */
 
-} /* CVC4 namespace */
+}/* CVC4 namespace */
+
+#include "expr/expr_value.h"
+
+namespace CVC4 {
+
+inline Kind Expr::getKind() const {
+  return Kind(d_ev->d_kind);
+}
+
+}/* CVC4 namespace */
 
 #endif /* __CVC4_EXPR_H */