diff options
73 files changed, 1400 insertions, 1044 deletions
@@ -1,22 +1,3 @@ -.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 diff --git a/Makefile.in b/Makefile.in index 85a9a9da1..6beb31597 100644 --- a/Makefile.in +++ b/Makefile.in @@ -132,6 +132,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ diff --git a/Makefile.subdir b/Makefile.subdir new file mode 100644 index 000000000..6aa62bf28 --- /dev/null +++ b/Makefile.subdir @@ -0,0 +1,13 @@ +.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 diff --git a/autogen.sh b/autogen.sh index 3ebd6c6a7..eed091821 100755 --- a/autogen.sh +++ b/autogen.sh @@ -33,10 +33,10 @@ 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 diff --git a/config/antlr.m4 b/config/antlr.m4 index ad0ddcd91..317159193 100644 --- a/config/antlr.m4 +++ b/config/antlr.m4 @@ -7,7 +7,7 @@ AC_DEFUN([AC_PROG_ANTLR], [ # 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] ), @@ -43,7 +43,7 @@ AC_DEFUN([AC_LIB_ANTLR],[ # 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 @@ -721,6 +721,7 @@ TEST_CPPFLAGS HAVE_CXXTESTGEN_FALSE HAVE_CXXTESTGEN_TRUE CXXTESTGEN +CXXTEST DOXYGEN ANTLR CXXCPP @@ -730,8 +731,6 @@ CXXDEPMODE ac_ct_CXX CXXFLAGS CXX -DLLTOOL -AS CPP OTOOL64 OTOOL @@ -741,7 +740,6 @@ DSYMUTIL lt_ECHO RANLIB AR -OBJDUMP LN_S NM ac_ct_DUMPBIN @@ -768,6 +766,9 @@ LDFLAGS CFLAGS CC LIBTOOL +OBJDUMP +DLLTOOL +AS am__untar am__tar AMTAR @@ -877,6 +878,7 @@ CXXFLAGS CCC CXXCPP DOXYGEN +CXXTEST TEST_CPPFLAGS TEST_CXXFLAGS TEST_LDFLAGS' @@ -1557,6 +1559,7 @@ Some influential environment variables: 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 @@ -2569,6 +2572,7 @@ ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $ 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 @@ -2876,6 +2880,12 @@ $as_echo "builds/$target/$build_type" >&6; } (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 @@ -3540,6 +3550,307 @@ if test -z "${LDFLAGS+set}" ; then user_ldflags=no ; else user_ldflags=yes ; fi { $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 @@ -5105,13 +5416,13 @@ if test "${lt_cv_nm_interface+set}" = set; then : 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" @@ -5457,9 +5768,6 @@ test -z "$OBJDUMP" && OBJDUMP=objdump - - - { $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 : @@ -6317,7 +6625,7 @@ ia64-*-hpux*) ;; *-*-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=$? @@ -7354,8 +7662,6 @@ done enable_dlopen=no - enable_win32_dll=no - @@ -7787,11 +8093,11 @@ else -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. @@ -8126,11 +8432,11 @@ else -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. @@ -8231,11 +8537,11 @@ else -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 @@ -8286,11 +8592,11 @@ else -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 @@ -10669,7 +10975,7 @@ else 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 @@ -10765,7 +11071,7 @@ else 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 @@ -10993,308 +11299,6 @@ CC="$lt_save_CC" -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 - - - - - - # Checks for programs. ac_ext=c @@ -14623,11 +14627,11 @@ else -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. @@ -14722,11 +14726,11 @@ else -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 @@ -14774,11 +14778,11 @@ else -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 @@ -15723,7 +15727,6 @@ ac_compiler_gnu=$ac_cv_c_compiler_gnu - # Check for ANTLR runantlr script (defined in config/antlr.m4) @@ -15877,6 +15880,7 @@ $as_echo "$as_me: WARNING: documentation targets require doxygen. Set your PATH 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 @@ -17083,6 +17087,9 @@ double_quote_subst='$double_quote_subst' 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"`' @@ -17109,7 +17116,6 @@ lt_SP2NL='`$ECHO "X$lt_SP2NL" | $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"`' @@ -17199,8 +17205,6 @@ enable_dlopen_self='`$ECHO "X$enable_dlopen_self" | $Xsed -e "$delay_single_quot 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"`' @@ -17270,7 +17274,6 @@ LN_S \ lt_SP2NL \ lt_NL2SP \ reload_flag \ -OBJDUMP \ deplibs_check_method \ file_magic_cmd \ AR \ @@ -18195,6 +18198,15 @@ build_libtool_libs=$enable_shared # 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 @@ -18258,9 +18270,6 @@ NL2SP=$lt_lt_NL2SP 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 @@ -18403,12 +18412,6 @@ dlopen_self_static=$enable_dlopen_self_static 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 @@ -19000,6 +19003,11 @@ $as_echo "$as_me: WARNING: " >&2;} 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 @@ -19013,6 +19021,7 @@ Tracing : $enable_tracing Muzzle : $enable_muzzle gcov support : $enable_coverage gprof support: $enable_profiling +unit tests : $support_unit_tests CPPFLAGS : $CPPFLAGS CXXFLAGS : $CXXFLAGS diff --git a/configure.ac b/configure.ac index 21e74726e..8b4a3ea64 100644 --- a/configure.ac +++ b/configure.ac @@ -3,8 +3,9 @@ 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]) @@ -111,6 +112,12 @@ elif test -e src/include/cvc4_config.h; then (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 @@ -245,17 +252,14 @@ AC_MSG_CHECKING([for user LDFLAGS]) 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 @@ -265,6 +269,7 @@ if test -z "$DOXYGEN"; then 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 @@ -371,6 +376,11 @@ if test "$non_standard_build_profile" = yes; 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 @@ -384,6 +394,7 @@ Tracing : $enable_tracing Muzzle : $enable_muzzle gcov support : $enable_coverage gprof support: $enable_profiling +unit tests : $support_unit_tests CPPFLAGS : $CPPFLAGS CXXFLAGS : $CXXFLAGS diff --git a/contrib/Makefile.in b/contrib/Makefile.in index a43e24709..e4bf7b362 100644 --- a/contrib/Makefile.in +++ b/contrib/Makefile.in @@ -75,6 +75,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ diff --git a/doc/Makefile.in b/doc/Makefile.in index 7dd071a2c..d5264caff 100644 --- a/doc/Makefile.in +++ b/doc/Makefile.in @@ -75,6 +75,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ diff --git a/src/Makefile b/src/Makefile new file mode 100644 index 000000000..e119c83d7 --- /dev/null +++ b/src/Makefile @@ -0,0 +1,5 @@ +topdir = .. +srcdir = src +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/Makefile.am b/src/Makefile.am index 1db9d9ecf..f429e8b2a 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -15,9 +15,10 @@ 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 diff --git a/src/Makefile.in b/src/Makefile.in index 8f33fd330..38d59d02a 100644 --- a/src/Makefile.in +++ b/src/Makefile.in @@ -159,6 +159,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -287,9 +288,8 @@ top_srcdir = @top_srcdir@ # 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) @@ -700,6 +700,8 @@ uninstall-am: uninstall-libLTLIBRARIES tags tags-recursive uninstall uninstall-am \ uninstall-libLTLIBRARIES + -D__BUILDING_CVC4LIB \ + -I@srcdir@/include -I@srcdir@ install-data-local: $(publicheaders) $(mkinstalldirs) $(DESTDIR)$(includedir)/cvc4 diff --git a/src/context/Makefile b/src/context/Makefile new file mode 100644 index 000000000..5286dd3ac --- /dev/null +++ b/src/context/Makefile @@ -0,0 +1,5 @@ +topdir = ../.. +srcdir = src/context +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/context/Makefile.am b/src/context/Makefile.am index e38f7f4eb..b36d5e69c 100644 --- a/src/context/Makefile.am +++ b/src/context/Makefile.am @@ -1,6 +1,7 @@ -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 diff --git a/src/context/Makefile.in b/src/context/Makefile.in index 0e5281ca6..51069583d 100644 --- a/src/context/Makefile.in +++ b/src/context/Makefile.in @@ -52,7 +52,7 @@ CONFIG_CLEAN_FILES = 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 @@ -104,6 +104,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -215,13 +216,17 @@ target_vendor = @target_vendor@ 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 @@ -276,6 +281,7 @@ distclean-compile: -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 $@ $< diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp index 51f192f2a..3b4089b25 100644 --- a/src/context/context_mm.cpp +++ b/src/context/context_mm.cpp @@ -14,14 +14,13 @@ #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 @@ -30,16 +29,16 @@ void ContextMemoryManager::newChunk() { "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(); @@ -47,30 +46,30 @@ void ContextMemoryManager::newChunk() { } -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; @@ -86,7 +85,7 @@ void* newData(size_t size) { } -void push() { +void ContextMemoryManager::push() { // Store current state on the stack d_nextFreeStack.push_back(d_nextFree); d_endChunkStack.push_back(d_endChunk); @@ -94,7 +93,7 @@ void push() { } -void pop() { +void ContextMemoryManager::pop() { // Restore state from stack d_nextFree = d_nextFreeStack.back(); d_nextFreeStack.pop_back(); @@ -103,7 +102,7 @@ void pop() { // 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; } @@ -111,12 +110,11 @@ void pop() { // 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 */ diff --git a/src/context/context_mm.h b/src/context/context_mm.h index 6b442d4a0..d48cbedc0 100644 --- a/src/context/context_mm.h +++ b/src/context/context_mm.h @@ -33,13 +33,13 @@ class ContextMemoryManager { /** * 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 diff --git a/src/expr/Makefile b/src/expr/Makefile new file mode 100644 index 000000000..b661835a5 --- /dev/null +++ b/src/expr/Makefile @@ -0,0 +1,5 @@ +topdir = ../.. +srcdir = src/expr +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index b8606e051..046281702 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -1,6 +1,7 @@ -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 @@ -10,7 +11,7 @@ libexpr_la_SOURCES = \ node.h \ node_builder.h \ expr.h \ - expr_value.h \ + node_value.h \ node_manager.h \ expr_manager.h \ node_attribute.h \ @@ -19,6 +20,6 @@ libexpr_la_SOURCES = \ node_builder.cpp \ node_manager.cpp \ expr_manager.cpp \ - expr_value.cpp \ + node_value.cpp \ expr.cpp diff --git a/src/expr/Makefile.in b/src/expr/Makefile.in index 6b1555e6c..c7d99dc84 100644 --- a/src/expr/Makefile.in +++ b/src/expr/Makefile.in @@ -53,7 +53,7 @@ CONFIG_CLEAN_VPATH_FILES = 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 @@ -105,6 +105,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -216,9 +217,11 @@ target_vendor = @target_vendor@ 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 \ @@ -226,7 +229,7 @@ libexpr_la_SOURCES = \ node.h \ node_builder.h \ expr.h \ - expr_value.h \ + node_value.h \ node_manager.h \ expr_manager.h \ node_attribute.h \ @@ -235,7 +238,7 @@ libexpr_la_SOURCES = \ node_builder.cpp \ node_manager.cpp \ expr_manager.cpp \ - expr_value.cpp \ + node_value.cpp \ expr.cpp all: all-am @@ -292,10 +295,10 @@ distclean-compile: @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 $@ $< diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp deleted file mode 100644 index af064f43d..000000000 --- a/src/expr/expr_value.cpp +++ /dev/null @@ -1,103 +0,0 @@ -/********************* -*- 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 */ diff --git a/src/expr/kind.h b/src/expr/kind.h index 5ac02ca7c..624ab7337 100644 --- a/src/expr/kind.h +++ b/src/expr/kind.h @@ -12,6 +12,7 @@ #ifndef __CVC4__KIND_H #define __CVC4__KIND_H +#include "cvc4_config.h" #include <iostream> namespace CVC4 { diff --git a/src/expr/node.cpp b/src/expr/node.cpp index be9ac995c..1a549973f 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -1,5 +1,5 @@ /********************* -*- 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 @@ -11,7 +11,7 @@ **/ #include "expr/node.h" -#include "expr/expr_value.h" +#include "expr/node_value.h" #include "expr/node_builder.h" #include "util/Assert.h" @@ -22,26 +22,29 @@ using namespace std; 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(); } @@ -57,7 +60,7 @@ Node::~Node() { d_ev->dec(); } -void Node::assignExprValue(ExprValue* ev) { +void Node::assignNodeValue(NodeValue* ev) { d_ev = ev; d_ev->inc(); } @@ -72,7 +75,7 @@ Node& Node::operator=(const Node& e) { 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; } @@ -83,35 +86,35 @@ uint64_t Node::hash() const { } 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 */ diff --git a/src/expr/node.h b/src/expr/node.h index 17d1c0111..5415a5b3c 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -10,6 +10,8 @@ ** Reference-counted encapsulation of a pointer to an expression. **/ +#include "expr/node_value.h" + #ifndef __CVC4__NODE_H #define __CVC4__NODE_H @@ -32,38 +34,44 @@ inline std::ostream& operator<<(std::ostream&, const Node&); 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 @@ -72,7 +80,15 @@ class Node { * * @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: @@ -82,7 +98,7 @@ 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; } @@ -117,8 +133,8 @@ public: 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(); @@ -134,7 +150,7 @@ public: }/* CVC4 namespace */ -#include "expr/expr_value.h" +#include "expr/node_value.h" namespace CVC4 { @@ -159,6 +175,22 @@ inline void Node::toStream(std::ostream& out) const { 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(); } diff --git a/src/expr/node_builder.cpp b/src/expr/node_builder.cpp index 7d30ff4e3..0a36421f2 100644 --- a/src/expr/node_builder.cpp +++ b/src/expr/node_builder.cpp @@ -1,5 +1,5 @@ /********************* -*- 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 @@ -11,214 +11,7 @@ #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 */ diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 5be3c284d..63048c1ac 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -1,5 +1,5 @@ /********************* -*- 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 @@ -14,68 +14,90 @@ #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); @@ -84,230 +106,413 @@ public: 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 */ diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 8da87c9eb..ab52b9f40 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -1,5 +1,5 @@ /********************* -*- 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 @@ -18,76 +18,116 @@ namespace CVC4 { __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 */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 6c20b29e8..3a28a22ff 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -20,22 +20,20 @@ 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); @@ -50,20 +48,20 @@ public: // 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.. diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp new file mode 100644 index 000000000..7af2cd2b5 --- /dev/null +++ b/src/expr/node_value.cpp @@ -0,0 +1,147 @@ +/********************* -*- 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 */ diff --git a/src/expr/expr_value.h b/src/expr/node_value.h index 25fada4af..9bdbb7f8c 100644 --- a/src/expr/expr_value.h +++ b/src/expr/node_value.h @@ -1,5 +1,5 @@ /********************* -*- C++ -*- */ -/** expr_value.h +/** 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 @@ -11,15 +11,15 @@ ** ** Instances of this class are generally referenced through ** cvc4::Node rather than by pointer; cvc4::Node maintains the - ** reference count on ExprValue instances and + ** reference count on NodeValue instances and **/ -/* this must be above the check for __CVC4__EXPR__EXPR_VALUE_H */ +/* this must be above the check for __CVC4__EXPR__NODE_VALUE_H */ /* to resolve a circular dependency */ -#include "expr/node.h" +//#include "expr/node.h" -#ifndef __CVC4__EXPR__EXPR_VALUE_H -#define __CVC4__EXPR__EXPR_VALUE_H +#ifndef __CVC4__EXPR__NODE_VALUE_H +#define __CVC4__EXPR__NODE_VALUE_H #include "cvc4_config.h" #include <stdint.h> @@ -30,17 +30,18 @@ namespace CVC4 { class Node; -class NodeBuilder; +template <unsigned> class NodeBuilder; +class NodeManager; namespace expr { /** - * This is an ExprValue. + * This is an NodeValue. */ -class ExprValue { +class NodeValue { /** A convenient null-valued expression value */ - static ExprValue s_null; + static NodeValue s_null; /** Maximum reference count possible. Used for sticky * reference-counting. Should be (1 << num_bits(d_rc)) - 1 */ @@ -61,25 +62,32 @@ class ExprValue { unsigned d_nchildren : 16; /** Variable number of child nodes */ - Node d_children[0]; + NodeValue *d_children[0]; // todo add exprMgr ref in debug case friend class CVC4::Node; - friend class CVC4::NodeBuilder; + template <unsigned> friend class CVC4::NodeBuilder; + friend class CVC4::NodeManager; - ExprValue* inc(); - ExprValue* dec(); + NodeValue* inc(); + NodeValue* dec(); static size_t next_id; /** Private default constructor for the null value. */ - ExprValue(); + 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 ExprValue. + * to NodeValue. * @param hash the initial value for the hash * @param begin the begining of the range * @param end the end of the range @@ -87,11 +95,55 @@ class ExprValue { */ 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(); + 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. */ @@ -99,8 +151,8 @@ public: // Iterator support - typedef Node* iterator; - typedef Node const* const_iterator; + typedef node_iterator iterator; + typedef node_iterator const_iterator; iterator begin(); iterator end(); @@ -113,7 +165,8 @@ public: const_iterator rend() const; unsigned getId() const { return d_id; } - unsigned getKind() const { return (Kind) d_kind; } + Kind getKind() const { return (Kind) d_kind; } + unsigned numChildren() const { return d_nchildren; } std::string toString() const; void toStream(std::ostream& out) const; }; @@ -121,4 +174,16 @@ public: }/* CVC4::expr namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__EXPR__EXPR_VALUE_H */ +#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 */ diff --git a/src/include/cvc4_config.h b/src/include/cvc4_config.h index a42ae28fb..f1877781f 100644 --- a/src/include/cvc4_config.h +++ b/src/include/cvc4_config.h @@ -10,6 +10,9 @@ ** [[ Add file-specific comments here ]] **/ +#ifndef __CVC4_CONFIG_H +#define __CVC4_CONFIG_H + #if defined _WIN32 || defined __CYGWIN__ # ifdef BUILDING_DLL # ifdef __GNUC__ @@ -35,3 +38,9 @@ #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 */ diff --git a/src/main/Makefile b/src/main/Makefile new file mode 100644 index 000000000..686674906 --- /dev/null +++ b/src/main/Makefile @@ -0,0 +1,5 @@ +topdir = ../.. +srcdir = src/main +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 6b8ea928c..f5b76fcfb 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -1,6 +1,6 @@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. +AM_CPPFLAGS = \ + -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = bin_PROGRAMS = cvc4 diff --git a/src/main/Makefile.in b/src/main/Makefile.in index ba924109e..26ea81859 100644 --- a/src/main/Makefile.in +++ b/src/main/Makefile.in @@ -106,6 +106,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -217,9 +218,10 @@ target_vendor = @target_vendor@ 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 \ diff --git a/src/parser/Makefile b/src/parser/Makefile new file mode 100644 index 000000000..1ea7edf5d --- /dev/null +++ b/src/parser/Makefile @@ -0,0 +1,5 @@ +topdir = ../.. +srcdir = src/parser +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index e54d4aa2d..7f1ddce1f 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -15,9 +15,10 @@ 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 diff --git a/src/parser/Makefile.in b/src/parser/Makefile.in index b2e066f8d..859329834 100644 --- a/src/parser/Makefile.in +++ b/src/parser/Makefile.in @@ -168,6 +168,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -296,9 +297,11 @@ top_srcdir = @top_srcdir@ # 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) diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index 2d3033a59..1baaf2139 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -133,10 +133,10 @@ void AntlrParser::rethrow(antlr::SemanticException& e, string new_message) 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); } diff --git a/src/parser/cvc/Makefile b/src/parser/cvc/Makefile new file mode 100644 index 000000000..c91554a47 --- /dev/null +++ b/src/parser/cvc/Makefile @@ -0,0 +1,5 @@ +topdir = ../../.. +srcdir = src/parser/cvc +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am index 6fb9689de..666c408cf 100644 --- a/src/parser/cvc/Makefile.am +++ b/src/parser/cvc/Makefile.am @@ -1,6 +1,7 @@ -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 diff --git a/src/parser/cvc/Makefile.in b/src/parser/cvc/Makefile.in index cbab2fd5c..57db98f0b 100644 --- a/src/parser/cvc/Makefile.in +++ b/src/parser/cvc/Makefile.in @@ -108,6 +108,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -219,9 +220,11 @@ target_vendor = @target_vendor@ 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 \ diff --git a/src/parser/smt/Makefile b/src/parser/smt/Makefile new file mode 100644 index 000000000..aa3e74236 --- /dev/null +++ b/src/parser/smt/Makefile @@ -0,0 +1,5 @@ +topdir = ../../.. +srcdir = src/parser/smt +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am index c3273f501..6f5f1bfd4 100644 --- a/src/parser/smt/Makefile.am +++ b/src/parser/smt/Makefile.am @@ -1,6 +1,7 @@ -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 diff --git a/src/parser/smt/Makefile.in b/src/parser/smt/Makefile.in index 281d2152b..2e9350486 100644 --- a/src/parser/smt/Makefile.in +++ b/src/parser/smt/Makefile.in @@ -108,6 +108,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -219,9 +220,11 @@ target_vendor = @target_vendor@ 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 \ diff --git a/src/prop/Makefile b/src/prop/Makefile new file mode 100644 index 000000000..79fe1084b --- /dev/null +++ b/src/prop/Makefile @@ -0,0 +1,5 @@ +topdir = ../.. +srcdir = src/prop +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am index 715e79d16..3473de30f 100644 --- a/src/prop/Makefile.am +++ b/src/prop/Makefile.am @@ -1,6 +1,7 @@ -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 diff --git a/src/prop/Makefile.in b/src/prop/Makefile.in index 6d4e7f0b5..311d3f8c7 100644 --- a/src/prop/Makefile.in +++ b/src/prop/Makefile.in @@ -142,6 +142,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -253,9 +254,11 @@ target_vendor = @target_vendor@ 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 \ diff --git a/src/prop/minisat/Makefile b/src/prop/minisat/Makefile new file mode 100644 index 000000000..49512a1cd --- /dev/null +++ b/src/prop/minisat/Makefile @@ -0,0 +1,5 @@ +topdir = ../../.. +srcdir = src/prop/minisat +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am index f066f8669..609c25dd7 100644 --- a/src/prop/minisat/Makefile.am +++ b/src/prop/minisat/Makefile.am @@ -1,6 +1,7 @@ -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 = \ diff --git a/src/prop/minisat/Makefile.in b/src/prop/minisat/Makefile.in index a2cc36300..a54518c74 100644 --- a/src/prop/minisat/Makefile.in +++ b/src/prop/minisat/Makefile.in @@ -104,6 +104,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -215,9 +216,11 @@ target_vendor = @target_vendor@ 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 \ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 166546a2c..caf87428b 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -34,7 +34,7 @@ void PropEngine::addVars(Node e) { 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; diff --git a/src/smt/Makefile b/src/smt/Makefile new file mode 100644 index 000000000..84a43ff39 --- /dev/null +++ b/src/smt/Makefile @@ -0,0 +1,5 @@ +topdir = ../.. +srcdir = src/smt +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am index b3637b6d9..bd75bacab 100644 --- a/src/smt/Makefile.am +++ b/src/smt/Makefile.am @@ -1,6 +1,7 @@ -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 diff --git a/src/smt/Makefile.in b/src/smt/Makefile.in index 7c60db89b..9647e51b9 100644 --- a/src/smt/Makefile.in +++ b/src/smt/Makefile.in @@ -104,6 +104,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -215,9 +216,11 @@ target_vendor = @target_vendor@ 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 \ diff --git a/src/theory/Makefile b/src/theory/Makefile new file mode 100644 index 000000000..2a4a03491 --- /dev/null +++ b/src/theory/Makefile @@ -0,0 +1,5 @@ +topdir = ../.. +srcdir = src/theory +builddir = $(topdir)/$(builds)/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index f8e9908c9..4eba7811c 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -1,6 +1,7 @@ -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 diff --git a/src/theory/Makefile.in b/src/theory/Makefile.in index 7af3f957c..d37387741 100644 --- a/src/theory/Makefile.in +++ b/src/theory/Makefile.in @@ -142,6 +142,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -253,9 +254,11 @@ target_vendor = @target_vendor@ 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 \ diff --git a/src/theory/uf/Makefile b/src/theory/uf/Makefile new file mode 100644 index 000000000..524ff2009 --- /dev/null +++ b/src/theory/uf/Makefile @@ -0,0 +1,5 @@ +topdir = ../../.. +srcdir = src/theory/uf +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index 11c9f536e..4b36d2fe8 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -1,6 +1,7 @@ -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 diff --git a/src/theory/uf/Makefile.in b/src/theory/uf/Makefile.in index 4920e7a0c..dfb8ea932 100644 --- a/src/theory/uf/Makefile.in +++ b/src/theory/uf/Makefile.in @@ -90,6 +90,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -201,9 +202,11 @@ target_vendor = @target_vendor@ 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 diff --git a/src/util/Makefile b/src/util/Makefile new file mode 100644 index 000000000..0bd2f197b --- /dev/null +++ b/src/util/Makefile @@ -0,0 +1,5 @@ +topdir = ../.. +srcdir = src/util +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/util/Makefile.am b/src/util/Makefile.am index b6c116a6d..316c747de 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -1,6 +1,7 @@ -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 diff --git a/src/util/Makefile.in b/src/util/Makefile.in index 61768f933..5627e01a9 100644 --- a/src/util/Makefile.in +++ b/src/util/Makefile.in @@ -105,6 +105,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -216,9 +217,11 @@ target_vendor = @target_vendor@ 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 \ diff --git a/test/Makefile b/test/Makefile new file mode 100644 index 000000000..80f8a1dd5 --- /dev/null +++ b/test/Makefile @@ -0,0 +1,5 @@ +topdir = .. +srcdir = test +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/test/Makefile.in b/test/Makefile.in index 0fecac937..69e05dd65 100644 --- a/test/Makefile.in +++ b/test/Makefile.in @@ -115,6 +115,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ diff --git a/test/regress/Makefile b/test/regress/Makefile new file mode 100644 index 000000000..c4e305306 --- /dev/null +++ b/test/regress/Makefile @@ -0,0 +1,5 @@ +topdir = ../.. +srcdir = test/regress +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am index a4a06c10b..61527e4d8 100644 --- a/test/regress/Makefile.am +++ b/test/regress/Makefile.am @@ -1,4 +1,4 @@ -TESTS_ENVIRONMENT = echo +TESTS_ENVIRONMENT = @top_builddir@/bin/cvc4 TESTS = \ simple.cvc \ simple.smt \ diff --git a/test/regress/Makefile.in b/test/regress/Makefile.in index 451d333e2..14c032220 100644 --- a/test/regress/Makefile.in +++ b/test/regress/Makefile.in @@ -77,6 +77,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -188,7 +189,7 @@ target_vendor = @target_vendor@ 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 \ diff --git a/test/unit/Makefile b/test/unit/Makefile new file mode 100644 index 000000000..f3f3767aa --- /dev/null +++ b/test/unit/Makefile @@ -0,0 +1,5 @@ +topdir = ../.. +srcdir = test/unit +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index d6908cef9..e10856bba 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -1,19 +1,27 @@ 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) diff --git a/test/unit/Makefile.in b/test/unit/Makefile.in index bcd2d239c..b630f7765 100644 --- a/test/unit/Makefile.in +++ b/test/unit/Makefile.in @@ -75,8 +75,8 @@ am__installdirs = "$(DESTDIR)$(libdir)" 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) @@ -122,6 +122,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -233,18 +234,26 @@ target_vendor = @target_vendor@ 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 @@ -321,7 +330,7 @@ mostlyclean-compile: 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 $@ $< @@ -344,12 +353,12 @@ distclean-compile: @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 @@ -655,7 +664,7 @@ uninstall-am: uninstall-libLTLIBRARIES @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) diff --git a/test/unit/expr/expr_black.h b/test/unit/expr/node_black.h index ad70bec91..5489e4803 100644 --- a/test/unit/expr/expr_black.h +++ b/test/unit/expr/node_black.h @@ -2,11 +2,11 @@ #include <cxxtest/TestSuite.h> -#include "expr/expr.h" +#include "expr/node.h" using namespace CVC4; -class ExprBlack : public CxxTest::TestSuite { +class NodeBlack : public CxxTest::TestSuite { public: void testNull() { diff --git a/test/unit/expr/expr_white.h b/test/unit/expr/node_white.h index 6b48d66e6..dd462fdd8 100644 --- a/test/unit/expr/expr_white.h +++ b/test/unit/expr/node_white.h @@ -2,11 +2,11 @@ #include <cxxtest/TestSuite.h> -#include "expr/expr.h" +#include "expr/node.h" using namespace CVC4; -class ExprWhite : public CxxTest::TestSuite { +class NodeWhite : public CxxTest::TestSuite { public: void testNull() { |