Fixes to the build system:

Makefile.am files - remove obsolete INCLUDES, incorporate into AM_CPPFLAGS
Makefile files in src/ - support "make" under src/ (current build profile)
configure.ac - updates to fix warnings
config/antlr.m4 - updates to fix warnings
autogen.sh - updates to generate warnings from autotools; also support Macs
src/include/cvc4_config.h - guard with #ifdef
total reimplementation of NodeBuilder
ExprValue => NodeValue
context_mm.{h,cpp} - fixed numerous compile errors

10 files changed, 59 insertions, 25 deletions

diff --git a/test/Makefile b/test/Makefile
new file mode 100644
index 000000000..80f8a1dd5
--- /dev/null
+++ b/test/Makefile
@@ -0,0 +1,5 @@
+topdir = ..
+srcdir = test
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
diff --git a/test/Makefile.in b/test/Makefile.in
index 0fecac937..69e05dd65 100644
--- a/test/Makefile.in
+++ b/test/Makefile.in
@@ -115,6 +115,7 @@ CXX = @CXX@
 CXXCPP = @CXXCPP@
 CXXDEPMODE = @CXXDEPMODE@
 CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
 CXXTESTGEN = @CXXTESTGEN@
 CYGPATH_W = @CYGPATH_W@
 DEFS = @DEFS@
diff --git a/test/regress/Makefile b/test/regress/Makefile
new file mode 100644
index 000000000..c4e305306
--- /dev/null
+++ b/test/regress/Makefile
@@ -0,0 +1,5 @@
+topdir = ../..
+srcdir = test/regress
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am
index a4a06c10b..61527e4d8 100644
--- a/test/regress/Makefile.am
+++ b/test/regress/Makefile.am
@@ -1,4 +1,4 @@
-TESTS_ENVIRONMENT = echo
+TESTS_ENVIRONMENT = @top_builddir@/bin/cvc4
 TESTS = \
 	simple.cvc \
 	simple.smt \
diff --git a/test/regress/Makefile.in b/test/regress/Makefile.in
index 451d333e2..14c032220 100644
--- a/test/regress/Makefile.in
+++ b/test/regress/Makefile.in
@@ -77,6 +77,7 @@ CXX = @CXX@
 CXXCPP = @CXXCPP@
 CXXDEPMODE = @CXXDEPMODE@
 CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
 CXXTESTGEN = @CXXTESTGEN@
 CYGPATH_W = @CYGPATH_W@
 DEFS = @DEFS@
@@ -188,7 +189,7 @@ target_vendor = @target_vendor@
 top_build_prefix = @top_build_prefix@
 top_builddir = @top_builddir@
 top_srcdir = @top_srcdir@
-TESTS_ENVIRONMENT = echo
+TESTS_ENVIRONMENT = @top_builddir@/bin/cvc4
 TESTS = \
 	simple.cvc \
 	simple.smt \
diff --git a/test/unit/Makefile b/test/unit/Makefile
new file mode 100644
index 000000000..f3f3767aa
--- /dev/null
+++ b/test/unit/Makefile
@@ -0,0 +1,5 @@
+topdir = ../..
+srcdir = test/unit
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index d6908cef9..e10856bba 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -1,19 +1,27 @@
 if HAVE_CXXTESTGEN
 
-AM_CPPFLAGS = -I. "-I$(CXXTEST)" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src"
+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.la
+
+TESTS_WHITE = \
+	expr/node_white
+
+TESTS_BLACK = \
+	expr/node_black
+
 TESTS = \
-	expr/expr_black \
-	expr/expr_white
+	$(TESTS_WHITE) \
+	$(TESTS_BLACK)
 
 lib_LTLIBRARIES = libdummy.la
-libdummy_la_SOURCES = expr/expr_black.cpp
+libdummy_la_SOURCES = expr/node_black.cpp
 libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la
 
 $(TESTS:%=%.cpp): %.cpp: %.h
 	mkdir -p `dirname "$@"`
-	$(CXXTESTGEN) --have-eh --have-std --error-printer -o "$@" "$<"
+	@CXXTESTGEN@ --have-eh --have-std --error-printer -o "$@" "$<"
 $(TESTS): %: %.cpp
 #	get these in here somehow
 #	$(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS)
