Merge branch 'master' into strRewritesstrRewrites

5 files changed, 0 insertions, 292 deletions

diff --git a/test/unit/.gitignore b/test/unit/.gitignore
deleted file mode 100644
index 77b1fc5e3..000000000
--- a/test/unit/.gitignore
+++ /dev/null
@@ -1,4 +0,0 @@
-*_black
-*_white
-*_black.cpp
-*_white.cpp
diff --git a/test/unit/Makefile b/test/unit/Makefile
deleted file mode 100644
index 16dc971e1..000000000
--- a/test/unit/Makefile
+++ /dev/null
@@ -1,8 +0,0 @@
-topdir = ../..
-srcdir = test/unit
-
-include $(topdir)/Makefile.subdir
-
-# synonyms for "check"
-.PHONY: test
-test: check
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
deleted file mode 100644
index 0ce6368c2..000000000
--- a/test/unit/Makefile.am
+++ /dev/null
@@ -1,248 +0,0 @@
-# All unit tests
-UNIT_TESTS = \
-	expr/expr_public \
-	expr/expr_manager_public \
-	expr/type_cardinality_public \
-	util/cardinality_public
-if WHITE_AND_BLACK_TESTS
-UNIT_TESTS += \
-	base/map_util_black \
-	theory/evaluator_white \
-	theory/logic_info_white \
-	theory/theory_arith_white \
-	theory/theory_black \
-	theory/theory_bv_white \
-	theory/theory_engine_white \
-	theory/theory_quantifiers_bv_instantiator_white \
-	theory/theory_quantifiers_bv_inverter_white \
-	theory/theory_strings_rewriter_white \
-	theory/theory_white \
-	theory/type_enumerator_white \
-	expr/node_white \
-	expr/node_black \
-	expr/kind_black \
-	expr/kind_map_black \
-	expr/node_builder_black \
-	expr/node_manager_black \
-	expr/node_manager_white \
-	expr/attribute_white \
-	expr/attribute_black \
-	expr/symbol_table_black \
-	expr/node_self_iterator_black \
-	expr/type_node_white \
-	parser/parser_black \
-	parser/parser_builder_black \
-	preprocessing/pass_bv_gauss_white \
-	prop/cnf_stream_white \
-	context/context_black \
-	context/context_white \
-	context/context_mm_black \
-	context/cdo_black \
-	context/cdlist_black \
-	context/cdmap_black \
-	context/cdmap_white \
-	util/array_store_all_black \
-	util/assert_white \
-	util/check_white \
-	util/binary_heap_black \
-	util/bitvector_black \
-	util/datatype_black \
-	util/configuration_black \
-	util/output_black \
-	util/exception_black \
-	util/integer_black \
-	util/integer_white \
-	util/listener_black \
-	util/rational_black \
-	util/rational_white \
-	util/stats_black \
-	util/boolean_simplification_black \
-	main/interactive_shell_black
-endif
-
-export VERBOSE = 1
-
-# Things that aren't tests but that tests rely on and need to
-# go into the distribution
-TEST_DEPS_DIST = \
-	memory.h \
-	Makefile.tests
-
-if HAVE_CXXTESTGEN
-
-AM_CPPFLAGS = \
-	-I. \
-	"-I@top_builddir@/src" \
-	"-I@top_srcdir@/src/include" \
-	"-I@top_srcdir@/lib" \
-	"-I@top_srcdir@/src" \
-	"-I@top_srcdir@/src/prop/minisat" \
-	-D __STDC_LIMIT_MACROS \
-	-D __STDC_FORMAT_MACROS \
-	$(ANTLR_INCLUDES) \
-	$(TEST_CPPFLAGS)
-AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(TEST_CXXFLAGS)
-AM_LDFLAGS = $(TEST_LDFLAGS) $(READLINE_LIBS) $(LIBS)
-CXXFLAGS=-Wno-suggest-override
-
-AM_CXXFLAGS_WHITE = -fno-access-control -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST
-AM_CXXFLAGS_BLACK = -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST
-AM_CXXFLAGS_PUBLIC =
-AM_LDFLAGS_WHITE =
-AM_LDFLAGS_BLACK =
-AM_LDFLAGS_PUBLIC =
-AM_LIBADD_WHITE = \
-	@abs_top_builddir@/src/main/libmain.a \
-	@abs_top_builddir@/src/parser/libcvc4parser.la \
-	@abs_top_builddir@/src/libcvc4.la
-AM_LIBADD_BLACK = \
-	@abs_top_builddir@/src/main/libmain.a \
-	@abs_top_builddir@/src/parser/libcvc4parser.la \
-	@abs_top_builddir@/src/libcvc4.la
-AM_LIBADD_PUBLIC = \
-	@abs_top_builddir@/src/parser/libcvc4parser.la \
-	@abs_top_builddir@/src/libcvc4.la
-
-EXTRA_DIST = \
-	no_cxxtest \
-	$(UNIT_TESTS:%=%.cpp) \
-	$(UNIT_TESTS:%=%.h) \
-	$(TEST_DEPS_DIST)
-
-MOSTLYCLEANFILES = $(UNIT_TESTS) $(UNIT_TESTS:%=%.cpp) $(UNIT_TESTS:%=%.lo)
-DISTCLEANFILES = $(UNIT_TESTS:%=@DEPDIR@/%.Plo)
-
-# the tests automake infrastructure doesn't clean up .o files :-(
-# handle both .libs and _libs variants
-mostlyclean-local:
-	@for f in $(UNIT_TESTS); do \
-		dir="$$(dirname "$$f")"; fil="$$(basename "$$f")"; \
-		for junk in	"$$dir/.libs/$$fil.o" \
-				"$$dir/_libs/$$fil.o" \
-				"$$dir/.libs/lt-$$fil" \
-				"$$dir/_libs/lt-$$fil" \
-				"$$dir/.libs/$$fil" \
-				"$$dir/_libs/$$fil"; do \
-			if test -e "$$junk"; then \
-				echo "rm -f \"$$junk\""; \
-				rm -f "$$junk"; \
-			fi; \
-		done; \
-	done
-
-@mk_include@ @srcdir@/Makefile.tests
-
-# We leave "TESTS" empty here; it's handled in Makefile.tests (see
-# that file for comment)
-TESTS = $(UNIT_TESTS)
-
-if STATIC_BINARY
-unit_LINK = $(CXXLINK) -all-static
-else
-unit_LINK = $(CXXLINK)
-endif
-
-@AMDEP_TRUE@@am__include@ $(UNIT_TESTS:%=@am__quote@./@DEPDIR@/%.Plo@am__quote@)
-
-$(UNIT_TESTS:%=@am__quote@./@DEPDIR@/%.Plo@am__quote@): %.Plo:
-	$(AM_V_at)$(MKDIR_P) `dirname "$@"`
-	$(AM_V_GEN)test -e "$@" || touch "$@"
-
-$(UNIT_TESTS:%=@abs_builddir@/%.cpp): @abs_builddir@/%.cpp: %.h
-	$(AM_V_at)$(MKDIR_P) `dirname "$@"`
-	$(AM_V_GEN)$(CXXTESTGEN) --no-static-init --have-eh --have-std --error-printer -o "$@" "$<"
-
-$(WHITE_TESTS:%=%.lo): %_white.lo: @abs_builddir@/%_white.cpp
-@am__fastdepCXX_TRUE@	$(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -MT $@ -MD -MP -MF $(DEPDIR)/$(@:%.lo=%).Tpo -c -o $@ $<
-@am__fastdepCXX_TRUE@	$(AM_V_at)$(am__mv) $(DEPDIR)/$(@:%.lo=%).Tpo $(DEPDIR)/$(@:%.lo=%).Plo
-@am__fastdepCXX_FALSE@	$(AM_V_CXX) @AM_BACKSLASH@
-@AMDEP_TRUE@@am__fastdepCXX_FALSE@	source='$<' object='$@' libtool=yes @AMDEPBACKSLASH@
-@AMDEP_TRUE@@am__fastdepCXX_FALSE@	DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
-@am__fastdepCXX_FALSE@	$(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@ $<
-
-$(WHITE_TESTS): %_white: %_white.lo $(AM_LIBADD_WHITE)
-	$(AM_V_CXXLD)$(unit_LINK) $(AM_LIBADD_WHITE) $(AM_LDFLAGS) $(AM_LDFLAGS_WHITE) $<
-
-$(BLACK_TESTS:%=%.lo): %_black.lo: @abs_builddir@/%_black.cpp
-@am__fastdepCXX_TRUE@	$(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -MT $@ -MD -MP -MF $(DEPDIR)/$(@:%.lo=%).Tpo -c -o $@ $<
-@am__fastdepCXX_TRUE@	$(AM_V_at)$(am__mv) $(DEPDIR)/$(@:%.lo=%).Tpo $(DEPDIR)/$(@:%.lo=%).Plo
-@am__fastdepCXX_FALSE@	$(AM_V_CXX) @AM_BACKSLASH@
-@AMDEP_TRUE@@am__fastdepCXX_FALSE@	source='$<' object='$@' libtool=yes @AMDEPBACKSLASH@
-@AMDEP_TRUE@@am__fastdepCXX_FALSE@	DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
-@am__fastdepCXX_FALSE@	$(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -c -o $@ $<
-
-$(BLACK_TESTS): %_black: %_black.lo $(AM_LIBADD_BLACK)
-	$(AM_V_CXXLD)$(unit_LINK) $(AM_LIBADD_BLACK) $(AM_LDFLAGS) $(AM_LDFLAGS_BLACK) $<
-
-$(PUBLIC_TESTS:%=%.lo): %_public.lo: @abs_builddir@/%_public.cpp
-@am__fastdepCXX_TRUE@	$(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -MT $@ -MD -MP -MF $(DEPDIR)/$(@:%.lo=%).Tpo -c -o $@ $<
-@am__fastdepCXX_TRUE@	$(AM_V_at)$(am__mv) $(DEPDIR)/$(@:%.lo=%).Tpo $(DEPDIR)/$(@:%.lo=%).Plo
-@am__fastdepCXX_FALSE@	$(AM_V_CXX) @AM_BACKSLASH@
-@AMDEP_TRUE@@am__fastdepCXX_FALSE@	source='$<' object='$@' libtool=yes @AMDEPBACKSLASH@
-@AMDEP_TRUE@@am__fastdepCXX_FALSE@	DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
-@am__fastdepCXX_FALSE@	$(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@ $<
-
-$(PUBLIC_TESTS): %_public: %_public.lo $(AM_LIBADD_PUBLIC)
-	$(AM_V_CXXLD)$(unit_LINK) $(AM_LIBADD_PUBLIC) $(AM_LDFLAGS) $(AM_LDFLAGS_PUBLIC) $<
-
-else
-
-# force a user-visible failure for "make check"
-TESTS = no_cxxtest
-
-EXTRA_DIST = \
-	no_cxxtest \
-	$(UNIT_TESTS:%=%.h) \
-	$(TEST_DEPS_DIST) \
-	no-cxxtest-available
-
-endif
-
-$(UNIT_TESTS:%=%.cpp): $(UNIT_TESTS:%=@abs_builddir@/%.cpp)
-
-# trick automake into setting LTCXXCOMPILE, CXXLINK, etc.
-if CVC4_FALSE
-noinst_LTLIBRARIES = libdummy.la
-nodist_libdummy_la_SOURCES = expr/node_black.cpp
-libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la
-endif
-
-# synonyms for "check" in this directory in this directory
-.PHONY: units test
-units test: check
-
-# no-ops here
-.PHONY: systemtests regress regress0 regress1 regress2 regress3 regress4
-regress regress0 regress1 regress2 regress3 regress4:
-
-if HAVE_CXXTESTGEN
-# all is fine with the world
-else
-# all is not !
-no-cxxtest-available:
-	@if test "$(I_REALLY_WANT_TO_BUILD_CVC4_DIST_WITHOUT_TESTS)" = 1; then \
-		echo; \
-		echo "WARNING:"; \
-		echo "WARNING: No CxxTest to build unit tests, but, then, you know that;"; \
-		echo "WARNING: I hope you know what you're doing."; \
-		echo "WARNING:"; \
-		echo; \
-		( echo "CxxTest was not available at the time this distribution was built,"; \
-		  echo "so the tests could not be built.  You'll need CxxTest to test this"; \
-		  echo "distribution." ) >no-cxxtest-available; \
-	else \
-		echo; \
-		echo "ERROR:"; \
-		echo "ERROR: You cannot make dist in this build directory, you do not have CxxTest."; \
-		echo "ERROR: The tests should be generated for the user and included in the tarball,"; \
-		echo "ERROR: otherwise they'll be required to have CxxTest just to test the standard"; \
-		echo "ERROR: distribution built correctly."; \
-		echo "ERROR: If you really want to do this, append the following to your make command."; \
-		echo "ERROR:"; \
-		echo "ERROR:     I_REALLY_WANT_TO_BUILD_CVC4_DIST_WITHOUT_TESTS=1"; \
-		echo "ERROR:"; \
-		echo; \
-		exit 1; \
-	fi >&2
-endif
-
diff --git a/test/unit/Makefile.tests b/test/unit/Makefile.tests
deleted file mode 100644
index e3ec536ce..000000000
--- a/test/unit/Makefile.tests
+++ /dev/null
@@ -1,20 +0,0 @@
-# This makefile is separated because it's not under automake control.
-# This gets confusing, because we want:
-#
-#  1. to (re)build only the tests in the "filtered" set of tests
-#     (those that we're going to run)
-#  2. run only the tests in the "filtered" set of tests.
-#
-# It's a pain to make automake happy.
-
-# Add "filtered" tests to the set of TESTS
-TESTS = $(filter $(TEST_PREFIX)%,$(filter %$(TEST_SUFFIX),$(UNIT_TESTS)))
-
-# subsets of the tests, based on name
-WHITE_TESTS = $(filter %_white,$(UNIT_TESTS))
-BLACK_TESTS = $(filter %_black,$(UNIT_TESTS))
-PUBLIC_TESTS = $(filter %_public,$(UNIT_TESTS))
-
-# This rule forces automake to correctly build our filtered
-# set of tests
-check-TESTS: $(TESTS)
diff --git a/test/unit/no_cxxtest b/test/unit/no_cxxtest
deleted file mode 100755
index fec2dfb82..000000000
--- a/test/unit/no_cxxtest
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/bin/sh
-
-echo
-echo '***************************************************************************'
-echo '*                                                                         *'
-echo '*  WARNING:  CxxTest not found at configure time; unit tests cannot run.  *'
-echo '*                                                                         *'
-echo '***************************************************************************'
-echo
-
-# skip this test, rather than reporting an error
-exit 77