README

   1 This is a prerelease version of CVC4.
   2
   3 *** Quick-start instructions
   4
   5 To build, you'll need reasonably new automake, autoconf, and libtool
   6 installed (see below). Execute,
   7
   8     ./autogen.sh
   9     ./configure
  10     make
  11
  12 You can then "make install" to install in the prefix you gave to
  13 the configure script (/usr/local by default).  ** You should run
  14 "make check" ** before installation to ensure that CVC4 has been
  15 built correctly.  In particular, GCC version 4.5.1 seems to have a
  16 bug in the optimizer that results in incorrect behavior (and wrong
  17 results) in many builds.  This is a known problem for Minisat, and
  18 since Minisat is at the core of CVC4, a problem for CVC4.  "make check"
  19 easily detects this problem (by showing a number of FAILed test cases).
  20 It is ok if the unit tests aren't run as part of "make check", but all
  21 system tests and regression tests should pass without incident.
  22
  23 To build a source release, use "make dist"; this will include the
  24 configure script and all the bits of automake/autoconf/libtool that
  25 are necessary for an independent install.  You'll find the resulting
  26 tarball in builds/cvc4-${VERSION}.tar.gz.
  27
  28 To build documentation, use "make doc".  Documentation is produced
  29 under doc/ but is not installed by "make install".
  30
  31 *** Dependencies
  32
  33 The following tools and libraries are required to run CVC4. Versions
  34 given are minimum versions; more recent versions should be compatible.
  35
  36 GNU C and C++ (gcc and g++), reasonably recent versions
  37 GNU Make
  38 GNU Bash
  39 GMP v4.2 (GNU Multi-Precision arithmetic library)
  40 libantlr3c v3.2 (ANTLR parser generator)
  41 Optional: CLN v1.3 (Class Library for Numbers)
  42 Optional: CUDD v2.4.2 (Colorado University Decision Diagram package)
  43 Optional: GNU Readline library (for an improved interactive experience)
  44 Optional: The Boost C++ threading library (libboost_thread)
  45
  46 If "make" is non-GNU on your system, make sure to invoke "gmake" (or
  47 whatever GNU Make is installed as).  If your usual shell is not
  48 Bash, the configure script should auto-correct this.  If it does not,
  49 you'll see strange shell syntax errors, and you may need to explicitly
  50 set SHELL or CONFIG_SHELL to the location of bash on your system.
  51
  52 CUDD, if desired, must be installed delicately.  The CVC4 configure
  53 script attempts to auto-detect the locations and names of CUDD headers
  54 and libraries the way that the Fedora RPMs install them, the way that
  55 our NYU-provided Debian packages install them, and the way they exist
  56 when you download and build the CUDD sources directly.  If you install
  57 from Fedora RPMs or our Debian packages (remember, you need the C++
  58 development package for CVC4), the process should be completely
  59 automatic, since the libraries and headers are installed in a standard
  60 location.  If you download the sources yourself, you need to build
  61 them in a special way.  Fortunately, the "contrib/build-cudd-with-libtool.sh"
  62 script in the CVC4 source tree does exactly what you need: it patches
  63 the CUDD makefiles to use libtool, builds the libtool libraries, then
  64 reverses the patch to leave the makefiles as they were.  Once you
  65 run this script on an unpacked CUDD 2.4.2 source distribution, then
  66 CVC4's configure script should pick up the libraries if you provide
  67 --with-cudd-dir=/PATH/TO/CUDD/SOURCES.
  68
  69 If you want to force linking to CUDD, provide --with-cudd to the
  70 configure script; this makes it a hard requirement rather than an
  71 optional add-on.
  72
  73 The NYU-provided Debian packaging of CUDD 2.4.2 is here:
  74
  75   deb http://goedel.cims.nyu.edu/cvc4-builds/debian unstable/
  76
  77 The Debian source package "cudd", available from the same repository,
  78 includes a diff of all changes made to cudd makefiles.
  79
  80 *** Build dependencies
  81
  82 The following tools and libraries are required to build CVC4 from
  83 scratch.
  84
  85 Automake v1.11
  86 Autoconf v2.61
  87 Libtool v2.2
  88 ANTLR3 v3.2
  89
  90 *** Emacs support
  91
  92 For a suggestion of editing CVC4 source code with emacs, see the file
  93 contrib/editing-with-emacs.  For a CVC language mode (the native input
  94 language for CVC4), see contrib/cvc-mode.el.
  95