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