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
|
# -*- Autoconf -*-
# Process this file with autoconf to produce a configure script.
AC_PREREQ([2.63])
AC_INIT([src/include/cvc4.h])
AC_CONFIG_AUX_DIR([config])
#AC_CONFIG_LIBOBJ_DIR([lib])
AC_CONFIG_MACRO_DIR([config])
AM_INIT_AUTOMAKE(cvc4, prerelease)
AC_CONFIG_HEADERS([config.h])
LT_INIT
AC_LIBTOOL_WIN32_DLL
# Features requested by the user
AC_MSG_CHECKING([whether to do a debug build of CVC4])
AC_ARG_ENABLE([debug], [AS_HELP_STRING([--enable-debug] ,[do a debug build of CVC4])])
if test -z "${enable_debug+set}"; then
enable_debug=no
fi
AC_MSG_RESULT([$enable_debug])
AC_MSG_CHECKING([whether to include assertions in build])
AC_ARG_ENABLE([assertions], [AS_HELP_STRING([--disable-assertions],[turn off assertions in build])])
if test -z "${enable_assertions+set}"; then
enable_assertions=yes
fi
AC_MSG_RESULT([$enable_assertions])
if test "$enable_assertions" = no -a "$enable_debug" = yes; then
AC_MSG_FAILURE([when debugging is on, so must assertions be.])
fi
# Checks for programs.
AC_PROG_CC
AC_PROG_CXX
AC_PROG_INSTALL
AC_PROG_LIBTOOL
AM_PROG_LEX
AC_PROG_YACC
AC_CHECK_PROG(DOXYGEN, doxygen, doxygen, [])
if test -z "$DOXYGEN"; then
AC_MSG_WARN([documentation targets require doxygen. Set your PATH appropriately or set DOXYGEN to point to a valid doxygen binary.])
fi
AC_ARG_VAR(DOXYGEN, [location of doxygen binary])
CXXTESTGEN=
AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH])
if test -z "$CXXTESTGEN"; then
AC_MSG_NOTICE([unit tests disabled, cxxtestgen.pl not found.])
elif test -z "$CXXTEST"; then
CXXTEST=$(dirname "$CXXTESTGEN")
AC_MSG_CHECKING([for location of CxxTest headers])
if test -e "$CXXTEST/cxxtest/TestRunner.h"; then
AC_MSG_RESULT([$CXXTEST])
else
AC_MSG_RESULT([not found])
AC_MSG_WARN([unit tests disabled, CxxTest headers not found.])
CXXTESTGEN=
CXXTEST=
fi
fi
AC_ARG_VAR(CXXTEST, [path to CxxTest installation])
AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"])
AC_ARG_VAR(TEST_CPPFLAGS, [CXXFLAGS to use when testing (default=$CPPFLAGS)])
AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)])
AC_ARG_VAR(TEST_LDFLAGS, [LDFLAGS to use when testing (default=$LDFLAGS)])
if test -n "$CXXTEST"; then
AC_CHECK_PROG(PERL, perl, perl, [])
if test -z "$PERL"; then
AC_MSG_WARN([unit tests disabled, perl not found.])
CXXTESTGEN=
CXXTEST=
fi
fi
# Checks for libraries.
AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP not found, see http://gmplib.org/])])
# Checks for header files.
AC_CHECK_HEADERS([getopt.h unistd.h])
# Checks for typedefs, structures, and compiler characteristics.
AC_HEADER_STDBOOL
AC_TYPE_UINT16_T
AC_TYPE_UINT32_T
AC_TYPE_UINT64_T
AC_TYPE_SIZE_T
# Checks for library functions.
# Some definitions for config.h
if test "$enable_debug" = yes; then
AC_DEFINE([CVC4_DEBUG], [], [Whether or not to include debugging code.])
fi
if test "$enable_assertions" = yes; then
AC_DEFINE([CVC4_ASSERTIONS], [], [Whether or not assertions are enabled.])
fi
# Prepare configure output
AC_CONFIG_FILES([
Makefile
contrib/Makefile
doc/Makefile
src/Makefile
src/expr/Makefile
src/smt/Makefile
src/main/Makefile
src/prop/minisat/Makefile
src/prop/Makefile
src/util/Makefile
src/context/Makefile
src/parser/Makefile
src/theory/Makefile
test/Makefile
test/regress/Makefile
test/unit/Makefile
])
AC_OUTPUT
# Final information to the user
debug=debug
if test "$enable_debug" = no; then
debug=non-debug
fi
withassertions=with
if test "$enable_assertions" = no; then
withassertions=without
fi
cat <<EOF
CVC4 $VERSION will be built as a $debug build $withassertions assertions.
Now just type make, followed by make check or make install, as you like.
EOF
|
