1dnl======================================================================== 2dnl The Yices SMT Solver. Copyright 2017 SRI International. 3dnl 4dnl Yices is free software: you can redistribute it and/or modify 5dnl it under the terms of the GNU General Public License as published by 6dnl the Free Software Foundation, either version 3 of the License, or 7dnl (at your option) any later version. 8dnl 9dnl Yices is distributed in the hope that it will be useful, 10dnl but WITHOUT ANY WARRANTY; without even the implied warranty of 11dnl MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 12dnl GNU General Public License for more details. 13dnl 14dnl You should have received a copy of the GNU General Public License 15dnl along with Yices. If not, see <http://www.gnu.org/licenses/>. 16dnl 17dnl======================================================================== 18 19dnl 20dnl Configure for Yices 21dnl 22dnl This builds a platform-dependent configuration 23dnl file stored in configs/Makefile.$ARCH 24dnl 25 26AC_PREREQ(2.60) 27AC_INIT([Yices],[2]) 28 29dnl 30dnl Our public repository (used if ./configure fails) 31dnl 32repo_url="https://github.com/SRI-CSL/yices2" 33 34dnl 35dnl Save CFLAGS (AC_PROC_CC modifies it) 36dnl 37saved_cflags=$CFLAGS 38 39 40dnl 41dnl Build platform 42dnl -------------- 43dnl 44dnl Changed this (07/12/2012) to allow cross-compilation (patch from 45dnl Dave Vitek, from Grammatch). 46dnl build = platform on which we run the build 47dnl host = platform for which we build 48dnl 49dnl Also changed AC_CHECK_PROG(LD, ..) to AC_CHECK_TOOL(LD, ...) etc. 50dnl 51AC_CANONICAL_BUILD 52 53AC_SUBST(ARCH) 54AC_SUBST(POSIXOS) 55POSIXOS=$host_os 56ARCH=$host 57 58if test "$POSIXOS" = unknown ; then 59 AC_MSG_ERROR([Unknown operating system]) 60fi 61 62 63dnl 64dnl define SET_MAKE if needed 65dnl ------------------------- 66dnl 67AC_PROG_MAKE_SET 68 69 70dnl 71dnl Tools for building Yices 72dnl ------------------------ 73dnl 74AC_PROG_SED 75AC_PROG_LN_S 76AC_PROG_MKDIR_P 77AC_PROG_INSTALL 78 79AC_PROG_CC_C99 80 81AC_PROG_RANLIB 82AC_PROG_EGREP 83AC_CHECK_TOOL(LD,ld,ld) 84AC_CHECK_TOOL(AR,ar,ar) 85AC_CHECK_TOOL(STRIP,strip,strip) 86 87# 88# gperf generates source files. Better 89# to keep AC_CHECK_PROG rather than AC_CHECK_TOOL 90# 91AC_CHECK_PROG(GPERF,gperf,gperf,nogperf) 92 93 94 95# 96# CHECK GPERF 97# ----------- 98# the src/Makefile uses command-line options that appeared in version 3.0 99# of gperf 100# 101if test "$GPERF" = nogperf; then 102 AC_MSG_ERROR([*** gperf not found. gperf version 3.0 or higher is required to build Yices ***]) 103else 104 AC_MSG_CHECKING([gperf version]) 105 gperfversion=`"$GPERF" --version 2>&1 | awk '/^GNU/ { print $3 }'` 106 case $gperfversion in 107 0.* | 1.* | 2.* ) 108 AC_MSG_RESULT([${gperfversion}]) 109 AC_MSG_ERROR([*** found $GPERF version $gperfversion but version 3.0 or higher is required ***]) 110 ;; 111 3.*) 112 AC_MSG_RESULT([${gperfversion}]) 113 ;; 114 *) 115 AC_MSG_RESULT([${gperfversion}]) 116 AC_MSG_WARN([*** Unexpected $GPERF output. Cannot determine version. Continuing anyway ***]);; 117 esac 118fi 119 120 121 122dnl 123dnl Check whether the C compiler accepts the flag -fno-stack-protector 124dnl ------------------------------------------------------------------- 125dnl 126dnl Several Linux distributions (also Darwin) come with GCC that has 127dnl -fstack-protector enabled by default. This may cause problems at 128dnl link time on the user machine (if the user doesn't have the right 129dnl runtime libraries). The symptom is: 130dnl undefined reference to '__stack_chk_fail' 131dnl To avoid this, we try to give flag -fno-stack-protector when 132dnl compiling Yices in release mode. However, this flag is not supported 133dnl by older versions of GCC (e.g., gcc-4.0.x don't seem to have it) 134dnl 135dnl The following test attempts to determine whether the C compiler 136dnl supports -fno-stack-protector. If it does, we set variable 137dnl NO_STACK_PROTECTOR to -fno-stack-protector. Otherwise, we leave 138dnl NO_STACK_PROTECTOR empty 139dnl 140NO_STACK_PROTECTOR="" 141AC_MSG_CHECKING([whether $CC accepts option -fno-stack-protector]) 142if $CC -fno-stack-protector -c -xc - -o /dev/null < /dev/null > /dev/null 2>&1 ; then 143 NO_STACK_PROTECTOR="-fno-stack-protector" 144 AC_MSG_RESULT(yes) 145else 146 AC_MSG_RESULT(no) 147fi; 148AC_SUBST(NO_STACK_PROTECTOR) 149 150 151dnl 152dnl Check for endianness 153dnl -------------------- 154dnl 155WORDS_BIGENDIAN="" 156AC_C_BIGENDIAN([WORDS_BIGENDIAN=yes],[WORDS_BIGENDIAN=no],[WORDS_BIGENDIAN=yes]) 157AC_SUBST(WORDS_BIGENDIAN) 158 159dnl 160dnl CHECK_THREAD_LOCAL 161dnl ------------------ 162dnl check whether we can declare variables with the __thread 163dnl attribute. If not we assume the platform doesn't support 164dnl thread-local storage. 165dnl 166dnl result: $has_tls is "yes" if the __thread attribute is supported 167dnl $has_tls is "no" otherwise 168dnl 169AC_DEFUN([CSL_CHECK_THREAD_LOCAL], 170[ 171save_cppflags=$CPPFLAGS 172save_libs=$LIBS 173AC_MSG_CHECKING([for thread-local storage support]) 174AC_RUN_IFELSE( 175[AC_LANG_PROGRAM([[__thread int test;]], 176 [[]])], 177has_tls=yes,has_tls=no,has_tls=no) 178AC_MSG_RESULT([$has_tls]) 179# 180# restore CPPFLAGS and LIBS 181# 182CPPFLAGS=$save_cppflags 183LIBS=$save_libs 184]) 185 186 187 188dnl 189dnl GMP Libraries 190dnl ------------- 191dnl 192dnl We need as many as three different versions of GMP: 193dnl 194dnl To build static executables and libraries, we link with the 195dnl default libgmp.a (usually /usr/local/lib/libgmp.a). 196dnl 197dnl To construct the yices library (libyices.so) with GMP included, 198dnl we need a version of libgmp.a that's position independent code. 199dnl On systems where -fPIC is not the default, we must build 200dnl a specific version of GMP from the source, using option CFLAG=-fPIC. 201dnl 202dnl To build dynamic executables and libraries without GMP included, 203dnl we need a a dynamic version of the GMP library (e.g., /usr/local/lib/libgmp.so). 204dnl 205dnl On mingw and cygwin, dynamic and static GMP libraries do not coexist well. 206dnl They must be installed in different locations and use different gmp.h files. 207dnl 208dnl To deal with this, the build Makefiles use the following variables: 209dnl STATIC_GMP = full path to a static version of gmp (e.g., /usr/local/lib/libgmp.a) 210dnl STATIC_GMP_INCLUDE_DIR = directory where a 'gmp.h' compatible with STATIC_GMP is located 211dnl (or empty if 'gmp.h' is in a standard place) 212dnl 213dnl PIC_GMP = full path to a libgmp.a that's PIC code 214dnl PIC_GMP_INCLUDE_DIR = directory where a 'gmp.h' header file compatible with PIC_GMP 215dnl is located 216dnl 217dnl By default, the configure script searches for a usable STATIC_GMP in default 218dnl locations and sets PIC_GMP to the same thing as STATIC_GMP. 219dnl 220dnl If the configure script does not find STATIC_GMP or if the defaults are 221dnl incorrect, the right libraries can be given as options to ./configure: 222dnl 223dnl --with-static-gmp=full-path-to-libgmp.a for static linking 224dnl --with-static-gmp-include-dir=corresponding directory for gmp.h 225dnl 226dnl --with-pic-gmp=full-path-to-relocatable-libgmp.a 227dnl --with-pic-gmp-include-dir=directory where the corresponding gmp.h resides 228dnl 229static_libgmp="" 230AC_ARG_WITH([static-gmp], 231 [AS_HELP_STRING([--with-static-gmp=<path>],[Full path to a static GMP library (e.g., libgmp.a)])], 232 [if test "x$withval" = x; then 233 AC_MSG_WARN([--with-static-gmp was used but no path was given. Using defaults]) 234 else 235 static_libgmp=$withval 236 fi 237 ], 238 []) 239 240static_includegmp="" 241AC_ARG_WITH([static-gmp-include-dir], 242 [AS_HELP_STRING([--with-static-gmp-include-dir=<directory>], 243 [Directory of include file "gmp.h" compatible with static GMP library])], 244 [if test "x$withval" = x; then 245 AC_MSG_WARN([--with-static-gmp-include-dir was used but no directory was given. Using defaults]) 246 else 247 static_includegmp=$withval 248 fi 249 ], 250 []) 251 252 253pic_libgmp="" 254AC_ARG_WITH([pic-gmp], 255 [AS_HELP_STRING([--with-pic-gmp=<path>],[Full path to a relocatable GMP library (e.g., libgmp.a)])], 256 [if test "x$withval" = x; then 257 AC_MSG_WARN([--with-pic-gmp was used but no path was given. Using defaults]) 258 else 259 pic_libgmp=$withval 260 fi 261 ], 262 []) 263 264pic_includegmp="" 265AC_ARG_WITH([pic-gmp-include-dir], 266 [AS_HELP_STRING([--with-pic-gmp-include-dir=<directory>], 267 [Directory of include file "gmp.h" compatible with relocatable GMP library])], 268 [if test "x$withval" = x; then 269 AC_MSG_WARN([--with-pic-gmp-include-dir was used but no directory was given. Using defaults]) 270 else 271 pic_includegmp=$withval 272 fi 273 ], 274 []) 275 276 277dnl 278dnl Options for mcsat and the libpoly library 279dnl ----------------------------------------- 280dnl --enable-mcsat: add support for MCSAT 281dnl 282dnl If mcsat is emabled, we provide options to specify 283dnl the static libraries, using the same conventions as for GMP. 284dnl 285use_mcsat="no" 286AC_ARG_ENABLE([mcsat], 287 [AS_HELP_STRING([--enable-mcsat],[Enable support for MCSAT. This requires the LibPoly library and the CUDD library.])], 288 [if test "$enableval" = yes ; then 289 use_mcsat="yes" 290 AC_MSG_NOTICE([Enabling support for MCSAT]) 291 fi], 292 []) 293 294 295static_lpoly="" 296AC_ARG_WITH([static-libpoly], 297 [AS_HELP_STRING([--with-static-libpoly=<path>],[Full path to libpoly.a])], 298 [if test $use_mcsat = "no" ; then 299 AC_MSG_WARN([Ignoring option --with-static-libpoly since MCSAT support is disabled]) 300 else 301 if test "x$withval" = x; then 302 AC_MSG_WARN([--with-static-poly was used but no path was given. Using defaults]) 303 else 304 static_lpoly=$withval 305 fi 306 fi 307 ], 308 []) 309 310static_includelpoly="" 311AC_ARG_WITH([static-libpoly-include-dir], 312 [AS_HELP_STRING([--with-static-libpoly-include-dir=<directory>], 313 [Path to include files compatible with libpoly.a (e.g., /usr/local/include)])], 314 [if test $use_mcsat = "no" ; then 315 AC_MSG_WARN([Ignoring option --with-static-libpoly-include-dir since MCSAT support is disabled]) 316 else 317 if test "x$withval" = x; then 318 AC_MSG_WARN([--with-static-libpoly-include-dir was used but no directory was given. Using defaults]) 319 else 320 static_includelpoly=$withval 321 fi 322 fi 323 ], 324 []) 325 326 327pic_lpoly="" 328AC_ARG_WITH([pic-libpoly], 329 [AS_HELP_STRING([--with-pic-libpoly=<path>],[Full path to a relocatable libpoly.a])], 330 [if test $use_mcsat = "no" ; then 331 AC_MSG_WARN([Ignoring option --with-pic-libpoly since MCSAT support is disabled]) 332 else 333 if test "x$withval" = x; then 334 AC_MSG_WARN([--with-pic-libpoly was used but no path was given. Using defaults]) 335 else 336 pic_lpoly=$withval 337 fi 338 fi 339 ], 340 []) 341 342pic_includelpoly="" 343AC_ARG_WITH([pic-libpoly-include-dir], 344 [AS_HELP_STRING([--with-pic-libpoly-include-dir=<directory>], 345 [Path to include files compatible with the relocatable libpoly.a])], 346 [if test $use_mcsat = "no" ; then 347 AC_MSG_WARN([Ignoring option --with-pic-libpoly-include-dir since MCSAT support is disabled]) 348 else 349 if test "x$withval" = x; then 350 AC_MSG_WARN([--with-pic-libpoly-include-dir was used but no directory was given. Using defaults]) 351 else 352 pic_includelpoly=$withval 353 fi 354 fi 355 ], 356 []) 357 358 359 360dnl 361dnl Option to enable thread-safety 362dnl ------------------------------ 363dnl --enable-thread-safety 364dnl 365dnl The default is don't build thread safe. If the --enable-thread-safety 366dnl is given, we check whether thread-local storage is supported. 367dnl 368thread_safe="no" 369AC_ARG_ENABLE([thread-safety], 370 [AS_HELP_STRING([--enable-thread-safety],[Build in thread-safe mode.])], 371 [if test "$enableval" = yes ; then 372 thread_safe="yes" 373 AC_MSG_NOTICE([Enabling thread-safe build]) 374 fi], 375 []) 376 377 378 379 380dnl 381dnl CSL_COLLECT_LIBRARY_PATHS 382dnl ------------------------- 383dnl Sets variable search_libs to a default list of directories in which to search for libraries. 384dnl The list include /usr/local/lib /usr/lib /lib + directories found by 385dnl ld --verbose + LD_LIBRARY_PATH + DYLD_LIBRARY_PATH + LDFLAGS if non-empty. 386dnl 387AC_DEFUN([CSL_COLLECT_LIBRARY_PATHS], 388[ 389# 390# Some (non-GNU) versions of ld do not recognize --verbose 391# 392# Also, some versions of GNU ld have things like SEARCH_DIR(=/usr/local/lib32) 393# and the '=' causes us trouble. 394# 395# man ld says 396# If searchdir begins with "=", then the "=" will be replaced by the 397# sysroot prefix, a path specified when the linker is configured. 398# 399# We ignore this here. If the search dir starts with =, we remove = 400# 401# NOTE: this sed command uses \? which, is a GNU extension. 402# 403if ld --verbose > /dev/null 2>&1; then 404 base_libs=`ld --verbose | grep SEARCH_DIR | sed -e 's,SEARCH_DIR(\"\?=\?,,g' -e 's,\"\?);,,g' | sed -e 's,SEARCH_DIR(\",,g' -e 's,\");,,g' ` 405else 406 base_libs="" 407fi 408# 409# Add LD_LIBRARY_PATH or DYLD_LIBRARY_PATH if they are defined 410# 411if test "x$LD_LIBRARY_PATH" != x; then 412 aux_libs=`echo $LD_LIBRARY_PATH | sed -e 's,:, ,g'` 413else 414 if test "x$DYLD_LIBRARY_PATH" != x; then 415 aux_libs=`echo $DYLD_LIBRARY_PATH | sed -e 's,:, ,g'` 416 else 417 aux_libs="" 418 fi 419fi 420search_libs="$aux_libs $base_libs /usr/local/lib /usr/lib /lib" 421# 422# Add other libraries from $LDFLAGS 423# 424prev_l_opt=false 425for ld_arg in $LDFLAGS; do 426 if test "$prev_l_opt" = "true"; then 427 search_libs=" $ld_arg $search_libs" 428 else 429 if test "$ld_arg" = "-L"; then 430 prev_l_opt=true 431 else 432 libprefix=`echo $ld_arg | cut -c -2` 433 body=`echo $ld_arg | cut -c 3-` 434 if test "$libprefix" = "-L"; then 435 search_libs=" $body $search_libs" 436 else 437 libprefix=`echo $ld_arg | cut -c -15` 438 body=`echo $ld_arg | cut -c 16-` 439 if test "$libprefix" = "--library-path"; then 440 search_libs=" $body $search_libs" 441 fi 442 fi 443 fi 444 fi 445done 446]) 447 448 449dnl 450dnl CSL_CHECK_LIB_PATH(path,option) 451dnl ---------------------------------- 452dnl path should be the full path to a static library. 453dnl this checks whether the given file exists. Prints an 454dnl error and exit otherwise. 455dnl 456dnl If the test succeeds, set variable testlib to path. 457dnl 458AC_DEFUN([CSL_CHECK_LIB_PATH], 459[ 460testlib="" 461AC_MSG_CHECKING([for $1]) 462if test -f $1; then 463 AC_MSG_RESULT(found) 464 testlib=$1 465else 466 AC_MSG_RESULT(no) 467 AC_MSG_ERROR([*** $1 was not found: Check option $2 ***]) 468fi 469]) 470 471 472dnl 473dnl CSL_CHECK_HEADER(header,includedir,option) 474dnl ---------------------------------------- 475dnl check whether a header file like 'gmp.h' is present in includedir 476dnl set variable $testincludedir to includedir if so 477dnl exit otherwise. 478dnl if includedir is empty, just set testincludedir to empty string too 479dnl 480dnl option must be the '--with-...-include-dir from which includedir was given 481dnl it's used to print the error message. 482dnl 483AC_DEFUN([CSL_CHECK_HEADER], 484[ 485testincludedir="" 486if test "x$2" != x; then 487 if test -d "$2" ; then 488 if test -f "$2/$1" ; then 489 testincludedir="$2" 490 else 491 AC_MSG_ERROR([*** $1 not found in $2. Check option $3 ***]) 492 fi 493 else 494 AC_MSG_ERROR([*** directory $2 not found. Check option $3 ***]) 495 fi 496fi 497]) 498 499 500 501dnl 502dnl CSL_CHECK_GMP(libgmp,includedir) 503dnl -------------------------------- 504dnl attempt to compile a test program that calls a gmp function 505dnl set run_ok to "yes" if the program executes and exits with 0 506dnl set run_ok to "no" otherwise 507dnl 508dnl libgmp must be the full-path name to the library to test 509dnl includedir must be the directory where the corresponding 'gmp.h' 510dnl can be found 511dnl 512AC_DEFUN([CSL_CHECK_GMP], 513[ 514save_cppflags=$CPPFLAGS 515save_libs=$LIBS 516# 517# Add -I option to CPPFLAGS (it must be first) 518# Add $1 to LIBS 519# 520if test "x$2" != x ; then 521 CPPFLAGS="-I$2 $CPPFLAGS" 522fi 523LIBS="$1 -lm" 524AC_MSG_CHECKING([whether $1 is usable]) 525# 526# Test program: check whether the GMP version is recent enough 527# 528AC_RUN_IFELSE( 529[AC_LANG_PROGRAM([[ 530#include <gmp.h> 531 532mpz_t tst; 533]], 534[[ 535mpz_init(tst); 536mpz_clear(tst); 537if ((__GNU_MP_VERSION < 4) || 538 ((__GNU_MP_VERSION == 4) && (__GNU_MP_VERSION_MINOR < 1))) { 539 return 1; 540 } 541]]) 542 543],run_ok=yes,run_ok=no,run_ok=no) 544AC_MSG_RESULT([$run_ok]) 545# 546# restore CPPFLAGS and LIBS 547# 548CPPFLAGS=$save_cppflags 549LIBS=$save_libs 550]) 551 552 553 554dnl 555dnl CSL_CHECK_STATIC_GMP(libgmp,includedir) 556dnl ------------------------------------ 557dnl try to find the full path to a usable libgmp.a, use $1 if not empty. 558dnl if $2 is not empty, then the checks are compiled with -I$2 559dnl if everything works, then set STATIC_GMP to the fullpath for libgmp.a 560dnl and set STATIC_GMP_INCLUDE_DIR to $2 561dnl 562dnl 563AC_DEFUN([CSL_CHECK_STATIC_GMP], 564[ 565AC_MSG_NOTICE([Trying to find a usable libgmp.a]) 566CSL_CHECK_HEADER([gmp.h],$2,--with-static-gmp-include-dir) 567# 568# if $1 is not given, search for it in library paths 569# 570if test -z "$1"; then 571 CSL_COLLECT_LIBRARY_PATHS 572 # 573 # now $search_libs contains all the directories to search 574 # 575 AC_MSG_NOTICE([Searching in $search_libs]) 576 for ldir in $search_libs; do 577 AC_MSG_CHECKING([for libgmp.a in $ldir]) 578 if test -f $ldir/libgmp.a; then 579 AC_MSG_RESULT(found) 580 testlib=$ldir/libgmp.a 581 CSL_CHECK_GMP($testlib,$testincludedir) 582 if test $run_ok = yes; then 583 STATIC_GMP=$testlib 584 STATIC_GMP_INCLUDE_DIR=$testincludedir 585 break 586 fi 587 else 588 AC_MSG_RESULT(no) 589 fi 590 done 591# 592# 593else 594 # 595 # User gave option --with-static-gmp=xxx 596 # Check whether the specified xxx actually works 597 # 598 CSL_CHECK_LIB_PATH($1,--with-static-gmp) 599 CSL_CHECK_GMP($testlib,$testincludedir) 600 if test $run_ok = yes; then 601 STATIC_GMP=$testlib 602 STATIC_GMP_INCLUDE_DIR=$testincludedir 603 else 604 AC_MSG_ERROR([*** $1 does not appear to be usable: check option --with-static-gmp ***]) 605 fi 606fi 607 608if test "x$STATIC_GMP" = x; then 609 AC_MSG_WARN([*** No usable libgmp.a library was found ***]) 610fi 611]) 612 613 614 615dnl 616dnl CSL_CHECK_LIBPOLY(libpoly,includedir,libs) 617dnl ------------------------------------------ 618dnl attempt to compile and run a test program that calls libpoly 619dnl set run_ok to "yes" if the program executes and exits with 0. 620dnl set run_ok to "no" otherwise. 621dnl 622dnl libpoly must be the full-path name to the library to test. 623dnl includedir must be a directory with 'poly/polyn.h' can be found. 624dnl libs may contain GMP libraries to use 625dnl 626AC_DEFUN([CSL_CHECK_LIBPOLY], 627[ 628save_cppflags=$CPPFLAGS 629save_libs=$LIBS 630# 631# Add the -I option to CPPFLAGS 632# Add $1 then $3 to LIBS 633# 634if test "x$2" != x ; then 635 CPPFLAGS="-I$2 $CPPFLAGS" 636fi 637LIBS="$1" 638if test "x$3" != x ; then 639 LIBS="$LIBS $3" 640fi 641AC_MSG_CHECKING([whether $1 is usable]) 642# 643# Test program 644# 645AC_RUN_IFELSE( 646[AC_LANG_PROGRAM([[ 647#include <poly/variable_db.h> 648#include <poly/variable_order.h> 649#include <poly/polynomial_context.h> 650#include <poly/polynomial.h> 651]], 652[[ 653lp_variable_db_t* var_db = lp_variable_db_new(); 654lp_variable_order_t* var_order = lp_variable_order_new(); 655lp_polynomial_context_t* ctx = lp_polynomial_context_new(lp_Z, var_db, var_order); 656lp_polynomial_t* p = lp_polynomial_new(ctx); 657lp_polynomial_delete(p); 658lp_polynomial_context_detach(ctx); 659lp_variable_order_detach(var_order); 660lp_variable_db_detach(var_db); 661]]) 662 663],run_ok=yes,run_ok=no,run_ok=no) 664AC_MSG_RESULT([$run_ok]) 665# 666# restore CPPFLAGS and LIBS 667# 668CPPFLAGS=$save_cppflags 669LIBS=$save_libs 670]) 671 672 673dnl 674dnl CSL_CHECK_STATIC_LIBPOLY(libpoly,includedir) 675dnl -------------------------------------------- 676dnl Try to find a usable libpoly.a. 677dnl If $1 is not empty, it's assumed to be the full path to libpoly.a 678dnl If $2 is not empty, it's assumed to be the path to the 679dnl corresponding include directory (i.e., the relevant headers are 680dnl assumed to be in $2/poly/... 681dnl If $3 is not empty, it's the GMP library to use 682dnl 683dnl If the test succeeds. then this macro sets STATIC_LIBPOLY to 684dnl the full path for libpoly.a and STATIC_LIBPOLY_INCLUDE_DIR to $2. 685dnl 686AC_DEFUN([CSL_CHECK_STATIC_LIBPOLY], 687[ 688AC_MSG_NOTICE([Searching for a usable libpoly.a]) 689CSL_CHECK_HEADER([poly/polynomial.h],$2,--with-static-libpoly-include-dir) 690# 691# If $1 is empty search for it in the 692# 693if test -z "$1" ; then 694 CSL_COLLECT_LIBRARY_PATHS 695 # 696 # $search_libs contains the directories to search 697 # 698 AC_MSG_NOTICE([Searching in $search_libs]) 699 for ldir in $search_libs ; do 700 AC_MSG_CHECKING([for libpoly.a in $ldir]) 701 if test -f $ldir/libpoly.a ; then 702 AC_MSG_RESULT(found) 703 testlib=$ldir/libpoly.a 704 CSL_CHECK_LIBPOLY($testlib,$testincludedir,$3) 705 if test $run_ok = yes ; then 706 STATIC_LIBPOLY=$testlib 707 STATIC_LIBPOLY_INCLUDE_DIR=$testincludedir 708 break 709 fi 710 else 711 AC_MSG_RESULT(no) 712 fi 713 done 714# 715else 716 # got --with-static-libpoly=xxxx 717 CSL_CHECK_LIB_PATH($1,--with-static-libpoly) 718 CSL_CHECK_LIBPOLY($testlib,$testincludedir,$3) 719 if test $run_ok = yes; then 720 STATIC_LIBPOLY=$testlib 721 STATIC_LIBPOLY_INCLUDE_DIR=$testincludedir 722 else 723 AC_MSG_ERROR([*** $1 does not appear to be usable: check option --with-static-libpoly ***]) 724 fi 725fi 726 727if test "x$STATIC_LIBPOLY" = x; then 728 AC_MSG_WARN([*** No usable libpoly.a library was found ***]) 729fi 730]) 731 732 733# 734# CHECK LIBRARIES 735# --------------- 736# 737AC_LANG([C]) 738 739# 740# We must search for the static versions first 741# since other tests may modify $LIBS and $CPPFLAGS 742# 743STATIC_GMP="" 744STATIC_GMP_INCLUDE_DIR="" 745AC_SUBST(STATIC_GMP) 746AC_SUBST(STATIC_GMP_INCLUDE_DIR) 747CSL_CHECK_STATIC_GMP($static_libgmp,$static_includegmp) 748 749# 750# Position-independent static version of GMP 751# 752PIC_GMP="$STATIC_GMP" 753PIC_GMP_INCLUDE_DIR="$STATIC_GMP_INCLUDE_DIR" 754AC_SUBST(PIC_GMP) 755AC_SUBST(PIC_GMP_INCLUDE_DIR) 756if test "x$pic_libgmp" != x ; then 757 # 758 # --with-pic-gmp was given on the command line 759 # 760 CSL_CHECK_HEADER([gmp.h],$pic_includegmp,--with-pic-gmp-include-dir) 761 CSL_CHECK_LIB_PATH($pic_libgmp,--with-pic-gmp) 762 CSL_CHECK_GMP($testlib,$testincludedir) 763 if test $run_ok = yes; then 764 PIC_GMP=$testlib 765 PIC_GMP_INCLUDE_DIR=$testincludedir 766 else 767 AC_MSG_ERROR([*** $testlib does not appear to be usable: check option --with-pic-gmp ***]) 768 fi 769fi 770 771 772# 773# We need -lm (for fclassify) 774# 775AC_CHECK_LIB([m], [main], [], []) 776 777# 778# MCSAT SUPPORT 779# ------------- 780ENABLE_MCSAT="$use_mcsat" 781AC_SUBST(ENABLE_MCSAT) 782 783# 784# libpoly.a 785# 786STATIC_LIBPOLY="" 787STATIC_LIBPOLY_INCLUDE_DIR="" 788AC_SUBST(STATIC_LIBPOLY) 789AC_SUBST(STATIC_LIBPOLY_INCLUDE_DIR) 790if test $use_mcsat = yes ; then 791 if test "x$STATIC_GMP" = x ; then 792 auxlibs="-lgmp" 793 else 794 auxlibs="$STATIC_GMP" 795 fi 796 CSL_CHECK_STATIC_LIBPOLY($static_lpoly,$static_includelpoly,$auxlibs) 797fi 798 799# 800# Position-independent static version of LIBPOLY 801# 802PIC_LIBPOLY="$STATIC_LIBPOLY" 803PIB_LIBPOLY_INCLUDE_DIR="$STATIC_LIBPOLY_INCLUDE_DIR" 804AC_SUBST(PIC_LIBPOLY) 805AC_SUBST(PIC_LIBPOLY_INCLUDE_DIR) 806if test $use_mcsat = yes ; then 807 if test "x$pic_lpoly" != x ; then 808 CSL_CHECK_HEADER([poly/polynomial.h],$pic_includelpoly,--with-pic-libpoly-include-dir) 809 CSL_CHECK_LIB_PATH($pic_lpoly,--with-pic-lpoly) 810 if test "x$PIC_GMP" != x ; then 811 auxlibs="$PIC_GMP" 812 else 813 if test "x$STATIC_GMP" != x ; then 814 auxlibs="$STATIC_GMP" 815 else 816 auxlibs="-lgmp" 817 fi 818 fi 819 CSL_CHECK_STATIC_LIBPOLY($pic_lpoly,$pic_includelpoly,$auxlibs) 820 if test $run_ok = yes; then 821 PIC_LIBPOLY=$testlib 822 PIC_LIBPOLY_INCLUDE_DIR=$testincludedir 823 else 824 AC_MSG_ERROR([*** $testlib does not appear to be usable: check option --with-pic-libpoly ***]) 825 fi 826 fi 827fi 828 829# 830# Default GMP 831# 832AC_CHECK_LIB(gmp, __gmpz_cmp, [], 833 [AC_MSG_ERROR([*** GMP library not found. Try to set LDFLAGS ***])]) 834 835 836# 837# Default libpoly 838# 839if test $use_mcsat = yes ; then 840 AC_CHECK_LIB([poly],[lp_polynomial_new], [], [AC_MSG_ERROR([*** libpoly library not found. Try to set LDFLAGS ***])]) 841fi 842 843# 844# Default CUDD 845# 846if test $use_mcsat = yes ; then 847 AC_CHECK_LIB([cudd],[Cudd_Init], [], [AC_MSG_ERROR([*** CUDD library not found. Try to set LDFLAGS ***])]) 848fi 849 850 851# 852# Fix MKDIR_P to an absolute path if it's set to './install-sh -c -d' 853# because the Makefiles import its definition via ./configs/make.include. 854# This may be unreliable (it won't handle spaces in directory names). 855# 856# case "$MKDIR_P" in 857# ./install-sh*) 858# curdir=`pwd` 859# new_mkdir_p="$curdir/$MKDIR_P" 860# AC_MSG_WARN([*** MKDIR_P is relative: converting $MKDIR_P to $new_mkdir_p ***]) 861# MKDIR_P=$new_mkdir_p 862# ;; 863# esac 864# 865 866# 867# THREAD-SAFE OPTION 868# ------------------ 869# 870AC_SUBST(THREAD_SAFE) 871if test "x$thread_safe" = xyes ; then 872 THREAD_SAFE=1 873 # iam: the aim is to eventually eliminate this restriction, but not before the 2.6.2 release. 874 if test $use_mcsat = yes ; then 875 AC_MSG_ERROR([Building with both --enable-mcsat and --enable-thread-safety is currently not supported.]) 876 fi 877fi 878 879dnl 880dnl Test support for thread-local storage 881dnl ------------------------------------- 882dnl 883AC_SUBST(HAVE_TLS) 884if test "x$thread_safe" = xyes ; then 885 has_tls="" 886 CSL_CHECK_THREAD_LOCAL 887 if test "x$has_tls" = xyes; then 888 HAVE_TLS=1 889 else 890 AC_MSG_ERROR([Building with --enable-thread-safety requires thread-local storage]) 891 fi 892fi 893 894 895 896 897dnl AC_CHECK_HEADERS([poly/poly.h], [], [AC_MSG_ERROR([*** libpoly headers not found. Try to set CPPFLAGS ***])]) 898 899 900# 901# Restore CFLAGS 902# 903CFLAGS=$saved_cflags 904 905# 906# Store config data in ./configs/make.include.$(ARCH) 907# 908AC_CONFIG_FILES([make.include]) 909AC_OUTPUT 910 911if test ! -d configs ; then 912 AC_MSG_NOTICE([Creating the configs directory]) 913 AS_MKDIR_P([configs]) 914fi 915 916if test "x$host" = x ; then 917 AC_MSG_NOTICE([Moving make.include to configs/make.include.$build]) 918 mv make.include "configs/make.include.$build" 919else 920 AC_MSG_NOTICE([Moving make.include to configs/make.include.$host]) 921 mv make.include "configs/make.include.$host" 922fi 923