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

57 files changed, 386 insertions, 213 deletions

diff --git a/Makefile.am b/Makefile.am
index 5b0f8d11a..74a28a51c 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -3,4 +3,7 @@ AM_CXXFLAGS = -Wall
 AUTOMAKE_OPTIONS = foreign
 ACLOCAL_AMFLAGS = -I config
 
-SUBDIRS = src doc contrib
+SUBDIRS = src test doc contrib
+
+.PHONY: test
+test: check
diff --git a/autogen.sh b/autogen.sh
index a250f6b82..c9e4200da 100755
--- a/autogen.sh
+++ b/autogen.sh
@@ -8,4 +8,4 @@ touch NEWS README AUTHORS ChangeLog
 touch stamp-h
 aclocal -I config
 autoconf -I config
-automake -ac --foreign
+automake -ac --foreign -Woverride
diff --git a/configure.ac b/configure.ac
index 77c03ef2c..57dde9b35 100644
--- a/configure.ac
+++ b/configure.ac
@@ -43,6 +43,30 @@ AC_CHECK_PROG(DOXYGEN, doxygen, doxygen, [])
 if test -z "$DOXYGEN"; then
   AC_MSG_WARN([documentation targets require doxygen.  Set your PATH appropriately or set DOXYGEN to point to a valid doxygen binary.])
 fi
+AC_ARG_VAR(DOXYGEN, [location of doxygen binary])
+
+CXXTESTGEN=
+AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH])
+if test -z "$CXXTESTGEN"; then
+  AC_MSG_NOTICE([unit tests disabled, cxxtestgen.pl not found.])
+elif test -z "$CXXTEST"; then
+  CXXTEST=$(dirname "$CXXTESTGEN")
+  AC_MSG_CHECKING([for location of CxxTest headers])
+  if test -e "$CXXTEST/cxxtest/TestRunner.h"; then
+    AC_MSG_RESULT([$CXXTEST])
+  else
+    AC_MSG_RESULT([not found])
+    AC_MSG_WARN([unit tests disabled, CxxTest headers not found.])
+    CXXTESTGEN=
+    CXXTEST=
+  fi
+fi
+AC_ARG_VAR(CXXTEST, [path to CxxTest installation])
+AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"])
+
+AC_ARG_VAR(TEST_CPPFLAGS, [CXXFLAGS to use when testing (default=$CPPFLAGS)])
+AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)])
+AC_ARG_VAR(TEST_LDFLAGS,  [LDFLAGS to use when testing (default=$LDFLAGS)])
 
 # Checks for libraries.
 AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP not found, see http://gmplib.org/])])
@@ -84,6 +108,7 @@ AC_CONFIG_FILES([
   src/context/Makefile
   src/parser/Makefile
   src/theory/Makefile
+  test/Makefile
 ])
 
 AC_OUTPUT
diff --git a/src/Makefile.am b/src/Makefile.am
index 8b897bf0f..57a67d6e5 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -1,4 +1,5 @@
 INCLUDES = -I@srcdir@/include -I@srcdir@
+AM_CXXFLAGS = -Wall -fvisibility=hidden
 
 SUBDIRS = util expr context prop smt theory parser main
 
diff --git a/src/context/Makefile.am b/src/context/Makefile.am
index e3226e88b..00858fb7b 100644
--- a/src/context/Makefile.am
+++ b/src/context/Makefile.am
@@ -1,5 +1,5 @@
 INCLUDES = -I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall
+AM_CXXFLAGS = -Wall -fvisibility=hidden
 
 noinst_LIBRARIES = libcontext.a
 
diff --git a/src/context/context.h b/src/context/context.h
index fce2f0b8d..6cc36ae9b 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -9,10 +9,11 @@
  **
  **/
 
