dReal: An SMT Solver for Nonlinear Theories of Reals
macOS 10.15 / 10.14 / 10.13:
/usr/bin/curl -fsSL https://raw.githubusercontent.com/dreal/dreal4/master/setup/mac/install.sh | bash
dreal
Ubuntu 20.04 / 18.04 / 16.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
# 16.04
sudo apt-get install curl
curl -fsSL https://raw.githubusercontent.com/dreal/dreal4/master/setup/ubuntu/16.04/install.sh | sudo bash
# Test the installation.
DREAL_VERSION=4.20.04.2
/opt/dreal/${DREAL_VERSION}/bin/dreal
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.
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"
macOS 10.15 / 10.14 / 10.13:
git clone https://github.com/dreal/dreal4 && cd dreal4
./setup/mac/install_prereqs.sh
Ubuntu 20.04 / 18.04 / 16.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, ibex, nlopt, python2.7.
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-8.0 bazel build //...
.
In CI, we test that dReal can be built using the following compilers:
- Ubuntu: gcc-10, gcc-9, gcc-8, gcc-7, gcc-6, gcc-5, clang-10, clang-9, clang-8, clang-7, clang-6.0, clang-5.0,
- macOS: Apple clang
Please check https://dreal.github.io/dreal4.
Run bazel build //:package_debian
and find .deb
file in bazel-bin
directory.
To build a Compilation Database, run:
bazel build //:compdb
We have prepared the following example projects using dReal as a library:
If you want to use
pkg-config,
you need to set up PKG_CONFIG_PATH
as follows:
macOS 10.15 / 10.14 / 10.13:
export PKG_CONFIG_PATH=/usr/local/opt/[email protected]/share/pkgconfig:${PKG_CONFIG_PATH}
Ubuntu 20.04 / 18.04 / 16.04:
export PKG_CONFIG_PATH=/opt/dreal/4.20.04.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).