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.

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\""'