libyices: build system: moved all config from Makefile to ./configure

What I tried to fix:
* Impossible to produces static archive libyices.a for the mingw32 host.
* So much configuration done in Makefile instead of ./configure.
* The 'make build OPTION= MODE=' is kind of unexpected and not really standard.
* As an end-user builder, it is hard to guess that my system-installed libgmp.a
  is not PIC. The build system should help me with that.
* CFLAGS and CPPFLAGS cannot be overritten by the end-user builder at 'make'
  time. See 'Preset Output Variables' in the autoconf manual.
* `smt2_commands.c`, `smt2_parser.c` and `smt2_term_stack.c` are all including
  `smt2_commands.h`, and in `smt2_commands.h` there is a definition of a type,
  so there is a clash of symbols at link time. Solution 1: use 'extern' in .h
  and definition in .c. Solution 2: typedef the enum.
* The build system should be fully parallel-proof. Note that 'make -j' is a
  thread bomb; prefer using 'make -j4' if you have 4 processors.
* Why removing libyices.a when using 'dist'? (rm -f $(distdir)/lib/libyices.a)
  libyices.a should be distributed to the end-users along with the shared lib.
* Why does libgmp.a contain more than libgmp.so? I guess it is because some
  function are needed by the tests and the tests are never dynamically linked
  to the shared libyices.so... For example, the test `test_type_matching` calls
  a function 'delete_pstore' that is not exported. This means we cannot use the
  created libyices.so! We must instead use the object files directly.

Features of the new build system:
* It is now possible to select what you want to build using --enable-static
  and --enable-shared. By default, both are built. You can speed up the build
  by disabling one of the modes, for example --disable-shared.
* Running ./configure will tell you if the libgmp.a found/given with
  --with-static-gmp or --with-pic-gmp is PIC or not.
* Libtool now handles all shared library naming with version number and symbolic
  links. on linux, .so, on mac os .dylib, on windows .a, .dll.a and .dll...
* It is now possible to choose if you want PIC-only code in the static
  library libyices.a using --with-pic.
* The ./configure now configures and the Makefile makes; moved all the
  configuration steps that were done in the Makefile.
* It is not required anymore to pass OPTION when using make. OPTION is now
  handled by passing for example --host=i686-w64-mingw32 when running
  ./configure, instead of 'make OPTION=mingw32',
* It is not required anymore to pass MODE in make. MODE is now handled by
  the argument --with-mode=release (for example) when running ./configure.
* Removed the confusing mess of build/<host>/... and configs/make.<host>.
  Build objects are simply put in build/.
* Merged the many Makefiles that were sharing a lot of code in common.
* Standardized the 'make' target and experience:
  - make build for building binaries and library (no need for OPTION or MODE)
  - make dist (non-standard) for showing the results of the build as it would
    be distributed
  - make distclean for removing any files created by ./configure
  - make lib if you only want the library
  - make install and uninstall for installing/uninstalling (DESTDIR supported)
* On Windows, we can now build a static library libyices.a.
* On Windows, shared and static libraries can be built at once. The static
  version of libyices.a can be renamed using --with-static-name.
* DESTDIR works as expected: it will reproduce the hierarchy using the prefix
  when running 'make install DESTDIR=/path'
* A nice summary of the configuration is now printed when running ./configure.
  It allows to check if libgmp.a is PIC or not, and helps to have a clear
  view of what is going to happen.
* Moved version number of Yices in configure.ac
* If the user wants to use --with-pic-gmp but his libgmp.a is not PIC, give him
  an indication of what command to run to build the with-PIC libgmp.a.
* Moved the gmaketest into configure; warn the user if 'make' is not gnu make.
* Parallel build is now fully supported (make -j)
* when using --with-static-gmp (and other similar flags), try to find gmp.h
  in . and ../include automatically, and fall back with the system-wide gmp.h
* check for gmp.h even when no --with-static-gmp-include-dir is given
* moved all csl_* functions into autoconf/m4/csl_check_libs.m4 so that they
  can be reused somewhere else
* compute dependencies only if not in release mode and at compile time
  instead of ahead of time. This saves time during compilation, because deps
  are not necessary if the .c or .h files are not changed (i.e., if the builder
  is the end-user). If the builder is a developer, then he will set
  --with-mode={debug,profile...} and this will trigger the deps to be computed.
* 'make test' compiles and runs all tests in tests/unit
* 'make test_api12' will compile and run the test tests/unit/test_api12.c
* removed version_*.c file as it is rebuilt at make time
* gperf is now only necessary when changing the tokens.txt or keywords.txt files,
  the end-user builder does not have to have gperf installed.

Side notes:
* CPPFLAGS, CFLAGS, LDFLAGS and any other makefile variable can be overwritten
  using 'make LDFLAGS=...' (was already the case with the previous version of the
  build system)