diff --git a/test/unit/Makefile.in b/test/unit/Makefile.in
index bcd2d239c..b630f7765 100644
--- a/test/unit/Makefile.in
+++ b/test/unit/Makefile.in
@@ -75,8 +75,8 @@ am__installdirs = "$(DESTDIR)$(libdir)"
 LTLIBRARIES = $(lib_LTLIBRARIES)
 @HAVE_CXXTESTGEN_TRUE@libdummy_la_DEPENDENCIES =  \
 @HAVE_CXXTESTGEN_TRUE@	@abs_top_builddir@/src/libcvc4.la
-am__libdummy_la_SOURCES_DIST = expr/expr_black.cpp
-@HAVE_CXXTESTGEN_TRUE@am_libdummy_la_OBJECTS = expr_black.lo
+am__libdummy_la_SOURCES_DIST = expr/node_black.cpp
+@HAVE_CXXTESTGEN_TRUE@am_libdummy_la_OBJECTS = node_black.lo
 libdummy_la_OBJECTS = $(am_libdummy_la_OBJECTS)
 @HAVE_CXXTESTGEN_TRUE@am_libdummy_la_rpath = -rpath $(libdir)
 DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
@@ -122,6 +122,7 @@ CXX = @CXX@
 CXXCPP = @CXXCPP@
 CXXDEPMODE = @CXXDEPMODE@
 CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
 CXXTESTGEN = @CXXTESTGEN@
 CYGPATH_W = @CYGPATH_W@
 DEFS = @DEFS@
@@ -233,18 +234,26 @@ target_vendor = @target_vendor@
 top_build_prefix = @top_build_prefix@
 top_builddir = @top_builddir@
 top_srcdir = @top_srcdir@
-@HAVE_CXXTESTGEN_TRUE@AM_CPPFLAGS = -I. "-I$(CXXTEST)" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src"
+@HAVE_CXXTESTGEN_TRUE@AM_CPPFLAGS = \
+@HAVE_CXXTESTGEN_TRUE@	-I. "-I@CXXTEST@" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src"
+
 @HAVE_CXXTESTGEN_TRUE@AM_CXXFLAGS = -fno-access-control
+#AM_LDFLAGS = -L@top_builddir@/src/libcvc4.la
+@HAVE_CXXTESTGEN_TRUE@TESTS_WHITE = \
+@HAVE_CXXTESTGEN_TRUE@	expr/node_white
+
+@HAVE_CXXTESTGEN_TRUE@TESTS_BLACK = \
+@HAVE_CXXTESTGEN_TRUE@	expr/node_black
+
 
 # force a user-visible failure for "make check"
 @HAVE_CXXTESTGEN_FALSE@TESTS = no_cxxtest
-#AM_LDFLAGS = -L@top_builddir@/src/libcvc4.la
 @HAVE_CXXTESTGEN_TRUE@TESTS = \
-@HAVE_CXXTESTGEN_TRUE@	expr/expr_black \
-@HAVE_CXXTESTGEN_TRUE@	expr/expr_white
+@HAVE_CXXTESTGEN_TRUE@	$(TESTS_WHITE) \
+@HAVE_CXXTESTGEN_TRUE@	$(TESTS_BLACK)
 
 @HAVE_CXXTESTGEN_TRUE@lib_LTLIBRARIES = libdummy.la
-@HAVE_CXXTESTGEN_TRUE@libdummy_la_SOURCES = expr/expr_black.cpp
+@HAVE_CXXTESTGEN_TRUE@libdummy_la_SOURCES = expr/node_black.cpp
 @HAVE_CXXTESTGEN_TRUE@libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la
 @HAVE_CXXTESTGEN_TRUE@MOSTLYCLEANFILES = $(TESTS) $(TESTS:%=%.cpp)
 all: all-am
@@ -321,7 +330,7 @@ mostlyclean-compile:
 distclean-compile:
 	-rm -f *.tab.c
 
