dLinear: A Delta-Complete SMT Solver for Linear Real Arithmetic

How to Build

Install Prerequisites (Ubuntu 20.04, 18.04, 16.04)

Get the source.

git clone https://github.com/martinjos/dlinear4.git
cd dlinear4

Install the Ubuntu-provided prerequisites: make, autoconf, automake, libtool, bison, flex, GMP, Python 3, and a C++ compiler (either g++ or Clang). If you are using Ubuntu 20.04, 18.04, or 16.04, you can install these (including g++) by running the following commands (or sudo setup/ubuntu/<version>/install_prereqs.sh):

sudo apt-get update
sudo apt-get install bison flex libgmp-dev python3-minimal make autoconf automake libtool
sudo apt-get install g++  # Or: sudo apt-get install clang

Install bazel (a build system by Google, also used by dReal4). Versions 3.1.0 and 3.4.1 have been tested, but later versions should also work. Instructions are provided on the website. Alternatively, you can install version 3.4.1 by running sudo setup/ubuntu/install_bazel.sh - however, this will not set up the apt repository, so you will not get updates.

Build and install the qsopt-ex fork by running setup/setup_qsopt-ex.sh. Note that sudo is NOT required for this step. The library is built under submodules/qsopt-ex and installed into install/qsopt-ex. Note that a normal release of qsopt-ex will not work - it must be this fork.

Build and Test

bazel build //...
bazel test //...        # Run all tests
./dlinear.sh <smt2_file>  # Run .smt2 file

By default, it builds a release build. To build a debug-build, run bazel build //... -c dbg. In macOS, pass --apple_generate_dsym to allow lldb/gdb to show symbols.

Bazel uses the system default compiler. To use a specific compiler, set up CC environment variable. For example, CC=gcc-8.0 bazel build //....

Note that although the program can be run using the script dlinear.sh, the underlying binary executable file is currently still called dreal, for historical reasons. This will probably change in future.