diff options
| -rw-r--r-- | README | 17 | ||||
| -rw-r--r-- | config/gcc_version.m4 | 7 | ||||
| -rw-r--r-- | configure.ac | 9 | ||||
| -rw-r--r-- | src/util/configuration.cpp | 15 | ||||
| -rw-r--r-- | src/util/configuration.h | 2 | ||||
| -rw-r--r-- | src/util/configuration_private.h | 3 |
6 files changed, 51 insertions, 2 deletions
@@ -10,7 +10,15 @@ installed (see below). Execute, make You can then "make install" to install in the prefix you gave to -the configure script (/usr/local by default). +the configure script (/usr/local by default). ** You should run +"make check" ** before installation to ensure that CVC4 has been +built correctly. In particular, GCC version 4.5.1 seems to have a +bug in the optimizer that results in incorrect behavior (and wrong +results) in many builds. This is a known problem for Minisat, and +since Minisat is at the core of CVC4, a problem for CVC4. "make check" +easily detects this problem (by showing a number of FAILed test cases). +It is ok if the unit tests aren't run as part of "make check", but all +system tests and regression tests should pass without incident. To build a source release, use "make dist"; this will include the configure script and all the bits of automake/autoconf/libtool that @@ -27,12 +35,19 @@ given are minimum versions; more recent versions should be compatible. GNU C and C++ (gcc and g++), reasonably recent versions GNU Make +GNU Bash GMP v4.2 (GNU Multi-Precision arithmetic library) libantlr3c v3.2 (ANTLR parser generator) Optional: CLN v1.3 (Class Library for Numbers) Optional: CUDD v2.4.2 (Colorado University Decision Diagram package) Optional: GNU Readline library (for an improved interactive experience) +If "make" is non-GNU on your system, make sure to invoke "gmake" (or +whatever GNU Make is installed as). If your usual shell is not +Bash, the configure script should auto-correct this. If it does not, +you'll see strange shell syntax errors, and you may need to explicitly +set SHELL or CONFIG_SHELL to the location of bash on your system. + CUDD, if desired, must be installed delicately. The CVC4 configure script attempts to auto-detect the locations and names of CUDD headers and libraries the way that the Fedora RPMs install them, the way that diff --git a/config/gcc_version.m4 b/config/gcc_version.m4 new file mode 100644 index 000000000..acd051042 --- /dev/null +++ b/config/gcc_version.m4 @@ -0,0 +1,7 @@ +# GCC version 4.5.1 builds Minisat incorrectly with -O2 +# and that gives incorrect answers! Warn the user! +AC_DEFUN([CVC4_GCC_VERSION], [ + if expr "$($CC -dumpversion)" : '4\.5\.1' &>/dev/null; then + CVC4_INTEGRITY_WARNING="GCC 4.5.1's optimizer is known to make errors building Minisat (and by extension CVC4)" + fi +])# CVC4_GCC_VERSION diff --git a/configure.ac b/configure.ac index 9d28d21fa..cabb50706 100644 --- a/configure.ac +++ b/configure.ac @@ -208,6 +208,8 @@ AC_PROG_CC AC_PROG_CXX AC_PROG_INSTALL +CVC4_GCC_VERSION + # [chris 8/24/2010] The user *must* specify --with-cln to get CLN # (and, thus, opt in to the GPL dependency). @@ -1062,3 +1064,10 @@ Install into : $prefix ${licensewarn}Now just type make, followed by make check or make install, as you like. EOF + +if test -n "$CVC4_INTEGRITY_WARNING"; then + AC_MSG_WARN([]) + AC_MSG_WARN($CVC4_INTEGRITY_WARNING) + AC_MSG_WARN([Please run "make check" after building to ensure integrity of the binary and library]) + AC_MSG_WARN([]) +fi diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index 7225b8108..3164b75a5 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -186,4 +186,19 @@ string Configuration::getSubversionId() { return ss.str(); } +string Configuration::getCompiler() { + stringstream ss; +#ifdef __GNUC__ + ss << "GCC"; +#else /* __GNUC__ */ + ss << "unknown compiler"; +#endif /* __GNUC__ */ +#ifdef __VERSION__ + ss << " version " << __VERSION__; +#else /* __VERSION__ */ + ss << ", unknown version"; +#endif /* __VERSION__ */ + return ss.str(); +} + }/* CVC4 namespace */ diff --git a/src/util/configuration.h b/src/util/configuration.h index b4caf842c..c3040f3fb 100644 --- a/src/util/configuration.h +++ b/src/util/configuration.h @@ -99,6 +99,8 @@ public: static bool hasSubversionModifications(); static std::string getSubversionId(); + static std::string getCompiler(); + };/* class Configuration */ }/* CVC4 namespace */ diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h index 13347d970..abff15b3b 100644 --- a/src/util/configuration_private.h +++ b/src/util/configuration_private.h @@ -114,7 +114,8 @@ This is CVC4 version " CVC4_RELEASE_STRING ) + \ ( ::CVC4::Configuration::isSubversionBuild() \ ? ( ::std::string(" [") + ::CVC4::Configuration::getSubversionId() + "]" ) \ : ::std::string("") \ - ) + "\n\n\ + ) + "\n\ +compiled with " + ::CVC4::Configuration::getCompiler() + "\n\n\ Copyright (C) 2009, 2010, 2011\n\ The ACSys Group\n\ Courant Institute of Mathematical Sciences\n\ |