-@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr_black.Plo@am__quote@
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node_black.Plo@am__quote@
 
 .cpp.o:
 @am__fastdepCXX_TRUE@	$(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $<
@@ -344,12 +353,12 @@ distclean-compile:
 @AMDEP_TRUE@@am__fastdepCXX_FALSE@	DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
 @am__fastdepCXX_FALSE@	$(LTCXXCOMPILE) -c -o $@ $<
 
-expr_black.lo: expr/expr_black.cpp
-@am__fastdepCXX_TRUE@	$(LIBTOOL)  --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) --mode=compile $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) -MT expr_black.lo -MD -MP -MF $(DEPDIR)/expr_black.Tpo -c -o expr_black.lo `test -f 'expr/expr_black.cpp' || echo '$(srcdir)/'`expr/expr_black.cpp
-@am__fastdepCXX_TRUE@	$(am__mv) $(DEPDIR)/expr_black.Tpo $(DEPDIR)/expr_black.Plo
-@AMDEP_TRUE@@am__fastdepCXX_FALSE@	source='expr/expr_black.cpp' object='expr_black.lo' libtool=yes @AMDEPBACKSLASH@
+node_black.lo: expr/node_black.cpp
+@am__fastdepCXX_TRUE@	$(LIBTOOL)  --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) --mode=compile $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) -MT node_black.lo -MD -MP -MF $(DEPDIR)/node_black.Tpo -c -o node_black.lo `test -f 'expr/node_black.cpp' || echo '$(srcdir)/'`expr/node_black.cpp
+@am__fastdepCXX_TRUE@	$(am__mv) $(DEPDIR)/node_black.Tpo $(DEPDIR)/node_black.Plo
+@AMDEP_TRUE@@am__fastdepCXX_FALSE@	source='expr/node_black.cpp' object='node_black.lo' libtool=yes @AMDEPBACKSLASH@
 @AMDEP_TRUE@@am__fastdepCXX_FALSE@	DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
-@am__fastdepCXX_FALSE@	$(LIBTOOL)  --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) --mode=compile $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) -c -o expr_black.lo `test -f 'expr/expr_black.cpp' || echo '$(srcdir)/'`expr/expr_black.cpp
+@am__fastdepCXX_FALSE@	$(LIBTOOL)  --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) --mode=compile $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) -c -o node_black.lo `test -f 'expr/node_black.cpp' || echo '$(srcdir)/'`expr/node_black.cpp
 
 mostlyclean-libtool:
 	-rm -f *.lo
@@ -655,7 +664,7 @@ uninstall-am: uninstall-libLTLIBRARIES
 
 @HAVE_CXXTESTGEN_TRUE@$(TESTS:%=%.cpp): %.cpp: %.h
 @HAVE_CXXTESTGEN_TRUE@	mkdir -p `dirname "$@"`
-@HAVE_CXXTESTGEN_TRUE@	$(CXXTESTGEN) --have-eh --have-std --error-printer -o "$@" "$<"
+@HAVE_CXXTESTGEN_TRUE@	@CXXTESTGEN@ --have-eh --have-std --error-printer -o "$@" "$<"
 @HAVE_CXXTESTGEN_TRUE@$(TESTS): %: %.cpp
 #	get these in here somehow
 #	$(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS)
diff --git a/test/unit/expr/expr_black.h b/test/unit/expr/node_black.h
index ad70bec91..5489e4803 100644
--- a/test/unit/expr/expr_black.h
+++ b/test/unit/expr/node_black.h
@@ -2,11 +2,11 @@
 
 #include <cxxtest/TestSuite.h>
 
-#include "expr/expr.h"
+#include "expr/node.h"
 
 using namespace CVC4;
 
-class ExprBlack : public CxxTest::TestSuite {
+class NodeBlack : public CxxTest::TestSuite {
 public:
 
   void testNull() {
diff --git a/test/unit/expr/expr_white.h b/test/unit/expr/node_white.h
index 6b48d66e6..dd462fdd8 100644
--- a/test/unit/expr/expr_white.h
+++ b/test/unit/expr/node_white.h
@@ -2,11 +2,11 @@
 
 #include <cxxtest/TestSuite.h>
 
-#include "expr/expr.h"
+#include "expr/node.h"
 
 using namespace CVC4;
 
-class ExprWhite : public CxxTest::TestSuite {
+class NodeWhite : public CxxTest::TestSuite {
 public:
 
   void testNull() {