config/cvc4.m4

   1 # CVC4_AC_INIT
   2 # ------------
   3 # Do early initialization/diversion of autoconf things for CVC4 build process.
   4 AC_DEFUN([CVC4_AC_INIT],
   5 dnl _AS_ME_PREPARE
   6 [CVC4_REWRITE_ARGS_FOR_BUILD_PROFILE
   7 ])# CVC4_AC_INIT
   8
   9
  10 # CVC4_REWRITE_ARGS_FOR_BUILD_PROFILE
  11 # -----------------------------------
  12 # Rewrite (e.g.) "./configure debug" to "./configure --with-build=debug"
  13 AC_DEFUN([CVC4_REWRITE_ARGS_FOR_BUILD_PROFILE],
  14 [m4_divert_push([PARSE_ARGS])dnl
  15
  16 CVC4_BSD_LICENSED_CODE_ONLY=1
  17
  18 m4_divert_once([HELP_ENABLE], [[
  19 Licensing and performance options:
  20   --bsd                   disable all GPL dependences (default)
  21   --enable-gpl            permit GPL dependences, if available
  22   --best                  turn on dependences known to give best performance]])dnl
  23
  24 handle_option() {
  25   ac_option="$[]1"
  26   case $ac_option in
  27     --bsd|--disable-gpl|CVC4_BSD_LICENSED_CODE_ONLY=1)
  28       if test "$CVC4_LICENSE_OPTION" = gpl; then AC_ERROR([cannot give both --bsd and --enable-gpl]); fi
  29       CVC4_LICENSE_OPTION=bsd
  30       ac_option="CVC4_BSD_LICENSED_CODE_ONLY=1"
  31       eval $ac_option
  32       ;;
  33     --enable-gpl|--gpl|CVC4_BSD_LICENSED_CODE_ONLY=0)
  34       if test "$CVC4_LICENSE_OPTION" = bsd; then AC_ERROR([cannot give both --bsd and --enable-gpl]); fi
  35       CVC4_LICENSE_OPTION=gpl
  36       ac_option="CVC4_BSD_LICENSED_CODE_ONLY=0"
  37       eval $ac_option
  38       ;;
  39     --best)
  40       # set the best configuration
  41       handle_option --with-readline
  42       handle_option --with-cln
  43       handle_option --with-glpk
  44       handle_option --with-abc
  45       return
  46       ;;
  47     -enable-proofs|--enable-proofs)
  48       ac_option='--enable-proof'
  49       ;;
  50     -*|*=*)
  51       ;;
  52     production|production-*|debug|debug-*|competition|competition-*|testing|testing-*)
  53       # regexp `\?' not supported on Mac OS X
  54       ac_option_build=`expr "$ac_option" : '\([[^-]]*\)-\{0,1\}'`
  55       ac_cvc4_build_profile_set=yes
  56       as_me=configure
  57       AC_MSG_NOTICE([CVC4: building profile $ac_option_build])
  58       for x in optimized proof statistics replay assertions tracing dumping muzzle coverage profiling; do
  59         if expr "$ac_option" : '.*-no'$x'$' >/dev/null || expr "$ac_option" : '.*-no'$x'-' >/dev/null; then
  60           eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--disable-$x\""'
  61         fi
  62         if expr "$ac_option" : '.*-'$x'$' >/dev/null || expr "$ac_option" : '.*-'$x'-' >/dev/null; then
  63           eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--enable-$x\""'
  64         fi
  65       done
  66       if expr "$ac_option" : '.*-nostaticbinary$' >/dev/null || expr "$ac_option" : '.*-nostaticbinary-' >/dev/null; then
  67         eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--disable-static-binary\""'
  68       fi
  69       if expr "$ac_option" : '.*-staticbinary$' >/dev/null || expr "$ac_option" : '.*-staticbinary-' >/dev/null; then
  70         eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--enable-static-binary\""'
  71       fi
  72       if expr "$ac_option" : '.*-nodebugsymbols$' >/dev/null || expr "$ac_option" : '.*-nodebugsymbols-' >/dev/null; then
  73         eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--disable-debug-symbols\""'
  74       fi
  75       if expr "$ac_option" : '.*-debugsymbols$' >/dev/null || expr "$ac_option" : '.*-debugsymbols-' >/dev/null; then
  76         eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--enable-debug-symbols\""'
  77       fi
  78       if expr "$ac_option" : '.*-noglpk' >/dev/null || expr "$ac_option" : '.*-noglpk-' >/dev/null; then
  79         eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--without-glpk\""'
  80       fi
  81       if expr "$ac_option" : '.*-glpk' >/dev/null || expr "$ac_option" : '.*-glpk-' >/dev/null; then
  82         eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--with-glpk\""'
  83       fi
  84       if expr "$ac_option" : '.*-noabc' >/dev/null || expr "$ac_option" : '.*-noabc-' >/dev/null; then
  85         eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--without-abc\""'
  86       fi
  87       if expr "$ac_option" : '.*-abc' >/dev/null || expr "$ac_option" : '.*-abc-' >/dev/null; then
  88         eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--with-abc\""'
  89       fi
  90       for x in cln gmp; do
  91         if expr "$ac_option" : '.*-no'$x'$' >/dev/null || expr "$ac_option" : '.*-no'$x'-' >/dev/null; then
  92           eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--without-$x\""'
  93         fi
  94         if expr "$ac_option" : '.*-'$x'$' >/dev/null || expr "$ac_option" : '.*-'$x'-' >/dev/null; then
  95           eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--with-$x\""'
  96         fi
  97       done
  98       ac_option="--with-build=$ac_option_build"
  99   esac
 100   eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }'\'\$ac_option\'\"
 101 }
 102
 103 unset ac_cvc4_rewritten_args
 104 for ac_option
 105 do
 106   handle_option "$ac_option"
 107 done
 108 eval set x $ac_cvc4_rewritten_args
 109 shift
 110 dnl echo "args are now:" "${@}"
 111 m4_divert_pop([PARSE_ARGS])dnl
 112 ])# CVC4_REWRITE_ARGS_FOR_BUILD_PROFILE
 113
 114
 115 # CVC4_COPY_IF_CHANGED(FROM, TO)
 116 # ------------------------------
 117 # Copy file FROM to TO, if they have textual differences.
 118 AC_DEFUN([CVC4_COPY_IF_CHANGED], [
 119 if diff -q "$1" "$2" >/dev/null 2>&1; then
 120   dnl they are the same
 121   :
 122 else
 123   dnl they are different
 124   cp "$1" "$2"
 125 fi
 126 ])# CVC4_COPY_IF_CHANGED
 127
 128
 129 # CVC4_CONFIG_FILE_ONLY_IF_CHANGED(FILE)
 130 # --------------------------------------
 131 # Run AC_CONFIG_FILES to generate file named in the argument, but if it
 132 # exists already, only replace it if it would be changed (this preserves
 133 # the old timestamp if no textual changes are to be made to the file).
 134 AC_DEFUN([CVC4_CONFIG_FILE_ONLY_IF_CHANGED], [
 135 AC_CONFIG_FILES([$1.tmp:$1.in],
 136                 CVC4_COPY_IF_CHANGED([$1.tmp],[$1]))
 137 ])# CVC4_CONFIG_FILE_ONLY_IF_CHANGED
 138
 139 # CVC4_CXX_OPTION(OPTION, VAR)
 140 # ----------------------------
 141 # Run $(CXX) $(CPPFLAGS) $(CXXFLAGS) OPTION and see if the compiler
 142 # likes it.  If so, add OPTION to shellvar VAR.
 143 AC_DEFUN([CVC4_CXX_OPTION], [
 144 AC_MSG_CHECKING([whether $CXX supports $1])
 145 cvc4_save_CXXFLAGS="$CXXFLAGS"
 146 CXXFLAGS="$CXXFLAGS $WERROR $1"
 147 AC_LANG_PUSH([C++])
 148 AC_COMPILE_IFELSE([AC_LANG_SOURCE([int main() { return 0; }])],
 149                   [AC_MSG_RESULT([yes]); $2='$1'],
 150                   [AC_MSG_RESULT([no])])
 151 AC_LANG_POP([C++])
 152 CXXFLAGS="$cvc4_save_CXXFLAGS"
 153 ])# CVC4_CXX_OPTION
 154
 155 # CVC4_C_OPTION(OPTION, VAR)
 156 # --------------------------
 157 # Run $(CC) $(CPPFLAGS) $(CFLAGS) OPTION and see if the compiler
 158 # likes it.  If so, add OPTION to shellvar VAR.
 159 AC_DEFUN([CVC4_C_OPTION], [
 160 AC_MSG_CHECKING([whether $CC supports $1])
 161 cvc4_save_CFLAGS="$CFLAGS"
 162 CFLAGS="$CFLAGS $C_WERROR $1"
 163 AC_LANG_PUSH([C])
 164 AC_COMPILE_IFELSE([AC_LANG_SOURCE([int main() { return 0; }])],
 165                   [AC_MSG_RESULT([yes]); $2='$1'],
 166                   [AC_MSG_RESULT([no])])
 167 AC_LANG_POP([C])
 168 CFLAGS="$cvc4_save_CFLAGS"
 169 ])# CVC4_C_OPTION