-#ifndef __CVC4_CONTEXT_H
-#define __CVC4_CONTEXT_H
+#ifndef __CVC4__CONTEXT__CONTEXT_H
+#define __CVC4__CONTEXT__CONTEXT_H
 
 namespace CVC4 {
+namespace context {
 
 class Context;
 
@@ -40,6 +41,7 @@ class CDList;
 template <class T>
 class CDSet;
 
+}/* CVC4::context namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4_CONTEXT_H */
+#endif /* __CVC4__CONTEXT__CONTEXT_H */
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 6833f9f97..17b7d8dcd 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -1,5 +1,5 @@
 INCLUDES = -I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall
+AM_CXXFLAGS = -Wall -fvisibility=hidden
 
 noinst_LIBRARIES = libexpr.a
 
diff --git a/src/expr/attr_type.h b/src/expr/attr_type.h
index d24385f8e..1d5e8eb0c 100644
--- a/src/expr/attr_type.h
+++ b/src/expr/attr_type.h
@@ -9,12 +9,13 @@
  **
  **/
 
-#ifndef __CVC4_ATTR_TYPE_H
-#define __CVC4_ATTR_TYPE_H
+#ifndef __CVC4__EXPR__ATTR_TYPE_H
+#define __CVC4__EXPR__ATTR_TYPE_H
 
 #include "expr_attribute.h"
 
 namespace CVC4 {
+namespace expr {
 
 class Type;
 
@@ -29,6 +30,7 @@ public:
 
 extern AttrTable<Type_attr> type_table;
 
-} /* CVC4 namespace */
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4_ATTR_TYPE_H */
+#endif /* __CVC4__EXPR__ATTR_TYPE_H */
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index b6484ef25..f1b334ff8 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -14,33 +14,31 @@
 #include "expr_value.h"
 #include "expr_builder.h"
 
+using namespace CVC4::expr;
+
 namespace CVC4 {
 
 Expr Expr::s_null(0);
 
 Expr::Expr(ExprValue* ev)
   : d_ev(ev) {
-  // FIXME: thread-safety
-  ++d_ev->d_rc;
+  d_ev->inc();
 }
 
 Expr::Expr(const Expr& e) {
-  // FIXME: thread-safety
   if((d_ev = e.d_ev))
-    ++d_ev->d_rc;
+    d_ev->inc();
 }
 
 Expr::~Expr() {
-  // FIXME: thread-safety
-  --d_ev->d_rc;
+  d_ev->dec();
 }
 
 Expr& Expr::operator=(const Expr& e) {
-  // FIXME: thread-safety
   if(d_ev)
-    --d_ev->d_rc;
+    d_ev->dec();
   if((d_ev = e.d_ev))
-    ++d_ev->d_rc;
+    d_ev->inc();
   return *this;
 }
 
@@ -97,4 +95,4 @@ Expr Expr::substExpr(const std::vector<Expr>& oldTerms,
   return ExprBuilder(*this).substExpr(oldTerms, newTerms);
 }
 
-} /* CVC4 namespace */
+}/* CVC4 namespace */
diff --git a/src/expr/expr_attribute.h b/src/expr/expr_attribute.h
index 3525a8370..b44c9af6f 100644
--- a/src/expr/expr_attribute.h
+++ b/src/expr/expr_attribute.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_EXPR_ATTRIBUTE_H
-#define __CVC4_EXPR_ATTRIBUTE_H
+#ifndef __CVC4__EXPR__EXPR_ATTRIBUTE_H
+#define __CVC4__EXPR__EXPR_ATTRIBUTE_H
 
 // TODO WARNING this file needs work !
 
@@ -20,6 +20,7 @@
 #include "cvc4_expr.h"
 
 namespace CVC4 {
+namespace expr {
 
 template <class value_type>
 class AttrTables;
@@ -93,6 +94,7 @@ class AttributeTable {
   
 };
 
-} /* CVC4 namespace */
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4_EXPR_ATTRIBUTE_H */
+#endif /* __CVC4__EXPR__EXPR_ATTRIBUTE_H */
diff --git a/src/expr/expr_builder.cpp b/src/expr/expr_builder.cpp
index 2f7114a9b..3b0cf4041 100644
--- a/src/expr/expr_builder.cpp
+++ b/src/expr/expr_builder.cpp
@@ -139,43 +139,41 @@ void ExprBuilder::addChild(const Expr& e) {
     v->reserve(nchild_thresh + 5);
     for(ExprValue** i = d_children.u_arr; i != d_children.u_arr + nchild_thresh; ++i) {
       v->push_back(Expr(*i));
-      i->dec();
+      (*i)->dec();
     }
-    v.push_back(e);
+    v->push_back(e);
     d_children.u_vec = v;
     ++d_nchildren;
   } else if(d_nchildren > nchild_thresh) {
-    d_children.u_vec.push_back(e);
+    d_children.u_vec->push_back(e);
     ++d_nchildren;
   } else {
-    ExprValue *ev = e->d_ev;
+    ExprValue *ev = e.d_ev;
     d_children.u_arr[d_nchildren] = ev;
     ev->inc();
     ++d_nchildren;
   }
-  return *this;
 }
 
-void ExprBuilder::addChild(const ExprValue* ev) {
+void ExprBuilder::addChild(ExprValue* ev) {
   if(d_nchildren == nchild_thresh) {
     vector<Expr>* v = new vector<Expr>();
     v->reserve(nchild_thresh + 5);
     for(ExprValue** i = d_children.u_arr; i != d_children.u_arr + nchild_thresh; ++i) {
       v->push_back(Expr(*i));
-      i->dec();
+      (*i)->dec();
     }
-    v.push_back(Expr(ev));
+    v->push_back(Expr(ev));
     d_children.u_vec = v;
     ++d_nchildren;
   } else if(d_nchildren > nchild_thresh) {
-    d_children.u_vec.push_back(Expr(ev));
+    d_children.u_vec->push_back(Expr(ev));
     ++d_nchildren;
   } else {
     d_children.u_arr[d_nchildren] = ev;
     ev->inc();
     ++d_nchildren;
   }
-  return *this;
 }
 
 void ExprBuilder::collapse() {
@@ -184,7 +182,6 @@ void ExprBuilder::collapse() {
     v->reserve(nchild_thresh + 5);
     
   }
-  return *this;
 }
 
 // not const
@@ -206,4 +203,4 @@ PlusExprBuilder  ExprBuilder::operator- (Expr) {
 MultExprBuilder  ExprBuilder::operator* (Expr) {
 }
 
-} /* CVC4 namespace */
+}/* CVC4 namespace */
diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h
index 1104c17f5..fc303572d 100644
--- a/src/expr/expr_builder.h
+++ b/src/expr/expr_builder.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_EXPR_BUILDER_H
-#define __CVC4_EXPR_BUILDER_H
+#ifndef __CVC4__EXPR_BUILDER_H
+#define __CVC4__EXPR_BUILDER_H
 
 #include <vector>
 #include "expr_manager.h"
@@ -42,13 +42,13 @@ class ExprBuilder {
   } d_children;
 
   void addChild(const Expr&);
-  void addChild(const ExprValue*);
+  void addChild(ExprValue*);
   void collapse();
 
   typedef ExprValue** ev_iterator;
   typedef ExprValue const** const_ev_iterator;
 
-  void reset(const ExprValue*);
+  ExprBuilder& reset(const ExprValue*);
 
 public:
 
@@ -154,6 +154,6 @@ public:
 
 };/* class MultExprBuilder */
 
