fixes to build/test system

19 files changed, 84 insertions, 51 deletions

diff --git a/Makefile.am b/Makefile.am
index 74a28a51c..b3e12c811 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -5,5 +5,3 @@ ACLOCAL_AMFLAGS = -I config
 
 SUBDIRS = src test doc contrib
 
-.PHONY: test
-test: check
diff --git a/configure.ac b/configure.ac
index e569dc5ab..b7e7975f7 100644
--- a/configure.ac
+++ b/configure.ac
@@ -118,6 +118,8 @@ AC_CONFIG_FILES([
   src/parser/Makefile
   src/theory/Makefile
   test/Makefile
+  test/regress/Makefile
+  test/unit/Makefile
 ])
 
 AC_OUTPUT
diff --git a/src/Makefile.am b/src/Makefile.am
index 57a67d6e5..f7404e514 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -1,18 +1,18 @@
 INCLUDES = -I@srcdir@/include -I@srcdir@
 AM_CXXFLAGS = -Wall -fvisibility=hidden
 
-SUBDIRS = util expr context prop smt theory parser main
+SUBDIRS = util expr context prop smt theory . parser main
 
 lib_LTLIBRARIES = libcvc4.la
 
+libcvc4_la_SOURCES =
 libcvc4_la_LIBADD = \
-	util/libutil.a \
-	expr/libexpr.a \
-	context/libcontext.a \
-	prop/minisat/libminisat.a \
-	smt/libsmt.a \
-	theory/libtheory.a \
-	parser/libparser.a
+	util/libutil.la \
+	expr/libexpr.la \
+	context/libcontext.la \
+	prop/minisat/libminisat.la \
+	smt/libsmt.la \
+	theory/libtheory.la
 
 EXTRA_DIST = \
 	include/cvc4.h \
diff --git a/src/context/Makefile.am b/src/context/Makefile.am
index 00858fb7b..87a4598c4 100644
--- a/src/context/Makefile.am
+++ b/src/context/Makefile.am
@@ -1,6 +1,6 @@
 INCLUDES = -I@srcdir@/../include -I@srcdir@/..
 AM_CXXFLAGS = -Wall -fvisibility=hidden
 
-noinst_LIBRARIES = libcontext.a
+noinst_LTLIBRARIES = libcontext.la
 
-libcontext_a_SOURCES =
+libcontext_la_SOURCES =
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 17b7d8dcd..da2839ad1 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -1,9 +1,9 @@
 INCLUDES = -I@srcdir@/../include -I@srcdir@/..
 AM_CXXFLAGS = -Wall -fvisibility=hidden
 
-noinst_LIBRARIES = libexpr.a
+noinst_LTLIBRARIES = libexpr.la
 
-libexpr_a_SOURCES = \
+libexpr_la_SOURCES = \
 	expr.cpp \
 	expr_builder.cpp \
 	expr_manager.cpp \
diff --git a/src/expr/expr_builder.cpp b/src/expr/expr_builder.cpp
index 3b0cf4041..c5f366654 100644
--- a/src/expr/expr_builder.cpp
+++ b/src/expr/expr_builder.cpp
@@ -129,10 +129,6 @@ ExprBuilder& ExprBuilder::operator<<(const Kind& op) {
 ExprBuilder& ExprBuilder::operator<<(const Expr& child) {
 }
 
-template <class Iterator>
-ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& end) {
-}
-
 void ExprBuilder::addChild(const Expr& e) {
   if(d_nchildren == nchild_thresh) {
     vector<Expr>* v = new vector<Expr>();
diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h
index fc303572d..07d069a9e 100644
--- a/src/expr/expr_builder.h
+++ b/src/expr/expr_builder.h
@@ -154,6 +154,11 @@ public:
 
 };/* class MultExprBuilder */
 
+template <class Iterator>
+ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& end) {
+  return *this;
+}
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__EXPR_BUILDER_H */
diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index 8f400241b..cf392f6b6 100644
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -7,3 +7,7 @@ cvc4_SOURCES = \
 	main.cpp \
 	getopt.cpp \
 	util.cpp
+
+cvc4_LDADD = \
+	../parser/libparser.la \
+	../libcvc4.la
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 2a1b83dba..8ea47d140 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -1,9 +1,9 @@
 INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -I@builddir@
 AM_CXXFLAGS = -Wall -fvisibility=hidden
 
-noinst_LIBRARIES = libparser.a
+noinst_LTLIBRARIES = libparser.la
 
