-.PHONY: _default_build_
-_default_build_: all
-%:
- @if test -e builds; then \
- echo cd builds; \
- cd builds; \
- echo $(MAKE) $@; \
- $(MAKE) $@; \
- else \
- echo; \
- echo 'Run configure first, or type "make" in a configured build directory.'; \
- echo; \
- fi
+builddir = builds
-distclean:
- @if test -e builds; then \
- echo cd builds; \
- cd builds; \
- echo $(MAKE) $@; \
- $(MAKE) $@; \
- fi
- rm -rf builds
+include Makefile.subdir
CXXCPP = @CXXCPP@
CXXDEPMODE = @CXXDEPMODE@
CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
CXXTESTGEN = @CXXTESTGEN@
CYGPATH_W = @CYGPATH_W@
DEFS = @DEFS@
--- /dev/null
+.PHONY: _default_build_
+_default_build_: all
+%:
+ @if test -e $(builddir); then \
+ echo cd $(builddir); \
+ cd $(builddir); \
+ echo $(MAKE) $@; \
+ $(MAKE) $@; \
+ else \
+ echo; \
+ echo 'Run configure first, or type "make" in a configured build directory.'; \
+ echo; \
+ fi
set -ex
cd "$(dirname "$0")"
-libtoolize --copy
-aclocal -I config
-autoheader -I config
+libtoolize -cf || glibtoolize -cf
+aclocal -I config --force --install -Wall
+autoheader -I config -f -Wall
touch NEWS README AUTHORS ChangeLog
touch stamp-h
-autoconf -I config
-automake -ac --foreign -Woverride
+autoconf -I config --force -Wall
+automake -acf --foreign -Woverride -Wall
# Get the location of the runantlr script
AC_ARG_WITH(
[antlr],
- AC_HELP_STRING(
+ AS_HELP_STRING(
[--with-antlr=RUNANTLR],
[location of the ANTLR's `runantlr` script]
),
# Get the location of the ANTLR c++ includes and libraries
AC_ARG_WITH(
[antlr-prefix],
- AC_HELP_STRING(
+ AS_HELP_STRING(
[--with-antlr-prefix=PATH],
[set the search path for ANTLR headers and libraries to `PATH/include`
and `PATH/lib`. By default we look in /usr, /usr/local, /opt and
HAVE_CXXTESTGEN_FALSE
HAVE_CXXTESTGEN_TRUE
CXXTESTGEN
+CXXTEST
DOXYGEN
ANTLR
CXXCPP
ac_ct_CXX
CXXFLAGS
CXX
-DLLTOOL
-AS
CPP
OTOOL64
OTOOL
lt_ECHO
RANLIB
AR
-OBJDUMP
LN_S
NM
ac_ct_DUMPBIN
CFLAGS
CC
LIBTOOL
+OBJDUMP
+DLLTOOL
+AS
am__untar
am__tar
AMTAR
CCC
CXXCPP
DOXYGEN
+CXXTEST
TEST_CPPFLAGS
TEST_CXXFLAGS
TEST_LDFLAGS'
CXXFLAGS C++ compiler flags
CXXCPP C++ preprocessor
DOXYGEN location of doxygen binary
+ CXXTEST path to cxxtest installation
TEST_CPPFLAGS
CXXFLAGS to use when testing (default=$CPPFLAGS)
TEST_CXXFLAGS
ac_compiler_gnu=$ac_cv_c_compiler_gnu
+
ac_aux_dir=
for ac_dir in config "$srcdir"/config; do
for ac_t in install-sh install.sh shtool; do
(echo "# This is the most-recently-configured CVC4 build"; \
echo "# 'make' in the top-level source directory applies to this build"; \
echo "CURRENT_BUILD = $target/$build_type") > builds/current
+ echo Linking builds/src...
+ rm -f builds/src
+ ln -sfv "$target/$build_type/src" builds/src
+ echo Linking builds/test...
+ rm -f builds/test
+ ln -sfv "$target/$build_type/test" builds/test
echo cd "builds/$target/$build_type"
cd "builds/$target/$build_type"
CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: ${LDFLAGS-none}" >&5
$as_echo "${LDFLAGS-none}" >&6; }
+enable_win32_dll=yes
+
+case $host in
+*-*-cygwin* | *-*-mingw* | *-*-pw32* | *-cegcc*)
+ if test -n "$ac_tool_prefix"; then
+ # Extract the first word of "${ac_tool_prefix}as", so it can be a program name with args.
+set dummy ${ac_tool_prefix}as; ac_word=$2
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
+$as_echo_n "checking for $ac_word... " >&6; }
+if test "${ac_cv_prog_AS+set}" = set; then :
+ $as_echo_n "(cached) " >&6
+else
+ if test -n "$AS"; then
+ ac_cv_prog_AS="$AS" # Let the user override the test.
+else
+as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
+for as_dir in $PATH
+do
+ IFS=$as_save_IFS
+ test -z "$as_dir" && as_dir=.
+ for ac_exec_ext in '' $ac_executable_extensions; do
+ if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
+ ac_cv_prog_AS="${ac_tool_prefix}as"
+ $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
+ break 2
+ fi
+done
+ done
+IFS=$as_save_IFS
+
+fi
+fi
+AS=$ac_cv_prog_AS
+if test -n "$AS"; then
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: $AS" >&5
+$as_echo "$AS" >&6; }
+else
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
+$as_echo "no" >&6; }
+fi
+
+
+fi
+if test -z "$ac_cv_prog_AS"; then
+ ac_ct_AS=$AS
+ # Extract the first word of "as", so it can be a program name with args.
+set dummy as; ac_word=$2
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
+$as_echo_n "checking for $ac_word... " >&6; }
+if test "${ac_cv_prog_ac_ct_AS+set}" = set; then :
+ $as_echo_n "(cached) " >&6
+else
+ if test -n "$ac_ct_AS"; then
+ ac_cv_prog_ac_ct_AS="$ac_ct_AS" # Let the user override the test.
+else
+as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
+for as_dir in $PATH
+do
+ IFS=$as_save_IFS
+ test -z "$as_dir" && as_dir=.
+ for ac_exec_ext in '' $ac_executable_extensions; do
+ if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
+ ac_cv_prog_ac_ct_AS="as"
+ $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
+ break 2
+ fi
+done
+ done
+IFS=$as_save_IFS
+
+fi
+fi
+ac_ct_AS=$ac_cv_prog_ac_ct_AS
+if test -n "$ac_ct_AS"; then
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_ct_AS" >&5
+$as_echo "$ac_ct_AS" >&6; }
+else
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
+$as_echo "no" >&6; }
+fi
+
+ if test "x$ac_ct_AS" = x; then
+ AS="false"
+ else
+ case $cross_compiling:$ac_tool_warned in
+yes:)
+{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: using cross tools not prefixed with host triplet" >&5
+$as_echo "$as_me: WARNING: using cross tools not prefixed with host triplet" >&2;}
+ac_tool_warned=yes ;;
+esac
+ AS=$ac_ct_AS
+ fi
+else
+ AS="$ac_cv_prog_AS"
+fi
+
+ if test -n "$ac_tool_prefix"; then
+ # Extract the first word of "${ac_tool_prefix}dlltool", so it can be a program name with args.
+set dummy ${ac_tool_prefix}dlltool; ac_word=$2
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
+$as_echo_n "checking for $ac_word... " >&6; }
+if test "${ac_cv_prog_DLLTOOL+set}" = set; then :
+ $as_echo_n "(cached) " >&6
+else
+ if test -n "$DLLTOOL"; then
+ ac_cv_prog_DLLTOOL="$DLLTOOL" # Let the user override the test.
+else
+as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
+for as_dir in $PATH
+do
+ IFS=$as_save_IFS
+ test -z "$as_dir" && as_dir=.
+ for ac_exec_ext in '' $ac_executable_extensions; do
+ if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
+ ac_cv_prog_DLLTOOL="${ac_tool_prefix}dlltool"
+ $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
+ break 2
+ fi
+done
+ done
+IFS=$as_save_IFS
+
+fi
+fi
+DLLTOOL=$ac_cv_prog_DLLTOOL
+if test -n "$DLLTOOL"; then
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: $DLLTOOL" >&5
+$as_echo "$DLLTOOL" >&6; }
+else
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
+$as_echo "no" >&6; }
+fi
+
+
+fi
+if test -z "$ac_cv_prog_DLLTOOL"; then
+ ac_ct_DLLTOOL=$DLLTOOL
+ # Extract the first word of "dlltool", so it can be a program name with args.
+set dummy dlltool; ac_word=$2
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
+$as_echo_n "checking for $ac_word... " >&6; }
+if test "${ac_cv_prog_ac_ct_DLLTOOL+set}" = set; then :
+ $as_echo_n "(cached) " >&6
+else
+ if test -n "$ac_ct_DLLTOOL"; then
+ ac_cv_prog_ac_ct_DLLTOOL="$ac_ct_DLLTOOL" # Let the user override the test.
+else
+as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
+for as_dir in $PATH
+do
+ IFS=$as_save_IFS
+ test -z "$as_dir" && as_dir=.
+ for ac_exec_ext in '' $ac_executable_extensions; do
+ if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
+ ac_cv_prog_ac_ct_DLLTOOL="dlltool"
+ $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
+ break 2
+ fi
+done
+ done
+IFS=$as_save_IFS
+
+fi
+fi
+ac_ct_DLLTOOL=$ac_cv_prog_ac_ct_DLLTOOL
+if test -n "$ac_ct_DLLTOOL"; then
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_ct_DLLTOOL" >&5
+$as_echo "$ac_ct_DLLTOOL" >&6; }
+else
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
+$as_echo "no" >&6; }
+fi
+
+ if test "x$ac_ct_DLLTOOL" = x; then
+ DLLTOOL="false"
+ else
+ case $cross_compiling:$ac_tool_warned in
+yes:)
+{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: using cross tools not prefixed with host triplet" >&5
+$as_echo "$as_me: WARNING: using cross tools not prefixed with host triplet" >&2;}
+ac_tool_warned=yes ;;
+esac
+ DLLTOOL=$ac_ct_DLLTOOL
+ fi
+else
+ DLLTOOL="$ac_cv_prog_DLLTOOL"
+fi
+
+ if test -n "$ac_tool_prefix"; then
+ # Extract the first word of "${ac_tool_prefix}objdump", so it can be a program name with args.
+set dummy ${ac_tool_prefix}objdump; ac_word=$2
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
+$as_echo_n "checking for $ac_word... " >&6; }
+if test "${ac_cv_prog_OBJDUMP+set}" = set; then :
+ $as_echo_n "(cached) " >&6
+else
+ if test -n "$OBJDUMP"; then
+ ac_cv_prog_OBJDUMP="$OBJDUMP" # Let the user override the test.
+else
+as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
+for as_dir in $PATH
+do
+ IFS=$as_save_IFS
+ test -z "$as_dir" && as_dir=.
+ for ac_exec_ext in '' $ac_executable_extensions; do
+ if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
+ ac_cv_prog_OBJDUMP="${ac_tool_prefix}objdump"
+ $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
+ break 2
+ fi
+done
+ done
+IFS=$as_save_IFS
+
+fi
+fi
+OBJDUMP=$ac_cv_prog_OBJDUMP
+if test -n "$OBJDUMP"; then
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: $OBJDUMP" >&5
+$as_echo "$OBJDUMP" >&6; }
+else
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
+$as_echo "no" >&6; }
+fi
+
+
+fi
+if test -z "$ac_cv_prog_OBJDUMP"; then
+ ac_ct_OBJDUMP=$OBJDUMP
+ # Extract the first word of "objdump", so it can be a program name with args.
+set dummy objdump; ac_word=$2
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
+$as_echo_n "checking for $ac_word... " >&6; }
+if test "${ac_cv_prog_ac_ct_OBJDUMP+set}" = set; then :
+ $as_echo_n "(cached) " >&6
+else
+ if test -n "$ac_ct_OBJDUMP"; then
+ ac_cv_prog_ac_ct_OBJDUMP="$ac_ct_OBJDUMP" # Let the user override the test.
+else
+as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
+for as_dir in $PATH
+do
+ IFS=$as_save_IFS
+ test -z "$as_dir" && as_dir=.
+ for ac_exec_ext in '' $ac_executable_extensions; do
+ if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
+ ac_cv_prog_ac_ct_OBJDUMP="objdump"
+ $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
+ break 2
+ fi
+done
+ done
+IFS=$as_save_IFS
+
+fi
+fi
+ac_ct_OBJDUMP=$ac_cv_prog_ac_ct_OBJDUMP
+if test -n "$ac_ct_OBJDUMP"; then
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_ct_OBJDUMP" >&5
+$as_echo "$ac_ct_OBJDUMP" >&6; }
+else
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
+$as_echo "no" >&6; }
+fi
+
+ if test "x$ac_ct_OBJDUMP" = x; then
+ OBJDUMP="false"
+ else
+ case $cross_compiling:$ac_tool_warned in
+yes:)
+{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: using cross tools not prefixed with host triplet" >&5
+$as_echo "$as_me: WARNING: using cross tools not prefixed with host triplet" >&2;}
+ac_tool_warned=yes ;;
+esac
+ OBJDUMP=$ac_ct_OBJDUMP
+ fi
+else
+ OBJDUMP="$ac_cv_prog_OBJDUMP"
+fi
+
+ ;;
+esac
+
+test -z "$AS" && AS=as
+
+
+
+
+
+test -z "$DLLTOOL" && DLLTOOL=dlltool
+
+
+
+
+
+test -z "$OBJDUMP" && OBJDUMP=objdump
+
+
+
+
+
case `pwd` in
*\ * | *\ *)
{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: Libtool does not cope well with whitespace in \`pwd\`" >&5
else
lt_cv_nm_interface="BSD nm"
echo "int some_variable = 0;" > conftest.$ac_ext
- (eval echo "\"\$as_me:5108: $ac_compile\"" >&5)
+ (eval echo "\"\$as_me:5419: $ac_compile\"" >&5)
(eval "$ac_compile" 2>conftest.err)
cat conftest.err >&5
- (eval echo "\"\$as_me:5111: $NM \\\"conftest.$ac_objext\\\"\"" >&5)
+ (eval echo "\"\$as_me:5422: $NM \\\"conftest.$ac_objext\\\"\"" >&5)
(eval "$NM \"conftest.$ac_objext\"" 2>conftest.err > conftest.out)
cat conftest.err >&5
- (eval echo "\"\$as_me:5114: output\"" >&5)
+ (eval echo "\"\$as_me:5425: output\"" >&5)
cat conftest.out >&5
if $GREP 'External.*some_variable' conftest.out > /dev/null; then
lt_cv_nm_interface="MS dumpbin"
-
-
-
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking how to recognize dependent libraries" >&5
$as_echo_n "checking how to recognize dependent libraries... " >&6; }
if test "${lt_cv_deplibs_check_method+set}" = set; then :
;;
*-*-irix6*)
# Find out which ABI we are using.
- echo '#line 6320 "configure"' > conftest.$ac_ext
+ echo '#line 6628 "configure"' > conftest.$ac_ext
if { { eval echo "\"\$as_me\":${as_lineno-$LINENO}: \"$ac_compile\""; } >&5
(eval $ac_compile) 2>&5
ac_status=$?
enable_dlopen=no
- enable_win32_dll=no
-
-e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
-e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
-e 's:$: $lt_compiler_flag:'`
- (eval echo "\"\$as_me:7790: $lt_compile\"" >&5)
+ (eval echo "\"\$as_me:8096: $lt_compile\"" >&5)
(eval "$lt_compile" 2>conftest.err)
ac_status=$?
cat conftest.err >&5
- echo "$as_me:7794: \$? = $ac_status" >&5
+ echo "$as_me:8100: \$? = $ac_status" >&5
if (exit $ac_status) && test -s "$ac_outfile"; then
# The compiler can only warn and ignore the option if not recognized
# So say no if there are warnings other than the usual output.
-e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
-e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
-e 's:$: $lt_compiler_flag:'`
- (eval echo "\"\$as_me:8129: $lt_compile\"" >&5)
+ (eval echo "\"\$as_me:8435: $lt_compile\"" >&5)
(eval "$lt_compile" 2>conftest.err)
ac_status=$?
cat conftest.err >&5
- echo "$as_me:8133: \$? = $ac_status" >&5
+ echo "$as_me:8439: \$? = $ac_status" >&5
if (exit $ac_status) && test -s "$ac_outfile"; then
# The compiler can only warn and ignore the option if not recognized
# So say no if there are warnings other than the usual output.
-e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
-e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
-e 's:$: $lt_compiler_flag:'`
- (eval echo "\"\$as_me:8234: $lt_compile\"" >&5)
+ (eval echo "\"\$as_me:8540: $lt_compile\"" >&5)
(eval "$lt_compile" 2>out/conftest.err)
ac_status=$?
cat out/conftest.err >&5
- echo "$as_me:8238: \$? = $ac_status" >&5
+ echo "$as_me:8544: \$? = $ac_status" >&5
if (exit $ac_status) && test -s out/conftest2.$ac_objext
then
# The compiler can only warn and ignore the option if not recognized
-e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
-e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
-e 's:$: $lt_compiler_flag:'`
- (eval echo "\"\$as_me:8289: $lt_compile\"" >&5)
+ (eval echo "\"\$as_me:8595: $lt_compile\"" >&5)
(eval "$lt_compile" 2>out/conftest.err)
ac_status=$?
cat out/conftest.err >&5
- echo "$as_me:8293: \$? = $ac_status" >&5
+ echo "$as_me:8599: \$? = $ac_status" >&5
if (exit $ac_status) && test -s out/conftest2.$ac_objext
then
# The compiler can only warn and ignore the option if not recognized
lt_dlunknown=0; lt_dlno_uscore=1; lt_dlneed_uscore=2
lt_status=$lt_dlunknown
cat > conftest.$ac_ext <<_LT_EOF
-#line 10672 "configure"
+#line 10978 "configure"
#include "confdefs.h"
#if HAVE_DLFCN_H
lt_dlunknown=0; lt_dlno_uscore=1; lt_dlneed_uscore=2
lt_status=$lt_dlunknown
cat > conftest.$ac_ext <<_LT_EOF
-#line 10768 "configure"
+#line 11074 "configure"
#include "confdefs.h"
#if HAVE_DLFCN_H
-
-striplib=
-old_striplib=
-{ $as_echo "$as_me:${as_lineno-$LINENO}: checking whether stripping libraries is possible" >&5
-$as_echo_n "checking whether stripping libraries is possible... " >&6; }
-if test -n "$STRIP" && $STRIP -V 2>&1 | $GREP "GNU strip" >/dev/null; then
- test -z "$old_striplib" && old_striplib="$STRIP --strip-debug"
- test -z "$striplib" && striplib="$STRIP --strip-unneeded"
- { $as_echo "$as_me:${as_lineno-$LINENO}: result: yes" >&5
-$as_echo "yes" >&6; }
-else
-# FIXME - insert some real tests, host_os isn't really good enough
- case $host_os in
- darwin*)
- if test -n "$STRIP" ; then
- striplib="$STRIP -x"
- old_striplib="$STRIP -S"
- { $as_echo "$as_me:${as_lineno-$LINENO}: result: yes" >&5
-$as_echo "yes" >&6; }
- else
- { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
-$as_echo "no" >&6; }
- fi
- ;;
- *)
- { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
-$as_echo "no" >&6; }
- ;;
- esac
-fi
-
-
-
-
-
-
-
-
-
-
-
-
- # Report which library types will actually be built
- { $as_echo "$as_me:${as_lineno-$LINENO}: checking if libtool supports shared libraries" >&5
-$as_echo_n "checking if libtool supports shared libraries... " >&6; }
- { $as_echo "$as_me:${as_lineno-$LINENO}: result: $can_build_shared" >&5
-$as_echo "$can_build_shared" >&6; }
-
- { $as_echo "$as_me:${as_lineno-$LINENO}: checking whether to build shared libraries" >&5
-$as_echo_n "checking whether to build shared libraries... " >&6; }
- test "$can_build_shared" = "no" && enable_shared=no
-
- # On AIX, shared libraries and static libraries use the same namespace, and
- # are all built from PIC.
- case $host_os in
- aix3*)
- test "$enable_shared" = yes && enable_static=no
- if test -n "$RANLIB"; then
- archive_cmds="$archive_cmds~\$RANLIB \$lib"
- postinstall_cmds='$RANLIB $lib'
- fi
- ;;
-
- aix[4-9]*)
- if test "$host_cpu" != ia64 && test "$aix_use_runtimelinking" = no ; then
- test "$enable_shared" = yes && enable_static=no
- fi
- ;;
- esac
- { $as_echo "$as_me:${as_lineno-$LINENO}: result: $enable_shared" >&5
-$as_echo "$enable_shared" >&6; }
-
- { $as_echo "$as_me:${as_lineno-$LINENO}: checking whether to build static libraries" >&5
-$as_echo_n "checking whether to build static libraries... " >&6; }
- # Make sure either enable_shared or enable_static is yes.
- test "$enable_shared" = yes || enable_static=yes
- { $as_echo "$as_me:${as_lineno-$LINENO}: result: $enable_static" >&5
-$as_echo "$enable_static" >&6; }
-
-
-
-
-fi
-ac_ext=c
-ac_cpp='$CPP $CPPFLAGS'
-ac_compile='$CC -c $CFLAGS $CPPFLAGS conftest.$ac_ext >&5'
-ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5'
-ac_compiler_gnu=$ac_cv_c_compiler_gnu
-
-CC="$lt_save_CC"
-
-
-
-
-
-
-
-
-
-
-
-
-
- ac_config_commands="$ac_config_commands libtool"
-
-
-
-
-# Only expand once:
-
-
-
-enable_win32_dll=yes
-
-case $host in
-*-*-cygwin* | *-*-mingw* | *-*-pw32* | *-cegcc*)
- if test -n "$ac_tool_prefix"; then
- # Extract the first word of "${ac_tool_prefix}as", so it can be a program name with args.
-set dummy ${ac_tool_prefix}as; ac_word=$2
-{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
-$as_echo_n "checking for $ac_word... " >&6; }
-if test "${ac_cv_prog_AS+set}" = set; then :
- $as_echo_n "(cached) " >&6
-else
- if test -n "$AS"; then
- ac_cv_prog_AS="$AS" # Let the user override the test.
-else
-as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
-for as_dir in $PATH
-do
- IFS=$as_save_IFS
- test -z "$as_dir" && as_dir=.
- for ac_exec_ext in '' $ac_executable_extensions; do
- if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
- ac_cv_prog_AS="${ac_tool_prefix}as"
- $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
- break 2
- fi
-done
- done
-IFS=$as_save_IFS
-
-fi
-fi
-AS=$ac_cv_prog_AS
-if test -n "$AS"; then
- { $as_echo "$as_me:${as_lineno-$LINENO}: result: $AS" >&5
-$as_echo "$AS" >&6; }
-else
- { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
-$as_echo "no" >&6; }
-fi
-
-
-fi
-if test -z "$ac_cv_prog_AS"; then
- ac_ct_AS=$AS
- # Extract the first word of "as", so it can be a program name with args.
-set dummy as; ac_word=$2
-{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
-$as_echo_n "checking for $ac_word... " >&6; }
-if test "${ac_cv_prog_ac_ct_AS+set}" = set; then :
- $as_echo_n "(cached) " >&6
-else
- if test -n "$ac_ct_AS"; then
- ac_cv_prog_ac_ct_AS="$ac_ct_AS" # Let the user override the test.
-else
-as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
-for as_dir in $PATH
-do
- IFS=$as_save_IFS
- test -z "$as_dir" && as_dir=.
- for ac_exec_ext in '' $ac_executable_extensions; do
- if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
- ac_cv_prog_ac_ct_AS="as"
- $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
- break 2
- fi
-done
- done
-IFS=$as_save_IFS
-
-fi
-fi
-ac_ct_AS=$ac_cv_prog_ac_ct_AS
-if test -n "$ac_ct_AS"; then
- { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_ct_AS" >&5
-$as_echo "$ac_ct_AS" >&6; }
-else
- { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
-$as_echo "no" >&6; }
-fi
-
- if test "x$ac_ct_AS" = x; then
- AS="false"
- else
- case $cross_compiling:$ac_tool_warned in
-yes:)
-{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: using cross tools not prefixed with host triplet" >&5
-$as_echo "$as_me: WARNING: using cross tools not prefixed with host triplet" >&2;}
-ac_tool_warned=yes ;;
-esac
- AS=$ac_ct_AS
- fi
-else
- AS="$ac_cv_prog_AS"
-fi
-
- if test -n "$ac_tool_prefix"; then
- # Extract the first word of "${ac_tool_prefix}dlltool", so it can be a program name with args.
-set dummy ${ac_tool_prefix}dlltool; ac_word=$2
-{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
-$as_echo_n "checking for $ac_word... " >&6; }
-if test "${ac_cv_prog_DLLTOOL+set}" = set; then :
- $as_echo_n "(cached) " >&6
-else
- if test -n "$DLLTOOL"; then
- ac_cv_prog_DLLTOOL="$DLLTOOL" # Let the user override the test.
-else
-as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
-for as_dir in $PATH
-do
- IFS=$as_save_IFS
- test -z "$as_dir" && as_dir=.
- for ac_exec_ext in '' $ac_executable_extensions; do
- if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
- ac_cv_prog_DLLTOOL="${ac_tool_prefix}dlltool"
- $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
- break 2
- fi
-done
- done
-IFS=$as_save_IFS
-
-fi
-fi
-DLLTOOL=$ac_cv_prog_DLLTOOL
-if test -n "$DLLTOOL"; then
- { $as_echo "$as_me:${as_lineno-$LINENO}: result: $DLLTOOL" >&5
-$as_echo "$DLLTOOL" >&6; }
-else
- { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
-$as_echo "no" >&6; }
-fi
-
-
-fi
-if test -z "$ac_cv_prog_DLLTOOL"; then
- ac_ct_DLLTOOL=$DLLTOOL
- # Extract the first word of "dlltool", so it can be a program name with args.
-set dummy dlltool; ac_word=$2
-{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
-$as_echo_n "checking for $ac_word... " >&6; }
-if test "${ac_cv_prog_ac_ct_DLLTOOL+set}" = set; then :
- $as_echo_n "(cached) " >&6
-else
- if test -n "$ac_ct_DLLTOOL"; then
- ac_cv_prog_ac_ct_DLLTOOL="$ac_ct_DLLTOOL" # Let the user override the test.
-else
-as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
-for as_dir in $PATH
-do
- IFS=$as_save_IFS
- test -z "$as_dir" && as_dir=.
- for ac_exec_ext in '' $ac_executable_extensions; do
- if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
- ac_cv_prog_ac_ct_DLLTOOL="dlltool"
- $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
- break 2
- fi
-done
- done
-IFS=$as_save_IFS
-
-fi
-fi
-ac_ct_DLLTOOL=$ac_cv_prog_ac_ct_DLLTOOL
-if test -n "$ac_ct_DLLTOOL"; then
- { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_ct_DLLTOOL" >&5
-$as_echo "$ac_ct_DLLTOOL" >&6; }
+
+striplib=
+old_striplib=
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking whether stripping libraries is possible" >&5
+$as_echo_n "checking whether stripping libraries is possible... " >&6; }
+if test -n "$STRIP" && $STRIP -V 2>&1 | $GREP "GNU strip" >/dev/null; then
+ test -z "$old_striplib" && old_striplib="$STRIP --strip-debug"
+ test -z "$striplib" && striplib="$STRIP --strip-unneeded"
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: yes" >&5
+$as_echo "yes" >&6; }
else
- { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
+# FIXME - insert some real tests, host_os isn't really good enough
+ case $host_os in
+ darwin*)
+ if test -n "$STRIP" ; then
+ striplib="$STRIP -x"
+ old_striplib="$STRIP -S"
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: yes" >&5
+$as_echo "yes" >&6; }
+ else
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
$as_echo "no" >&6; }
+ fi
+ ;;
+ *)
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
+$as_echo "no" >&6; }
+ ;;
+ esac
fi
- if test "x$ac_ct_DLLTOOL" = x; then
- DLLTOOL="false"
- else
- case $cross_compiling:$ac_tool_warned in
-yes:)
-{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: using cross tools not prefixed with host triplet" >&5
-$as_echo "$as_me: WARNING: using cross tools not prefixed with host triplet" >&2;}
-ac_tool_warned=yes ;;
-esac
- DLLTOOL=$ac_ct_DLLTOOL
- fi
-else
- DLLTOOL="$ac_cv_prog_DLLTOOL"
-fi
- if test -n "$ac_tool_prefix"; then
- # Extract the first word of "${ac_tool_prefix}objdump", so it can be a program name with args.
-set dummy ${ac_tool_prefix}objdump; ac_word=$2
-{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
-$as_echo_n "checking for $ac_word... " >&6; }
-if test "${ac_cv_prog_OBJDUMP+set}" = set; then :
- $as_echo_n "(cached) " >&6
-else
- if test -n "$OBJDUMP"; then
- ac_cv_prog_OBJDUMP="$OBJDUMP" # Let the user override the test.
-else
-as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
-for as_dir in $PATH
-do
- IFS=$as_save_IFS
- test -z "$as_dir" && as_dir=.
- for ac_exec_ext in '' $ac_executable_extensions; do
- if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
- ac_cv_prog_OBJDUMP="${ac_tool_prefix}objdump"
- $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
- break 2
- fi
-done
- done
-IFS=$as_save_IFS
-fi
-fi
-OBJDUMP=$ac_cv_prog_OBJDUMP
-if test -n "$OBJDUMP"; then
- { $as_echo "$as_me:${as_lineno-$LINENO}: result: $OBJDUMP" >&5
-$as_echo "$OBJDUMP" >&6; }
-else
- { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
-$as_echo "no" >&6; }
-fi
-fi
-if test -z "$ac_cv_prog_OBJDUMP"; then
- ac_ct_OBJDUMP=$OBJDUMP
- # Extract the first word of "objdump", so it can be a program name with args.
-set dummy objdump; ac_word=$2
-{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
-$as_echo_n "checking for $ac_word... " >&6; }
-if test "${ac_cv_prog_ac_ct_OBJDUMP+set}" = set; then :
- $as_echo_n "(cached) " >&6
-else
- if test -n "$ac_ct_OBJDUMP"; then
- ac_cv_prog_ac_ct_OBJDUMP="$ac_ct_OBJDUMP" # Let the user override the test.
-else
-as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
-for as_dir in $PATH
-do
- IFS=$as_save_IFS
- test -z "$as_dir" && as_dir=.
- for ac_exec_ext in '' $ac_executable_extensions; do
- if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
- ac_cv_prog_ac_ct_OBJDUMP="objdump"
- $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
- break 2
- fi
-done
- done
-IFS=$as_save_IFS
-fi
-fi
-ac_ct_OBJDUMP=$ac_cv_prog_ac_ct_OBJDUMP
-if test -n "$ac_ct_OBJDUMP"; then
- { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_ct_OBJDUMP" >&5
-$as_echo "$ac_ct_OBJDUMP" >&6; }
-else
- { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
-$as_echo "no" >&6; }
-fi
- if test "x$ac_ct_OBJDUMP" = x; then
- OBJDUMP="false"
- else
- case $cross_compiling:$ac_tool_warned in
-yes:)
-{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: using cross tools not prefixed with host triplet" >&5
-$as_echo "$as_me: WARNING: using cross tools not prefixed with host triplet" >&2;}
-ac_tool_warned=yes ;;
-esac
- OBJDUMP=$ac_ct_OBJDUMP
- fi
-else
- OBJDUMP="$ac_cv_prog_OBJDUMP"
+
+
+
+
+
+ # Report which library types will actually be built
+ { $as_echo "$as_me:${as_lineno-$LINENO}: checking if libtool supports shared libraries" >&5
+$as_echo_n "checking if libtool supports shared libraries... " >&6; }
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: $can_build_shared" >&5
+$as_echo "$can_build_shared" >&6; }
+
+ { $as_echo "$as_me:${as_lineno-$LINENO}: checking whether to build shared libraries" >&5
+$as_echo_n "checking whether to build shared libraries... " >&6; }
+ test "$can_build_shared" = "no" && enable_shared=no
+
+ # On AIX, shared libraries and static libraries use the same namespace, and
+ # are all built from PIC.
+ case $host_os in
+ aix3*)
+ test "$enable_shared" = yes && enable_static=no
+ if test -n "$RANLIB"; then
+ archive_cmds="$archive_cmds~\$RANLIB \$lib"
+ postinstall_cmds='$RANLIB $lib'
+ fi
+ ;;
+
+ aix[4-9]*)
+ if test "$host_cpu" != ia64 && test "$aix_use_runtimelinking" = no ; then
+ test "$enable_shared" = yes && enable_static=no
+ fi
+ ;;
+ esac
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: $enable_shared" >&5
+$as_echo "$enable_shared" >&6; }
+
+ { $as_echo "$as_me:${as_lineno-$LINENO}: checking whether to build static libraries" >&5
+$as_echo_n "checking whether to build static libraries... " >&6; }
+ # Make sure either enable_shared or enable_static is yes.
+ test "$enable_shared" = yes || enable_static=yes
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: $enable_static" >&5
+$as_echo "$enable_static" >&6; }
+
+
+
+
fi
+ac_ext=c
+ac_cpp='$CPP $CPPFLAGS'
+ac_compile='$CC -c $CFLAGS $CPPFLAGS conftest.$ac_ext >&5'
+ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5'
+ac_compiler_gnu=$ac_cv_c_compiler_gnu
- ;;
-esac
+CC="$lt_save_CC"
-test -z "$AS" && AS=as
-test -z "$DLLTOOL" && DLLTOOL=dlltool
-test -z "$OBJDUMP" && OBJDUMP=objdump
+
+
+ ac_config_commands="$ac_config_commands libtool"
+
+# Only expand once:
-e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
-e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
-e 's:$: $lt_compiler_flag:'`
- (eval echo "\"\$as_me:14626: $lt_compile\"" >&5)
+ (eval echo "\"\$as_me:14630: $lt_compile\"" >&5)
(eval "$lt_compile" 2>conftest.err)
ac_status=$?
cat conftest.err >&5
- echo "$as_me:14630: \$? = $ac_status" >&5
+ echo "$as_me:14634: \$? = $ac_status" >&5
if (exit $ac_status) && test -s "$ac_outfile"; then
# The compiler can only warn and ignore the option if not recognized
# So say no if there are warnings other than the usual output.
-e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
-e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
-e 's:$: $lt_compiler_flag:'`
- (eval echo "\"\$as_me:14725: $lt_compile\"" >&5)
+ (eval echo "\"\$as_me:14729: $lt_compile\"" >&5)
(eval "$lt_compile" 2>out/conftest.err)
ac_status=$?
cat out/conftest.err >&5
- echo "$as_me:14729: \$? = $ac_status" >&5
+ echo "$as_me:14733: \$? = $ac_status" >&5
if (exit $ac_status) && test -s out/conftest2.$ac_objext
then
# The compiler can only warn and ignore the option if not recognized
-e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
-e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
-e 's:$: $lt_compiler_flag:'`
- (eval echo "\"\$as_me:14777: $lt_compile\"" >&5)
+ (eval echo "\"\$as_me:14781: $lt_compile\"" >&5)
(eval "$lt_compile" 2>out/conftest.err)
ac_status=$?
cat out/conftest.err >&5
- echo "$as_me:14781: \$? = $ac_status" >&5
+ echo "$as_me:14785: \$? = $ac_status" >&5
if (exit $ac_status) && test -s out/conftest2.$ac_objext
then
# The compiler can only warn and ignore the option if not recognized
-
# Check for ANTLR runantlr script (defined in config/antlr.m4)
fi
+
CXXTESTGEN=
# Extract the first word of "cxxtestgen.pl", so it can be a program name with args.
set dummy cxxtestgen.pl; ac_word=$2
delay_variable_subst='$delay_variable_subst'
enable_shared='`$ECHO "X$enable_shared" | $Xsed -e "$delay_single_quote_subst"`'
enable_static='`$ECHO "X$enable_static" | $Xsed -e "$delay_single_quote_subst"`'
+AS='`$ECHO "X$AS" | $Xsed -e "$delay_single_quote_subst"`'
+DLLTOOL='`$ECHO "X$DLLTOOL" | $Xsed -e "$delay_single_quote_subst"`'
+OBJDUMP='`$ECHO "X$OBJDUMP" | $Xsed -e "$delay_single_quote_subst"`'
macro_version='`$ECHO "X$macro_version" | $Xsed -e "$delay_single_quote_subst"`'
macro_revision='`$ECHO "X$macro_revision" | $Xsed -e "$delay_single_quote_subst"`'
pic_mode='`$ECHO "X$pic_mode" | $Xsed -e "$delay_single_quote_subst"`'
lt_NL2SP='`$ECHO "X$lt_NL2SP" | $Xsed -e "$delay_single_quote_subst"`'
reload_flag='`$ECHO "X$reload_flag" | $Xsed -e "$delay_single_quote_subst"`'
reload_cmds='`$ECHO "X$reload_cmds" | $Xsed -e "$delay_single_quote_subst"`'
-OBJDUMP='`$ECHO "X$OBJDUMP" | $Xsed -e "$delay_single_quote_subst"`'
deplibs_check_method='`$ECHO "X$deplibs_check_method" | $Xsed -e "$delay_single_quote_subst"`'
file_magic_cmd='`$ECHO "X$file_magic_cmd" | $Xsed -e "$delay_single_quote_subst"`'
AR='`$ECHO "X$AR" | $Xsed -e "$delay_single_quote_subst"`'
enable_dlopen_self_static='`$ECHO "X$enable_dlopen_self_static" | $Xsed -e "$delay_single_quote_subst"`'
old_striplib='`$ECHO "X$old_striplib" | $Xsed -e "$delay_single_quote_subst"`'
striplib='`$ECHO "X$striplib" | $Xsed -e "$delay_single_quote_subst"`'
-AS='`$ECHO "X$AS" | $Xsed -e "$delay_single_quote_subst"`'
-DLLTOOL='`$ECHO "X$DLLTOOL" | $Xsed -e "$delay_single_quote_subst"`'
compiler_lib_search_dirs='`$ECHO "X$compiler_lib_search_dirs" | $Xsed -e "$delay_single_quote_subst"`'
predep_objects='`$ECHO "X$predep_objects" | $Xsed -e "$delay_single_quote_subst"`'
postdep_objects='`$ECHO "X$postdep_objects" | $Xsed -e "$delay_single_quote_subst"`'
lt_SP2NL \
lt_NL2SP \
reload_flag \
-OBJDUMP \
deplibs_check_method \
file_magic_cmd \
AR \
# Whether or not to build static libraries.
build_old_libs=$enable_static
+# Assembler program.
+AS=$AS
+
+# DLL creation program.
+DLLTOOL=$DLLTOOL
+
+# Object dumper program.
+OBJDUMP=$OBJDUMP
+
# Which release of libtool.m4 was used?
macro_version=$macro_version
macro_revision=$macro_revision
reload_flag=$lt_reload_flag
reload_cmds=$lt_reload_cmds
-# An object symbol dumper.
-OBJDUMP=$lt_OBJDUMP
-
# Method to check whether dependent libraries are shared objects.
deplibs_check_method=$lt_deplibs_check_method
old_striplib=$lt_old_striplib
striplib=$lt_striplib
-# Assembler program.
-AS=$AS
-
-# DLL creation program.
-DLLTOOL=$DLLTOOL
-
# The linker used to build libraries.
LD=$lt_LD
fi
fi
+support_unit_tests='cxxtest not found; unit tests not supported'
+if test -n "$CXXTEST"; then
+ support_unit_tests='unit testing infrastructure enabled in build directory'
+fi
+
cat <<EOF
CVC4 $VERSION
Muzzle : $enable_muzzle
gcov support : $enable_coverage
gprof support: $enable_profiling
+unit tests : $support_unit_tests
CPPFLAGS : $CPPFLAGS
CXXFLAGS : $CXXFLAGS
CVC4_AC_INIT
-AC_PREREQ([2.59])
-AC_INIT([src/include/cvc4_config.h])
+AC_PREREQ(2.64)
+AC_INIT
+AC_CONFIG_SRCDIR([src/include/cvc4_config.h])
AC_CONFIG_AUX_DIR([config])
AC_CONFIG_MACRO_DIR([config])
(echo "# This is the most-recently-configured CVC4 build"; \
echo "# 'make' in the top-level source directory applies to this build"; \
echo "CURRENT_BUILD = $target/$build_type") > builds/current
+ echo Linking builds/src...
+ rm -f builds/src
+ ln -sfv "$target/$build_type/src" builds/src
+ echo Linking builds/test...
+ rm -f builds/test
+ ln -sfv "$target/$build_type/test" builds/test
echo cd "builds/$target/$build_type"
cd "builds/$target/$build_type"
CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS
if test -z "${LDFLAGS+set}" ; then user_ldflags=no ; else user_ldflags=yes ; fi
AC_MSG_RESULT([${LDFLAGS-none}])
+_LT_SET_OPTION([LT_INIT],[win32-dll])
LT_INIT
-AC_LIBTOOL_WIN32_DLL
-
-
# Checks for programs.
AC_PROG_CC
AC_PROG_CXX
AC_PROG_INSTALL
-AC_PROG_LIBTOOL
# Check for ANTLR runantlr script (defined in config/antlr.m4)
AC_PROG_ANTLR
fi
AC_ARG_VAR(DOXYGEN, [location of doxygen binary])
+AC_ARG_VAR(CXXTEST, [path to cxxtest installation])
CXXTESTGEN=
AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH])
if test -z "$CXXTESTGEN"; then
fi
fi
+support_unit_tests='cxxtest not found; unit tests not supported'
+if test -n "$CXXTEST"; then
+ support_unit_tests='unit testing infrastructure enabled in build directory'
+fi
+
cat <<EOF
CVC4 $VERSION
Muzzle : $enable_muzzle
gcov support : $enable_coverage
gprof support: $enable_profiling
+unit tests : $support_unit_tests
CPPFLAGS : $CPPFLAGS
CXXFLAGS : $CXXFLAGS
CXXCPP = @CXXCPP@
CXXDEPMODE = @CXXDEPMODE@
CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
CXXTESTGEN = @CXXTESTGEN@
CYGPATH_W = @CYGPATH_W@
DEFS = @DEFS@
CXXCPP = @CXXCPP@
CXXDEPMODE = @CXXDEPMODE@
CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
CXXTESTGEN = @CXXTESTGEN@
CYGPATH_W = @CYGPATH_W@
DEFS = @DEFS@
--- /dev/null
+topdir = ..
+srcdir = src
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
LIBCVC4_RELEASE = @CVC4_LIBRARY_RELEASE_CODE@
LIBCVC4_VERSION = @CVC4_LIBRARY_VERSION@
-INCLUDES = -I@srcdir@/include -I@srcdir@
+AM_CPPFLAGS =
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/include -I@srcdir@
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
SUBDIRS = util expr context prop smt theory . parser main
CXXCPP = @CXXCPP@
CXXDEPMODE = @CXXDEPMODE@
CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
CXXTESTGEN = @CXXTESTGEN@
CYGPATH_W = @CYGPATH_W@
DEFS = @DEFS@
#
LIBCVC4_RELEASE = @CVC4_LIBRARY_RELEASE_CODE@
LIBCVC4_VERSION = @CVC4_LIBRARY_VERSION@
-INCLUDES = -I@srcdir@/include -I@srcdir@
+AM_CPPFLAGS =
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
SUBDIRS = util expr context prop smt theory . parser main
lib_LTLIBRARIES = libcvc4.la
libcvc4_la_LDFLAGS = -version-info $(LIBCVC4_VERSION) -release $(LIBCVC4_RELEASE)
tags tags-recursive uninstall uninstall-am \
uninstall-libLTLIBRARIES
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/include -I@srcdir@
install-data-local: $(publicheaders)
$(mkinstalldirs) $(DESTDIR)$(includedir)/cvc4
--- /dev/null
+topdir = ../..
+srcdir = src/context
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/../include -I@srcdir@/..
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libcontext.la
CONFIG_CLEAN_VPATH_FILES =
LTLIBRARIES = $(noinst_LTLIBRARIES)
libcontext_la_LIBADD =
-am_libcontext_la_OBJECTS = context.lo
+am_libcontext_la_OBJECTS = context.lo context_mm.lo
libcontext_la_OBJECTS = $(am_libcontext_la_OBJECTS)
DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
depcomp = $(SHELL) $(top_srcdir)/config/depcomp
CXXCPP = @CXXCPP@
CXXDEPMODE = @CXXDEPMODE@
CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
CXXTESTGEN = @CXXTESTGEN@
CYGPATH_W = @CYGPATH_W@
DEFS = @DEFS@
top_build_prefix = @top_build_prefix@
top_builddir = @top_builddir@
top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/../include -I@srcdir@/..
+
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libcontext.la
libcontext_la_SOURCES = \
context.cpp \
- context.h
+ context.h \
+ context_mm.cpp \
+ context_mm.h
all: all-am
-rm -f *.tab.c
@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/context.Plo@am__quote@
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/context_mm.Plo@am__quote@
.cpp.o:
@am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $<
#include <cstdlib>
#include <vector>
#include <deque>
+#include <new>
#include "context/context_mm.h"
#include "util/Assert.h"
-
namespace CVC4 {
namespace context {
-
void ContextMemoryManager::newChunk() {
// Increment index to chunk list
"Index should be at the end of the list");
// Create new chunk if no free chunk available
- if (d_freePages.empty()) {
+ if (d_freeChunks.empty()) {
d_chunkList.push_back((char*)malloc(chunkSizeBytes));
if (d_chunkList.back() == NULL) {
- throw bad_alloc();
+ throw std::bad_alloc();
}
}
// If there is a free chunk, use that
else {
- d_chunkList.push_back(d_freePages.back());
- d_freePages.pop_back();
+ d_chunkList.push_back(d_freeChunks.back());
+ d_freeChunks.pop_back();
}
// Set up the current chunk pointers
d_nextFree = d_chunkList.back();
}
-ContextMemoryManager() : d_indexChunkList(0) {
+ContextMemoryManager::ContextMemoryManager() : d_indexChunkList(0) {
// Create initial chunk
d_chunkList.push_back((char*)malloc(chunkSizeBytes));
d_nextFree = d_chunkList.back();
if (d_nextFree == NULL) {
- throw bad_alloc;
+ throw std::bad_alloc();
}
d_endChunk = d_nextFree + chunkSizeBytes;
}
-~ContextMemoryManager() {
+ContextMemoryManager::~ContextMemoryManager() {
// Delete all chunks
while (!d_chunkList.empty()) {
free(d_chunkList.back());
d_chunkList.pop_back();
}
- while (!d_freePages.empty()) {
- free(d_freePages.back());
- d_freePages.pop_back();
+ while (!d_freeChunks.empty()) {
+ free(d_freeChunks.back());
+ d_freeChunks.pop_back();
}
}
-void* newData(size_t size) {
+void* ContextMemoryManager::newData(size_t size) {
// Use next available free location in current chunk
void* res = (void*)d_nextFree;
d_nextFree += size;
}
-void push() {
+void ContextMemoryManager::push() {
// Store current state on the stack
d_nextFreeStack.push_back(d_nextFree);
d_endChunkStack.push_back(d_endChunk);
}
-void pop() {
+void ContextMemoryManager::pop() {
// Restore state from stack
d_nextFree = d_nextFreeStack.back();
d_nextFreeStack.pop_back();
// Free all the new chunks since the last push
while (d_indexChunkList > d_indexChunkListStack.back()) {
- d_freePages.push_back(d_chunkList.back());
+ d_freeChunks.push_back(d_chunkList.back());
d_chunkList.pop_back();
--d_indexChunkList;
}
// Delete excess free chunks
while (d_freeChunks.size() > maxFreeChunks) {
- free(d_freePages.front());
- d_freePages.pop_front();
+ free(d_freeChunks.front());
+ d_freeChunks.pop_front();
}
}
}/* CVC4::context namespace */
-
}/* CVC4 namespace */
/**
* Memory in regions is allocated in chunks. This is the minimum chunk size
*/
- const unsigned chunkSizeBytes = 16384; // #bytes in each chunk
+ static const unsigned chunkSizeBytes = 16384; // #bytes in each chunk
/**
* A list of free chunks is maintained. This is the maximum number of
* free chunks.
*/
- const unsigned maxFreeChunks = 100;
+ static const unsigned maxFreeChunks = 100;
/**
* List of all chunks that are currently active
--- /dev/null
+topdir = ../..
+srcdir = src/expr
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/../include -I@srcdir@/..
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libexpr.la
node.h \
node_builder.h \
expr.h \
- expr_value.h \
+ node_value.h \
node_manager.h \
expr_manager.h \
node_attribute.h \
node_builder.cpp \
node_manager.cpp \
expr_manager.cpp \
- expr_value.cpp \
+ node_value.cpp \
expr.cpp
LTLIBRARIES = $(noinst_LTLIBRARIES)
libexpr_la_LIBADD =
am_libexpr_la_OBJECTS = node.lo node_builder.lo node_manager.lo \
- expr_manager.lo expr_value.lo expr.lo
+ expr_manager.lo node_value.lo expr.lo
libexpr_la_OBJECTS = $(am_libexpr_la_OBJECTS)
DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
depcomp = $(SHELL) $(top_srcdir)/config/depcomp
CXXCPP = @CXXCPP@
CXXDEPMODE = @CXXDEPMODE@
CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
CXXTESTGEN = @CXXTESTGEN@
CYGPATH_W = @CYGPATH_W@
DEFS = @DEFS@
top_build_prefix = @top_build_prefix@
top_builddir = @top_builddir@
top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/../include -I@srcdir@/..
+
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libexpr.la
libexpr_la_SOURCES = \
attr_type.h \
node.h \
node_builder.h \
expr.h \
- expr_value.h \
+ node_value.h \
node_manager.h \
expr_manager.h \
node_attribute.h \
node_builder.cpp \
node_manager.cpp \
expr_manager.cpp \
- expr_value.cpp \
+ node_value.cpp \
expr.cpp
all: all-am
@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr.Plo@am__quote@
@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr_manager.Plo@am__quote@
-@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr_value.Plo@am__quote@
@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node.Plo@am__quote@
@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node_builder.Plo@am__quote@
@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node_manager.Plo@am__quote@
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node_value.Plo@am__quote@
.cpp.o:
@am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $<
+++ /dev/null
-/********************* -*- C++ -*- */
-/** expr_value.cpp
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.
- **
- ** An expression node.
- **
- ** Instances of this class are generally referenced through
- ** cvc4::Node rather than by pointer; cvc4::Node maintains the
- ** reference count on ExprValue instances and
- **/
-
-#include "expr_value.h"
-#include <sstream>
-
-using namespace std;
-
-namespace CVC4 {
-
-size_t ExprValue::next_id = 1;
-
-ExprValue::ExprValue() :
- d_id(0), d_rc(MAX_RC), d_kind(NULL_EXPR), d_nchildren(0) {
-}
-
-uint64_t ExprValue::hash() const {
- return computeHash<const_iterator>(d_kind, begin(), end());
-}
-
-ExprValue* ExprValue::inc() {
- // FIXME multithreading
- if(d_rc < MAX_RC)
- ++d_rc;
- return this;
-}
-
-ExprValue* ExprValue::dec() {
- // FIXME multithreading
- if(d_rc < MAX_RC)
- if(--d_rc == 0) {
- // FIXME gc
- return 0;
- }
- return this;
-}
-
-ExprValue::iterator ExprValue::begin() {
- return d_children;
-}
-
-ExprValue::iterator ExprValue::end() {
- return d_children + d_nchildren;
-}
-
-ExprValue::iterator ExprValue::rbegin() {
- return d_children + d_nchildren - 1;
-}
-
-ExprValue::iterator ExprValue::rend() {
- return d_children - 1;
-}
-
-ExprValue::const_iterator ExprValue::begin() const {
- return d_children;
-}
-
-ExprValue::const_iterator ExprValue::end() const {
- return d_children + d_nchildren;
-}
-
-ExprValue::const_iterator ExprValue::rbegin() const {
- return d_children + d_nchildren - 1;
-}
-
-ExprValue::const_iterator ExprValue::rend() const {
- return d_children - 1;
-}
-
-string ExprValue::toString() const {
- stringstream ss;
- toStream(ss);
- return ss.str();
-}
-
-void ExprValue::toStream(std::ostream& out) const {
- out << "(" << Kind(d_kind);
- if(d_kind == VARIABLE) {
- out << ":" << this;
- } else {
- for(const_iterator i = begin(); i != end(); ++i) {
- if(i != end())
- out << " ";
- out << *i;
- }
- }
- out << ")";
-}
-
-}/* CVC4 namespace */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** expr_value.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.
- **
- ** An expression node.
- **
- ** Instances of this class are generally referenced through
- ** cvc4::Node rather than by pointer; cvc4::Node maintains the
- ** reference count on ExprValue instances and
- **/
-
-/* this must be above the check for __CVC4__EXPR__EXPR_VALUE_H */
-/* to resolve a circular dependency */
-#include "expr/node.h"
-
-#ifndef __CVC4__EXPR__EXPR_VALUE_H
-#define __CVC4__EXPR__EXPR_VALUE_H
-
-#include "cvc4_config.h"
-#include <stdint.h>
-#include "kind.h"
-
-#include <string>
-
-namespace CVC4 {
-
-class Node;
-class NodeBuilder;
-
-namespace expr {
-
-/**
- * This is an ExprValue.
- */
-class ExprValue {
-
- /** A convenient null-valued expression value */
- static ExprValue s_null;
-
- /** Maximum reference count possible. Used for sticky
- * reference-counting. Should be (1 << num_bits(d_rc)) - 1 */
- static const unsigned MAX_RC = 255;
-
- // this header fits into one 64-bit word
-
- /** The ID (0 is reserved for the null value) */
- unsigned d_id : 32;
-
- /** The expression's reference count. @see cvc4::Node. */
- unsigned d_rc : 8;
-
- /** Kind of the expression */
- unsigned d_kind : 8;
-
- /** Number of children */
- unsigned d_nchildren : 16;
-
- /** Variable number of child nodes */
- Node d_children[0];
-
- // todo add exprMgr ref in debug case
-
- friend class CVC4::Node;
- friend class CVC4::NodeBuilder;
-
- ExprValue* inc();
- ExprValue* dec();
-
- static size_t next_id;
-
- /** Private default constructor for the null value. */
- ExprValue();
-
- /**
- * Computes the hash over the given iterator span of children, and the
- * root hash. The iterator should be either over a range of Node or pointers
- * to ExprValue.
- * @param hash the initial value for the hash
- * @param begin the begining of the range
- * @param end the end of the range
- * @return the hash value
- */
- template<typename const_iterator_type>
- static uint64_t computeHash(uint64_t hash, const_iterator_type begin, const_iterator_type end) {
- for(const_iterator_type i = begin; i != end; ++i)
- hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ (*i)->getId();
- return hash;
- }
-
-public:
- /** Hash this expression.
- * @return the hash value of this expression. */
- uint64_t hash() const;
-
- // Iterator support
-
- typedef Node* iterator;
- typedef Node const* const_iterator;
-
- iterator begin();
- iterator end();
- iterator rbegin();
- iterator rend();
-
- const_iterator begin() const;
- const_iterator end() const;
- const_iterator rbegin() const;
- const_iterator rend() const;
-
- unsigned getId() const { return d_id; }
- unsigned getKind() const { return (Kind) d_kind; }
- std::string toString() const;
- void toStream(std::ostream& out) const;
-};
-
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__EXPR__EXPR_VALUE_H */
#ifndef __CVC4__KIND_H
#define __CVC4__KIND_H
+#include "cvc4_config.h"
#include <iostream>
namespace CVC4 {
/********************* -*- C++ -*- */
-/** expr.cpp
+/** node.cpp
** This file is part of the CVC4 prototype.
** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
**/
#include "expr/node.h"
-#include "expr/expr_value.h"
+#include "expr/node_value.h"
#include "expr/node_builder.h"
#include "util/Assert.h"
namespace CVC4 {
-ExprValue ExprValue::s_null;
+NodeValue NodeValue::s_null;
-Node Node::s_null(&ExprValue::s_null);
+Node Node::s_null(&NodeValue::s_null);
Node Node::null() {
return s_null;
}
-
bool Node::isNull() const {
- return d_ev == &ExprValue::s_null;
+ return d_ev == &NodeValue::s_null;
}
Node::Node() :
- d_ev(&ExprValue::s_null) {
+ d_ev(&NodeValue::s_null) {
// No refcount needed
}
-Node::Node(ExprValue* ev)
- : d_ev(ev) {
+// FIXME: escape from type system convenient but is there a better
+// way? Nodes conceptually don't change their expr values but of
+// course they do modify the refcount. But it's nice to be able to
+// support node_iterators over const NodeValue*. So.... hm.
+Node::Node(const NodeValue* ev)
+ : d_ev(const_cast<NodeValue*>(ev)) {
Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
d_ev->inc();
}
d_ev->dec();
}
-void Node::assignExprValue(ExprValue* ev) {
+void Node::assignNodeValue(NodeValue* ev) {
d_ev = ev;
d_ev->inc();
}
return *this;
}
-ExprValue const* Node::operator->() const {
+NodeValue const* Node::operator->() const {
Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
return d_ev;
}
}
Node Node::eqExpr(const Node& right) const {
- return NodeManager::currentEM()->mkExpr(EQUAL, *this, right);
+ return NodeManager::currentNM()->mkExpr(EQUAL, *this, right);
}
Node Node::notExpr() const {
- return NodeManager::currentEM()->mkExpr(NOT, *this);
+ return NodeManager::currentNM()->mkExpr(NOT, *this);
}
Node Node::andExpr(const Node& right) const {
- return NodeManager::currentEM()->mkExpr(AND, *this, right);
+ return NodeManager::currentNM()->mkExpr(AND, *this, right);
}
Node Node::orExpr(const Node& right) const {
- return NodeManager::currentEM()->mkExpr(OR, *this, right);
+ return NodeManager::currentNM()->mkExpr(OR, *this, right);
}
Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const {
- return NodeManager::currentEM()->mkExpr(ITE, *this, thenpart, elsepart);
+ return NodeManager::currentNM()->mkExpr(ITE, *this, thenpart, elsepart);
}
Node Node::iffExpr(const Node& right) const {
- return NodeManager::currentEM()->mkExpr(IFF, *this, right);
+ return NodeManager::currentNM()->mkExpr(IFF, *this, right);
}
Node Node::impExpr(const Node& right) const {
- return NodeManager::currentEM()->mkExpr(IMPLIES, *this, right);
+ return NodeManager::currentNM()->mkExpr(IMPLIES, *this, right);
}
Node Node::xorExpr(const Node& right) const {
- return NodeManager::currentEM()->mkExpr(XOR, *this, right);
+ return NodeManager::currentNM()->mkExpr(XOR, *this, right);
}
}/* CVC4 namespace */
** Reference-counted encapsulation of a pointer to an expression.
**/
+#include "expr/node_value.h"
+
#ifndef __CVC4__NODE_H
#define __CVC4__NODE_H
class NodeManager;
namespace expr {
- class ExprValue;
+ class NodeValue;
}/* CVC4::expr namespace */
-using CVC4::expr::ExprValue;
+using CVC4::expr::NodeValue;
/**
- * Encapsulation of an ExprValue pointer. The reference count is
- * maintained in the ExprValue.
+ * Encapsulation of an NodeValue pointer. The reference count is
+ * maintained in the NodeValue.
*/
class Node {
- friend class ExprValue;
+ friend class NodeValue;
/** A convenient null-valued encapsulated pointer */
static Node s_null;
- /** The referenced ExprValue */
- ExprValue* d_ev;
+ /** The referenced NodeValue */
+ NodeValue* d_ev;
/** This constructor is reserved for use by the Node package; one
* must construct an Node using one of the build mechanisms of the
* Node package.
*
- * Increments the reference count. */
- explicit Node(ExprValue*);
-
- friend class NodeBuilder;
+ * Increments the reference count.
+ *
+ * FIXME: there's a type-system escape here to cast away the const,
+ * since the refcount needs to be updated. But conceptually Nodes
+ * don't change their arguments, and it's nice to have
+ * const_iterators over them. See notes in .cpp file for
+ * details. */
+ explicit Node(const NodeValue*);
+
+ template <unsigned> friend class NodeBuilder;
friend class NodeManager;
/** Access to the encapsulated expression.
* @return the encapsulated expression. */
- ExprValue const* operator->() const;
+ NodeValue const* operator->() const;
/**
* Assigns the expression value and does reference counting. No assumptions are
*
* @param ev the expression value to assign
*/
- void assignExprValue(ExprValue* ev);
+ void assignNodeValue(NodeValue* ev);
+
+ typedef NodeValue::iterator ev_iterator;
+ typedef NodeValue::const_iterator const_ev_iterator;
+
+ inline ev_iterator ev_begin();
+ inline ev_iterator ev_end();
+ inline const_ev_iterator ev_begin() const;
+ inline const_ev_iterator ev_end() const;
public:
Node(const Node&);
/** Destructor. Decrements the reference count and, if zero,
- * collects the ExprValue. */
+ * collects the NodeValue. */
~Node();
bool operator==(const Node& e) const { return d_ev == e.d_ev; }
static Node null();
- typedef Node* iterator;
- typedef Node const* const_iterator;
+ typedef NodeValue::node_iterator iterator;
+ typedef NodeValue::node_iterator const_iterator;
inline iterator begin();
inline iterator end();
}/* CVC4 namespace */
-#include "expr/expr_value.h"
+#include "expr/node_value.h"
namespace CVC4 {
d_ev->toStream(out);
}
+inline Node::ev_iterator Node::ev_begin() {
+ return d_ev->ev_begin();
+}
+
+inline Node::ev_iterator Node::ev_end() {
+ return d_ev->ev_end();
+}
+
+inline Node::const_ev_iterator Node::ev_begin() const {
+ return d_ev->ev_begin();
+}
+
+inline Node::const_ev_iterator Node::ev_end() const {
+ return d_ev->ev_end();
+}
+
inline Node::iterator Node::begin() {
return d_ev->begin();
}
/********************* -*- C++ -*- */
-/** expr_builder.cpp
+/** node_builder.cpp
** This file is part of the CVC4 prototype.
** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
#include "expr/node_builder.h"
#include "expr/node_manager.h"
-#include "expr/expr_value.h"
+#include "expr/node_value.h"
#include "util/output.h"
using namespace std;
-
-namespace CVC4 {
-
-NodeBuilder::NodeBuilder() :
- d_em(NodeManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false),
- d_nchildren(0) {
-}
-
-NodeBuilder::NodeBuilder(Kind k) :
- d_em(NodeManager::currentEM()), d_kind(k), d_used(false), d_nchildren(0) {
-}
-
-NodeBuilder::NodeBuilder(const Node& e) :
- d_em(NodeManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) {
- d_children.u_arr[0] = e.d_ev->inc();;
-}
-
-NodeBuilder& NodeBuilder::reset(const ExprValue* ev) {
- this->~NodeBuilder();
- d_kind = Kind(ev->d_kind);
- d_used = false;
- d_nchildren = ev->d_nchildren;
- for(Node::const_iterator i = ev->begin(); i != ev->end(); ++i)
- addChild(i->d_ev);
- return *this;
-}
-
-NodeBuilder::NodeBuilder(const NodeBuilder& eb) :
- d_em(eb.d_em), d_kind(eb.d_kind), d_used(eb.d_used),
- d_nchildren(eb.d_nchildren) {
- Assert( !d_used );
-
- if(d_nchildren > nchild_thresh) {
- d_children.u_vec = new vector<Node> ();
- d_children.u_vec->reserve(d_nchildren + 5);
- copy(eb.d_children.u_vec->begin(), eb.d_children.u_vec->end(),
- back_inserter(*d_children.u_vec));
- } else {
- ev_iterator j = d_children.u_arr;
- ExprValue* const * i = eb.d_children.u_arr;
- ExprValue* const * i_end = i + eb.d_nchildren;
- for(; i != i_end; ++i, ++j)
- *j = (*i)->inc();
- }
-}
-
-NodeBuilder::NodeBuilder(NodeManager* em) :
- d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(0) {
-}
-
-NodeBuilder::NodeBuilder(NodeManager* em, Kind k) :
- d_em(em), d_kind(k), d_used(false), d_nchildren(0) {
-}
-
-NodeBuilder::NodeBuilder(NodeManager* em, const Node& e) :
- d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) {
- d_children.u_arr[0] = e.d_ev->inc();
-}
-
-NodeBuilder::~NodeBuilder() {
- if(d_nchildren > nchild_thresh) {
- delete d_children.u_vec;
- } else {
- ev_iterator i = d_children.u_arr;
- ev_iterator i_end = d_children.u_arr + d_nchildren;
- for(; i != i_end ; ++i) {
- (*i)->dec();
- }
- }
-}
-
-// Compound expression constructors
-NodeBuilder& NodeBuilder::eqExpr(const Node& right) {
- Assert( d_kind != UNDEFINED_KIND );
- if(EXPECT_TRUE( d_kind != EQUAL )) {
- collapse();
- d_kind = EQUAL;
- }
- addChild(right);
- return *this;
-}
-
-NodeBuilder& NodeBuilder::notExpr() {
- Assert( d_kind != UNDEFINED_KIND );
- collapse();
- d_kind = NOT;
- return *this;
-}
-
-NodeBuilder& NodeBuilder::andExpr(const Node& right) {
- Assert( d_kind != UNDEFINED_KIND );
- if(d_kind != AND) {
- collapse();
- d_kind = AND;
- }
- addChild(right);
- return *this;
-}
-
-NodeBuilder& NodeBuilder::orExpr(const Node& right) {
- Assert( d_kind != UNDEFINED_KIND );
- if(EXPECT_TRUE( d_kind != OR )) {
- collapse();
- d_kind = OR;
- }
- addChild(right);
- return *this;
-}
-
-NodeBuilder& NodeBuilder::iteExpr(const Node& thenpart, const Node& elsepart) {
- Assert( d_kind != UNDEFINED_KIND );
- collapse();
- d_kind = ITE;
- addChild(thenpart);
- addChild(elsepart);
- return *this;
-}
-
-NodeBuilder& NodeBuilder::iffExpr(const Node& right) {
- Assert( d_kind != UNDEFINED_KIND );
- if(EXPECT_TRUE( d_kind != IFF )) {
- collapse();
- d_kind = IFF;
- }
- addChild(right);
- return *this;
-}
-
-NodeBuilder& NodeBuilder::impExpr(const Node& right) {
- Assert( d_kind != UNDEFINED_KIND );
- collapse();
- d_kind = IMPLIES;
- addChild(right);
- return *this;
-}
-
-NodeBuilder& NodeBuilder::xorExpr(const Node& right) {
- Assert( d_kind != UNDEFINED_KIND );
- if(EXPECT_TRUE( d_kind != XOR )) {
- collapse();
- d_kind = XOR;
- }
- addChild(right);
- return *this;
-}
-
-// "Stream" expression constructor syntax
-NodeBuilder& NodeBuilder::operator<<(const Kind& op) {
- d_kind = op;
- return *this;
-}
-
-NodeBuilder& NodeBuilder::operator<<(const Node& child) {
- addChild(child);
- return *this;
-}
-
-/**
- * We keep the children either:
- * (a) In the array of expression values if the number of children is less than
- * nchild_thresh. Hence (last else) we increase the reference count.
- * (b) If the number of children reaches the nchild_thresh, we allocate a vector
- * for the children. Children are now expressions, so we also decrement the
- * reference count for each child.
- * (c) Otherwise we just add to the end of the vector.
- */
-void NodeBuilder::addChild(ExprValue* ev) {
- Assert(d_nchildren <= nchild_thresh ||
- d_nchildren == d_children.u_vec->size(),
- "children count doesn't reflect the size of the vector!");
- Debug("expr") << "adding child ev " << ev << endl;
- if(d_nchildren == nchild_thresh) {
- Debug("expr") << "reached thresh " << nchild_thresh << ", copying" << endl;
- vector<Node>* v = new vector<Node> ();
- v->reserve(nchild_thresh + 5);
- ExprValue** i = d_children.u_arr;
- ExprValue** i_end = i + nchild_thresh;
- for(;i != i_end; ++ i) {
- v->push_back(Node(*i));
- (*i)->dec();
- }
- v->push_back(Node(ev));
- d_children.u_vec = v;
- ++d_nchildren;
- } else if(d_nchildren > nchild_thresh) {
- Debug("expr") << "over thresh " << d_nchildren
- << " > " << nchild_thresh << endl;
- d_children.u_vec->push_back(Node(ev));
- // ++d_nchildren; no need for this
- } else {
- Debug("expr") << "under thresh " << d_nchildren
- << " < " << nchild_thresh << endl;
- d_children.u_arr[d_nchildren ++] = ev->inc();
- }
-}
-
-NodeBuilder& NodeBuilder::collapse() {
- if(d_nchildren == nchild_thresh) {
- vector<Node>* v = new vector<Node> ();
- v->reserve(nchild_thresh + 5);
- //
- Unreachable();// unimplemented
- }
- return *this;
-}
-
-}/* CVC4 namespace */
/********************* -*- C++ -*- */
-/** expr_builder.h
+/** node_builder.h
** This file is part of the CVC4 prototype.
** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
#include <vector>
#include <cstdlib>
+#include <stdint.h>
+
+namespace CVC4 {
+ static const unsigned default_nchild_thresh = 10;
+
+ template <unsigned nchild_thresh = default_nchild_thresh>
+ class NodeBuilder;
+
+ class NodeManager;
+}/* CVC4 namespace */
-#include "expr/node_manager.h"
#include "expr/kind.h"
#include "util/Assert.h"
+#include "expr/node_value.h"
namespace CVC4 {
-class AndExprBuilder;
-class OrExprBuilder;
-class PlusExprBuilder;
-class MinusExprBuilder;
-class MultExprBuilder;
+class AndNodeBuilder;
+class OrNodeBuilder;
+class PlusNodeBuilder;
+class MinusNodeBuilder;
+class MultNodeBuilder;
+template <unsigned nchild_thresh>
class NodeBuilder {
- NodeManager* d_em;
+ unsigned d_size;
- Kind d_kind;
+ uint64_t d_hash;
+
+ NodeManager* d_nm;
// initially false, when you extract the Node this is set and you can't
// extract another
bool d_used;
- static const unsigned nchild_thresh = 10;
-
- unsigned d_nchildren;
- union {
- ExprValue* u_arr[nchild_thresh];
- std::vector<Node>* u_vec;
- } d_children;
-
- void addChild(const Node& e) { addChild(e.d_ev); }
- void addChild(ExprValue*);
- NodeBuilder& collapse();
+ NodeValue *d_ev;
+ NodeValue d_inlineEv;
+ NodeValue *d_childrenStorage[nchild_thresh];
- typedef ExprValue** ev_iterator;
- typedef ExprValue const** const_ev_iterator;
+ bool evIsAllocated() {
+ return d_ev->d_nchildren > nchild_thresh;
+ }
- ev_iterator ev_begin() {
- return d_children.u_arr;
+ template <unsigned N>
+ bool evIsAllocated(const NodeBuilder<N>& nb) {
+ return nb.d_ev->d_nchildren > N;
}
- ev_iterator ev_end() {
- return d_children.u_arr + d_nchildren;
+ bool evNeedsToBeAllocated() {
+ return d_ev->d_nchildren == d_size;
}
- NodeBuilder& reset(const ExprValue*);
+ // realloc in the default way
+ void realloc();
+
+ // realloc to a specific size
+ void realloc(size_t toSize, bool copy = true);
+
+ void allocateEvIfNecessaryForAppend() {
+ if(EXPECT_FALSE( evNeedsToBeAllocated() )) {
+ realloc();
+ }
+ }
public:
- NodeBuilder();
- NodeBuilder(Kind k);
- NodeBuilder(const Node&);
- NodeBuilder(const NodeBuilder&);
+ inline NodeBuilder();
+ inline NodeBuilder(Kind k);
+ inline NodeBuilder(const NodeBuilder<nchild_thresh>& nb);
+ template <unsigned N> inline NodeBuilder(const NodeBuilder<N>& nb);
+ inline NodeBuilder(NodeManager* nm);
+ inline NodeBuilder(NodeManager* nm, Kind k);
+ inline ~NodeBuilder();
- NodeBuilder(NodeManager*);
- NodeBuilder(NodeManager*, Kind k);
- NodeBuilder(NodeManager*, const Node&);
- NodeBuilder(NodeManager*, const NodeBuilder&);
+ typedef NodeValue::ev_iterator iterator;
+ typedef NodeValue::const_ev_iterator const_iterator;
- ~NodeBuilder();
+ iterator begin() { return d_ev->ev_begin(); }
+ iterator end() { return d_ev->ev_end(); }
+ const_iterator begin() const { return d_ev->ev_begin(); }
+ const_iterator end() const { return d_ev->ev_end(); }
// Compound expression constructors
+ /*
NodeBuilder& eqExpr(const Node& right);
NodeBuilder& notExpr();
NodeBuilder& andExpr(const Node& right);
NodeBuilder& iffExpr(const Node& right);
NodeBuilder& impExpr(const Node& right);
NodeBuilder& xorExpr(const Node& right);
+ */
- /* TODO design: these modify NodeBuilder */
+ /* TODO design: these modify NodeBuilder ?? */
+ /*
NodeBuilder& operator!() { return notExpr(); }
NodeBuilder& operator&&(const Node& right) { return andExpr(right); }
NodeBuilder& operator||(const Node& right) { return orExpr(right); }
+ */
+
+ /*
+ NodeBuilder& operator&&=(const Node& right) { return andExpr(right); }
+ NodeBuilder& operator||=(const Node& right) { return orExpr(right); }
+ */
// "Stream" expression constructor syntax
- NodeBuilder& operator<<(const Kind& op);
- NodeBuilder& operator<<(const Node& child);
+
+ NodeBuilder& operator<<(const Kind& k) {
+ Assert(d_ev->d_kind == UNDEFINED_KIND);
+ d_ev->d_kind = k;
+ return *this;
+ }
+
+ NodeBuilder& operator<<(const Node& n) {
+ return append(n);
+ }
// For pushing sequences of children
- NodeBuilder& append(const std::vector<Node>& children) { return append(children.begin(), children.end()); }
- NodeBuilder& append(Node child) { return append(&child, (&child) + 1); }
- template <class Iterator> NodeBuilder& append(const Iterator& begin, const Iterator& end);
-
- operator Node();// not const
-
- AndExprBuilder operator&&(Node);
- OrExprBuilder operator||(Node);
- PlusExprBuilder operator+ (Node);
- PlusExprBuilder operator- (Node);
- MultExprBuilder operator* (Node);
-
- friend class AndExprBuilder;
- friend class OrExprBuilder;
- friend class PlusExprBuilder;
- friend class MultExprBuilder;
+ NodeBuilder& append(const std::vector<Node>& children) {
+ return append(children.begin(), children.end());
+ }
+
+ NodeBuilder& append(const Node& n) {
+ allocateEvIfNecessaryForAppend();
+ NodeValue* ev = n.d_ev;
+ d_hash = NodeValue::computeHash(d_hash, ev);
+ ev->inc();
+ d_ev->d_children[d_ev->d_nchildren++] = ev;
+ return *this;
+ }
+
+ template <class Iterator>
+ NodeBuilder& append(const Iterator& begin, const Iterator& end) {
+ for(Iterator i = begin; i != end; ++i) {
+ append(*i);
+ }
+ return *this;
+ }
+
+ void crop() {
+ if(EXPECT_FALSE( evIsAllocated() ) && d_size > d_ev->d_nchildren) {
+ d_ev = (NodeValue*)
+ std::realloc(d_ev, sizeof(NodeValue) +
+ ( sizeof(NodeValue*) * (d_size = d_ev->d_nchildren) ));
+ }
+ }
+
+ // not const
+ operator Node();
+
+ /*
+ AndNodeBuilder operator&&(Node);
+ OrNodeBuilder operator||(Node);
+ PlusNodeBuilder operator+ (Node);
+ PlusNodeBuilder operator- (Node);
+ MultNodeBuilder operator* (Node);
+
+ friend class AndNodeBuilder;
+ friend class OrNodeBuilder;
+ friend class PlusNodeBuilder;
+ friend class MultNodeBuilder;
+ */
};/* class NodeBuilder */
-class AndExprBuilder {
+#if 0
+class AndNodeBuilder {
NodeBuilder d_eb;
public:
- AndExprBuilder(const NodeBuilder& eb) : d_eb(eb) {
+ AndNodeBuilder(const NodeBuilder& eb) : d_eb(eb) {
if(d_eb.d_kind != AND) {
d_eb.collapse();
d_eb.d_kind = AND;
}
}
- AndExprBuilder& operator&&(Node);
- OrExprBuilder operator||(Node);
+ AndNodeBuilder& operator&&(Node);
+ OrNodeBuilder operator||(Node);
operator NodeBuilder() { return d_eb; }
-};/* class AndExprBuilder */
+};/* class AndNodeBuilder */
-class OrExprBuilder {
+class OrNodeBuilder {
NodeBuilder d_eb;
public:
- OrExprBuilder(const NodeBuilder& eb) : d_eb(eb) {
+ OrNodeBuilder(const NodeBuilder& eb) : d_eb(eb) {
if(d_eb.d_kind != OR) {
d_eb.collapse();
d_eb.d_kind = OR;
}
}
- AndExprBuilder operator&&(Node);
- OrExprBuilder& operator||(Node);
+ AndNodeBuilder operator&&(Node);
+ OrNodeBuilder& operator||(Node);
operator NodeBuilder() { return d_eb; }
-};/* class OrExprBuilder */
+};/* class OrNodeBuilder */
-class PlusExprBuilder {
+class PlusNodeBuilder {
NodeBuilder d_eb;
public:
- PlusExprBuilder(const NodeBuilder& eb) : d_eb(eb) {
+ PlusNodeBuilder(const NodeBuilder& eb) : d_eb(eb) {
if(d_eb.d_kind != PLUS) {
d_eb.collapse();
d_eb.d_kind = PLUS;
}
}
- PlusExprBuilder& operator+(Node);
- PlusExprBuilder& operator-(Node);
- MultExprBuilder operator*(Node);
+ PlusNodeBuilder& operator+(Node);
+ PlusNodeBuilder& operator-(Node);
+ MultNodeBuilder operator*(Node);
operator NodeBuilder() { return d_eb; }
-};/* class PlusExprBuilder */
+};/* class PlusNodeBuilder */
-class MultExprBuilder {
+class MultNodeBuilder {
NodeBuilder d_eb;
public:
- MultExprBuilder(const NodeBuilder& eb) : d_eb(eb) {
+ MultNodeBuilder(const NodeBuilder& eb) : d_eb(eb) {
if(d_eb.d_kind != MULT) {
d_eb.collapse();
d_eb.d_kind = MULT;
}
}
- PlusExprBuilder operator+(Node);
- PlusExprBuilder operator-(Node);
- MultExprBuilder& operator*(Node);
+ PlusNodeBuilder operator+(Node);
+ PlusNodeBuilder operator-(Node);
+ MultNodeBuilder& operator*(Node);
operator NodeBuilder() { return d_eb; }
-};/* class MultExprBuilder */
-
-template <class Iterator>
-inline NodeBuilder& NodeBuilder::append(const Iterator& begin, const Iterator& end) {
- for(Iterator i = begin; i != end; ++i)
- addChild(*i);
- return *this;
-}
-
-// not const
-inline NodeBuilder::operator Node() {
- ExprValue *ev;
- uint64_t hash;
-
- Assert(d_kind != UNDEFINED_KIND, "Can't make an expression of an undefined kind!");
+};/* class MultNodeBuilder */
- // variables are permitted to be duplicates (from POV of the expression manager)
- if(d_kind == VARIABLE) {
- ev = new ExprValue;
- ev->d_kind = d_kind;
- ev->d_id = ExprValue::next_id++;// FIXME multithreading
- return Node(ev);
- } else {
- if(d_nchildren <= nchild_thresh) {
- hash = ExprValue::computeHash<ev_iterator>(d_kind, ev_begin(), ev_end());
- void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Node));
- ev = new (space) ExprValue;
- size_t nc = 0;
- ev_iterator i = ev_begin();
- ev_iterator i_end = ev_end();
- for(; i != i_end; ++i) {
- // The expressions in the allocated children are all 0, so we must
- // construct it without using an assignment operator
- ev->d_children[nc++].assignExprValue(*i);
- }
- } else {
- hash = ExprValue::computeHash<std::vector<Node>::const_iterator>(d_kind, d_children.u_vec->begin(), d_children.u_vec->end());
- void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Node));
- ev = new (space) ExprValue;
- size_t nc = 0;
- for(std::vector<Node>::iterator i = d_children.u_vec->begin(); i != d_children.u_vec->end(); ++i)
- ev->d_children[nc++] = Node(*i);
- }
- }
-
- ev->d_nchildren = d_nchildren;
- ev->d_kind = d_kind;
- ev->d_id = ExprValue::next_id++;// FIXME multithreading
- ev->d_rc = 0;
- Node e(ev);
-
- return d_em->lookup(hash, e);
-}
-
-inline AndExprBuilder NodeBuilder::operator&&(Node e) {
- return AndExprBuilder(*this) && e;
+inline AndNodeBuilder NodeBuilder::operator&&(Node e) {
+ return AndNodeBuilder(*this) && e;
}
-inline OrExprBuilder NodeBuilder::operator||(Node e) {
- return OrExprBuilder(*this) || e;
+inline OrNodeBuilder NodeBuilder::operator||(Node e) {
+ return OrNodeBuilder(*this) || e;
}
-inline PlusExprBuilder NodeBuilder::operator+ (Node e) {
- return PlusExprBuilder(*this) + e;
+inline PlusNodeBuilder NodeBuilder::operator+ (Node e) {
+ return PlusNodeBuilder(*this) + e;
}
-inline PlusExprBuilder NodeBuilder::operator- (Node e) {
- return PlusExprBuilder(*this) - e;
+inline PlusNodeBuilder NodeBuilder::operator- (Node e) {
+ return PlusNodeBuilder(*this) - e;
}
-inline MultExprBuilder NodeBuilder::operator* (Node e) {
- return MultExprBuilder(*this) * e;
+inline MultNodeBuilder NodeBuilder::operator* (Node e) {
+ return MultNodeBuilder(*this) * e;
}
-inline AndExprBuilder& AndExprBuilder::operator&&(Node e) {
+inline AndNodeBuilder& AndNodeBuilder::operator&&(Node e) {
d_eb.append(e);
return *this;
}
-inline OrExprBuilder AndExprBuilder::operator||(Node e) {
- return OrExprBuilder(d_eb.collapse()) || e;
+inline OrNodeBuilder AndNodeBuilder::operator||(Node e) {
+ return OrNodeBuilder(d_eb.collapse()) || e;
}
-inline AndExprBuilder OrExprBuilder::operator&&(Node e) {
- return AndExprBuilder(d_eb.collapse()) && e;
+inline AndNodeBuilder OrNodeBuilder::operator&&(Node e) {
+ return AndNodeBuilder(d_eb.collapse()) && e;
}
-inline OrExprBuilder& OrExprBuilder::operator||(Node e) {
+inline OrNodeBuilder& OrNodeBuilder::operator||(Node e) {
d_eb.append(e);
return *this;
}
-inline PlusExprBuilder& PlusExprBuilder::operator+(Node e) {
+inline PlusNodeBuilder& PlusNodeBuilder::operator+(Node e) {
d_eb.append(e);
return *this;
}
-inline PlusExprBuilder& PlusExprBuilder::operator-(Node e) {
+inline PlusNodeBuilder& PlusNodeBuilder::operator-(Node e) {
d_eb.append(e.uMinusExpr());
return *this;
}
-inline MultExprBuilder PlusExprBuilder::operator*(Node e) {
- return MultExprBuilder(d_eb.collapse()) * e;
+inline MultNodeBuilder PlusNodeBuilder::operator*(Node e) {
+ return MultNodeBuilder(d_eb.collapse()) * e;
}
-inline PlusExprBuilder MultExprBuilder::operator+(Node e) {
- return MultExprBuilder(d_eb.collapse()) + e;
+inline PlusNodeBuilder MultNodeBuilder::operator+(Node e) {
+ return MultNodeBuilder(d_eb.collapse()) + e;
}
-inline PlusExprBuilder MultExprBuilder::operator-(Node e) {
- return MultExprBuilder(d_eb.collapse()) - e;
+inline PlusNodeBuilder MultNodeBuilder::operator-(Node e) {
+ return MultNodeBuilder(d_eb.collapse()) - e;
}
-inline MultExprBuilder& MultExprBuilder::operator*(Node e) {
+inline MultNodeBuilder& MultNodeBuilder::operator*(Node e) {
d_eb.append(e);
return *this;
}
+#endif /* 0 */
+
+}/* CVC4 namespace */
+
+#include "expr/node.h"
+#include "expr/node_manager.h"
+
+// template implementations
+
+namespace CVC4 {
+
+template <unsigned nchild_thresh>
+inline NodeBuilder<nchild_thresh>::NodeBuilder() :
+ d_size(nchild_thresh),
+ d_nm(NodeManager::currentNM()),
+ d_used(false),
+ d_ev(&d_inlineEv),
+ d_inlineEv(0),
+ d_childrenStorage(0) {}
+
+template <unsigned nchild_thresh>
+inline NodeBuilder<nchild_thresh>::NodeBuilder(Kind k) :
+ d_size(nchild_thresh),
+ d_nm(NodeManager::currentNM()),
+ d_used(false),
+ d_ev(&d_inlineEv),
+ d_inlineEv(0),
+ d_childrenStorage(0) {
+
+ d_inlineEv.d_kind = k;
+}
+
+template <unsigned nchild_thresh>
+inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<nchild_thresh>& nb) :
+ d_size(nchild_thresh),
+ d_nm(nb.d_nm),
+ d_used(nb.d_used),
+ d_ev(&d_inlineEv),
+ d_inlineEv(0),
+ d_childrenStorage(0) {
+
+ if(evIsAllocated(nb)) {
+ realloc(nb->d_size, false);
+ std::copy(d_ev->begin(), nb.d_ev->begin(), nb.d_ev->end());
+ } else {
+ std::copy(d_inlineEv.begin(), nb.d_ev->begin(), nb.d_ev->end());
+ }
+}
+
+template <unsigned nchild_thresh>
+template <unsigned N>
+inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<N>& nb) :
+ d_size(nchild_thresh),
+ d_nm(NodeManager::currentNM()),
+ d_used(nb.d_used),
+ d_ev(&d_inlineEv),
+ d_inlineEv(0),
+ d_childrenStorage(0) {
+
+ if(nb.d_ev->d_nchildren > nchild_thresh) {
+ realloc(nb.d_size, false);
+ std::copy(d_ev->begin(), nb.d_ev->begin(), nb.d_ev->end());
+ } else {
+ std::copy(d_inlineEv.begin(), nb.d_ev->begin(), nb.d_ev->end());
+ }
+}
+
+template <unsigned nchild_thresh>
+inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm) :
+ d_size(nchild_thresh),
+ d_nm(nm),
+ d_used(false),
+ d_ev(&d_inlineEv),
+ d_inlineEv(0),
+ d_childrenStorage(0) {}
+
+template <unsigned nchild_thresh>
+inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm, Kind k) :
+ d_size(nchild_thresh),
+ d_nm(nm),
+ d_used(false),
+ d_ev(&d_inlineEv),
+ d_inlineEv(0),
+ d_childrenStorage() {
+
+ d_inlineEv.d_kind = k;
+}
+
+template <unsigned nchild_thresh>
+inline NodeBuilder<nchild_thresh>::~NodeBuilder() {
+ for(iterator i = begin();
+ i != end();
+ ++i) {
+ (*i)->dec();
+ }
+ if(evIsAllocated()) {
+ free(d_ev);
+ }
+}
+
+template <unsigned nchild_thresh>
+void NodeBuilder<nchild_thresh>::realloc() {
+ if(EXPECT_FALSE( evIsAllocated() )) {
+ d_ev = (NodeValue*)
+ std::realloc(d_ev,
+ sizeof(NodeValue) + ( sizeof(NodeValue*) * (d_size *= 2) ));
+ } else {
+ d_ev = (NodeValue*)
+ std::malloc(sizeof(NodeValue) + ( sizeof(NodeValue*) * (d_size *= 2) ));
+ d_ev->d_id = 0;
+ d_ev->d_rc = 0;
+ d_ev->d_kind = d_inlineEv.d_kind;
+ d_ev->d_nchildren = nchild_thresh;
+ std::copy(d_ev->d_children,
+ d_inlineEv.d_children,
+ d_inlineEv.d_children + nchild_thresh);
+ }
+}
+
+template <unsigned nchild_thresh>
+void NodeBuilder<nchild_thresh>::realloc(size_t toSize, bool copy) {
+ Assert( d_size < toSize );
+
+ if(EXPECT_FALSE( evIsAllocated() )) {
+ d_ev = (NodeValue*)
+ std::realloc(d_ev, sizeof(NodeValue) +
+ ( sizeof(NodeValue*) * (d_size = toSize) ));
+ } else {
+ d_ev = (NodeValue*)
+ std::malloc(sizeof(NodeValue) +
+ ( sizeof(NodeValue*) * (d_size = toSize) ));
+ d_ev->d_id = 0;
+ d_ev->d_rc = 0;
+ d_ev->d_kind = d_inlineEv.d_kind;
+ d_ev->d_nchildren = nchild_thresh;
+ if(copy) {
+ std::copy(d_ev->d_children,
+ d_inlineEv.d_children,
+ d_inlineEv.d_children + nchild_thresh);
+ }
+ }
+}
+
+template <unsigned nchild_thresh>
+NodeBuilder<nchild_thresh>::operator Node() {// not const
+ Assert(d_ev->d_kind != UNDEFINED_KIND,
+ "Can't make an expression of an undefined kind!");
+ Assert(! d_used, "This NodeBuilder has already been used!");
+
+ // implementation differs depending on whether the expression value
+ // was malloc'ed or not
+
+ if(EXPECT_FALSE( evIsAllocated() )) {
+ NodeValue *ev = d_nm->lookupNoInsert(d_hash, d_ev);
+ if(ev != d_ev) {
+ // expression already exists in node manager
+ return Node(ev);
+ }
+
+ // otherwise create the canonical expression value for this node
+ crop();
+ d_used = true;
+ ev = d_ev;
+ d_ev = NULL;
+ // this inserts into the NodeManager;
+ // return the result of lookup() in case another thread beat us to it
+ return d_nm->lookup(d_hash, ev);
+ }
+
+ NodeValue *ev = d_nm->lookupNoInsert(d_hash, &d_inlineEv);
+ if(ev != &d_inlineEv) {
+ // expression already exists in node manager
+ return Node(ev);
+ }
+
+ // otherwise create the canonical expression value for this node
+ ev = (NodeValue*)
+ std::malloc(sizeof(NodeValue) +
+ ( sizeof(NodeValue*) * d_inlineEv.d_nchildren) );
+ ev->d_nchildren = d_ev->d_nchildren;
+ ev->d_kind = d_ev->d_kind;
+ ev->d_id = NodeValue::next_id++;// FIXME multithreading
+ ev->d_rc = 0;
+ d_used = true;
+ d_ev = NULL;
+
+ // this inserts into the NodeManager;
+ // return the result of lookup() in case another thread beat us to it
+ return d_nm->lookup(d_hash, ev);
+}
}/* CVC4 namespace */
/********************* -*- C++ -*- */
-/** expr_manager.cpp
+/** node_manager.cpp
** This file is part of the CVC4 prototype.
** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
__thread NodeManager* NodeManager::s_current = 0;
-Node NodeManager::lookup(uint64_t hash, const Node& e) {
- Assert(this != NULL, "Woops, we have a bad expression manager!");
+Node NodeManager::lookup(uint64_t hash, NodeValue* ev) {
+ Assert(this != NULL, "Whoops, we have a bad expression manager!");
hash_t::iterator i = d_hash.find(hash);
if(i == d_hash.end()) {
// insert
std::vector<Node> v;
+ Node e(ev);
v.push_back(e);
d_hash.insert(std::make_pair(hash, v));
return e;
} else {
for(std::vector<Node>::iterator j = i->second.begin(); j != i->second.end(); ++j) {
- if(e.getKind() != j->getKind())
+ if(ev->getKind() != j->getKind()) {
continue;
+ }
- if(e.numChildren() != j->numChildren())
+ if(ev->numChildren() != j->numChildren()) {
continue;
+ }
- Node::const_iterator c1 = e.begin();
- Node::iterator c2 = j->begin();
- for(; c1 != e.end() && c2 != j->end(); ++c1, ++c2) {
- if(c1->d_ev != c2->d_ev)
+ NodeValue::const_iterator c1 = ev->ev_begin();
+ NodeValue::iterator c2 = j->d_ev->ev_begin();
+ for(; c1 != ev->ev_end() && c2 != j->d_ev->ev_end(); ++c1, ++c2) {
+ if((*c1).d_ev != (*c2).d_ev) {
break;
+ }
}
- if(c1 != e.end() || c2 != j->end())
+ if(c1 != ev->ev_end() || c2 != j->end()) {
continue;
+ }
return *j;
}
// didn't find it, insert
std::vector<Node> v;
+ Node e(ev);
v.push_back(e);
d_hash.insert(std::make_pair(hash, v));
return e;
}
}
+NodeValue* NodeManager::lookupNoInsert(uint64_t hash, NodeValue* ev) {
+ Assert(this != NULL, "Whoops, we have a bad expression manager!");
+ hash_t::iterator i = d_hash.find(hash);
+ if(i == d_hash.end()) {
+ return NULL;
+ } else {
+ for(std::vector<Node>::iterator j = i->second.begin(); j != i->second.end(); ++j) {
+ if(ev->getKind() != j->getKind()) {
+ continue;
+ }
+
+ if(ev->numChildren() != j->numChildren()) {
+ continue;
+ }
+
+ NodeValue::const_iterator c1 = ev->ev_begin();
+ NodeValue::iterator c2 = j->d_ev->ev_begin();
+ for(; c1 != ev->ev_end() && c2 != j->d_ev->ev_end(); ++c1, ++c2) {
+ if((*c1).d_ev != (*c2).d_ev) {
+ break;
+ }
+ }
+
+ if(c1 != ev->ev_end() || c2 != j->end()) {
+ continue;
+ }
+
+ return j->d_ev;
+ }
+ // didn't find it
+ return 0;
+ }
+}
+
// general expression-builders
Node NodeManager::mkExpr(Kind kind) {
- return NodeBuilder(this, kind);
+ return NodeBuilder<>(this, kind);
}
Node NodeManager::mkExpr(Kind kind, const Node& child1) {
- return NodeBuilder(this, kind) << child1;
+ return NodeBuilder<>(this, kind) << child1;
}
Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2) {
- return NodeBuilder(this, kind) << child1 << child2;
+ return NodeBuilder<>(this, kind) << child1 << child2;
}
Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3) {
- return NodeBuilder(this, kind) << child1 << child2 << child3;
+ return NodeBuilder<>(this, kind) << child1 << child2 << child3;
}
Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4) {
- return NodeBuilder(this, kind) << child1 << child2 << child3 << child4;
+ return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4;
}
Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5) {
- return NodeBuilder(this, kind) << child1 << child2 << child3 << child4 << child5;
+ return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4 << child5;
}
// N-ary version
Node NodeManager::mkExpr(Kind kind, const std::vector<Node>& children) {
- return NodeBuilder(this, kind).append(children);
+ return NodeBuilder<>(this, kind).append(children);
}
Node NodeManager::mkVar() {
- return NodeBuilder(this, VARIABLE);
+ return NodeBuilder<>(this, VARIABLE);
}
}/* CVC4 namespace */
namespace CVC4 {
-namespace expr {
- class ExprBuilder;
-}/* CVC4::expr namespace */
-
class NodeManager {
static __thread NodeManager* s_current;
- friend class CVC4::NodeBuilder;
+ template <unsigned> friend class CVC4::NodeBuilder;
typedef std::map<uint64_t, std::vector<Node> > hash_t;
hash_t d_hash;
- Node lookup(uint64_t hash, const Node& e);
+ Node lookup(uint64_t hash, const Node& e) { return lookup(hash, e.d_ev); }
+ Node lookup(uint64_t hash, NodeValue* e);
+ NodeValue* lookupNoInsert(uint64_t hash, NodeValue* e);
public:
- static NodeManager* currentEM() { return s_current; }
+ static NodeManager* currentNM() { return s_current; }
// general expression-builders
Node mkExpr(Kind kind);
// variables are special, because duplicates are permitted
Node mkVar();
- // TODO: these use the current EM (but must be renamed)
+ // TODO: these use the current NM (but must be renamed)
/*
static Node mkExpr(Kind kind)
- { currentEM()->mkExpr(kind); }
+ { currentNM()->mkExpr(kind); }
static Node mkExpr(Kind kind, Node child1);
- { currentEM()->mkExpr(kind, child1); }
+ { currentNM()->mkExpr(kind, child1); }
static Node mkExpr(Kind kind, Node child1, Node child2);
- { currentEM()->mkExpr(kind, child1, child2); }
+ { currentNM()->mkExpr(kind, child1, child2); }
static Node mkExpr(Kind kind, Node child1, Node child2, Node child3);
- { currentEM()->mkExpr(kind, child1, child2, child3); }
+ { currentNM()->mkExpr(kind, child1, child2, child3); }
static Node mkExpr(Kind kind, Node child1, Node child2, Node child3, Node child4);
- { currentEM()->mkExpr(kind, child1, child2, child3, child4); }
+ { currentNM()->mkExpr(kind, child1, child2, child3, child4); }
static Node mkExpr(Kind kind, Node child1, Node child2, Node child3, Node child4, Node child5);
- { currentEM()->mkExpr(kind, child1, child2, child3, child4, child5); }
+ { currentNM()->mkExpr(kind, child1, child2, child3, child4, child5); }
*/
// do we want a varargs one? perhaps not..
--- /dev/null
+/********************* -*- C++ -*- */
+/** node_value.cpp
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** An expression node.
+ **
+ ** Instances of this class are generally referenced through
+ ** cvc4::Node rather than by pointer; cvc4::Node maintains the
+ ** reference count on NodeValue instances and
+ **/
+
+#include "node_value.h"
+#include <sstream>
+
+using namespace std;
+
+namespace CVC4 {
+
+size_t NodeValue::next_id = 1;
+
+NodeValue::NodeValue() :
+ d_id(0), d_rc(MAX_RC), d_kind(NULL_EXPR), d_nchildren(0) {
+}
+
+NodeValue::NodeValue(int) :
+ d_id(0), d_rc(0), d_kind(unsigned(UNDEFINED_KIND)), d_nchildren(0) {
+}
+
+NodeValue::~NodeValue() {
+ for(ev_iterator i = ev_begin(); i != ev_end(); ++i) {
+ (*i)->dec();
+ }
+}
+
+uint64_t NodeValue::hash() const {
+ return computeHash(d_kind, ev_begin(), ev_end());
+}
+
+NodeValue* NodeValue::inc() {
+ // FIXME multithreading
+ if(d_rc < MAX_RC)
+ ++d_rc;
+ return this;
+}
+
+NodeValue* NodeValue::dec() {
+ // FIXME multithreading
+ if(d_rc < MAX_RC) {
+ if(--d_rc == 0) {
+ // FIXME gc
+ return 0;
+ }
+ }
+ return this;
+}
+
+NodeValue::iterator NodeValue::begin() {
+ return node_iterator(d_children);
+}
+
+NodeValue::iterator NodeValue::end() {
+ return node_iterator(d_children + d_nchildren);
+}
+
+NodeValue::iterator NodeValue::rbegin() {
+ return node_iterator(d_children + d_nchildren - 1);
+}
+
+NodeValue::iterator NodeValue::rend() {
+ return node_iterator(d_children - 1);
+}
+
+NodeValue::const_iterator NodeValue::begin() const {
+ return const_node_iterator(d_children);
+}
+
+NodeValue::const_iterator NodeValue::end() const {
+ return const_node_iterator(d_children + d_nchildren);
+}
+
+NodeValue::const_iterator NodeValue::rbegin() const {
+ return const_node_iterator(d_children + d_nchildren - 1);
+}
+
+NodeValue::const_iterator NodeValue::rend() const {
+ return const_node_iterator(d_children - 1);
+}
+
+NodeValue::ev_iterator NodeValue::ev_begin() {
+ return d_children;
+}
+
+NodeValue::ev_iterator NodeValue::ev_end() {
+ return d_children + d_nchildren;
+}
+
+NodeValue::ev_iterator NodeValue::ev_rbegin() {
+ return d_children + d_nchildren - 1;
+}
+
+NodeValue::ev_iterator NodeValue::ev_rend() {
+ return d_children - 1;
+}
+
+NodeValue::const_ev_iterator NodeValue::ev_begin() const {
+ return d_children;
+}
+
+NodeValue::const_ev_iterator NodeValue::ev_end() const {
+ return d_children + d_nchildren;
+}
+
+NodeValue::const_ev_iterator NodeValue::ev_rbegin() const {
+ return d_children + d_nchildren - 1;
+}
+
+NodeValue::const_ev_iterator NodeValue::ev_rend() const {
+ return d_children - 1;
+}
+
+string NodeValue::toString() const {
+ stringstream ss;
+ toStream(ss);
+ return ss.str();
+}
+
+void NodeValue::toStream(std::ostream& out) const {
+ out << "(" << Kind(d_kind);
+ if(d_kind == VARIABLE) {
+ out << ":" << this;
+ } else {
+ for(const_iterator i = begin(); i != end(); ++i) {
+ if(i != end()) {
+ out << " ";
+ }
+ out << *i;
+ }
+ }
+ out << ")";
+}
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* -*- C++ -*- */
+/** node_value.h
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** An expression node.
+ **
+ ** Instances of this class are generally referenced through
+ ** cvc4::Node rather than by pointer; cvc4::Node maintains the
+ ** reference count on NodeValue instances and
+ **/
+
+/* this must be above the check for __CVC4__EXPR__NODE_VALUE_H */
+/* to resolve a circular dependency */
+//#include "expr/node.h"
+
+#ifndef __CVC4__EXPR__NODE_VALUE_H
+#define __CVC4__EXPR__NODE_VALUE_H
+
+#include "cvc4_config.h"
+#include <stdint.h>
+#include "kind.h"
+
+#include <string>
+
+namespace CVC4 {
+
+class Node;
+template <unsigned> class NodeBuilder;
+class NodeManager;
+
+namespace expr {
+
+/**
+ * This is an NodeValue.
+ */
+class NodeValue {
+
+ /** A convenient null-valued expression value */
+ static NodeValue s_null;
+
+ /** Maximum reference count possible. Used for sticky
+ * reference-counting. Should be (1 << num_bits(d_rc)) - 1 */
+ static const unsigned MAX_RC = 255;
+
+ // this header fits into one 64-bit word
+
+ /** The ID (0 is reserved for the null value) */
+ unsigned d_id : 32;
+
+ /** The expression's reference count. @see cvc4::Node. */
+ unsigned d_rc : 8;
+
+ /** Kind of the expression */
+ unsigned d_kind : 8;
+
+ /** Number of children */
+ unsigned d_nchildren : 16;
+
+ /** Variable number of child nodes */
+ NodeValue *d_children[0];
+
+ // todo add exprMgr ref in debug case
+
+ friend class CVC4::Node;
+ template <unsigned> friend class CVC4::NodeBuilder;
+ friend class CVC4::NodeManager;
+
+ NodeValue* inc();
+ NodeValue* dec();
+
+ static size_t next_id;
+
+ /** Private default constructor for the null value. */
+ NodeValue();
+
+ /** Private default constructor for the NodeBuilder. */
+ NodeValue(int);
+
+ /** Destructor decrements the ref counts of its children */
+ ~NodeValue();
+
+ /**
+ * Computes the hash over the given iterator span of children, and the
+ * root hash. The iterator should be either over a range of Node or pointers
+ * to NodeValue.
+ * @param hash the initial value for the hash
+ * @param begin the begining of the range
+ * @param end the end of the range
+ * @return the hash value
+ */
+ template<typename const_iterator_type>
+ static uint64_t computeHash(uint64_t hash, const_iterator_type begin, const_iterator_type end) {
+ for(const_iterator_type i = begin; i != end; ++i) {
+ hash = computeHash(hash, *i);
+ }
+ return hash;
+ }
+
+ static uint64_t computeHash(uint64_t hash, const NodeValue* ev) {
+ return ( (hash << 3) | ((hash & 0xE000000000000000ull) >> 61) ) ^ ev->getId();
+ }
+
+ typedef NodeValue** ev_iterator;
+ typedef NodeValue const* const* const_ev_iterator;
+
+ ev_iterator ev_begin();
+ ev_iterator ev_end();
+ ev_iterator ev_rbegin();
+ ev_iterator ev_rend();
+
+ const_ev_iterator ev_begin() const;
+ const_ev_iterator ev_end() const;
+ const_ev_iterator ev_rbegin() const;
+ const_ev_iterator ev_rend() const;
+
+ class node_iterator {
+ const_ev_iterator d_i;
+ public:
+ node_iterator(const_ev_iterator i) : d_i(i) {}
+
+ inline Node operator*();
+
+ bool operator==(const node_iterator& i) {
+ return d_i == i.d_i;
+ }
+
+ bool operator!=(const node_iterator& i) {
+ return d_i != i.d_i;
+ }
+
+ node_iterator& operator++() {
+ ++d_i;
+ return *this;
+ }
+
+ node_iterator operator++(int) {
+ return node_iterator(d_i++);
+ }
+ };
+ typedef node_iterator const_node_iterator;
+
+public:
+ /** Hash this expression.
+ * @return the hash value of this expression. */
+ uint64_t hash() const;
+
+ // Iterator support
+
+ typedef node_iterator iterator;
+ typedef node_iterator const_iterator;
+
+ iterator begin();
+ iterator end();
+ iterator rbegin();
+ iterator rend();
+
+ const_iterator begin() const;
+ const_iterator end() const;
+ const_iterator rbegin() const;
+ const_iterator rend() const;
+
+ unsigned getId() const { return d_id; }
+ Kind getKind() const { return (Kind) d_kind; }
+ unsigned numChildren() const { return d_nchildren; }
+ std::string toString() const;
+ void toStream(std::ostream& out) const;
+};
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace expr {
+
+inline Node NodeValue::node_iterator::operator*() {
+ return Node(*d_i);
+}
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR__NODE_VALUE_H */
** [[ Add file-specific comments here ]]
**/
+#ifndef __CVC4_CONFIG_H
+#define __CVC4_CONFIG_H
+
#if defined _WIN32 || defined __CYGWIN__
# ifdef BUILDING_DLL
# ifdef __GNUC__
#define EXPECT_TRUE(x) __builtin_expect( (x), true)
#define EXPECT_FALSE(x) __builtin_expect( (x), false)
#define NORETURN __attribute__ ((noreturn))
+
+#ifndef NULL
+# define NULL ((void*) 0)
+#endif
+
+#endif /* __CVC4_CONFIG_H */
--- /dev/null
+topdir = ../..
+srcdir = src/main
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+ -I@srcdir@/../include -I@srcdir@/..
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS =
bin_PROGRAMS = cvc4
CXXCPP = @CXXCPP@
CXXDEPMODE = @CXXDEPMODE@
CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
CXXTESTGEN = @CXXTESTGEN@
CYGPATH_W = @CYGPATH_W@
DEFS = @DEFS@
top_build_prefix = @top_build_prefix@
top_builddir = @top_builddir@
top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+ -I@srcdir@/../include -I@srcdir@/..
+
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS =
cvc4_SOURCES = \
main.cpp \
getopt.cpp \
--- /dev/null
+topdir = ../..
+srcdir = src/parser
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
LIBCVC4PARSER_RELEASE = @CVC4_LIBRARY_RELEASE_CODE@
LIBCVC4PARSER_VERSION = @CVC4_PARSER_LIBRARY_VERSION@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/.. $(ANTLR_INCLUDES)
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4PARSERLIB \
+ -I@srcdir@/../include -I@srcdir@/.. $(ANTLR_INCLUDES)
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
SUBDIRS = smt cvc
CXXCPP = @CXXCPP@
CXXDEPMODE = @CXXDEPMODE@
CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
CXXTESTGEN = @CXXTESTGEN@
CYGPATH_W = @CYGPATH_W@
DEFS = @DEFS@
#
LIBCVC4PARSER_RELEASE = @CVC4_LIBRARY_RELEASE_CODE@
LIBCVC4PARSER_VERSION = @CVC4_PARSER_LIBRARY_VERSION@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/.. $(ANTLR_INCLUDES)
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4PARSERLIB \
+ -I@srcdir@/../include -I@srcdir@/.. $(ANTLR_INCLUDES)
+
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
SUBDIRS = smt cvc
nobase_lib_LTLIBRARIES = libcvc4parser.la
libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS)
LT(0).get()->getColumn());
}
-Expr AntlrParser::createPrecedenceExpr(const vector<Expr>& exprs, const vector<
- Kind>& kinds) {
+Expr AntlrParser::createPrecedenceExpr(const vector<Expr>& exprs,
+ const vector<Kind>& kinds) {
Assert( exprs.size() > 0, "Expected non-empty vector expr");
- Assert( vectors.size() + 1 == exprs.size(), "Expected kinds to match exprs");
+ Assert( kinds.size() + 1 == exprs.size(), "Expected kinds to match exprs");
return createPrecedenceExpr(exprs, kinds, 0, exprs.size() - 1);
}
--- /dev/null
+topdir = ../../..
+srcdir = src/parser/cvc
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
-INCLUDES = -I@srcdir@/../../include -I@srcdir@/../..
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4PARSERLIB \
+ -I@srcdir@/../../include -I@srcdir@/../..
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
noinst_LTLIBRARIES = libparsercvc.la
CXXCPP = @CXXCPP@
CXXDEPMODE = @CXXDEPMODE@
CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
CXXTESTGEN = @CXXTESTGEN@
CYGPATH_W = @CYGPATH_W@
DEFS = @DEFS@
top_build_prefix = @top_build_prefix@
top_builddir = @top_builddir@
top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/../../include -I@srcdir@/../..
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4PARSERLIB \
+ -I@srcdir@/../../include -I@srcdir@/../..
+
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
noinst_LTLIBRARIES = libparsercvc.la
ANTLR_TOKEN_STUFF = \
@srcdir@/generated/CvcVocabularyTokenTypes.hpp \
--- /dev/null
+topdir = ../../..
+srcdir = src/parser/smt
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
-INCLUDES = -I@srcdir@/../../include -I@srcdir@/../..
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4PARSERLIB \
+ -I@srcdir@/../../include -I@srcdir@/../..
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
noinst_LTLIBRARIES = libparsersmt.la
CXXCPP = @CXXCPP@
CXXDEPMODE = @CXXDEPMODE@
CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
CXXTESTGEN = @CXXTESTGEN@
CYGPATH_W = @CYGPATH_W@
DEFS = @DEFS@
top_build_prefix = @top_build_prefix@
top_builddir = @top_builddir@
top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/../../include -I@srcdir@/../..
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4PARSERLIB \
+ -I@srcdir@/../../include -I@srcdir@/../..
+
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
noinst_LTLIBRARIES = libparsersmt.la
ANTLR_TOKEN_STUFF = \
@srcdir@/generated/SmtVocabularyTokenTypes.hpp \
--- /dev/null
+topdir = ../..
+srcdir = src/prop
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/../include -I@srcdir@/..
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libprop.la
CXXCPP = @CXXCPP@
CXXDEPMODE = @CXXDEPMODE@
CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
CXXTESTGEN = @CXXTESTGEN@
CYGPATH_W = @CYGPATH_W@
DEFS = @DEFS@
top_build_prefix = @top_build_prefix@
top_builddir = @top_builddir@
top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/../include -I@srcdir@/..
+
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libprop.la
libprop_la_SOURCES = \
prop_engine.cpp \
--- /dev/null
+topdir = ../../..
+srcdir = src/prop/minisat
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
-INCLUDES = -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../../include
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../../include
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libminisat.la
libminisat_la_SOURCES = \
CXXCPP = @CXXCPP@
CXXDEPMODE = @CXXDEPMODE@
CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
CXXTESTGEN = @CXXTESTGEN@
CYGPATH_W = @CYGPATH_W@
DEFS = @DEFS@
top_build_prefix = @top_build_prefix@
top_builddir = @top_builddir@
top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../../include
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../../include
+
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libminisat.la
libminisat_la_SOURCES = \
core/Solver.C \
Debug("prop") << "adding vars to " << e << endl;
for(Node::iterator i = e.begin(); i != e.end(); ++i) {
Debug("prop") << "expr " << *i << endl;
- if(i->getKind() == VARIABLE) {
+ if((*i).getKind() == VARIABLE) {
if(d_vars.find(*i) == d_vars.end()) {
Var v = d_sat.newVar();
Debug("prop") << "adding var " << *i << " <--> " << v << endl;
--- /dev/null
+topdir = ../..
+srcdir = src/smt
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/../include -I@srcdir@/..
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libsmt.la
CXXCPP = @CXXCPP@
CXXDEPMODE = @CXXDEPMODE@
CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
CXXTESTGEN = @CXXTESTGEN@
CYGPATH_W = @CYGPATH_W@
DEFS = @DEFS@
top_build_prefix = @top_build_prefix@
top_builddir = @top_builddir@
top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/../include -I@srcdir@/..
+
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libsmt.la
libsmt_la_SOURCES = \
smt_engine.cpp \
--- /dev/null
+topdir = ../..
+srcdir = src/theory
+builddir = $(topdir)/$(builds)/$(srcdir)
+
+include $(topdir)/Makefile.subdir
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/../include -I@srcdir@/..
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libtheory.la
CXXCPP = @CXXCPP@
CXXDEPMODE = @CXXDEPMODE@
CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
CXXTESTGEN = @CXXTESTGEN@
CYGPATH_W = @CYGPATH_W@
DEFS = @DEFS@
top_build_prefix = @top_build_prefix@
top_builddir = @top_builddir@
top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/../include -I@srcdir@/..
+
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libtheory.la
libtheory_la_SOURCES = \
theory_engine.h \
--- /dev/null
+topdir = ../../..
+srcdir = src/theory/uf
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
-INCLUDES = -I@srcdir@/../../include -I@srcdir@/../..
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/../../include -I@srcdir@/../..
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libuf.la
CXXCPP = @CXXCPP@
CXXDEPMODE = @CXXDEPMODE@
CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
CXXTESTGEN = @CXXTESTGEN@
CYGPATH_W = @CYGPATH_W@
DEFS = @DEFS@
top_build_prefix = @top_build_prefix@
top_builddir = @top_builddir@
top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/../../include -I@srcdir@/../..
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/../../include -I@srcdir@/../..
+
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libuf.la
libuf_la_SOURCES =
all: all-am
--- /dev/null
+topdir = ../..
+srcdir = src/util
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/../include -I@srcdir@/..
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libutil.la
CXXCPP = @CXXCPP@
CXXDEPMODE = @CXXDEPMODE@
CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
CXXTESTGEN = @CXXTESTGEN@
CYGPATH_W = @CYGPATH_W@
DEFS = @DEFS@
top_build_prefix = @top_build_prefix@
top_builddir = @top_builddir@
top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/../include -I@srcdir@/..
+
AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libutil.la
libutil_la_SOURCES = \
Assert.h \
--- /dev/null
+topdir = ..
+srcdir = test
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
CXXCPP = @CXXCPP@
CXXDEPMODE = @CXXDEPMODE@
CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
CXXTESTGEN = @CXXTESTGEN@
CYGPATH_W = @CYGPATH_W@
DEFS = @DEFS@
--- /dev/null
+topdir = ../..
+srcdir = test/regress
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
-TESTS_ENVIRONMENT = echo
+TESTS_ENVIRONMENT = @top_builddir@/bin/cvc4
TESTS = \
simple.cvc \
simple.smt \
CXXCPP = @CXXCPP@
CXXDEPMODE = @CXXDEPMODE@
CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
CXXTESTGEN = @CXXTESTGEN@
CYGPATH_W = @CYGPATH_W@
DEFS = @DEFS@
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 \
--- /dev/null
+topdir = ../..
+srcdir = test/unit
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
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)
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)
CXXCPP = @CXXCPP@
CXXDEPMODE = @CXXDEPMODE@
CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
CXXTESTGEN = @CXXTESTGEN@
CYGPATH_W = @CYGPATH_W@
DEFS = @DEFS@
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
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 $@ $<
@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
@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)
+++ /dev/null
-/* Black box testing of CVC4::Node. */
-
-#include <cxxtest/TestSuite.h>
-
-#include "expr/expr.h"
-
-using namespace CVC4;
-
-class ExprBlack : public CxxTest::TestSuite {
-public:
-
- void testNull() {
- Node::s_null;
- }
-
- void testCopyCtor() {
- Node e(Node::s_null);
- }
-};
+++ /dev/null
-/* White box testing of CVC4::Node. */
-
-#include <cxxtest/TestSuite.h>
-
-#include "expr/expr.h"
-
-using namespace CVC4;
-
-class ExprWhite : public CxxTest::TestSuite {
-public:
-
- void testNull() {
- Node::s_null;
- }
-
- void testCopyCtor() {
- Node e(Node::s_null);
- }
-};
--- /dev/null
+/* Black box testing of CVC4::Node. */
+
+#include <cxxtest/TestSuite.h>
+
+#include "expr/node.h"
+
+using namespace CVC4;
+
+class NodeBlack : public CxxTest::TestSuite {
+public:
+
+ void testNull() {
+ Node::s_null;
+ }
+
+ void testCopyCtor() {
+ Node e(Node::s_null);
+ }
+};
--- /dev/null
+/* White box testing of CVC4::Node. */
+
+#include <cxxtest/TestSuite.h>
+
+#include "expr/node.h"
+
+using namespace CVC4;
+
+class NodeWhite : public CxxTest::TestSuite {
+public:
+
+ void testNull() {
+ Node::s_null;
+ }
+
+ void testCopyCtor() {
+ Node e(Node::s_null);
+ }
+};
projects / cvc5.git / commitdiff