diff options
| author | Dan Liew <daniel.liew@imperial.ac.uk> | 2016-01-14 16:03:33 +0000 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2016-02-10 20:56:22 +0000 |
| commit | e6ba74cf608cf733916f0df2471c6a5fc5a804cf (patch) | |
| tree | 97511f9e9e2d412e58099b96d03368363265f3d0 /autoconf | |
| parent | 1e22c1d667e36a84c6212e68aa1eb00b81c811e1 (diff) | |
| download | klee-e6ba74cf608cf733916f0df2471c6a5fc5a804cf.tar.gz | |
Teach the configure script to configure the build to use the Z3 SMT
solver using the new ``--with-z3=`` option.
Diffstat (limited to 'autoconf')
| -rw-r--r-- | autoconf/configure.ac | 53 |
1 files changed, 51 insertions, 2 deletions
diff --git a/autoconf/configure.ac b/autoconf/configure.ac index 0cf08a60..94928fcc 100644 --- a/autoconf/configure.ac +++ b/autoconf/configure.ac @@ -614,6 +614,55 @@ AC_SUBST(ENABLE_STP) AC_SUBST(STP_CFLAGS) AC_SUBST(STP_LDFLAGS) +dnl ************************************************************************** +dnl Find an install of Z3 +dnl ************************************************************************** + +ENABLE_Z3=0 +AC_ARG_WITH(z3, + AS_HELP_STRING([--with-z3], [Location of Z3 installation directory]), [ + # Check for empty argument + if test "X$withval" = X ; then + AC_MSG_ERROR([<path> cannot be empty in --with-z3=<path>]) + fi + z3_root=`(cd $withval && pwd) 2> /dev/null` + + #Check for bad path + if test "X$z3_root" = X ; then + AC_MSG_ERROR([Cannot access path $with_z3 passed to --with-z3]) + fi + + Z3_CFLAGS="-I$z3_root/include" + Z3_LDFLAGS="-L$z3_root/lib" + ENABLE_Z3=1 + ]) + +if test "X$ENABLE_Z3" != X0 ; then + old_CPPFLAGS="$CPPFLAGS" + CPPFLAGS="$CPPFLAGS $Z3_CFLAGS" + old_CPPFLAGS="$CPPFLAGS" + AC_CHECK_HEADER(z3.h,, + [ + AC_MSG_ERROR([Unable to use z3.h header]) + ]) + CPPFLAGS="$old_CPPFLAGS" + + AC_CHECK_LIB(z3, Z3_mk_context,[:], [ + AC_MSG_ERROR([Unable to link against z3]) + ], "$Z3_LDFLAGS") + + Z3_LDFLAGS="${Z3_LDFLAGS} -lz3" + AC_MSG_NOTICE([Using Z3 solver backend]) + CPPFLAGS="$old_CPPFLAGS" + AC_DEFINE(ENABLE_Z3, [1], [Using Z3 Solver backend]) +else + AC_MSG_NOTICE([Not using Z3 solver backend]) +fi + +AC_SUBST(ENABLE_Z3) +AC_SUBST(Z3_CFLAGS) +AC_SUBST(Z3_LDFLAGS) + dnl ************************************************************************** dnl User option to enable metaSMT constraint solvers and to specify the @@ -661,8 +710,8 @@ dnl ************************************************************************** dnl Check at least one solver backend is enabled dnl ************************************************************************** -if test "X$ENABLE_STP$ENABLE_METASMT" == X00 ; then - AC_MSG_ERROR([At least one solver backend must be enabled, try using --with-stp or --with-metasmt]) +if test "X$ENABLE_STP$ENABLE_Z3$ENABLE_METASMT" == X000 ; then + AC_MSG_ERROR([At least one solver backend must be enabled, try using --with-stp, --with-z3 or --with-metasmt]) fi |