libyices: added option --without-gmp-embedded

This option will disable the partial linking that allows to embed
GMP into libyices.a (only with --enable-static).

For example, on Arch linux, the partial linking command

    ld -r -lgmp *.o -o libyices.o

would fail even if libgmp.so is correclty installed. It seems that 'ld -r'
would only work with a static libgmp.a (but the arch linux repo only installs
the shared gmp library).

Why this `ld -r`? This command is the only way I found to compile a
static libyices.a from either a shared or a static libgmp and produce
a gmp-depend-free libyices.a.

Two solutions:

1. Drop the necessity for building a libyices.a free of gmp dependency.
   In this case, I could remove the `ld -r`.
   It would then create a libyices.a that depends on libgmp.a/so.
2. Separate the gmp-dependency-free libyices.a from the normal
   gmp-dependent libyices.a. For example, I could use the option
   `--without-gmp-embedded`

So I did the solution (2).

ext/yices/Makefile

@@ -500,33 +500,42 @@ ifeq ($(enable_shared),yes)
 lib: $(builddir)/lib/libyices.la
 endif
 # Table of possibilities:
-# 1) static library
+# 1) static library with gmp embedded (= partially linked)
 #   a) if libgmp.a has been found, create a libyices.a with gmp statically
 #      linked. This uses partial linking offered by 'ld -r'.
 #      Note: I think PIC should be disabled on libgmp.a for embeding it.
 #   b) if libgmp.a has not been found, default to -lgmp. Most of the time,
 #      this means that the gmp library will be dynamically linked.
+# 1b) static library with gmp not embedded (with --without-gmp-embedded)
+#   a) and b) are the same except that 'ld -r' is not used.
 # 2) shared library
 #   a) if libgmp.a has been found and contains PIC (position-independant code),
 #      create a shared library that embeds the gmp library statically.
 #   b) if libgmp.a has not been found, default to using -lgmp which means that
 #      libyices.so (or .dylib or .dll) will also depend on the GMP shared library.
+
 #
-# Static library.
+# Static library with and without GMP embedded.
 #
 # Precondition: STATIC_GMP and -lgmp most not be set simultanously. This
 # precondition is enforced in configure.ac.
 $(builddir)/lib/$(libyices_a): $(base_obj)
 	$(MKDIR_P) $(dir $@)
+ifeq ($(GMP_EMBEDDED),yes)
+#   1) static library with gmp embedded (= partially linked)
 	$(LD) -r -o $(builddir)/obj/libyices.o $(^:%.lo=%.o) $(LDFLAGS) $(STATIC_GMP) $(STATIC_LIBS) $(LIBS)
 	$(AR) cru $@ $(builddir)/obj/libyices.o
+else
+#   1b) static library with gmp not embedded (with --without-gmp-embedded)
+	$(LIBTOOL) $(LTFLAGS) --mode=link $(CC) -static -o $@ $^ $(STATIC_LIBS) $(LIBS)
+endif
 # NOTE: We use the variable libyices_a because on Windows, static and shared
 # both produce libyices.a. In this case, set libyices_a to something different
 # than libyices.a from the shared version.
 # NOTE: we cannot use libtool --mode=link instead of ld -r + ar cru because:
-# 1) for partially linking with 'ld -r', libtool --mode=link discards the arg
+# i) for partially linking with 'ld -r', libtool --mode=link discards the arg
 #    'libgmp.a' for some reason, even with the -Wl,libgmp.a trick.
-# 2) for archiving with 'ar cru', libtool --mode=link discards the *.o created
+# ii) for archiving with 'ar cru', libtool --mode=link discards the *.o created
 #    in the previous stage. Some answers on these linker flags stripped:
 # https://www.gnu.org/software/libtool/manual/html_node/Stripped-link-flags.html
 #
@@ -537,6 +546,7 @@ $(builddir)/lib/$(libyices_a): $(base_obj)
 # Precondition: PIC_GMP and -lgmp most not be set simultanously
 RPATH ?= $(libdir)
 $(builddir)/lib/libyices.la: $(base_obj)