-} /* CVC4 namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4_EXPR_BUILDER_H */
+#endif /* __CVC4__EXPR_BUILDER_H */
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
index 80091bef6..a65a2f3cd 100644
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager.cpp
@@ -49,4 +49,4 @@ Expr ExprManager::mkExpr(Kind kind, std::vector<Expr> children) {
   return ExprBuilder(this, kind).append(children);
 }
 
-} /* CVC4 namespace */
+}/* CVC4 namespace */
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index 7e0da01c6..802cfe9c0 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_EXPR_MANAGER_H
-#define __CVC4_EXPR_MANAGER_H
+#ifndef __CVC4__EXPR_MANAGER_H
+#define __CVC4__EXPR_MANAGER_H
 
 #include <vector>
 #include "cvc4_expr.h"
@@ -53,6 +53,6 @@ public:
   // do we want a varargs one?  perhaps not..
 };
 
-} /* CVC4 namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4_EXPR_MANAGER_H */
+#endif /* __CVC4__EXPR_MANAGER_H */
diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp
index 451538f3f..fa5628e26 100644
--- a/src/expr/expr_value.cpp
+++ b/src/expr/expr_value.cpp
@@ -76,4 +76,4 @@ ExprValue::const_iterator ExprValue::rend() const {
   return d_children - 1;
 }
 
-} /* CVC4 namespace */
+}/* CVC4 namespace */
diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h
index 4b4b4f612..88984d286 100644
--- a/src/expr/expr_value.h
+++ b/src/expr/expr_value.h
@@ -14,14 +14,19 @@
  ** reference count on ExprValue instances and
  **/
 
