Move LFSC checker out of the CVC repository. (#222)

LFSC now lives outside of the CVC4 repository and is not part of the CVC4 distribution
anymore. As a consequence, we

+ Add --with-lfsc and --with-lfsc-directory as configure options.
   In the case where CVC4 has not been built with integrated LFSC, all code that interacts with
   LFSC is disabled.

+ Disable proof checking if CVC4_USE_LFSC is not defined.
   Configuring the build with --check-proofs but without --with-lfsc results in an error.

+ Do not call LFSC's cleanup function (but we should in the future).
   LFSC checker segfaults during cleanup on regression testcase regress0/bv/core/bitvec7.smt.
   Disabled call to lfscc_cleanup until the problem in lfscc is fixed.

+ Disable building with LFSC for the distcheck travis build since it is not part of the distribution
   anymore. Further, make distcheck with LFSC would require to call contrib/get-lfsc-checker
   before calling make check on the temp build (the build of the unpacked distribution tar ball).

1 files changed, 85 insertions, 0 deletions

diff --git a/config/lfsc.m4 b/config/lfsc.m4
new file mode 100644
index 000000000..eabc71564
--- /dev/null
+++ b/config/lfsc.m4
@@ -0,0 +1,85 @@
+# CVC4_CHECK_FOR_LFSC
+# ------------------
+# Look for LFSC and link it in, but only if user requested.
+AC_DEFUN([CVC4_CHECK_FOR_LFSC], [
+AC_MSG_CHECKING([whether user requested LFSC support])
+
+have_liblfsc=0
+LFSC_LIBS=
+LFSC_LDFLAGS=
+
+have_liblfsc=0
+if test "$with_lfsc" = no; then
+  AC_MSG_RESULT([no, LFSC disabled by user])
+elif test -n "$with_lfsc"; then
+  AC_MSG_RESULT([yes, LFSC requested by user])
+  AC_ARG_VAR(LFSC_HOME, [path to top level of LFSC source tree])
+  AC_ARG_WITH(
+    [lfsc-dir],
+    AS_HELP_STRING(
+      [--with-lfsc-dir=PATH],
+      [path to top level of lfsc source tree]
+    ),
+    [LFSC_HOME="$withval"],
+    []
+  )
+
+  if test -z "$LFSC_HOME" -a -e "$ac_abs_confdir/lfsc-checker"; then
+    AC_MSG_CHECKING([for LFSC checker library])
+    LFSC_HOME="$ac_abs_confdir/lfsc-checker/install"
+    AC_MSG_RESULT([found LFSC checker in $LFSC_HOME])
+  fi
+  
+  if test -z "$LFSC_HOME"; then
+    AC_MSG_FAILURE([must give --with-lfsc-dir=PATH or define environment variable LFSC_HOME!])
+  fi
+
+  if ! test -d "$LFSC_HOME" || ! test -x "$LFSC_HOME/bin/lfscc" ; then
+    AC_MSG_FAILURE([either $LFSC_HOME is not a LFSC install tree or it's not yet built])
+  fi
+
+  CPPFLAGS="$CPPFLAGS -I$LFSC_HOME/include"
+
+  AC_MSG_CHECKING([how to link LFSC])
+  CVC4_TRY_LFSC_LIB
+
+  if test -z "$LFSC_LIBS"; then
+    AC_MSG_FAILURE([cannot link against liblfscc!])
+  else
+    AC_MSG_RESULT([$LFSC_LIBS])
+    have_liblfsc=1
+  fi
+
+  LFSC_LDFLAGS="-L$LFSC_HOME/lib"
+
+else
+  AC_MSG_RESULT([no, user didn't request LFSC])
+  with_lfsc=no
+fi
+
+])# CVC4_CHECK_FOR_LFSC
+
+# CVC4_TRY_LFSC_LIB
+# ------------------------------
+# Try AC_CHECK_LIB(lfsc) with the given linking libraries
+AC_DEFUN([CVC4_TRY_LFSC_LIB], [
+  AC_LANG_PUSH([C++])
+
+  cvc4_save_LIBS="$LIBS"
+  cvc4_save_LDFLAGS="$LDFLAGS"
+  cvc4_save_CPPFLAGS="$CPPFLAGS"
+
+  LDFLAGS="-L$LFSC_HOME/lib"
+  LIBS="-llfscc -lgmp"
+
+  AC_LINK_IFELSE(
+    [AC_LANG_PROGRAM([[#include <lfscc.h>]], [[lfscc_init()]])],
+    [LFSC_LIBS="-llfscc -lgmp"],
+    [LFSC_LIBS=])
+
+  LDFLAGS="$cvc4_save_LDFLAGS"
+  CPPFLAGS="$cvc4_save_CPPFLAGS"
+  LIBS="$cvc4_save_LIBS"
+
+  AC_LANG_POP([C++])
+])# CVC4_TRY_LFSC_LIB