+#   2) shared library
 	$(MKDIR_P) $(dir $@)
 	$(LIBTOOL) $(LTFLAGS) --mode=link $(CC) -shared -o $@ $^ -rpath $(RPATH) \
 	-version-number $(MAJOR):$(MINOR):$(PATCH_LEVEL) -no-undefined \

ext/yices/configure

@@ -655,6 +655,7 @@ PIC_GMP
 STATIC_GMP_HAS_PIC
 STATIC_GMP_INCLUDE_DIR
 STATIC_GMP
+GMP_EMBEDDED
 MCSAT_CPPFLAGS
 NO_STACK_PROTECTOR
 STATIC_CPPFLAGS
@@ -770,6 +771,7 @@ with_static_libpoly_include_dir
 with_pic_libpoly
 with_pic_libpoly_include_dir
 with_shared_gmp
+with_gmp_embedded
 with_mode
 with_static_name
 '
@@ -1440,6 +1442,12 @@ Optional Packages:
                           be searched. This option forces the use of the
                           shared version. This applies for both shared and
                           static libraries.
+  --without-gmp-embedded  (Only when --enable-static) By default, the static
+                          library libyices.a created will be partially linked
+                          (ld -r) so that the GMP library is not needed
+                          afterwards (i.e., only -lyices is needed). If you
+                          want to disable the partial linking (and thus -lgmp
+                          and -lyices will be needed), you can use this flag.
   --with-mode=MODE        The mode used during compilation/distribution. It
                           can be one of release, debug, devel, profile, gcov,
                           valgrind, purify, quantify or gperftools. (default:
@@ -12368,6 +12376,16 @@ else
 fi
 
 
+
+# Check whether --with-gmp-embedded was given.
+if test "${with_gmp_embedded+set}" = set; then :
+  withval=$with_gmp_embedded; GMP_EMBEDDED=no
+else
+  GMP_EMBEDDED=yes
+fi
+
+
+
 #
 # CHECK LIBRARIES
 # ---------------
@@ -17760,6 +17778,7 @@ For static library          $libyices_a:
   Libgmp.a path:            $STATIC_GMP
   Libgmp.a is pic:          $STATIC_GMP_HAS_PIC (non-PIC is faster for the static library)
   Use shared gmp instead of libgmp.a:  $STATIC_YICES_USES_SHARED_GMP
+  Embed gmp in libyices.a:  $GMP_EMBEDDED
 
 For shared library:
   Enable:                   $enable_shared

ext/yices/configure.ac

@@ -334,6 +334,16 @@ AC_ARG_WITH([shared-gmp],[AS_HELP_STRING([--with-shared-gmp],
       [FORCE_SHARED_GMP=yes],
       [FORCE_SHARED_GMP=no])
 
+AC_ARG_WITH([gmp-embedded],[AS_HELP_STRING([--without-gmp-embedded],
+      [(Only when --enable-static) By default, the static library libyices.a
+      created will be partially linked (ld -r) so that the GMP library is not
+      needed afterwards (i.e., only -lyices is needed). If you want to disable
+      the partial linking (and thus -lgmp and -lyices will be needed), you
+      can use this flag.])],
+      [GMP_EMBEDDED=no],
+      [GMP_EMBEDDED=yes])
+AC_SUBST(GMP_EMBEDDED)
+
 #
 # CHECK LIBRARIES
 # ---------------
@@ -854,6 +864,7 @@ For static library          $libyices_a:
   Libgmp.a path:            $STATIC_GMP
   Libgmp.a is pic:          $STATIC_GMP_HAS_PIC (non-PIC is faster for the static library)
   Use shared gmp instead of libgmp.a:  $STATIC_YICES_USES_SHARED_GMP
+  Embed gmp in libyices.a:  $GMP_EMBEDDED
 
 For shared library:
   Enable:                   $enable_shared

ext/yices/make.include.in

@@ -69,6 +69,7 @@ STATIC_GMP_LIB_DIR = @STATIC_GMP_LIB_DIR@
 STATIC_GMP_HAS_PIC = @STATIC_GMP_HAS_PIC@
 HAS_STATIC_GMP = @HAS_STATIC_GMP@
 HAS_SHARED_GMP = @HAS_SHARED_GMP@
+GMP_EMBEDDED = @GMP_EMBEDDED@
 
 libyices_a = @libyices_a@