soonhokong/dreal4

SMT Solver for Nonlinear Theories of Reals

dReal: An SMT Solver for Nonlinear Theories of Reals

How to Install

macOS 13 / 12 / 11:

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

Ubuntu 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

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 13 / 12 / 11:

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

Ubuntu 22.04 / 20.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-10, clang-11, clang-12, clang-13, clang-14, gcc-9, gcc-10, gcc-11, gcc-12
• 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 13 / 12 / 11:

export PKG_CONFIG_PATH=/usr/local/opt/ibex@2.7.4/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).

Command-line Options

-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.