Skip to content

Commit

Permalink
docs: update documentation
Browse files Browse the repository at this point in the history
  • Loading branch information
TendTo committed Jun 20, 2024
1 parent 7e203db commit 055ded1
Show file tree
Hide file tree
Showing 13 changed files with 162 additions and 116 deletions.
7 changes: 1 addition & 6 deletions MODULE.bazel
Original file line number Diff line number Diff line change
Expand Up @@ -64,12 +64,7 @@ git_override(
)

# MIT | rules for dealing with target dependencies
bazel_dep(name = "depend_on_what_you_use", version = "0.0.0", dev_dependency = True)
git_override(
module_name = "depend_on_what_you_use",
commit = "b817c225d79c492c25b28872445e34be4a36d5aa",
remote = "https://github.com/martis42/depend_on_what_you_use",
)
bazel_dep(name = "depend_on_what_you_use", version = "0.3.0", dev_dependency = True)

# Repository dependencies (see WORKSPACE for more details)

Expand Down
61 changes: 38 additions & 23 deletions MODULE.bazel.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

79 changes: 7 additions & 72 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,38 +7,25 @@
Delta-complete SMT solver for linear programming.
Fork of [dlinear4](https://github.com/martinjos/dlinear4) and [dReal4](https://github.com/dreal/dreal4).

## Installation
### 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](https://tendto.github.io/dlinear/md_docs_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](docs/Installation.md).

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

## Usage
### Usage

For more information, refer to the [usage guide](https://tendto.github.io/dlinear/md_docs_Usage).
For more information, refer to the [usage guide](docs/Usage.md).

```bash
dlinear --help
```

## Default parsing and solving behavior

dlinear will parse and solve problems in `smt2` or `mps` format.
The default behavior is to parse the input and produce a satisfiability result, either `delta-sat` or `unsat`.

> [!warning]
> Some `smt` directives will be ignored, since their role is taken by the command line flags:
>
> - `(check-sat)` is assumed to be present by default. It can be disabled with `--no-check-sat`
> - `(produce-models)` is ignored by default. It can be enabled with `-m/--produce-models`
> - `(minimize)`/`(maximize)` are ignored by default. They can be enabled with `-m/--produce-models`
>
> This also implies that, when parsing a `mps` file, the objective function is ignored, unless the `-m/--produce-models` flag is used.
### Useful commands

```bash
Expand Down Expand Up @@ -79,63 +66,11 @@ bazel test --test_tag_filters=pydlinear //pydlinear/...
bazel run //benchmark
```

### Compilation flags

- `--//tools:enable_dynamic_build=[True|False]` to enable or disable dynamic linking. Used for the python bindings. Default is `False`

## Enabling autocompletion

### On Ubuntu
### Enabling autocompletion on Ubuntu

```bash
# 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
```

## Install Python bindings

### Requirements

- [python-dev](https://packages.ubuntu.com/bionic/python-dev)

### Install

```bash
pip install .
# For development
pip install -e .
```

### Upload to PyPI

```bash
script/upload_pydlinear.sh
```

### Running dlinear from Python

If the package has been installed, either locally or from PyPI, it can be invoked with the same command as the binary.

```bash
pydlinear --help
```

Furthermore, the `pydlinear` module can be imported and used as a library.

```python
import sys
import pydlinear as pdl


def main():
config = pdl.Config.from_command_line(sys.argv)
with pdl.Solver(config) as s:
print(s.CheckSat())


if __name__ == "__main__":
main()

```
5 changes: 4 additions & 1 deletion dlinear/parser/mps/BUILD.bazel
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,10 @@ dlinear_cc_library(
"//tools:pydlinear_build": ["DLINEAR_PYDLINEAR"],
"//conditions:default": [],
}),
tags = ["no-iwyu"],
tags = [
"no-dwyu",
"no-iwyu",
],
deps = [
":mps_data",
"//dlinear/libs:gmp",
Expand Down
5 changes: 4 additions & 1 deletion dlinear/parser/smt2/BUILD.bazel
Original file line number Diff line number Diff line change
Expand Up @@ -107,7 +107,10 @@ dlinear_cc_library(
"//tools:pydlinear_build": ["DLINEAR_PYDLINEAR"],
"//conditions:default": [],
}),
tags = ["no-iwyu"],
tags = [
"no-dwyu",
"no-iwyu",
],
deps = [
":function_definition",
":term",
Expand Down
7 changes: 4 additions & 3 deletions dlinear/solver/BUILD.bazel
Original file line number Diff line number Diff line change
Expand Up @@ -170,10 +170,13 @@ dlinear_cc_library(
"CompleteSoplexTheorySolver.h",
"DeltaSoplexTheorySolver.h",
"SoplexTheorySolver.h",
"//dlinear/util:stats",
],
"//conditions:default": [],
}),
implementation_deps = [
"//dlinear/util:exception",
"//dlinear/util:timer",
],
deps = [
":lp_bound",
":lp_sense",
Expand All @@ -187,8 +190,6 @@ dlinear_cc_library(
"//dlinear/util:bit_increment_iterator",
"//dlinear/util:box",
"//dlinear/util:config",
"//dlinear/util:exception",
"//dlinear/util:infinity",
"//dlinear/util:logging",
"//dlinear/util:stats",
] + select({
Expand Down
11 changes: 7 additions & 4 deletions dlinear/symbolic/BUILD.bazel
Original file line number Diff line number Diff line change
Expand Up @@ -173,14 +173,17 @@ dlinear_cc_library(
name = "tseitin_cnfizer",
srcs = ["TseitinCnfizer.cpp"],
hdrs = ["TseitinCnfizer.h"],
implementation_deps = [
"//dlinear/util:exception",
"//dlinear/util:stats",
"//dlinear/util:timer",
],
deps = [
":cnfizer",
":formula_visitor",
":literal",
":symbolic",
"//dlinear/util:exception",
"//dlinear/util:logging",
"//dlinear/util:stats",
"//dlinear/util:timer",
"//dlinear/util:config",
],
)

Expand Down
Loading

0 comments on commit 055ded1

Please sign in to comment.