testing framework, configure fixes, incorporations from meeting, continued work

2 files changed, 26 insertions, 8 deletions

diff --git a/src/include/cvc4.h b/src/include/cvc4.h
index 109496001..c5e3bb013 100644
--- a/src/include/cvc4.h
+++ b/src/include/cvc4.h
@@ -9,10 +9,10 @@
  **
  **/
 
-#ifndef __CVC4_VC_H
-#define __CVC4_VC_H
+#ifndef __CVC4_H
+#define __CVC4_H
 
-#include "command.h"
+#include "util/command.h"
 #include "cvc4_expr.h"
 
 /* TODO provide way of querying whether you fall into a fragment /
@@ -37,6 +37,6 @@ public:
   void query(Expr);
 };
 
-} /* CVC4 namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4_VC_H */
+#endif /* __CVC4_H */
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 */