Known issues:
* on Mac OS X, linking executables agains non-PIC libgmp.a will throw the
  following warning:
  ld: warning: PIE disabled. Absolute addressing (perhaps -mdynamic-no-pic)
  not allowed in code signed PIE, but used in ___gmpn_mul_1 from libgmp.a(mul_1.o).
  To fix this warning, don't compile with -mdynamic-no-pic or link with -Wl,-no_pie

Todo:
* produce libyices.def on Windows
* make sure the test on libgmp-10.dll is future-proof (remove the '-10')
* fix the 'echo summary'
* I did not test the checks made configure.ac on mcsat and libpoly; we should
  do the same tests as done on libgmp.a (for checking that it is PIC) and
  add a helping message at the end of configure.ac.
* For the tests, I read that two kind of tests were compiled:
  - 'tests' where the tests are linked to the non-PIC libgmp.a and static libgmp.a
  - 'tests-static' where the tests are linked to the PIC libgmp.a and shared
    GMP library.
  I changed the second one: it links to the shared version of libyices and shared
  version of GMP. But building the with-PIC libyices.a would be really easy
  (and it is still possible using the flag --with-pic).
* 'make dist' is not a staging area (for now) for 'make install'. They both
  install from built objects.
* it is not possible to compile the tests against the shared library
  because many symbols which are used in the tests are not exported ('export'
  in the C code). They exist if we do 'nm' but they are just not usable.

* pstore issue:

The visibility is T (visible) in static mode and t (hidden) in shared mode. This
is because 'abstract_values.c' has not been 'exported' (=added in `yices_api.c`).
Here is an example of the difference (functions from )
```
# nm build/lib/libyices.a | grep pstore
0000000000000090 T _delete_pstore
0000000000000000 T _init_pstore
# nm build/lib/.libs/libyices.2.dylib | grep pstore
0000000000037e10 t _delete_pstore
0000000000037d80 t _init_pstore
```

I tweaked the ltmain.sh to be able to pass different CPPFLAGS for the compilation
of static and shared objects by the `%.o: %.c` rule. CPPFLAGS must be different
because of Windows dlls: `-DNOYICES_DLL -D__GMP_LIBGMP_DLL=0` for example.

``` diff
diff --git a/ext/yices/autoconf/ltmain.sh b/ext/yices/autoconf/ltmain.sh
index bf5d83b..7b7dd3a 100644
--- a/ext/yices/autoconf/ltmain.sh
+++ b/ext/yices/autoconf/ltmain.sh
@@ -3500,10 +3500,10 @@ compiler."
       fbsd_hideous_sh_bug=$base_compile

       if test no != "$pic_mode"; then
-	command="$base_compile $qsrcfile $pic_flag"
+	command="$base_compile $LT_SHARED_CFLAGS $qsrcfile $pic_flag"
       else
 	# Don't build PIC code
-	command="$base_compile $qsrcfile"
+	command="$base_compile $LT_SHARED_CFLAGS $qsrcfile"
       fi

       func_mkdir_p "$xdir$objdir"
@@ -3552,9 +3552,9 @@ compiler."
     if test yes = "$build_old_libs"; then
       if test yes != "$pic_mode"; then
 	# Don't build PIC code
-	command="$base_compile $qsrcfile$pie_flag"
+	command="$base_compile $LT_STATIC_CFLAGS $qsrcfile$pie_flag"
       else
-	command="$base_compile $qsrcfile $pic_flag"
+	command="$base_compile $LT_STATIC_CFLAGS $qsrcfile $pic_flag"
       fi
       if test yes = "$compiler_c_o"; then
 	func_append command " -o $obj"
```

Author: maelvls

ext/yices/Makefile

@@ -0,0 +1,19 @@
+# generated automatically by aclocal 1.15 -*- Autoconf -*-
+
+# Copyright (C) 1996-2014 Free Software Foundation, Inc.
+
+# This file is free software; the Free Software Foundation
+# gives unlimited permission to copy and/or distribute it,
+# with or without modifications, as long as this notice is preserved.
+
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY, to the extent permitted by law; without
+# even the implied warranty of MERCHANTABILITY or FITNESS FOR A
+# PARTICULAR PURPOSE.
+
+m4_ifndef([AC_CONFIG_MACRO_DIRS], [m4_defun([_AM_CONFIG_MACRO_DIRS], [])m4_defun([AC_CONFIG_MACRO_DIRS], [_AM_CONFIG_MACRO_DIRS($@)])])
+m4_include([autoconf/m4/libtool.m4])
+m4_include([autoconf/m4/ltoptions.m4])
+m4_include([autoconf/m4/ltsugar.m4])
+m4_include([autoconf/m4/ltversion.m4])
+m4_include([autoconf/m4/lt~obsolete.m4])