diff options
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 |