1dnl Process with autoconf to generate configure script -*- sh -*- 2 3dnl Init with sanity check for source directory 4AC_INIT(cvc3,2.4.1) 5 6 7###################################################################### 8# Library version information 9# 10# IMPORTANT: This version number needs to be bumped if binary 11# incompatibilities are introduced in the shared library. 12# 13# NOTE: This is the *library* version, not the version of the CVC3 14# release (which is set by the VERSION variable below). In general, 15# LIB_MAJOR_VERSION will be greater than VERSION, because we break 16# compatibility fairly often in point releases. 17###################################################################### 18 19# Major version: increases for non-backwards-compatible API changes 20AC_SUBST(LIB_MAJOR_VERSION) 21# Minor version: increases for backwards-compatible API changes 22AC_SUBST(LIB_MINOR_VERSION) 23# Teeny version: increases for library bug fixes (API hasn't changed) 24AC_SUBST(LIB_TEENY_VERSION) 25 26LIB_MAJOR_VERSION=5 27LIB_MINOR_VERSION=0 28LIB_TEENY_VERSION=0 29 30dnl We don't want the default autoconf CXXFLAGS=-g -O2 31if test "${CXXFLAGS+set}" != set; then 32 CXXFLAGS="" 33fi 34 35dnl Set C++ as the default language for all tests 36AC_LANG([C++]) 37AC_REQUIRE_CPP 38 39AC_ARG_VAR([AR],[C/C++ linker/archiver]) 40AC_CHECK_TOOL([AR],ar) 41 42AC_SUBST(EXTRA_SAT_HEADERS) 43AC_SUBST(EXTRA_SAT_CPP) 44AC_SUBST_FILE([LICENSE_INFO]) 45AC_SUBST(DPLL_BASIC) 46EXTRA_SAT_HEADERS="" 47EXTRA_SAT_CPP="" 48LICENSE_INFO=/dev/null 49DPLL_BASIC="" 50#BEGIN zchaff 51cvc_use_zchaff="yes" 52AC_ARG_ENABLE(zchaff, 53[ --enable-zchaff Include zchaff code (default = yes) 54 --disable-zchaff Remove zchaff code (default = no)], 55if test "$enableval" = "no"; then 56 cvc_use_zchaff="no" 57fi) 58if test "$cvc_use_zchaff" = "yes"; then 59/bin/sh >.zchaff <<EOF 60echo "This copy of CVC3 is also configured to use the SAT solver zchaff whose" 61echo "copyright is owned by Princeton University and is more restrictive." 62echo "" 63echo "Specifically, it may be used for internal, noncommercial, research purposes" 64echo "only. See the copyright notice in the following files for more information." 65echo "To build CVC3 without these files, please delete them and then run:" 66echo "<pre>" 67echo " ./configure --disable-zchaff" 68echo " make" 69echo "</pre>" 70echo "" 71echo "<pre>" 72echo "src/sat/xchaff_base.h" 73echo "src/sat/xchaff_dbase.h" 74echo "src/sat/xchaff_solver.h" 75echo "src/sat/xchaff_utils.h" 76echo "src/sat/xchaff_dbase.cpp" 77echo "src/sat/xchaff_solver.cpp" 78echo "src/sat/xchaff_utils.cpp" 79echo "</pre>" 80echo "" 81EOF 82EXTRA_SAT_HEADERS="xchaff.h xchaff_base.h xchaff_dbase.h xchaff_solver.h xchaff_utils.h" 83EXTRA_SAT_CPP="xchaff.cpp xchaff_dbase.cpp xchaff_solver.cpp xchaff_utils.cpp " 84LICENSE_INFO=.zchaff 85DPLL_BASIC="-DDPLL_BASIC" 86fi 87#END zchaff 88 89dnl # Name of the OS 90dnl AC_SUBST(OSTYPE) 91 92# Version of CVC 93AC_SUBST(VERSION) 94 95AC_SUBST(OPTIMIZED) 96OPTIMIZED="0" 97AC_SUBST(GCOV) 98GCOV="0" 99AC_SUBST(GPROF) 100GPROF="0" 101 102AC_ARG_WITH([build], 103[ --with-build=optimized Specify the type of build (default = optimized). 104 Possible values: debug, optimized, gprof, gcov], 105[if test "$withval" = "optimized"; then 106 OPTIMIZED="1" 107elif test "$withval" = "gprof"; then 108 OPTIMIZED="1" 109 GPROF="1" 110elif test "$withval" = "gcov"; then 111 GCOV="1" 112else 113 DEBUG_MSG="yes" 114fi], 115# --with-build is not given, default is "optimized" build 116 [OPTIMIZED="1"] 117) 118 119AC_SUBST(CXXFLAGS) 120CXXFLAGS="$CXXFLAGS" 121AC_ARG_ENABLE(debug-yacc, 122[ --enable-debug-yacc Enable debugging of yacc (default = no).], 123if test "$enableval" = "yes"; then 124 CXXFLAGS="$CXXFLAGS -DYYDEBUG" 125fi) 126 127dnl Some extra features 128AC_SUBST(LD) 129LD='$(CXX)' 130AC_ARG_WITH(ld, 131[ --with-ld Use a specific program for linking.], 132if test ! "x$withval" = "xno" && test ! "x$withval" = "x"; then 133 LD="$withval" 134fi) 135 136AC_SUBST(LDFLAGS) 137LDFLAGS="$LDFLAGS" 138AC_ARG_WITH(extra-libs, 139[ --with-extra-libs List of paths to additional static libraries 140 separated with ":".], 141if test ! "x$withval" = "xno" && test ! "x$withval" = "x"; then 142 LDFLAGS="$LDFLAGS -L"`echo "$withval" | sed -e 's/:/ -L/g'` 143fi) 144 145AC_SUBST(CPPFLAGS) 146CPPFLAGS="$CPPFLAGS" 147AC_ARG_WITH(extra-includes, 148[ --with-extra-includes List of paths to additional include files 149 separated with ":".], 150if test ! "x$withval" = "xno" && test ! "x$withval" = "x"; then 151 CPPFLAGS="$CPPFLAGS -I"`echo "$withval" | sed -e 's/:/ -I/g'` 152fi) 153 154AC_ARG_WITH(version, 155[ --with-version=<version string> 156 The version string to report on cvc3 -version], 157# If option is given 158VERSION="$withval", 159# If not given 160VERSION=`cat VERSION`) 161 162dnl Override check for "broken" compilers 163AC_ARG_ENABLE(broken-cxx, 164[ --enable-broken-cxx[=no] Force configure to accept the compiler, 165 even if it thinks that it is broken.], 166# If option is given 167if test "x$enableval" = "xyes"; then 168 enable_broken_cxx="yes" 169else 170 enable_broken_cxx="no" 171fi, 172# If option is not given 173enable_broken_cxx="no") 174 175dnl Find out what OS-specific subdirectory name to use 176 177AC_CANONICAL_HOST 178AC_EXEEXT 179 180case "$host_os" in 181 none) 182 host_os="unknown" 183 ;; 184 185 darwin*) 186 MAC_OSX=1 187 ;; 188 189 cygwin) 190 CYGWIN=1 191 ;; 192esac 193 194case "$host_cpu" in 195 i?86) 196 # punt for Mac OS-- it gives you i386 even on 64-bit 197 # let darwin's gcc build what it wants (or have the user add 198 # -mXX to CXXFLAGS themselves) 199 if test "$MAC_OSX" = 1; then :; else 200 CXXFLAGS="$CXXFLAGS -m32" 201 if test "$CYGWIN" = 1; then :; else 202 # Sun's Java on Windows doesn't have -d* 203 JREFLAGS="$JREFLAGS -d32" 204 fi 205 fi 206 ;; 207 208 x86_64) 209 CXXFLAGS="$CXXFLAGS -m64" 210 JREFLAGS="$JREFLAGS -d64" 211 ;; 212esac 213 214OSTYPE="$host_cpu-$host_os" 215dnl OSTYPE=`echo "$OSTYPE" | sed 'y%ABCDEFGHIJKLMNOPQRSTUVWXYZ %abcdefghijklmnopqrstuvwxyz_%'` 216 217# The standard macro does something stupid. Check it explicitly. 218# AC_PROG_INSTALL 219 220AC_SUBST(INSTALL) 221AC_SUBST(INSTALL_FLAGS) 222AC_PATH_PROG(INSTALL, install, cp) 223 224if test "$INSTALL" = "cp"; then 225 INSTALL_FLAGS="" 226else 227# INSTALL_FLAGS="-C --owner=root --group=root" 228# INSTALL_FLAGS="-C" 229# Seems like the arguments to 'install' are changing wildly with platform... 230 INSTALL_FLAGS="" 231fi 232 233AC_SUBST(LDCONFIG) 234AC_PATH_PROG(LDCONFIG, ldconfig, 235 AC_MSG_WARN([ldconfig not found. Library installation may fail.]), 236 [$PATH:/sbin:/usr/sbin]) 237 238AC_SUBST(TIME) 239if test -n "$MAC_OSX"; then 240AC_PATH_PROG(TIME, gtime, [not found]) 241else 242AC_PATH_PROG(TIME, time, [not found]) 243fi 244 245if test "$TIME" = "not found"; then 246 AC_MSG_WARN(Regression tests depend upon GNU time.) 247if test -n "$MAC_OSX"; then 248 AC_MSG_WARN(Please install GNU time; we suggest using MacPorts, see INSTALL.) 249fi 250fi 251 252AC_SUBST(PERL) 253AC_PATH_PROG(PERL, perl, [not found]) 254 255if test "$PERL" = "not found"; then 256 perl_found=0 257 AC_MSG_WARN(Perl not found. Static build will probably fail.) 258 # Set default path for perl, just in case 259 PERL=/usr/bin/perl 260else 261 perl_found=1 262fi 263 264dnl These checks rely on the behavior of autoconf and *require* bison and flex, rather than yacc or lex. 265 266AC_PROG_YACC 267 268if test "$YACC" != "bison -y"; then 269 AC_MSG_ERROR([bison not found]) 270fi 271 272AC_PROG_LEX 273 274if test "$LEX" != "flex"; then 275 AC_MSG_ERROR([flex not found]) 276fi 277 278dnl Check compiler version (we know that 3.0 does not compile) 279AC_CACHE_CHECK(for compiler version ($CXX --version), cvc_cv_cxx_version, 280cvc_cv_cxx_version=`$CXX --version | grep "[[[0-9]]][[[0-9]]]*[[[.]]][[[0-9]]]*" | sed -e 's/^[[[^0-9]]]*\([[[0-9.]]]*\).*$/\1/'`) 281 282cxx_major_version=`echo $cvc_cv_cxx_version | sed -e 's/^\([[0-9]]*\).*/\1/'` 283cxx_minor_version=`echo $cvc_cv_cxx_version | sed -e 's/^[[0-9]]*[[.]]\([[0-9]]*\).*/\1/'` 284 285if test "$cxx_major_version.$cxx_minor_version" = "3.0"; then 286 if test "$enable_broken_cxx" = "no"; then 287 AC_MSG_ERROR( 288 289[Compiler version $cvc_cv_cxx_version is known to generate bad executables. 290If you still want to compile with it, configure with option 291--enable-broken-cxx, but then do not ask for help unless you know how 292to fix it.]) 293 294 else 295# The user asked for bad compiler. Warn him/her at the end. 296 cxx_bad_version_warning="yes" 297 fi 298fi 299 300AC_SUBST(STATIC) 301STATIC="1" 302 303AC_SUBST(BUILD_SHARED_LIB) 304BUILD_SHARED_LIB="0" 305 306 307AC_SUBST(STATIC_FLAG) 308AC_SUBST(DYNAMIC_FLAG) 309AC_SUBST(SHARED) 310AC_SUBST(LD_SWITCHES_PRE) 311AC_SUBST(LD_SWITCHES_POST) 312AC_SUBST(LD_LIB_DIR) 313 314if test -n "$MAC_OSX"; then 315 DYNAMIC_FLAG="-dynamic" 316 STATIC_FLAG="" 317 SHARED="-dynamiclib -undefined dynamic_lookup" 318 LD_SWITCHES_PRE="" 319 LD_SWITCHES_POST="" 320elif test -n "$CYGWIN"; then 321 DYNAMIC_FLAG="" 322 STATIC_FLAG="" 323 SHARED="-shared" 324 LD_SWITCHES_PRE="-Wl,-static -Wl,--whole-archive" 325 LD_SWITCHES_POST="-Wl,--no-whole-archive -Wl,-call_shared" 326else 327 DYNAMIC_FLAG="" 328 STATIC_FLAG="-static" 329 SHARED="-shared" 330 LD_SWITCHES_PRE="-Wl,-static -Wl,--whole-archive" 331 LD_SWITCHES_POST="-Wl,--no-whole-archive -Wl,-call_shared" 332fi 333 334AC_ARG_ENABLE(static, 335[ --enable-static 336 --disable-dynamic Enable static build of cvc3 (default=yes). 337 Disable for faster link times.], 338# If options is given 339if test "$enableval" = "no"; then 340 STATIC="0" 341fi) 342 343AC_ARG_ENABLE(dynamic, 344[ --enable-dynamic 345 --disable-static Enable shared library build of cvc3 (default = no).], 346# If option is given 347if test "$enableval" = "yes"; then 348 STATIC="0" 349fi) 350 351AC_ARG_ENABLE(sharedlibs, 352[ --enable-sharedlibs 353 --disable-sharedlibs Enable building of individual shared libraries 354 (default = yes).], 355# If option is given 356if test "$enableval" = "yes"; then 357 BUILD_SHARED_LIB="1" 358fi) 359 360 361AC_SUBST(STATIC_LIB_SUFFIX) 362STATIC_LIB_SUFFIX="a" 363 364AC_SUBST(SHARED_LIB_SUFFIX) 365if test -n "$MAC_OSX"; then 366 SHARED_LIB_SUFFIX="dylib" 367elif test -n "$CYGWIN"; then 368 SHARED_LIB_SUFFIX="dll" 369else 370 SHARED_LIB_SUFFIX="so" 371fi 372 373AC_SUBST(RATIONAL_IMPL) 374AC_ARG_WITH(arith, 375[ --with-arith=gmp Specify the arithmetic option to use: 376 gmp: C-only GMP package (default) 377 gmpxx: GMP package with C++ extensions (deprecated) 378 native: native computer arithmetic (finite precision)], 379if test "$withval" = gmpxx; then 380 RATIONAL_IMPL="-DRATIONAL_GMPXX" 381elif test "$withval" = gmp; then 382 RATIONAL_IMPL="-DRATIONAL_GMP" 383elif test "$withval" = native; then 384 RATIONAL_IMPL="-DRATIONAL_NATIVE" 385else 386 RATIONAL_IMPL="" 387fi, 388# if option is not given 389RATIONAL_IMPL="-DRATIONAL_GMP" 390) 391 392 393dnl Checks for libraries. Adds -lfoo to LIBS for each found library 'foo' 394dnl and defines HAVE_LIBfoo, unless 3rd and 4th args are specified. 395 396# Make sure we check the appropriate static / shared library 397 398if test "$RATIONAL_IMPL" = "-DRATIONAL_GMP"; then 399 AC_MSG_CHECKING(for gmp) 400 LIBS="-lgmp $LIBS" 401 AC_LINK_IFELSE([AC_LANG_PROGRAM([[ 402#include <gmp.h> 403#include <iostream> 404]], [[ mpq_t x; 405 mpq_init(x); 406]])],[cvc_gmp_works="yes"],[cvc_gmp_works="no"]) 407if test "$cvc_gmp_works" = "no"; then 408if test -n "$MAC_OSX"; then 409 AC_MSG_RESULT(no) 410 AC_MSG_CHECKING(for gmp in /opt/local) 411 CPPFLAGS="-I/opt/local/include $CPPFLAGS" 412 LDFLAGS="-L/opt/local/lib $LDFLAGS" 413 AC_LINK_IFELSE([AC_LANG_PROGRAM([[ 414#include <gmp.h> 415#include <iostream> 416]], [[ mpq_t x; 417 mpq_init(x); 418]])],[cvc_gmp_works="yes"],[cvc_gmp_works="no"]) 419fi 420fi 421if test "$cvc_gmp_works" = "no"; then 422 AC_MSG_ERROR([[libgmp.a is not found. 423You can still compile CVC3 with native computer arithmetic: 424 425 ./configure --with-arith=native 426 427WARNING: native arithmetic may cause overflows and assertion failures. 428 429If CVC3 fails due to an overflow in native arithmetic, do NOT 430report a bug; it is an intended feature to prevent soundness errors. 431 432For these reasons, we STRONGLY recommend installing GMP.]]) 433else 434AC_MSG_RESULT(yes) 435fi 436elif test "$RATIONAL_IMPL" = "-DRATIONAL_GMPXX"; then 437 AC_CHECK_LIB(gmp, main, , AC_MSG_ERROR(libgmp.a is not found)) 438 AC_CHECK_LIB(gmpxx, main, , AC_MSG_ERROR(libgmpxx.a is not found)) 439elif test -z "$RATIONAL_IMPL"; then 440 AC_MSG_ERROR("Unknown argument to with-arith") 441fi 442 443if test "$RATIONAL_IMPL" = "-DRATIONAL_GMPXX"; then 444# Do some more extensive check of gmpxx, since it may be compiled with 445# a wrong compiler. 446AC_CACHE_CHECK(whether gmpxx library works, cvc_cv_gmpxx_works, 447 cvc_cv_gmpxx_works="no" 448 AC_LINK_IFELSE([AC_LANG_PROGRAM([[ 449#include <gmpxx.h> 450#include <iostream> 451]], [[ mpz_class x; 452 std::cout << x; 453]])],[cvc_cv_gmpxx_works="yes"],[])) 454 455if test "$cvc_cv_gmpxx_works" = "no"; then 456 AC_MSG_ERROR([libgmpxx.a did not link. 457You may have to recompile GMP with the current compiler: $CXX.]) 458fi 459fi 460 461dnl Java interface options 462 463AC_SUBST(BUILD_JAVA) 464BUILD_JAVA="0" 465 466AC_ARG_VAR([javadir],[installation directory for Java libraries]) 467AC_ARG_VAR([JAR],[JAR archive utility command]) 468AC_ARG_VAR([JAVA],[Java runtime command]) 469AC_ARG_VAR([JAVAC],[Java compiler command]) 470AC_ARG_VAR([JAVAH],[JNI utility command]) 471AC_ARG_VAR([JFLAGS],[Java compiler flags]) 472AC_ARG_VAR([JREFLAGS],[Java runtime flags]) 473AC_ARG_VAR([PYTHON],[Python runtime]) 474 475javadir='${exec_prefix}/java' 476 477dnl Take JNI_INC as a configuration option. By default, assume it's in 478dnl the standard Sun JDK 6 location. 479 480AC_SUBST([JNI_INC]) 481 482 483AC_ARG_ENABLE([java], 484[ --enable-java 485 --disable-java Enable building of CVC3 Java interface (default = no).], 486# If option is given 487if test "$enableval" = "yes"; then 488 BUILD_JAVA="1" 489fi) 490 491dnl AC_ARG_WITH([jni-include], 492dnl [AS_HELP_STRING([--with-jni-include=PATH], 493dnl [specify PATH of the JNI include directory])], 494dnl [JNI_INC=$withval], 495dnl [JNI_INC=/usr/lib/jvm/java-6-sun/include]) 496 497 498if test "$BUILD_JAVA" = "1"; then 499 if test "$STATIC" = "1"; then 500 AC_MSG_ERROR([The Java interface requires a dynamic library build. Use --enable-dynamic.]) 501 fi 502 503dnl [chris] BEGIN: crib from libjmagick6-jni (significantly altered) 504dnl Determine if we have a decent Java distribution 505 AC_ARG_WITH([java-home], 506 [AS_HELP_STRING([--with-java-home=PATH], [Java installation path])], 507 [JAVA_HOME=${withval}]) 508 AC_ARG_WITH([java-includes], 509 [AS_HELP_STRING([--with-java-includes=PATH],[Java includes path])], 510 [JAVA_INCLUDE_PATH="${withval}"]) 511 512dnl [chris] Use a sensible default for JAVA_HOME on Mac 513 if test -n "${MAC_OSX}" -a -z "${JAVA_HOME}" ; then 514 JAVA_HOME=/System/Library/Frameworks/JavaVM.framework/Home 515 fi 516 517 dnl If we don't have a Java include path, try to derive one from JAVA_HOME 518 if ! ( test -n "${JAVA_INCLUDE_PATH}" -a -d "${JAVA_INCLUDE_PATH}" ) ; then 519 if test -d ${JAVA_HOME}/include ; then 520 JAVA_INCLUDE_PATH=${JAVA_HOME}/include 521 dnl check for Mac OS X series of systems 522 elif test -d ${JAVA_HOME}/Headers; then 523 JAVA_INCLUDE_PATH=-I${JAVA_HOME}/Headers 524 else 525 AC_MSG_ERROR([Unable to locate Java directories]) 526 fi 527 fi 528 529 JAVA_INCLUDES=-I${JAVA_INCLUDE_PATH} 530 dnl The Blackdown JDK seems to have genunix. 531 if test -d ${JAVA_INCLUDE_PATH}/genunix ; then 532 JAVA_INCLUDES="$JAVA_INCLUDES -I${JAVA_INCLUDE_PATH}/genunix" 533 fi 534 dnl The Sun Linux JDK seems to use linux 535 if test -d ${JAVA_INCLUDE_PATH}/linux ; then 536 JAVA_INCLUDES="$JAVA_INCLUDES -I${JAVA_INCLUDE_PATH}/linux" 537 fi 538 dnl The Sun Solaris JDK seems to use solaris 539 if test -d ${JAVA_INCLUDE_PATH}/solaris ; then 540 JAVA_INCLUDES="$JAVA_INCLUDES -I${JAVA_INCLUDE_PATH}/solaris" 541 fi 542 dnl The Sun FreeBSD JDK seems to use freebsd 543 if test -d ${JAVA_INCLUDE_PATH}/freebsd ; then 544 JAVA_INCLUDES="$JAVA_INCLUDES -I${JAVA_INCLUDE_PATH}/freebsd" 545 fi 546 dnl The Sun Windows JDK seems to use win32 547 if test -d ${JAVA_INCLUDE_PATH}/win32 ; then 548 JAVA_INCLUDES="$JAVA_INCLUDES -I${JAVA_INCLUDE_PATH}/win32" 549 fi 550 if test -d ${JAVA_INCLUDE_PATH}/bsd ; then 551 JAVA_INCLUDES="$JAVA_INCLUDES -I${JAVA_INCLUDE_PATH}/bsd" 552 fi 553 554 dnl [chris] END: crib from libjmagick6-jni 555 556 if test -d ${JAVA_HOME}/bin; then 557 PATH=${JAVA_HOME}/bin:$PATH 558 fi 559 560 # Check for Java tools 561 AC_PATH_PROG([JAVAC],[javac], 562 [AC_MSG_ERROR([javac not found: adjust PATH or set JAVAC])]) 563 564 AC_PATH_PROG([JAVAH],[javah], 565 [AC_MSG_ERROR([javah not found: adjust PATH or set JAVAH])] ) 566 567 AC_PATH_PROG([JAR],[jar], 568 [AC_MSG_ERROR([jar not found: adjust PATH or set JAR])] ) 569 570 AC_PATH_PROG([JAVA],[java], 571 [AC_MSG_ERROR([java not found: adjust PATH or set JAVA])] ) 572 573 dnl Save and restore CPPFLAGS while checking for JNI headers 574 575 OLD_CPPFLAGS="$CPPFLAGS" 576 CPPFLAGS="${JAVA_INCLUDES} $CPPFLAGS" 577 578 AC_CHECK_HEADER([jni.h],, 579 [AC_MSG_ERROR(jni.h not found: try setting --with-java-home or --with-java-includes)]) 580 AC_CHECK_HEADER([jni_md.h],, 581 [AC_MSG_ERROR(jni_md.h not found: try setting --with-java-home or --with-java-includes)]) 582 583 dnl Restore original CPPFLAGS 584 CPPFLAGS="$OLD_CPPFLAGS" 585 586 AC_PATH_PROG([PYTHON],[python], 587 [AC_MSG_ERROR([python not found: adjust PATH or set PYTHON])]) 588fi 589dnl end of Java tests 590 591AC_SUBST(JAVA_INCLUDES) 592 593dnl Checks for header files. 594dnl Defines HAVE_headerFile for each headerFile found 595 596AC_CHECK_HEADERS([vector list deque set string cstdlib cstdio \ 597 functional algorithm], , 598 AC_MSG_ERROR(header is not found)) 599 600dnl Checks for typedefs, structures, and compiler characteristics. 601 602dnl Checks for library functions. 603 604dnl Other tests 605 606dnl Define the build and source directories for all sub-projects and 607dnl flags for optional packages if we want them to be built 608 609dnl CVC 610 611dnl Top-level directory for CVC 612AC_SUBST(TOP) 613TOP=`pwd` 614 615# Checking for documentation related programs 616AC_SUBST(DOXYGEN) 617AC_CHECK_PROG(DOXYGEN, doxygen, doxygen) 618AC_SUBST(DOXYTAG) 619AC_CHECK_PROG(DOXYTAG, doxytag, doxytag) 620AC_SUBST(FIG2DEV) 621AC_CHECK_PROG(FIG2DEV, fig2dev, fig2dev) 622AC_SUBST(HAVE_DOT) 623AC_CHECK_PROG(HAVE_DOT, dot, "YES", "NO") 624AC_SUBST(ETAGS) 625AC_CHECK_PROG(ETAGS, etags, "etags") 626AC_SUBST(EBROWSE) 627AC_CHECK_PROG(EBROWSE, ebrowse, "ebrowse") 628 629CVC_OUTPUT_FILES="Makefile.local \ 630LICENSE \ 631src/cvc3.pc" 632 633OTHER_OUTPUT_FILES="bin/unpack \ 634bin/run_tests \ 635bin/cvc2smt \ 636doc/Doxyfile \ 637doc/Makefile" 638 639 640AC_CONFIG_FILES([$CVC_OUTPUT_FILES \ 641$OTHER_OUTPUT_FILES 642]) 643AC_OUTPUT 644 645chmod a+x bin/run_tests 646chmod a+x bin/cvc2smt 647chmod a+x bin/unpack 648 649opt_arith="$RAITONAL_IMPL" 650 651if test "$RATIONAL_IMPL" = "-DRATIONAL_NATIVE"; then 652 opt_arith="native" 653elif test "$RATIONAL_IMPL" = "-DRATIONAL_GMP"; then 654 opt_arith="GMP" 655elif test "$RATIONAL_IMPL" = "-DRATIONAL_GMPXX"; then 656 opt_arith="GMP with C++ extensions" 657fi 658 659cat <<EOF 660 661CVC3 is configured successfully. 662Platform: $OSTYPE 663Version: $VERSION 664Computer arithmetic: $opt_arith 665 666Run ./configure --help for additional configuration options. 667 668Type 'make' to compile CVC3. 669EOF 670 671if test $RATIONAL_IMPL = "-DRATIONAL_NATIVE"; then 672echo "" 673echo "*** You have chosen to compile CVC3 with native arithmetic support." 674echo "*** If an arithmetic overflow occurs, you will get an assertion failure." 675echo "*** To avoid overflow issues, install the GMP library." 676fi 677 678if test -n "$DEBUG_MSG"; then 679echo "" 680echo "*** CVC3 is configured to compile in debugging mode. You can increase" 681echo "*** the performance significantly by compiling an optimized executable:" 682echo "*** ./configure --with-build=optimized" 683fi 684 685if test "$STATIC" = "0"; then 686echo "" 687echo "*** CVC3 is configured to compile using shared libraries." 688echo '*** Type "make ld_sh" for bash shells or "make ld_csh" for csh shells' 689echo "*** to see how to set LD_LIBRARY_PATH appropriately. To use static" 690echo "*** libraries and executables instead, run:" 691echo "*** ./configure --enable-static" 692fi 693 694if test "$cxx_bad_version_warning" = "yes"; then 695echo "" 696echo "*** Warning: Compiler version $cvc_cv_cxx_version is known to generate bad" 697echo "*** executables." 698fi 699 700