From: Morgan Deters Date: Fri, 20 Nov 2009 23:47:56 +0000 (+0000) Subject: fixes to build/test system X-Git-Tag: cvc5-1.0.0~9417 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=95e5ca98d4c22897c0192a78ebeeb05e4838db2b;p=cvc5.git fixes to build/test system --- 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 -ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& end) { -} - void ExprBuilder::addChild(const Expr& e) { if(d_nchildren == nchild_thresh) { vector* v = new vector(); 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 +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/expr/expr_black.h b/test/expr/expr_black.h deleted file mode 100644 index 97746d1c4..000000000 --- a/test/expr/expr_black.h +++ /dev/null @@ -1,19 +0,0 @@ -/* Black box testing of CVC4::Expr. */ - -#include - -#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 index b6bfdd394..000000000 --- a/test/expr/expr_white.h +++ /dev/null @@ -1,19 +0,0 @@ -/* White box testing of CVC4::Expr. */ - -#include - -#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 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/unit/expr/expr_black.h b/test/unit/expr/expr_black.h new file mode 100644 index 000000000..97746d1c4 --- /dev/null +++ b/test/unit/expr/expr_black.h @@ -0,0 +1,19 @@ +/* Black box testing of CVC4::Expr. */ + +#include + +#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 index 000000000..b6bfdd394 --- /dev/null +++ b/test/unit/expr/expr_white.h @@ -0,0 +1,19 @@ +/* White box testing of CVC4::Expr. */ + +#include + +#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); + } +};