dReal: An SMT Solver for Nonlinear Theories of Reals

How to Install

macOS 11.0 / 10.15 / 10.14:

/usr/bin/curl -fsSL https://raw.githubusercontent.com/dreal/dreal4/master/setup/mac/install.sh | bash
dreal

Ubuntu 20.04 / 18.04:

# 20.04
sudo apt-get install curl
curl -fsSL https://raw.githubusercontent.com/dreal/dreal4/master/setup/ubuntu/20.04/install.sh | sudo bash

# 18.04
sudo apt-get install curl
curl -fsSL https://raw.githubusercontent.com/dreal/dreal4/master/setup/ubuntu/18.04/install.sh | sudo bash

# Test the installation.
DREAL_VERSION=4.21.06.2
/opt/dreal/${DREAL_VERSION}/bin/dreal

Python Binding

Some of the functionality of dReal is accessible via Python3. To install the binding, run the following:

pip3 install dreal

Note that you still need to install dReal prerequisites such as IBEX and CLP in your system. Please follow the instructions.

To test the Python binding, run python3 in a terminal and type the followings:

from dreal import *

x = Variable("x")
y = Variable("y")
z = Variable("z")

f_sat = And(0 <= x, x <= 10,
            0 <= y, y <= 10,
            0 <= z, z <= 10,
            sin(x) + cos(y) == z)

result = CheckSatisfiability(f_sat, 0.001)
print(result)

The last print statement should give:

x : [1.247234518484574339, 1.247580203674002686]
y : [8.929064928123818135, 8.929756298502674383]
z : [0.06815055407334302817, 0.06858905276351445757]

More examples are available at dreal4/dreal/test/python.

Docker

We provide a Docker image of dReal4 which is based on Ubuntu 18.04. Try the following to test it:

docker pull dreal/dreal4
docker run --rm dreal/dreal4 dreal -h  # Run "dreal -h"

How to Build

Install Prerequisites

macOS 11.0 / 10.15 / 10.14:

git clone https://github.com/dreal/dreal4 && cd dreal4
./setup/mac/install_prereqs.sh

Ubuntu 20.04 / 18.04

git clone https://github.com/dreal/dreal4 && cd dreal4
sudo ./setup/ubuntu/`lsb_release -r -s`/install_prereqs.sh

The install_prereqs.sh installs the following packages: bazel, bison, coinor-clp, flex, gmp, ibex, nlopt, python.

Build and Test

bazel build //...
bazel test //...                     # Run all tests
./bazel-bin/dreal/dreal <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-7 bazel build //....

In CI, we test that dReal can be built using the following compilers:

• Ubuntu: clang-9, clang-10, clang-11, gcc-7, gcc-9, gcc-10
• macOS: Apple clang

C++ Documentation

Please check https://dreal.github.io/dreal4.

Build Debian Package

Run bazel build //:package_debian and find .deb file in bazel-bin directory.

How to Build Compilation Database

To build a Compilation Database, run:

bazel build //:compdb

How to Use dReal as a Library

We have prepared the following example projects using dReal as a library:

• dreal-cmake-example-project
• dreal-bazel-example-project

If you want to use pkg-config, you need to set up PKG_CONFIG_PATH as follows:

macOS 11.0 / 10.15 / 10.14:

export PKG_CONFIG_PATH=/usr/local/opt/ibex@2.7.4/share/pkgconfig:${PKG_CONFIG_PATH}

Ubuntu 20.04 / 18.04:

export PKG_CONFIG_PATH=/opt/dreal/4.21.06.2/lib/pkgconfig:/opt/libibex/2.7.4/share/pkgconfig:${PKG_CONFIG_PATH}

Then, pkg-config dreal --cflags and pkg-config dreal --libs should provide necessary information to use dReal. Note that setting up PKG_CONFIG_PATH is necessary to avoid possible conflicts (i.e. with ibex formula in Mac).