Ensure disequality splits are processed as lemmas (#4380)

[cvc5.git] / INSTALL.md

diff --git a/INSTALL.md b/INSTALL.md
index 2f0c7a051b678b3507564bf080c4a4761e47bf84..17d31fe1a4ccb8b93cf9abfc246312eb54d732fa 100644 (file)
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -1,6 +1,19 @@
-CVC4 prerelease version 1.7.
+CVC4 prerelease version 1.8.
 ============================
 
+## Building CVC4
+
+    ./contrib/get-antlr-3.4  # download and build ANTLR
+    ./configure.sh   # use --prefix to specify a prefix (default: /usr/local)
+                     # use --name=<PATH> for custom build directory
+    cd <build_dir>   # default is ./build
+    make             # use -jN for parallel build with N threads
+    make check       # to run default set of tests
+    make install     # to install into the prefix specified above
+
+All binaries are built into `<build_dir>/bin`, the CVC4 library is built into
+`<build_dir>/lib`.
+
 ## Supported Operating Systems
 
 CVC4 can be built on Linux and macOS.  For Windows, CVC4 can be cross-compiled
@@ -10,6 +23,21 @@ 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 .
 
+### Cross-compiling for Windows
+
+Cross-compiling CVC4 with Mingw-w64 can be done as follows:
+
+```
+  HOST=x86_64-w64-mingw32 ./contrib/get-win-dependencies
+  ./configure --win64 --static <configure options...>
+
+  cd <build_dir>   # default is ./build
+  make             # use -jN for parallel build with N threads
+```
+
+The built binary `cvc4.exe` is located in `<build_dir>/bin` and the CVC4 library
+can be found in `<build_dir>/lib`.
+
 ## Build dependencies
 
 The following tools and libraries are required to build and run CVC4.  
@@ -21,15 +49,17 @@ compatible.
 - [CMake >= 3.1](https://cmake.org)
 - [GNU Bash](https://www.gnu.org/software/bash/)
 - [Python >= 2.7](https://www.python.org)
+  + module [toml](https://pypi.org/project/toml/)
 - [GMP v4.2 (GNU Multi-Precision arithmetic library)](https://gmplib.org)
 - [libantlr3c v3.2 or v3.4 (ANTLR parser generator C support library)](http://www.antlr3.org/)
+- [Java >= 1.6](https://www.java.com)
 
 Some features, such as the theory of floating-point numbers, require
 [optional dependencies](optional-dependencies) (see below).
 
 ### Installing libantlr3c: ANTLR parser generator C support library
 
-For libantlr3c, you can use the script contrib/get-antlr-3.4.
+For libantlr3c, you can use the script `contrib/get-antlr-3.4`.
 This will download, patch, and install libantlr3c.
 
 If you're on a 32-bit machine, or if you have difficulty building
@@ -80,7 +110,7 @@ Configure CVC4 with `configure.sh --lfsc` to build with this dependency.
 ### SWIG >= 3.0.x (Simplified Wrapper and Interface Generator)
 
 SWIG 3.0.x (and a JDK) is necessary to build the Java API.
-See [Language Bindings](language-bindings) below for build instructions.
+See [Language Bindings](#language-bindings) below for build instructions.
 
 ### CLN >= v1.3 (Class Library for Numbers)
 
@@ -151,21 +181,10 @@ provided with CVC4.
 ### CxxTest Unit Testing Framework (Unit Tests)
 
 [CxxTest](http://cxxtest.com) is required to optionally run CVC4's unit tests
-(included with the distribution). See [Testing](testing) below for more details.
+(included with the distribution). 
+See [Testing CVC4](#Testing-CVC4) below for more details.
 
 
-## Building CVC4
-
-    ./configure.sh   # use --prefix to specify a prefix (default: /usr/local)
-                     # use --name=<PATH> for custom build directory
-    cd <build_dir>   # default is ./build
-    make             # use -jN for parallel build with N threads
-    make check       # to run default set of tests
-    make install     # to install into the prefix specified above
-
-All binaries are built into `<build_dir>/bin`, the CVC4 library is built into
-`<build_dir>/src`.
-
 ## Language bindings
 
 CVC4 provides a complete and flexible C++ API (see `examples/api` for examples).
@@ -297,7 +316,7 @@ All custom test targets build and run a preconfigured set of tests.
 
 - `make check [-jN] [ARGS=-jN]`  
   The default build-and-test target for CVC4, builds and runs all examples,
-  all system and unit tests, and regression tests from levels 0 and 1.
+  all system and unit tests, and regression tests from levels 0 to 2.
 
 - `make systemtests [-jN] [ARGS=-jN]`  
   Build and run all system tests.
@@ -306,7 +325,7 @@ All custom test targets build and run a preconfigured set of tests.
   Build and run all unit tests.
 
 - `make regress [-jN] [ARGS=-jN]`  
-  Build and run all regression tests.
+  Build and run regression tests from levels 0 to 2.
 
 - `make runexamples [-jN] [ARGS=-jN]`  
   Build and run all examples.