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.

1 files changed, 18 insertions, 24 deletions

diff --git a/configure.ac b/configure.ac
index cfd65aef4..92a9c10ce 100644
--- a/configure.ac
+++ b/configure.ac
@@ -113,7 +113,7 @@ AC_ARG_WITH([build],
 if test -z "${with_build+set}"; then
   with_build=production
 fi
-if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_dumping+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}" -a -z "${enable_replay+set}" -a -z "${with_gmp+set}" -a -z "${with_cln+set}" -a -z "${with_glpk+set}"; then
+if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_dumping+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}" -a -z "${enable_replay+set}" -a -z "${with_gmp+set}" -a -z "${with_cln+set}" -a -z "${with_glpk+set}" -a -z "${with_abc+set}"; then
   custom_build_profile=no
 else
   custom_build_profile=yes
@@ -208,6 +208,11 @@ if test -n "${with_glpk+set}"; then
     btargs="$btargs glpk"
   fi
 fi
+if test -n "${with_abc+set}"; then
+  if test "$with_abc" = yes; then
+    btargs="$btargs abc"
+  fi
+fi
 AC_MSG_RESULT([$with_build])
 
 AM_INIT_AUTOMAKE([1.11 no-define tar-pax parallel-tests color-tests subdir-objects])
@@ -254,9 +259,6 @@ AC_ARG_WITH(
   ]
 )
 
-# [chris 8/24/2010] --with-gmp has no practical effect, since GMP is
-# the default. Could be useful if other options are added later.
-
 AC_ARG_WITH(
   [gmp],
   AS_HELP_STRING(
@@ -748,26 +750,17 @@ fi
 AM_CONDITIONAL([CVC4_USE_GLPK], [test $have_libglpk -eq 1])
 AC_SUBST([GLPK_LIBS])
 
-AC_ARG_WITH(
-  [abc],
-  AS_HELP_STRING(
-    [--with-abc],
-    [use the ABC AIG library]
-  ),
-  [case "$withval" in
-   y|ye|yes|Y|YE|YES) cvc4_use_abc=1 ;;
-   n|no|N|NO) cvc4_use_abc=0 ;;
-   esac
-  ]
-)
-
-if test $cvc4_use_abc -eq 1; then
-   # must add dl and pthread separately and before abc
-   AC_CHECK_LIB(dl, dlopen, , [AC_MSG_ERROR([dl not found])], [])
-   AC_CHECK_LIB(pthread, pthread_create, , [AC_MSG_ERROR([pthread not found])], [])
-   AC_CHECK_LIB(abc, Abc_Start, , [AC_MSG_ERROR([abc not found])], [-lm -ldl -rdynamic -lreadline -ltermcap -lpthread -lrt -ldl])
-   AC_DEFINE_UNQUOTED(CVC4_USE_ABC, [], [Defined if linked against the ABC AIG library.]) 
+# Build with libabc (defined in config/abc.m4)
+AC_ARG_WITH([abc],
+  [AS_HELP_STRING([--with-abc],
+     [use the ABC AIG library])], [], [with_abc=])
+CVC4_CHECK_FOR_ABC
+if test $have_libabc -eq 1; then
+  CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_ABC"
 fi
+AM_CONDITIONAL([CVC4_USE_ABC], [test $have_libabc -eq 1])
+AC_SUBST([ABC_LDFLAGS])
+AC_SUBST([ABC_LIBS])
 
 # Check to see if this version/architecture of GNU C++ explicitly
 # instantiates __gnu_cxx::hash<uint64_t> or not.  Some do, some don't.
@@ -1238,7 +1231,7 @@ AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full releas
 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions"
-LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS -ldl"
+LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
 
 # visibility flag not supported for Windows builds
 # also increase default stack size for Windows binaries
@@ -1455,6 +1448,7 @@ Portfolio    : $with_portfolio
 
 MP library   : $mplibrary
 GLPK         : $with_glpk
+ABC          : $with_abc
 Readline     : $with_readline
 
 CPPFLAGS     : $CPPFLAGS