diff options
Diffstat (limited to 'config/abc.m4')
| -rw-r--r-- | config/abc.m4 | 135 |
1 files changed, 135 insertions, 0 deletions
diff --git a/config/abc.m4 b/config/abc.m4 new file mode 100644 index 000000000..d86b2f465 --- /dev/null +++ b/config/abc.m4 @@ -0,0 +1,135 @@ +# CVC4_CHECK_FOR_ABC +# ------------------ +# Look for abc and link it in, but only if user requested. +AC_DEFUN([CVC4_CHECK_FOR_ABC], [ +AC_MSG_CHECKING([whether user requested abc support]) +LIBABC= +have_libabc=0 +ABC_LIBS= +if test "$with_abc" = no; then + AC_MSG_RESULT([no, abc disabled by user]) +elif test "$with_abc" = yes; then + AC_MSG_RESULT([yes, abc requested by user]) + + # Get the location of all the ABC stuff + AC_ARG_VAR(ABC_HOME, [path to top level of abc source tree]) + AC_ARG_WITH( + [abc-dir], + AS_HELP_STRING( + [--with-abc-dir=PATH], + [path to top level of abc source tree] + ), + [ABC_HOME="$withval"], + [ if test -z "$ABC_HOME"; then + AC_MSG_FAILURE([must give --with-abc-dir=PATH or define environment variable ABC_HOME!]) + fi + ] + ) + if ! test -d "$ABC_HOME" || ! test -x "$ABC_HOME/arch_flags"; then + AC_MSG_FAILURE([either $ABC_HOME is not an abc source tree or it's not yet built]) + fi + + AC_MSG_CHECKING([for arch_flags to use with libabc]) + libabc_arch_flags="$("$ABC_HOME/arch_flags")" + AC_MSG_RESULT([$libabc_arch_flags]) + CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$ABC_HOME/src $libabc_arch_flags" + ABC_LDFLAGS="-L$ABC_HOME" + + dnl Try a bunch of combinations until something works :-/ + cvc4_save_LDFLAGS="$LDFLAGS" + ABC_LIBS= + CPPFLAGS="$CPPFLAGS -I$ABC_HOME/src $libabc_arch_flags" + LDFLAGS="$LDFLAGS $ABC_LDFLAGS" + AC_CHECK_HEADER([base/abc/abc.h], [], [AC_MSG_FAILURE([cannot find abc.h, the ABC header!])]) + AC_MSG_CHECKING([how to link abc]) + CVC4_TRY_ABC_WITH([]) + CVC4_TRY_ABC_WITH([-lm]) + CVC4_TRY_ABC_WITH([-lm -lrt]) + CVC4_TRY_ABC_WITH([-lm -lrt -ldl]) + CVC4_TRY_ABC_WITH([-lm -lrt -lreadline -ldl]) + CVC4_TRY_ABC_WITH([-lm -lpthread]) + CVC4_TRY_ABC_WITH([-lm -lpthread -lrt]) + CVC4_TRY_ABC_WITH([-lm -lpthread -lrt -ldl]) + CVC4_TRY_ABC_WITH([-lm -lpthread -lrt -lreadline -ldl]) + dnl CVC4_TRY_ABC_WITH([-lm -rdynamic -lreadline -lpthread -lrt -ldl]) + if test -z "$ABC_LIBS"; then + AC_MSG_FAILURE([cannot link against libabc!]) + else + AC_MSG_RESULT([$ABC_LIBS]) + # make sure it works in static builds, too + if test "$enable_static_binary" = yes; then + ABC_LIBS= + AC_MSG_CHECKING([whether statically-linked abc is functional]) + CVC4_TRY_STATIC_ABC_WITH([]) + CVC4_TRY_STATIC_ABC_WITH([-lm]) + CVC4_TRY_STATIC_ABC_WITH([-lm -lrt]) + CVC4_TRY_STATIC_ABC_WITH([-lm -lrt -ldl]) + CVC4_TRY_STATIC_ABC_WITH([-lm -lrt -lreadline -ldl]) + CVC4_TRY_STATIC_ABC_WITH([-lm -lpthread]) + CVC4_TRY_STATIC_ABC_WITH([-lm -lpthread -lrt]) + CVC4_TRY_STATIC_ABC_WITH([-lm -lpthread -lrt -ldl]) + CVC4_TRY_STATIC_ABC_WITH([-lm -lpthread -lrt -lreadline -ldl]) + if test -n "$ABC_LIBS"; then + AC_MSG_RESULT([yes, it works]) + with_abc=yes + else + AC_MSG_RESULT([no]) + AC_MSG_FAILURE([abc installation appears incompatible with static-binary]) + fi + else + with_abc=yes + fi + fi + if test "$with_abc" = yes; then + have_libabc=1 + else + with_abc=no + have_libreadline=0 + ABC_LIBS= + fi + LDFLAGS="$cvc4_save_LDFLAGS" +else + AC_MSG_RESULT([no, user didn't request abc]) + with_abc=no +fi +])# CVC4_CHECK_FOR_ABC + +# CVC4_TRY_ABC_WITH(LIBS) +# ----------------------- +# Try AC_CHECK_LIB(abc) with the given linking libraries +AC_DEFUN([CVC4_TRY_ABC_WITH], [ +if test -z "$ABC_LIBS"; then + AC_LANG_PUSH([C++]) + cvc4_save_LIBS="$LIBS" + LIBS="-labc $1" + AC_LINK_IFELSE([AC_LANG_PROGRAM([extern "C" { void Abc_Start(); }], + [Abc_Start()])], + [ABC_LIBS="-labc $1"], + []) + LIBS="$cvc4_save_LIBS" + AC_LANG_POP([C++]) +fi +])# CVC4_TRY_ABC_WITH + +# CVC4_TRY_STATIC_ABC_WITH(LIBS) +# ------------------------------ +# Try AC_CHECK_LIB(abc) with the given linking libraries +AC_DEFUN([CVC4_TRY_STATIC_ABC_WITH], [ +if test -z "$ABC_LIBS"; then + AC_LANG_PUSH([C++]) + cvc4_save_LIBS="$LIBS" + cvc4_save_LDFLAGS="$LDFLAGS" + LDFLAGS="-static $LDFLAGS" + LIBS="-labc-static $1" + AC_LINK_IFELSE([AC_LANG_PROGRAM([extern "C" { void Abc_Start(); }], + [Abc_Start()])], + [ABC_LIBS="-labc-static $1"], + [ LIBS="-labc $1" + AC_LINK_IFELSE([AC_LANG_PROGRAM([extern "C" { void Abc_Start(); }], + [Abc_Start()])], + [ABC_LIBS="-labc $1"]) ]) + LIBS="$cvc4_save_LIBS" + LDFLAGS="$cvc4_save_LDFLAGS" + AC_LANG_POP([C++]) +fi +])# CVC4_TRY_STATIC_ABC_WITH |