-#ifndef __CVC4_EXPR_VALUE_H
-#define __CVC4_EXPR_VALUE_H
+#ifndef __CVC4__EXPR__EXPR_VALUE_H
+#define __CVC4__EXPR__EXPR_VALUE_H
 
 #include <stdint.h>
 #include "cvc4_expr.h"
 
 namespace CVC4 {
 
+class Expr;
+class ExprBuilder;
+
+namespace expr {
+
 /**
  * This is an ExprValue.
  */
@@ -47,11 +52,13 @@ class ExprValue {
   /** Variable number of child nodes */
   Expr     d_children[0];
 
-  friend class Expr;
-  friend class ExprBuilder;
+  // todo add exprMgr ref in debug case
+
+  friend class CVC4::Expr;
+  friend class CVC4::ExprBuilder;
 
-  ExprValue* inc() { /* FIXME thread safety */ ++d_rc; return this; }
-  ExprValue* dec() { /* FIXME thread safety */ --d_rc; return this; }
+  ExprValue* inc();
+  ExprValue* dec();
 
 public:
   /** Hash this expression.
@@ -74,6 +81,7 @@ public:
   const_iterator rend() const;
 };
 
-} /* CVC4 namespace */
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4_EXPR_VALUE_H */
+#endif /* __CVC4__EXPR__EXPR_VALUE_H */
diff --git a/src/expr/kind.h b/src/expr/kind.h
index 9c4e4d5ab..98cc7e2e3 100644
--- a/src/expr/kind.h
+++ b/src/expr/kind.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_KIND_H
-#define __CVC4_KIND_H
+#ifndef __CVC4__KIND_H
+#define __CVC4__KIND_H
 
 namespace CVC4 {
 
@@ -19,20 +19,32 @@ namespace CVC4 {
 // placeholder for design & development work.
 
 enum Kind {
+  /* undefined */
   UNDEFINED_KIND = -1,
+
+  /* built-ins */
   EQUAL,
+  ITE,
+  SKOLEM,
+  VARIABLE,
+
+  /* propositional connectives */
+  FALSE,
+  TRUE,
+
+  NOT,
+
   AND,
+  IFF,
   OR,
   XOR,
-  NOT,
+
+  /* from arith */
   PLUS,
-  MINUS,
-  ITE,
-  IFF,
-  SKOLEM,
-  SUBST
+  MINUS
+
 };/* enum Kind */
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4_KIND_H */
+#endif /* __CVC4__KIND_H */
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 */
diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index 3b2ccb05a..8f400241b 100644
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -1,5 +1,5 @@
 INCLUDES = -I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall
+AM_CXXFLAGS = -Wall -fvisibility=hidden
 
 bin_PROGRAMS = cvc4
 
diff --git a/src/main/about.h b/src/main/about.h
index f582debf0..e02183ba7 100644
--- a/src/main/about.h
+++ b/src/main/about.h
@@ -1,8 +1,8 @@
-#ifndef __CVC4_ABOUT_H
-#define __CVC4_ABOUT_H
+#ifndef __CVC4__MAIN__ABOUT_H
+#define __CVC4__MAIN__ABOUT_H
 
 namespace CVC4 {
-namespace Main {
+namespace main {
 
 const char about[] = "\
 This is a pre-release of CVC4.\n\
@@ -11,7 +11,7 @@ Copyright (C) 2009 The ACSys Group\n\
                    New York University\n\
 ";
 
-}/* CVC4::Main namespace */
+}/* CVC4::main namespace */
 }/* CVC4 namespace */
 
 #endif /* __CVC4_MAIN_H */
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 4850d475f..d2c6cb26d 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -36,6 +36,15 @@ int main(int argc, char *argv[]) {
         throw new Exception(string("Could not open input file `") + argv[firstArgIndex] + "' for reading: " + strerror(errno));
         exit(1);
       }
+
+      // ExprManager *exprMgr = ...;
+      // SmtEngine smt(exprMgr, &opts);
+      // Parser parser(infile, exprMgr, &opts);
+      // while(!parser.done) {
+      //   Command *cmd = parser.get();
+      //   cmd->invoke(smt);
+      //   delete cmd;
+      // }
     }
   } catch(CVC4::Main::OptionException* e) {
     if(opts.smtcomp_mode) {
diff --git a/src/main/main.h b/src/main/main.h
index 4101f4fe4..d0a517967 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -6,11 +6,11 @@
 #include "util/exception.h"
 #include "util/options.h"
 
-#ifndef __CVC4_MAIN_H
-#define __CVC4_MAIN_H
+#ifndef __CVC4__MAIN__MAIN_H
+#define __CVC4__MAIN__MAIN_H
 
 namespace CVC4 {
-namespace Main {
+namespace main {
 
 class OptionException : public CVC4::Exception {
 public:
@@ -20,7 +20,7 @@ public:
 int parseOptions(int argc, char** argv, CVC4::Options*) throw(CVC4::Exception*);
 void cvc4_init() throw();
 
-}/* CVC4::Main namespace */
+}/* CVC4::main namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4_MAIN_H */
+#endif /* __CVC4__MAIN__MAIN_H */
diff --git a/src/main/usage.h b/src/main/usage.h
index 971ba7640..edc9ad1d1 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -1,8 +1,8 @@
-#ifndef __CVC4_USAGE_H
-#define __CVC4_USAGE_H
+#ifndef __CVC4__MAIN__USAGE_H
+#define __CVC4__MAIN__USAGE_H
 
 namespace CVC4 {
-namespace Main {
+namespace main {
 
 // no more % chars in here without being escaped; it's used as a
 // printf() format string
@@ -23,7 +23,7 @@ CVC4 options:\n\
    --stats         give statistics on exit\n\
 ";
 
-}/* CVC4::Main namespace */
+}/* CVC4::main namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4_USAGE_H */
+#endif /* __CVC4__MAIN__USAGE_H */
diff --git a/src/main/util.cpp b/src/main/util.cpp
index da4d4b0c0..63c8cc860 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -16,12 +16,12 @@ namespace Main {
 
 void sigint_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 interrupted by user.\n");
-  exit(info->si_signo + 128);
+  abort();
 }
 
 void segv_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 suffered a segfault.\n");
-  exit(info->si_signo + 128);
+  abort();
 }
 
 void cvc4_init() throw() {
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 918ab2fb2..2a1b83dba 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -1,5 +1,5 @@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall
+INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -I@builddir@
+AM_CXXFLAGS = -Wall -fvisibility=hidden
 
 noinst_LIBRARIES = libparser.a
 
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 967f20e95..36b8c34eb 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -10,13 +10,14 @@
  ** Parser abstraction.
  **/
 
-#ifndef __CVC4_PARSER_H
-#define __CVC4_PARSER_H
+#ifndef __CVC4__PARSER__PARSER_H
+#define __CVC4__PARSER__PARSER_H
 
 #include "core/exception.h"
 #include "core/lang.h"
 
 namespace CVC4 {
+namespace parser {
 
   class ValidityChecker;
   class Expr;
@@ -59,6 +60,7 @@ namespace CVC4 {
   class ParserTemp;
   extern ParserTemp* parserTemp;
 
+}/* CVC4::parser namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4_PARSER_H */
+#endif /* __CVC4__PARSER__PARSER_H */
diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h
index 18f027e44..89490fad8 100644
--- a/src/parser/parser_exception.h
+++ b/src/parser/parser_exception.h
@@ -10,14 +10,15 @@
  ** Exception class.
  **/
 
-#ifndef __CVC4_PARSER_EXCEPTION_H
-#define __CVC4_PARSER_EXCEPTION_H
+#ifndef __CVC4__PARSER__PARSER_EXCEPTION_H
+#define __CVC4__PARSER__PARSER_EXCEPTION_H
 
-#include "core/exception.h"
+#include "util/exception.h"
 #include <string>
 #include <iostream>
 
 namespace CVC4 {
+namespace parser {
 
   class ParserException: public Exception {
   public:
@@ -32,6 +33,7 @@ namespace CVC4 {
     }
   }; // end of class ParserException
 
+}/* CVC4::parser namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4_PARSER_EXCEPTION_H */
+#endif /* __CVC4__PARSER__PARSER_EXCEPTION_H */
diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h
index f82980196..c1fd0ae96 100644
--- a/src/parser/parser_state.h
+++ b/src/parser/parser_state.h
@@ -14,17 +14,19 @@
  ** New York University
  **/
 
-#ifndef __CVC4_PARSER_STATE_H
-#define __CVC4_PARSER_STATE_H
+#ifndef __CVC4__PARSER__PARSER_STATE_H
+#define __CVC4__PARSER__PARSER_STATE_H
 
 #include <iostream>
 #include <sstream>
 #include "cvc4_expr.h"
-#include "exception.h"
+#include "util/exception.h"
 
 namespace CVC4 {
 
-class ValidityChecker;
+class SmtEngine;
+
+namespace parser {
 
 class ParserState {
 private:
@@ -37,7 +39,7 @@ private:
   // The currently used prompt
   std::string prompt;
 public:
-  ValidityChecker* vc;
+  SmtEngine* vc;
   std::istream* is;
   // The current input line
   int lineNum;
@@ -89,6 +91,7 @@ public:
   void setPrompt2() { prompt = prompt2; }
 };
 
-} /* CVC4 namespace */
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4_PARSER_STATE_H */
+#endif /* __CVC4__PARSER__PARSER_STATE_H */
diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp
index d8fd57c8c..012f468eb 100644
--- a/src/parser/pl.ypp
+++ b/src/parser/pl.ypp
@@ -13,19 +13,22 @@
 
 %{
 
-#include "vc.h"
-#include "parser_exception.h"
-#include "parser_state.h"
+#include "cvc4.h"
+#include "parser/parser_exception.h"
+#include "parser/parser_state.h"
 //#include "rational.h"
 
 // Exported shared data
 namespace CVC4 {
-  extern ParserState* parserState;
-}
+  namespace parser {
+    extern ParserState* parserState;
+  }/* CVC4::parser namespace */
+}/* CVC4 hnamespace */
+
 // Define shortcuts for various things
-#define TMP CVC4::parserState
-#define EXPR CVC4::parserState->expr
-#define VC (CVC4::parserState->vc)
+#define TMP CVC4::parser::parserState
+#define EXPR CVC4::parser::parserState->expr
+#define VC (CVC4::parser::parserState->vc)
 #define RAT(args) CVC4::newRational args
 
 // Suppress the bogus warning suppression in bison (it generates
@@ -38,9 +41,9 @@ extern int PLlex(void);
 int PLerror(const char *s)
 {
   std::ostringstream ss;
-  ss << CVC4::parserState->fileName << ":" << CVC4::parserState->lineNum
+  ss << CVC4::parser::parserState->fileName << ":" << CVC4::parser::parserState->lineNum
      << ": " << s;
-  return CVC4::parserState->error(ss.str());
+  return CVC4::parser::parserState->error(ss.str());
 }
 
 
diff --git a/src/parser/pl_scanner.lpp b/src/parser/pl_scanner.lpp
index ba8a8e85d..262eb5c88 100644
--- a/src/parser/pl_scanner.lpp
+++ b/src/parser/pl_scanner.lpp
@@ -21,30 +21,32 @@
 %{
 
 #include <iostream>
-#include "expr_manager.h" /* for the benefit of parsePL_defs.h */
-#include "parser_state.h"
-#include "pl.hpp"
-#include "debug.h"
+#include "expr/expr_manager.h" /* for the benefit of parsePL_defs.h */
+#include "parser/parser_state.h"
+#include "parser/pl.hpp"
+#include "util/debug.h"
 
 namespace CVC4 {
-  extern ParserState* parserState;
-}
+  namespace parser {
+    extern ParserState* parserState;
+  }/* CVC4::parser namespace */
+}/* CVC4 namespace */
 
 extern int PL_inputLine;
 extern char *PLtext;
 
-extern int PLerror (const char *msg);
+extern int PLerror(const char *msg);
 
 static int PLinput(std::istream& is, char* buf, int size) {
   int res;
   if(is) {
     // If interactive, read line by line; otherwise read as much as we
     // can gobble
-    if(CVC4::parserState->interactive) {
+    if(CVC4::parser::parserState->interactive) {
       // Print the current prompt
-      std::cout << CVC4::parserState->getPrompt() << std::flush;
+      std::cout << CVC4::parser::parserState->getPrompt() << std::flush;
       // Set the prompt to "middle of the command" one
-      CVC4::parserState->setPrompt2();
+      CVC4::parser::parserState->setPrompt2();
       // Read the line
       is.getline(buf, size-1);
     } else // Set the terminator char to 0
@@ -69,7 +71,7 @@ static int PLinput(std::istream& is, char* buf, int size) {
 
 // Redefine the input buffer function to read from an istream
 #define YY_INPUT(buf,result,max_size) \
-  result = PLinput(*CVC4::parserState->is, buf, max_size);
+  result = PLinput(*CVC4::parser::parserState->is, buf, max_size);
 
 int PL_bufSize() { return YY_BUF_SIZE; }
 YY_BUFFER_STATE PL_buf_state() { return YY_CURRENT_BUFFER; }
@@ -123,7 +125,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR})
 
 %%
 
-[\n]            { CVC4::parserState->lineNum++; }
+[\n]            { CVC4::parser::parserState->lineNum++; }
 
 [ \t\r\f]	{ /* skip whitespace */ }
 
@@ -136,7 +138,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR})
 
 "%"		{ BEGIN COMMENT; }
 <COMMENT>"\n"	{ BEGIN INITIAL; /* return to normal mode */ 
-                  CVC4::parserState->lineNum++; }
+                  CVC4::parser::parserState->lineNum++; }
 <COMMENT>.	{ /* stay in comment mode */ }
 
 <INITIAL>"\""		{ BEGIN STRING_LITERAL; 
diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp
index 0f3aa8cf4..692a9cda5 100644
--- a/src/parser/smtlib.ypp
+++ b/src/parser/smtlib.ypp
@@ -11,9 +11,9 @@
  ** commands in SMT-LIB language.
  **/
 
-#include "vc.h"
-#include "parser_exception.h"
-#include "parser_state.h"
+#include "cvc4.h"
+#include "parser/parser_exception.h"
+#include "parser/parser_state.h"
 
 // Exported shared data
 namespace CVC4 {
diff --git a/src/parser/smtlib_scanner.lpp b/src/parser/smtlib_scanner.lpp
index bb5802aed..b367b0d93 100644
--- a/src/parser/smtlib_scanner.lpp
+++ b/src/parser/smtlib_scanner.lpp
@@ -20,8 +20,8 @@
 
 %{
 #include <iostream>
-#include "smtlib.hpp"
-#include "debug.h"
+#include "parser/smtlib.hpp"
+#include "util/debug.h"
 
 namespace CVC4 {
   extern ParserTemp* parserTemp;
diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am
index 5051420a2..941b0c653 100644
--- a/src/prop/Makefile.am
+++ b/src/prop/Makefile.am
@@ -1,4 +1,4 @@
 INCLUDES = -I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall
+AM_CXXFLAGS = -Wall -fvisibility=hidden
 
 SUBDIRS = minisat
diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am
index 74d72d48d..97cfc438a 100644
--- a/src/prop/minisat/Makefile.am
+++ b/src/prop/minisat/Makefile.am
@@ -1,4 +1,5 @@
 INCLUDES = -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../../include
+AM_CXXFLAGS = -Wall -fvisibility=hidden
 
 noinst_LIBRARIES = libminisat.a
 libminisat_a_SOURCES = \
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 0febd2927..5572b47f7 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -9,14 +9,15 @@
  **
  **/
 
-#ifndef __CVC4_PROP_ENGINE_H
-#define __CVC4_PROP_ENGINE_H
+#ifndef __CVC4__PROP__PROP_ENGINE_H
+#define __CVC4__PROP__PROP_ENGINE_H
 
 #include "core/cvc4_expr.h"
 #include "core/decision_engine.h"
 #include "core/theory_engine.h"
 
 namespace CVC4 {
+namespace prop {
 
 // In terms of abstraction, this is below (and provides services to)
 // Prover and above (and requires the services of) a specific
@@ -38,6 +39,7 @@ public:
 
 };/* class PropEngine */
 
-}
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4_PROP_ENGINE_H */
+#endif /* __CVC4__PROP__PROP_ENGINE_H */
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 00a94c142..32ca9e983 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -9,11 +9,13 @@
  **
  **/
 
-#ifndef __CVC4_SAT_H
-#define __CVC4_SAT_H
+#ifndef __CVC4__PROP__SAT_H
+#define __CVC4__PROP__SAT_H
 
 namespace CVC4 {
+namespace prop {
 
-} /* CVC4 namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4_SAT_H */
+#endif /* __CVC4__PROP__SAT_H */
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index f719b1283..ff740aa56 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -1,5 +1,5 @@
 INCLUDES = -I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall
+AM_CXXFLAGS = -Wall -fvisibility=hidden
 
 noinst_LIBRARIES = libsmt.a
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 6f6fb355a..078bf9cde 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_PROVER_H
-#define __CVC4_PROVER_H
+#ifndef __CVC4__SMT__SMT_ENGINE_H
+#define __CVC4__SMT__SMT_ENGINE_H
 
 #include <vector>
 #include "core/cvc4_expr.h"
@@ -22,6 +22,7 @@
 // PropEngine.
 
 namespace CVC4 {
+namespace smt {
 
 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
 // hood): use a type parameter and have check() delegate, or subclass
@@ -109,6 +110,7 @@ public:
   void pop();
 };/* class SmtEngine */
 
-} /* CVC4 namespace */
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4_PROVER_H */
+#endif /* __CVC4__SMT__SMT_ENGINE_H */
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index 5c64f4f38..f022d0445 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -1,5 +1,5 @@
 INCLUDES = -I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall
+AM_CXXFLAGS = -Wall -fvisibility=hidden
 
 noinst_LIBRARIES = libtheory.a
 
diff --git a/src/theory/theory.h b/src/theory/theory.h
index eeaba58d1..05e8e1b01 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -9,13 +9,14 @@
  **
  **/
 
-#ifndef __CVC4_THEORY_H
-#define __CVC4_THEORY_H
+#ifndef __CVC4__THEORY__THEORY_H
+#define __CVC4__THEORY__THEORY_H
 
 #include "core/cvc4_expr.h"
 #include "core/literal.h"
 
 namespace CVC4 {
+namespace theory {
 
 /**
  * Base class for T-solvers.  Abstract DPLL(T).
@@ -78,6 +79,7 @@ public:
 
 };/* class Theory */
 
+}/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4_THEORY_H */
+#endif /* __CVC4__THEORY__THEORY_H */
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 2a0841d8d..fead8e224 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -9,10 +9,11 @@
  **
  **/
 
-#ifndef __CVC4_THEORY_ENGINE_H
-#define __CVC4_THEORY_ENGINE_H
+#ifndef __CVC4__THEORY__THEORY_ENGINE_H
+#define __CVC4__THEORY__THEORY_ENGINE_H
 
 namespace CVC4 {
+namespace theory {
 
 // In terms of abstraction, this is below (and provides services to)
 // PropEngine.
@@ -27,6 +28,7 @@ class TheoryEngine {
 public:
 };/* class TheoryEngine */
 
+}/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4_THEORY_ENGINE_H */
+#endif /* __CVC4__THEORY__THEORY_ENGINE_H */
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index de5f0da9d..415893680 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -1,5 +1,5 @@
 INCLUDES = -I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall
+AM_CXXFLAGS = -Wall -fvisibility=hidden
 
 noinst_LIBRARIES = libutil.a
 
diff --git a/src/util/assert.h b/src/util/assert.h
index a66503641..24e3a4cdf 100644
--- a/src/util/assert.h
+++ b/src/util/assert.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_ASSERT_H
-#define __CVC4_ASSERT_H
+#ifndef __CVC4__ASSERT_H
+#define __CVC4__ASSERT_H
 
 #include <cassert>
 
@@ -23,4 +23,4 @@
 # define cvc4assert(x)
 #endif /* DEBUG */
 
-#endif /* __CVC4_ASSERT_H */
+#endif /* __CVC4__ASSERT_H */
diff --git a/src/util/command.h b/src/util/command.h
index 944b9c621..d1257f323 100644
--- a/src/util/command.h
+++ b/src/util/command.h
@@ -9,14 +9,14 @@
  **
  **/
 
-#ifndef __CVC4_COMMAND_H
-#define __CVC4_COMMAND_H
+#ifndef __CVC4__COMMAND_H
+#define __CVC4__COMMAND_H
 
 namespace CVC4 {
 
 class Command { // distinct from Exprs
 };
 
-} /* CVC4 namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4_COMMAND_H */
+#endif /* __CVC4__COMMAND_H */
diff --git a/src/util/debug.h b/src/util/debug.h
index 36942d1ae..14dc0fbd1 100644
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_DEBUG_H
-#define __CVC4_DEBUG_H
+#ifndef __CVC4__DEBUG_H
+#define __CVC4__DEBUG_H
 
 #include <cassert>
 
@@ -23,4 +23,4 @@
 # define cvc4assert(x)
 #endif /* DEBUG */
 
-#endif /* __CVC4_DEBUG_H */
+#endif /* __CVC4__DEBUG_H */
diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h
index 81d820eaa..2064e3687 100644
--- a/src/util/decision_engine.h
+++ b/src/util/decision_engine.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_DECISION_ENGINE_H
-#define __CVC4_DECISION_ENGINE_H
+#ifndef __CVC4__DECISION_ENGINE_H
+#define __CVC4__DECISION_ENGINE_H
 
 #include "core/literal.h"
 
@@ -39,4 +39,4 @@ public:
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4_DECISION_ENGINE_H */
+#endif /* __CVC4__DECISION_ENGINE_H */
diff --git a/src/util/exception.h b/src/util/exception.h
index 792a98701..e3b8f2293 100644
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -10,39 +10,39 @@
  ** Exception class.
  **/
 
-#ifndef __CVC4_EXCEPTION_H
-#define __CVC4_EXCEPTION_H
+#ifndef __CVC4__EXCEPTION_H
+#define __CVC4__EXCEPTION_H
 
 #include <string>
 #include <iostream>
 
 namespace CVC4 {
 
-  class Exception {
-  protected:
-    std::string d_msg;
-  public:
-    // Constructors
-    Exception(): d_msg("Unknown exception") { }
-    Exception(const std::string& msg): d_msg(msg) { }
-    Exception(const char* msg): d_msg(msg) { }
-    // Destructor
-    virtual ~Exception() { }
-    // NON-VIRTUAL METHODs for setting and printing the error message
-    void setMessage(const std::string& msg) { d_msg = msg; }
-    // Printing: feel free to redefine toString().  When inherited,
-    // it's recommended that this method print the type of exception
-    // before the actual message.
-    virtual std::string toString() const { return d_msg; }
-    // No need to overload operator<< for the inherited classes
-    friend std::ostream& operator<<(std::ostream& os, const Exception& e);
-
-  }; // end of class Exception
-
-  inline std::ostream& operator<<(std::ostream& os, const Exception& e) {
-    return os << e.toString();
-  }
+class Exception {
+protected:
+  std::string d_msg;
+public:
+  // Constructors
+  Exception(): d_msg("Unknown exception") { }
+  Exception(const std::string& msg): d_msg(msg) { }
+  Exception(const char* msg): d_msg(msg) { }
+  // Destructor
+  virtual ~Exception() { }
+  // NON-VIRTUAL METHODs for setting and printing the error message
+  void setMessage(const std::string& msg) { d_msg = msg; }
+  // Printing: feel free to redefine toString().  When inherited,
+  // it's recommended that this method print the type of exception
+  // before the actual message.
+  virtual std::string toString() const { return d_msg; }
+  // No need to overload operator<< for the inherited classes
+  friend std::ostream& operator<<(std::ostream& os, const Exception& e);
+
+}; // end of class Exception
+
+inline std::ostream& operator<<(std::ostream& os, const Exception& e) {
+  return os << e.toString();
+}
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4_EXCEPTION_H */
+#endif /* __CVC4__EXCEPTION_H */
diff --git a/src/util/literal.h b/src/util/literal.h
index 8b147c640..7af9826bb 100644
--- a/src/util/literal.h
+++ b/src/util/literal.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_LITERAL_H
-#define __CVC4_LITERAL_H
+#ifndef __CVC4__LITERAL_H
+#define __CVC4__LITERAL_H
 
 namespace CVC4 {
 
@@ -18,4 +18,4 @@ class Literal;
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4_LITERAL_H */
+#endif /* __CVC4__LITERAL_H */
diff --git a/src/util/model.h b/src/util/model.h
index c07b75dfa..cf006b3e1 100644
--- a/src/util/model.h
+++ b/src/util/model.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_MODEL_H
-#define __CVC4_MODEL_H
+#ifndef __CVC4__MODEL_H
+#define __CVC4__MODEL_H
 
 namespace CVC4 {
 
@@ -19,4 +19,4 @@ class Model {
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4_MODEL_H */
+#endif /* __CVC4__MODEL_H */
diff --git a/src/util/options.h b/src/util/options.h
index f04b06f10..6104470d2 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -1,5 +1,5 @@
-#ifndef __CVC4_OPTIONS_H
-#define __CVC4_OPTIONS_H
+#ifndef __CVC4__OPTIONS_H
+#define __CVC4__OPTIONS_H
 
 namespace CVC4 {
 
@@ -28,4 +28,4 @@ struct Options {
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4_OPTIONS_H */
+#endif /* __CVC4__OPTIONS_H */
diff --git a/src/util/result.h b/src/util/result.h
index 50f488682..1e2b61738 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_RESULT_H
-#define __CVC4_RESULT_H
+#ifndef __CVC4__RESULT_H
+#define __CVC4__RESULT_H
 
 namespace CVC4 {
 
@@ -62,4 +62,4 @@ public:
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4_RESULT_H */
+#endif /* __CVC4__RESULT_H */
diff --git a/src/util/unique_id.h b/src/util/unique_id.h
index 1a6f3427a..4ac80f772 100644
--- a/src/util/unique_id.h
+++ b/src/util/unique_id.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_UNIQUE_ID_H
-#define __CVC4_UNIQUE_ID_H
+#ifndef __CVC4__UNIQUE_ID_H
+#define __CVC4__UNIQUE_ID_H
 
 namespace CVC4 {
 
@@ -30,6 +30,6 @@ public:
 template <class T>
 unsigned UniqueID<T>::s_topID = 0;
 
-} /* CVC4 namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4_UNIQUE_ID_H */
+#endif /* __CVC4__UNIQUE_ID_H */
diff --git a/test/Makefile.am b/test/Makefile.am
new file mode 100644
index 000000000..bf74eaa47
--- /dev/null
+++ b/test/Makefile.am
@@ -0,0 +1,23 @@
+if HAVE_CXXTESTGEN
+
+AM_CPPFLAGS = -I. "-I$(CXXTEST)" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src"
+AM_CXXFLAGS = -fno-access-control
+AM_LDFLAGS = -L@top_builddir@/src/libcvc4.a
+TESTS = \
+	expr/expr_black \
+	expr/expr_white
+
+%.cpp: %.h
+	$(CXXTESTGEN) --have-eh --have-std --error-printer -o $@ $<
+%: %.cpp
+	$(CXX) $(TEST_CPPFLAGS) $(AM_CPPFLAGS) $(TEST_CXXFLAGS) $(AM_CXXFLAGS) -o $@ $(TEST_LDFLAGS) $(AM_LDFLAGS) $< @top_builddir@/src/libcvc4.a
+
+MOSTLYCLEANFILES = $(TESTS) $(TESTS:%=%.cpp)
+
+else
+
+# force a user-visible failure for "make check"
+TESTS = no_cxxtest
+
+endif
+
diff --git a/test/expr/expr_black.h b/test/expr/expr_black.h
new file mode 100644
index 000000000..97746d1c4
--- /dev/null
+++ b/test/expr/expr_black.h
@@ -0,0 +1,19 @@
+/* Black box testing of CVC4::Expr. */
+
+#include <cxxtest/TestSuite.h>
+
+#include "cvc4_expr.h"
+
+using namespace CVC4;
+
+class ExprBlack : public CxxTest::TestSuite {
+public:
+
+  void testNull() {
+    Expr::s_null;
+  }
+
+  void testCopyCtor() {
+    Expr e(Expr::s_null);
+  }
+};
diff --git a/test/expr/expr_white.h b/test/expr/expr_white.h
new file mode 100644
index 000000000..b6bfdd394
--- /dev/null
+++ b/test/expr/expr_white.h
@@ -0,0 +1,19 @@
+/* White box testing of CVC4::Expr. */
+
+#include <cxxtest/TestSuite.h>
+
+#include "cvc4_expr.h"
+
+using namespace CVC4;
+
+class ExprWhite : public CxxTest::TestSuite {
+public:
+
+  void testNull() {
+    Expr::s_null;
+  }
+
+  void testCopyCtor() {
+    Expr e(Expr::s_null);
+  }
+};
diff --git a/test/no_cxxtest b/test/no_cxxtest
new file mode 100755
index 000000000..cf8b8d729
--- /dev/null
+++ b/test/no_cxxtest
@@ -0,0 +1,12 @@
+#!/bin/sh
+
+echo
+echo '***************************************************************************'
+echo '*                                                                         *'
+echo '*  ERROR:  CxxTest was not found at configure-time; tests cannot be run.  *'
+echo '*                                                                         *'
+echo '***************************************************************************'
+echo
+
+exit 1
+