-libparser_a_SOURCES = \
+libparser_la_SOURCES = \
 	pl_scanner.lpp \
 	pl.ypp \
 	smtlib_scanner.lpp \
diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am
index 97cfc438a..db646fef4 100644
--- a/src/prop/minisat/Makefile.am
+++ b/src/prop/minisat/Makefile.am
@@ -1,7 +1,7 @@
 INCLUDES = -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../../include
 AM_CXXFLAGS = -Wall -fvisibility=hidden
 
-noinst_LIBRARIES = libminisat.a
-libminisat_a_SOURCES = \
+noinst_LTLIBRARIES = libminisat.la
+libminisat_la_SOURCES = \
 	core/Solver.C \
 	simp/SimpSolver.C
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index ff740aa56..c2967ad14 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -1,6 +1,6 @@
 INCLUDES = -I@srcdir@/../include -I@srcdir@/..
 AM_CXXFLAGS = -Wall -fvisibility=hidden
 
-noinst_LIBRARIES = libsmt.a
+noinst_LTLIBRARIES = libsmt.la
 
-libsmt_a_SOURCES =
+libsmt_la_SOURCES =
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index f022d0445..97cb116e0 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -1,6 +1,6 @@
 INCLUDES = -I@srcdir@/../include -I@srcdir@/..
 AM_CXXFLAGS = -Wall -fvisibility=hidden
 
-noinst_LIBRARIES = libtheory.a
+noinst_LTLIBRARIES = libtheory.la
 
-libtheory_a_SOURCES =
+libtheory_la_SOURCES =
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 415893680..f25f52ac0 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -1,6 +1,6 @@
 INCLUDES = -I@srcdir@/../include -I@srcdir@/..
 AM_CXXFLAGS = -Wall -fvisibility=hidden
 
-noinst_LIBRARIES = libutil.a
+noinst_LTLIBRARIES = libutil.la
 
-libutil_a_SOURCES =
+libutil_la_SOURCES =
diff --git a/test/Makefile.am b/test/Makefile.am
index bf74eaa47..ff449f768 100644
--- a/test/Makefile.am
+++ b/test/Makefile.am
@@ -1,23 +1 @@
-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
-
+SUBDIRS = unit regress
diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am
new file mode 100644
index 000000000..61deb03e6
--- /dev/null
+++ b/test/regress/Makefile.am
@@ -0,0 +1,3 @@
+TESTS_ENVIRONMENT = echo
+TESTS = \
+	bug1.cvc
diff --git a/test/regress/bug1.cvc b/test/regress/bug1.cvc
new file mode 100644
index 000000000..d2c24a438
--- /dev/null
+++ b/test/regress/bug1.cvc
@@ -0,0 +1,11 @@
+%% Regression level = 0
+%% Result = Valid
+%% Runtime = 1
+%% Language = presentation
+x : REAL;
+y : REAL;
+f : REAL -> REAL;
+ASSERT ((x > y) => f(x) > f (y));
+ASSERT (x = 3);
+ASSERT (y = 2);
+QUERY(f(x) > f (y));
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
new file mode 100644
index 000000000..0f9df5e2f
--- /dev/null
+++ b/test/unit/Makefile.am
@@ -0,0 +1,36 @@
+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.la
+TESTS = \
+	expr/expr_black \
+	expr/expr_white
+
+lib_LTLIBRARIES = libdummy.la
+libdummy_la_SOURCES = expr/expr_black.cpp
+libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la
+
+$(TESTS:%=%.cpp): %.cpp: %.h
+	$(CXXTESTGEN) --have-eh --have-std --error-printer -o $@ $<
+$(TESTS): %: %.cpp
+#	get these in here somehow
+#	$(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS)
+	$(LTCXXCOMPILE) -c -o $@.lo $<
+	$(CXXLINK) $@.lo \
+		@abs_top_builddir@/src/context/libcontext.la \
+		@abs_top_builddir@/src/expr/libexpr.la \
+		@abs_top_builddir@/src/smt/libsmt.la \
+		@abs_top_builddir@/src/theory/libtheory.la \
+		@abs_top_builddir@/src/util/libutil.la \
+		@abs_top_builddir@/src/prop/minisat/libminisat.la
+
+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/unit/expr/expr_black.h
index 97746d1c4..97746d1c4 100644
--- a/test/expr/expr_black.h
+++ b/test/unit/expr/expr_black.h
diff --git a/test/expr/expr_white.h b/test/unit/expr/expr_white.h
index b6bfdd394..b6bfdd394 100644
--- a/test/expr/expr_white.h
+++ b/test/unit/expr/expr_white.h