diff options
Diffstat (limited to 'INSTALL')
| -rw-r--r-- | INSTALL | 259 |
1 files changed, 0 insertions, 259 deletions
diff --git a/INSTALL b/INSTALL deleted file mode 100644 index 655c0e005..000000000 --- a/INSTALL +++ /dev/null @@ -1,259 +0,0 @@ -CVC4 prerelease version 1.7. - -** Quick-start instructions - -*** Supported operating systems - -CVC4 can be built on Linux and macOS. For Windows, CVC4 can be cross-compiled -using Mingw-w64. We recommend a 64-bit operating system. - -On macOS, we recommend using Homebrew (https://brew.sh/) to install the -dependencies. We also have a Homebrew Tap available at -https://github.com/CVC4/homebrew-cvc4 . - -*** Build dependencies - -The following tools and libraries are required to build and run CVC4. -Versions given are minimum versions; more recent versions should be -compatible. - - GNU C and C++ (gcc and g++) or Clang, reasonably recent versions - GNU Make - GNU Bash - GMP v4.2 (GNU Multi-Precision arithmetic library) - libantlr3c v3.2 or v3.4 (ANTLR parser generator C support library) - The Boost C++ base libraries - -Some features, such as the theory of floating-point numbers, require optional -dependencies, please refer to the section "Optional dependencies" below for -details. - -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. - -*** Installing libantlr3c: ANTLR parser generator C support library - -For libantlr3c, you can use the convenience script in -contrib/get-antlr-3.4. This will download, patch, and install -libantlr3c. On a 32-bit machine, or if you have difficulty building -libantlr3c (or difficulty getting CVC4 to link against it later), you -may need to remove the --enable-64bit part in the script. (If you're -curious, the manual instructions are at -http://cvc4.cs.stanford.edu/wiki/Developer%27s_Guide#ANTLR3 .) - -*** Installing the Boost C++ base libraries - -A Boost package is available on most Linux distributions and Homebrew; check -yours for a package named something like libboost-dev or boost-devel. There -are a number of additional Boost packages in some distributions, but this -"basic" one should be sufficient for building CVC4. - -Should you want to install Boost manually, or to learn more about the -Boost project, please visit http://www.boost.org/. - -*** Optional dependencies - -None of these is required, but can improve CVC4 as described below: - - Optional: SymFPU (an implementation of SMT-LIB/IEEE-754 floating-point - operations in terms of bit-vector operations) - Optional: CaDiCaL (optional SAT solver) - Optional: CryptoMiniSat (optional SAT solver) - Optional: LFSC (the LFSC proof checker) - Optional: SWIG 3.0.x (Simplified Wrapper and Interface Generator) - Optional: CLN v1.3 or newer (Class Library for Numbers) - Optional: glpk-cut-log (A fork of the GNU Linear Programming Kit) - Optional: ABC library (for improved bitvector support) - Optional: GNU Readline library (for an improved interactive experience) - Optional: The Boost C++ threading library (libboost_thread) - Optional: CxxTest unit testing framework - -SymFPU is required for supporting the theory of floating-point numbers. It can -be installed using the contrib/get-symfpu script. Use --with-symfpu when -configuring CVC4 to build with the dependency. - -CaDiCaL is a SAT solver that can be used for solving non-incremental bit-vector -problems when using eager bit-blasting. This dependency may improve -performance. It can be installed using the contrib/get-cadical script. Use ---with-cadical when configuring CVC4 to build with this dependency. - -CryptoMiniSat is a SAT solver that can be used for solving bit-vector problems -when using eager bit-blasting. This dependency may improve performance. It can -be installed using the contrib/get-cryptominisat script. Use ---with-cryptominisat when configuring CVC4 to build with this dependency. - -LFSC is required to check proofs internally with --check-proofs. It can be -installed using the contrib/get-lfsc script. Use --with-lfsc when configuring -CVC4 to build with this dependency. - -SWIG is necessary to build the Java API (and of course a JDK is -necessary, too). SWIG 1.x/2.x won't work; you'll need 3.0, and the more -recent the better. See "Language bindings" below for build instructions. - -CLN is an alternative multiprecision arithmetic package that can offer -better performance and memory footprint than GMP. CLN is covered by -the GNU General Public License, version 3; so if you choose to use -CVC4 with CLN support, you are licensing CVC4 under that same license. -(Usually CVC4's license is more permissive than GPL is; see the file -COPYING in the CVC4 source distribution for details.) Please visit -http://www.ginac.de/CLN/ for more details about CLN. - -glpk-cut-log is a fork of GLPK (the GNU Linear Programming Kit). -This can be used to speed up certain classes of problems for the arithmetic -implementation in CVC4. (This is not recommended for most users.) The source -code for glpk-cut-log is available at: -https://github.com/timothy-king/glpk-cut-log/ -The only option for installation of glpk-cut-log is downloading the library, -compiling and installing it manually. CVC4 is no longer compatible with the -main GLPK library. GLPK and glpk-cut-log are covered by the GNU General Public -License, version 3; so if you choose to use CVC4 with GLPK support, you are -licensing CVC4 under that same license. -(Usually CVC4's license is more permissive; see above discussion.) -Please visit http://www.gnu.org/software/glpk/ for more details about GLPK. - -ABC: A System for Sequential Synthesis and Verification is a library -for synthesis and verification of logic circuits. This can be used to -speed up the eager bit-vector solver by first encoding the bit-blasted -formula into AIG format and then using ABC to simplify the AIG. To -install abc run the contrib/get-abc script which will download and -install a compatible version of ABC in the cvc4 directory. To configure -CVC4 to use abc configure with --with-abc and --with-abc-dir=PATH, where -PATH corresponds to the install path of ABC. To run CVC4 using ABC use -the --bitblast-aig command line argument. -Please visit http://www.eecs.berkeley.edu/~alanmi/abc/ for more details -on ABC. - -The GNU Readline library is optionally used to provide command -editing, tab completion, and history functionality at the CVC prompt -(when running in interactive mode). Check your distribution for a -package named "libreadline-dev" or "readline-devel" or similar. This -library is covered by the GNU General Public License, version 3. Like -the above-mentioned libraries, if you choose to use CVC4 with readline -support, you are licensing CVC4 under that same license. (Please visit -http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html for more -details about readline.) - -The Boost C++ threading library (often packaged independently of the -Boost base library) is needed to run CVC4 in "portfolio" -(multithreaded) mode. Check your distribution for a package named -"libboost-thread-dev" or similar. - -CxxTest is necessary to run CVC4's unit tests (included with the -distribution). Running these is not really required for users of -CVC4; "make check" will skip unit tests if CxxTest isn't available, -and go on to run the extensive system- and regression-tests in the -source tree. However, if you're interested, you can download CxxTest -at http://cxxtest.com/ . - -*** Building CVC4 - -Once the build dependencies are satisfied, you should be able to configure, -make, make check, and make install without incident: - - ./autogen.sh [not required when building from a source distribution] - ./configure [use --prefix to specify a prefix; default /usr/local - use --with-* to use optional dependencies] - make - make check [optional but a good idea!] - -To build from a repository checkout (rather than a distributed CVC4 -tarball), there are additional dependencies; see below. - -You can then "make install" to install in the prefix you gave to -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 API documentation, use "make doc". Documentation is produced -under doc/ but is not installed by "make install". - -Examples and tutorials are not installed with "make install." You may -want to "make install-examples". See below. - -For more information about the build system itself (probably not -necessary for casual users), see the Appendix at the bottom of this -file. - -*** Language bindings - -There are several options available for using CVC4 from the API. - -First, CVC4 offers a complete and flexible API for manipulating -expressions, maintaining a stack of assertions, and checking -satisfiability, and related things. The C++ libraries (libcvc4.so and -libcvc4parser.so) and required headers are installed normally via a -"make install". This API is also available from Java (via CVC4.jar -and libcvc4jni.so) by configuring with --enable-language-bindings=java. -You'll also need SWIG 2.0 installed (and you might need to help -configure find it if you installed it in a nonstandard place with ---with-swig-dir=/path/to/swig/installation). You may also need to -give the configure script the path to your Java headers (in -particular, jni.h). You might do so with (for example): - - ./configure --enable-language-bindings=java \ - JAVA_CPPFLAGS=-I/usr/lib/jvm/java-6-openjdk-amd64/include - -The examples/ directory includes some basic examples (the "simple vc" family of -examples) of all these interfaces. - -In principle, since we use SWIG to generate the native Java API, we -could support other languages as well. However, using CVC4 from other -languages is not supported, nor expected to work, at this time. If -you're interested in helping to develop, maintain, and test a language -binding, please contact one of the project leaders. - -*** Building CVC4 from a repository checkout - -CVC4's main repository is kept on GitHub at: - - https://github.com/CVC4/CVC4 - -and there are numerous experimental forks housed on GitHub as well, -by different developers, implementing various features. - -The following tools and libraries are additionally required to build -CVC4 from from a repository checkout rather than from a prepared -source tarball. - - Automake v1.11 or later - Autoconf v2.61 or later - Libtool v2.2 or later - ANTLR3 v3.2 or v3.4 - Python (2.x or 3.x) - -First, use "./autogen.sh" to create the configure script. Then proceed as -normal for any distribution tarball. The parsers are pre-generated for the -tarballs, but don't exist in the repository; hence the extra ANTLR3 requirement -to generate the source code for the parsers, when building from the repository. -Similarly, Python is required for generating some of the code. - -*** Examples and tutorials are not built or installed - -Examples are not built by "make" or "make install". See -examples/README for information on what to find in the examples/ -directory, as well as information about building and installing them. - -*** Appendix: Build architecture - -The build system is generated by automake, libtool, and autoconf. It -is somewhat nonstandard, though, which (for one thing) requires that -GNU Make be used. If you ./configure in the top-level source -directory, the objects will actually all appear in -builds/${arch}/${build_id}. This is to allow multiple, separate -builds in the same place (e.g., an assertions-enabled debugging build -alongside a production build), without changing directories at the -shell. The "current" build is maintained until you re-configure. - -You can also create your own build directory inside or outside of the -source tree and configure from there. All objects will then be built -in that directory, and you'll ultimately find the "cvc4" binary in -src/main/, and the libraries under src/ and src/parser/. |