diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-10 17:52:26 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-11 16:18:23 -0400 |
commit | 6f1454d2082d4e8783c3b35c30144ff557b99444 (patch) | |
tree | 3339ec7eb47f5aa272fbe1511e1036e9790d0507 /config | |
parent | 3c2458b633501345fba2679c611ce9e5c7a9f538 (diff) |
Some clean-up, post bv-merge.
Add abc to build id and fix static building.
Add abc to --show-config output and Configuration class API.
Add ability to select abc source path.
Fix arch_flags for abc.
Diffstat (limited to 'config')
-rw-r--r-- | config/abc.m4 | 135 | ||||
-rwxr-xr-x | config/build-type | 4 | ||||
-rw-r--r-- | config/cvc4.m4 | 6 |
3 files changed, 143 insertions, 2 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 diff --git a/config/build-type b/config/build-type index 1ef9191f7..ae4e292f4 100755 --- a/config/build-type +++ b/config/build-type @@ -33,7 +33,7 @@ # Also you can specify "cln" or "gmp". If "gmp", the build dir # contains the string "gmp". (gmp is considered the default.) # -# Also for glpk. +# Also for glpk and abc. # if [ $# -eq 0 ]; then @@ -55,7 +55,7 @@ while [ $# -gt 0 ]; do done build_type_suffix= -for arg in cln glpk staticbinary optimized proof debugsymbols statistics replay assertions tracing muzzle coverage profiling; do +for arg in cln glpk abc staticbinary optimized proof debugsymbols statistics replay assertions tracing muzzle coverage profiling; do if eval [ -n '"${'$arg'+set}"' ]; then if eval [ '"${'$arg'}"' -eq 0 ]; then build_type_suffix=$build_type_suffix-no$arg diff --git a/config/cvc4.m4 b/config/cvc4.m4 index 40e2054e6..ea202e94f 100644 --- a/config/cvc4.m4 +++ b/config/cvc4.m4 @@ -79,6 +79,12 @@ handle_option() { 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 + if expr "$ac_option" : '.*-noabc' >/dev/null || expr "$ac_option" : '.*-noabc-' >/dev/null; then + eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--without-abc\""' + fi + if expr "$ac_option" : '.*-abc' >/dev/null || expr "$ac_option" : '.*-abc-' >/dev/null; then + eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--with-abc\""' + 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\""' |