From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 7 Jul 2011 05:31:13 +0000 (+0000)
Subject: cudd-building prefs with --with-cudd / --without-cudd
X-Git-Tag: cvc5-1.0.0~8521
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c5ffeb50b60e0aaaac0b1e64a345f048def1629f;p=cvc5.git

cudd-building prefs with --with-cudd / --without-cudd
---

diff --git a/configure.ac b/configure.ac
index f6f2f5a04..192bfcff2 100644
--- a/configure.ac
+++ b/configure.ac
@@ -684,49 +684,64 @@ AC_SEARCH_LIBS([clock_gettime], [rt],
                           [Defined to 1 if clock_gettime() is supported by the platform.])],
                [AC_LIBOBJ([clock_gettime])])
 
-AC_ARG_WITH([cudd-dir],
-  [AS_HELP_STRING([--with-cudd-dir=DIR], [path to cudd installation])],
-  [CUDD_DIR="$withval"])
-if test -z "$CUDD_DIR"; then
-  CUDD_DIR=/usr
-fi
-AC_MSG_CHECKING([for cudd includes under $CUDD_DIR])
 CUDD_CPPFLAGS=
 CUDD_LDFLAGS=
 cvc4cudd=no
-result="not found"
-for cuddinc in "$CUDD_DIR/include" "$CUDD_DIR/include/cudd" "$CUDD_DIR"; do
-  if test -r "$cuddinc/cudd.h"; then
-    dnl TODO - should do a TRY_COMPILE instead
-    CUDD_CPPFLAGS="\"-I$cuddinc\""
-    result="$cuddinc"
-    cvc4cudd=yes
-    break
+AC_MSG_CHECKING([whether user requested CUDD support])
+AC_ARG_WITH([cudd], [AS_HELP_STRING([--with-cudd], [force linking/not linking against CUDD])], [], [with_cudd=check])
+if test "$with_cudd" = no; then
+  AC_MSG_RESULT([no, CUDD disabled by user])
+else
+  if test "$with_cudd" = check; then
+    AC_MSG_RESULT([no preference by user, will auto-detect])
+  else
+    AC_MSG_RESULT([yes, CUDD enabled by user])
+  fi
+  AC_ARG_WITH([cudd-dir],
+    [AS_HELP_STRING([--with-cudd-dir=DIR], [path to cudd installation])],
+    [CUDD_DIR="$withval"])
+  if test -z "$CUDD_DIR"; then
+    CUDD_DIR=/usr
   fi
-done
-AC_MSG_RESULT([$result])
-if test $cvc4cudd = yes; then
-  AC_MSG_CHECKING([for cudd libraries under $CUDD_DIR])
-  cvc4cudd=no
+  AC_MSG_CHECKING([for cudd includes under $CUDD_DIR])
   result="not found"
-  for cuddlib in "$CUDD_DIR/lib" "$CUDD_DIR/lib/cudd" "$CUDD_DIR"; do
-    if test -r "$cuddlib/libcuddxx.la"; then
-      dnl TODO - should do a TRY_LINK instead, that has the extra benefit
-      dnl of making sure both shared & static work
-      CUDD_LDFLAGS="\"-L$cuddlib\" -lcuddxx"
-      result="$cuddlib"
+  for cuddinc in "$CUDD_DIR/include" "$CUDD_DIR/include/cudd" "$CUDD_DIR"; do
+    if test -r "$cuddinc/cudd.h"; then
+      dnl TODO - should do a TRY_COMPILE instead
+      CUDD_CPPFLAGS="\"-I$cuddinc\""
+      result="$cuddinc"
       cvc4cudd=yes
       break
     fi
   done
-  AC_MSG_RESULT([$result]);
+  AC_MSG_RESULT([$result])
   if test $cvc4cudd = yes; then
-    AC_DEFINE_UNQUOTED(CVC4_CUDD, [], [Defined if using the CU Decision Diagram package (cudd).])
+    AC_MSG_CHECKING([for cudd libraries under $CUDD_DIR])
+    cvc4cudd=no
+    result="not found"
+    for cuddlib in "$CUDD_DIR/lib" "$CUDD_DIR/lib/cudd" "$CUDD_DIR"; do
+      if test -r "$cuddlib/libcuddxx.la"; then
+        dnl TODO - should do a TRY_LINK instead, that has the extra benefit
+        dnl of making sure both shared & static work
+        CUDD_LDFLAGS="\"-L$cuddlib\" -lcuddxx"
+        result="$cuddlib"
+        cvc4cudd=yes
+        break
+      fi
+    done
+    AC_MSG_RESULT([$result]);
+    if test $cvc4cudd = yes; then
+      AC_DEFINE_UNQUOTED(CVC4_CUDD, [], [Defined if using the CU Decision Diagram package (cudd).])
+    fi
   fi
 fi
 AC_SUBST([CUDD_CPPFLAGS])
 AC_SUBST([CUDD_LDFLAGS])
 
+if test "$with_cudd" = yes -a "$cvc4cudd" = no; then
+  AC_ERROR([--with-cudd was given, but cudd not available])
+fi
+
 # Check for antlr C++ runtime (defined in config/antlr.m4)
 AC_LIB_ANTLR
 
@@ -914,6 +929,7 @@ Muzzle       : $enable_muzzle
 Unit tests   : $support_unit_tests
 gcov support : $enable_coverage
 gprof support: $enable_profiling
+CUDD         : $cvc4cudd
 Readline     : $with_readline
 TLS support  : $CVC4_TLS