Dlinear

Delta-complete SMT solver for linear programming. Fork of dlinear4 and dReal4.

Installation

The following instructions are for Linux systems. The installation process for Windows and MacOS is not yet supported. For more information, refer to the installation guide.

bazel build //:package_deb
sudo dpkg -i bazel-bin/dlinear/dlinear.deb

Usage

For more information, refer to the usage guide.

dlinear --help

Useful commands

# Compile dlinear
bazel build //dlinear
# Run dlinear
bazel-bin/dlinear/dlinear

# CPPlint
bazel test //dlinear/...

# Run dlinear unit tests
bazel test --test_tag_filters=dlinear //test/...

# Run dlinear integration tests by solving a bunch of problems
# and confronting the results with the expected ones
bazel test --test_tag_filters=solver //test/...

# Run linting
bazel test --test_tag_filters=cpplint //dlinear/...

# Run pydlinear tests
bazel test --test_tag_filters=pydlinear //pydlinear/...

# Run benchmarks
bazel run //benchmark

Enabling autocompletion on Ubuntu

# Install bash-completion
sudo apt install bash-completion
# Move the completion script to the bash-completion directory
sudo cp script/dlinear_completion.sh /etc/bash_completion.d/dlinear.sh