dReal: An SMT Solver for Nonlinear Theories of Reals
macOS 13 / 12 / 11:
/usr/bin/curl -fsSL https://raw.githubusercontent.com/dreal/dreal4/master/setup/mac/install.sh | bash
drealUbuntu 22.04 / 20.04:
# 22.04
sudo apt-get install curl
curl -fsSL https://raw.githubusercontent.com/dreal/dreal4/master/setup/ubuntu/22.04/install.sh | sudo bash
# 20.04
sudo apt-get install curl
curl -fsSL https://raw.githubusercontent.com/dreal/dreal4/master/setup/ubuntu/20.04/install.sh | sudo bash
# Test the installation.
DREAL_VERSION=4.21.06.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 drealNote 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 13 / 12 / 11:
git clone https://github.com/dreal/dreal4 && cd dreal4
./setup/mac/install_prereqs.shUbuntu 22.04 / 20.04
git clone https://github.com/dreal/dreal4 && cd dreal4
sudo ./setup/ubuntu/`lsb_release -r -s`/install_prereqs.shThe install_prereqs.sh installs the following packages:
bazel,
bison,
coinor-clp,
flex,
gmp,
ibex,
nlopt,
python.
bazel build //...
bazel test //... # Run all tests
./bazel-bin/dreal/dreal <smt2_file> # Run .smt2 fileBy 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-10, clang-11, clang-12, clang-13, clang-14, gcc-9, gcc-10, gcc-11, gcc-12
- 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 //:compdbWe 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 13 / 12 / 11:
export PKG_CONFIG_PATH=/usr/local/opt/[email protected]/share/pkgconfig:${PKG_CONFIG_PATH}Ubuntu 22.04 / 20.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).
-h, -help, --help, --usage Display usage instructions.
-j, --jobs ARG Number of jobs.
-v, --version Print version number of dReal.
--debug-parsing Debug parsing
--debug-scanning Debug scanning/lexing
--forall-polytope Use polytope contractor in forall contractor.
--format ARG File format. Any one of these (default = auto):
smt2, dr, auto (use file extension)
--in Read from standard input. Uses smt2 by default.
--local-optimization Use local optimization algorithm for exist-forall
problems.
--model, --produce-models Produce models if delta-sat
--nlopt-ftol-abs ARG [NLopt] Absolute tolerance on function value
(default = 1e-06)
--nlopt-ftol-rel ARG [NLopt] Relative tolerance on function value
(default = 1e-06)
--nlopt-maxeval ARG [NLopt] Number of maximum function evaluations
(default = 100)
--nlopt-maxtime ARG [NLopt] Maximum optimization time (in second)
(default = 0.01 sec)
--polytope Use polytope contractor.
--precision ARG Precision (default = 0.001)
--random-seed ARG Set a seed for the random number generator.
--sat-default-phase ARG Set default initial phase for SAT solver.
0 = false
1 = true
2 = Jeroslow-Wang (default)
3 = random initial phase
--smtlib2-compliant Strictly follow the smtlib2 standard.
--verbose ARG Verbosity level. Either one of these (default =
error):
trace, debug, info, warning, error, critical, off
--worklist-fixpoint Use worklist fixpoint algorithm in ICP.
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent