fixes to build/test system

diff --git a/Makefile.am b/Makefile.am
index 74a28a51ccaeece402d4ac09a0e52a6883e44a30..b3e12c811f7d3465e03789bda4b7ff3ca83ff834 100644 (file)
--- 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 e569dc5abced7e3801202dd40e609cd40fad4e3e..b7e7975f7ad0e76e3b1d8b3bff3e9604e51f71ff 100644 (file)
--- 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 57a67d6e50d4da59a3eab40c9e7a1c95d6f97c1f..f7404e5149df52042142399194aa92d3d724a579 100644 (file)
--- 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 00858fb7b6ca58d0a047b323ca6e25d42b92a19c..87a4598c4a3f1454dacf8951408763ea38263afc 100644 (file)
--- 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 17b7d8dcd77532a053fcc308cdbd2415553b318c..da2839ad10c177f3eb84667e60c878db1d9a0981 100644 (file)
--- 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 3b0cf40417b5394b13c3ca5dc6f0c7d42f4c03fe..c5f366654b9432d5e2d9f0a2019ca8e0b17506ee 100644 (file)
--- 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 fc303572d4fa56088ebbac09a292742c4aa37378..07d069a9ea55909e7c70bcfe96a247d8f6ffe576 100644 (file)
--- 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 8f400241baf530c3fb41dbaba9c7ba675f92ac27..cf392f6b695640eaf4fe8785d8aef10820ae75b8 100644 (file)
--- 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 2a1b83dba74f38750b5688cc63da53b8a27a92b8..8ea47d1406f3a2e3e9cf48101e7670cf5d2af07b 100644 (file)
--- 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 97cfc438a381217a2285a76772cbe5afdc1b9250..db646fef454b22ac70f31cecf0c9341cfba78e91 100644 (file)
--- 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 ff740aa56013ded34f77de775ff03b9e546ade67..c2967ad146be40a24c6f0107baf7a422d4e08c59 100644 (file)
--- 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 f022d0445fd7aecc3a9afec84b7fc1aa5b06a294..97cb116e0e605056bd82d1a9c6a8c432b6eae152 100644 (file)
--- 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 4158936807bbcb0efb2d1815a68b793ea72bd1af..f25f52ac0fcb4ae7797a4f6d924d922253e8f708 100644 (file)
--- 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 bf74eaa47fa850b42bca6f254e3fcc5f0e86ed46..ff449f768a291f4dbf972d782bd7d89139fa791f 100644 (file)
--- 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/expr/expr_black.h b/test/expr/expr_black.h
deleted file mode 100644 (file)
index 97746d1..0000000
--- a/test/expr/expr_black.h
+++ /dev/null
@@ -1,19 +0,0 @@
-/* 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
deleted file mode 100644 (file)
index b6bfdd3..0000000
--- a/test/expr/expr_white.h
+++ /dev/null
@@ -1,19 +0,0 @@
-/* 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/regress/Makefile.am b/test/regress/Makefile.am
new file mode 100644 (file)
index 0000000..61deb03
--- /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 (file)
index 0000000..d2c24a4
--- /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 (file)
index 0000000..0f9df5e
--- /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/unit/expr/expr_black.h b/test/unit/expr/expr_black.h
new file mode 100644 (file)
index 0000000..97746d1
--- /dev/null
+++ b/test/unit/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/unit/expr/expr_white.h b/test/unit/expr/expr_white.h
new file mode 100644 (file)
index 0000000..b6bfdd3
--- /dev/null
+++ b/test/unit/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);
+  }
+};