dReal: An SMT Solver for Nonlinear Theories of Reals
macOS 10.14 / 10.13 / 10.12:
/usr/bin/curl -fsSL https://raw.githubusercontent.com/dreal/dreal4/master/setup/mac/install.sh | bash
dreal
Ubuntu 18.04 / 16.04:
# 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.18.11.4
/opt/dreal/${DREAL_VERSION}/bin/dreal
Some of the functionality of dReal is accessible via Python2/3. To install the binding, run the following:
pip install dreal
To test it, run python2
or 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 --version # Run "dreal --version"
macOS 10.14 / 10.13 / 10.12:
git clone https://github.com/dreal/dreal4 && cd dreal4
./setup/mac/install_prereqs.sh
Ubuntu 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-8, gcc-7, gcc-6, gcc-5, clang-7.0, clang-6.0, clang-5.0, clang-4.0, clang-3.9
- 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:
./third_party/com_github_grailbio_bazel-compilation-database/generate.sh
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.14 / 10.13 / 10.12:
export PKG_CONFIG_PATH=/usr/local/opt/ibex@2.6.5/share/pkgconfig:${PKG_CONFIG_PATH}
Ubuntu 18.04 / 16.04:
export PKG_CONFIG_PATH=/opt/dreal/4.18.11.4/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).