Skip to content

Commit

Permalink
stricter clippy settings
Browse files Browse the repository at this point in the history
  • Loading branch information
@timbeurskens
timbeurskens committed Jan 29, 2024
1 parent bb20cbd commit 1e7fbf7
Show file tree
Hide file tree
Showing 26 changed files with 493 additions and 409 deletions.
95 changes: 46 additions & 49 deletions .devcontainer/devcontainer.json
View file
Original file line number Diff line number Diff line change
@@ -1,55 +1,52 @@
// For format details, see https://aka.ms/devcontainer.json. For config options, see the README at:
// https://github.com/microsoft/vscode-dev-containers/tree/v0.238.1/containers/rust
{
"name": "Rust",
"build": {
"dockerfile": "Dockerfile",
"args": {
// Use the VARIANT arg to pick a Debian OS version: buster, bullseye
// Use bullseye when on local on arm64/Apple Silicon.
"VARIANT": "buster"
}
},
"runArgs": [
"--cap-add=SYS_PTRACE",
"--security-opt",
"seccomp=unconfined"
],
"name": "Rust",
"build": {
"dockerfile": "Dockerfile",
"args": {
// Use the VARIANT arg to pick a Debian OS version: buster, bullseye
// Use bullseye when on local on arm64/Apple Silicon.
"VARIANT": "buster"
}
},
"runArgs": [
"--cap-add=SYS_PTRACE",
"--security-opt",
"seccomp=unconfined"
],
// Configure tool-specific properties.
"customizations": {
// Configure properties specific to VS Code.
"vscode": {
// Set *default* container specific settings.json values on container create.
"settings": {
"lldb.executable": "/usr/bin/lldb",
// VS Code don't watch files under ./target
"files.watcherExclude": {
"**/target/**": true
},
"rust-analyzer.checkOnSave.command": "clippy"
},
// Add the IDs of extensions you want installed when the container is created.
"extensions": [
"vadimcn.vscode-lldb",
"mutantdino.resourcemonitor",
"rust-lang.rust-analyzer",
"tamasfe.even-better-toml",
"serayuzgur.crates"
]
}
},
// Use 'forwardPorts' to make a list of ports inside the container available locally.
// "forwardPorts": [],

// Configure tool-specific properties.
"customizations": {
// Configure properties specific to VS Code.
"vscode": {
// Set *default* container specific settings.json values on container create.
"settings": {
"lldb.executable": "/usr/bin/lldb",
// VS Code don't watch files under ./target
"files.watcherExclude": {
"**/target/**": true
},
"rust-analyzer.checkOnSave.command": "clippy"
},

// Add the IDs of extensions you want installed when the container is created.
"extensions": [
"vadimcn.vscode-lldb",
"mutantdino.resourcemonitor",
"rust-lang.rust-analyzer",
"tamasfe.even-better-toml",
"serayuzgur.crates"
]
}
},
// Use 'postCreateCommand' to run commands after the container is created.
// "postCreateCommand": "rustc --version",

// Use 'forwardPorts' to make a list of ports inside the container available locally.
// "forwardPorts": [],

// Use 'postCreateCommand' to run commands after the container is created.
// "postCreateCommand": "rustc --version",

// Comment out to connect as root instead. More info: https://aka.ms/vscode-remote/containers/non-root.
"remoteUser": "vscode",
"features": {
"git": "latest"
}
// Comment out to connect as root instead. More info: https://aka.ms/vscode-remote/containers/non-root.
"remoteUser": "vscode",
"features": {
"git": "latest"
}
}
10 changes: 5 additions & 5 deletions .github/workflows/rust.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,8 @@ jobs:
runs-on: ubuntu-latest

steps:
- uses: actions/checkout@v2
- name: Build
run: cargo build --verbose --release --examples --bins --lib
- name: Run tests
run: cargo test --verbose --release --workspace
- uses: actions/checkout@v2
- name: Build
run: cargo build --verbose --release --examples --bins --lib
- name: Run tests
run: cargo test --verbose --release --workspace
4 changes: 2 additions & 2 deletions Cargo.lock
View file

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

15 changes: 14 additions & 1 deletion Cargo.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,9 @@ version = "0.14.3"
edition.workspace = true
authors.workspace = true

[lints]
workspace = true

[dependencies]
dot.workspace = true
itertools.workspace = true
Expand All @@ -33,7 +36,7 @@ pretty_assertions.workspace = true

[workspace.dependencies]
dot = "0.1"
itertools = "0.11"
itertools = "0.12"
lazy_static = "1.4"
rand = "0.8"
rustc-hash = "1.1"
Expand All @@ -46,3 +49,13 @@ anyhow = "1.0"
rayon = "1.8"
argfile = "0.1"
wild = "2.2"

[workspace.lints.rust]
unsafe_code = "forbid"

[workspace.lints.clippy]
enum_glob_use = "deny"
#pedantic = "deny"
nursery = "deny"
unwrap_used = "deny"
future_not_send = "allow"
70 changes: 46 additions & 24 deletions README.md
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# RsBDD

[![Rust](https://github.com/timbeurskens/rsbdd/actions/workflows/rust.yml/badge.svg)](https://github.com/timbeurskens/rsbdd/actions/workflows/rust.yml)
[![Rust](https://github.com/timbeurskens/rsbdd/actions/workflows/rust.yml/badge.svg)](https://github.com/timbeurskens/rsbdd/actions/workflows/rust.yml)

_Solving satisfiability problems in Rust_

Expand All @@ -9,11 +9,13 @@ _Solving satisfiability problems in Rust_
1) Make sure to install the [Rust toolchain](https://www.rust-lang.org/tools/install).

2) Clone the latest version of this repository:

```
$ git clone [email protected]:timbeurskens/rsbdd.git
```

3) Build and install the RsBDD tools:

```
$ cd rsbdd
$ cargo install --bins --path .
Expand All @@ -31,11 +33,13 @@ The following tools will be available after installing the RsBDD package:

### Comments

Characters contained within "..." (excluding the " char itself) are regarded as comments and can be placed at any point in the formula.
Characters contained within "..." (excluding the " char itself) are regarded as comments and can be placed at any point
in the formula.

### Constants

The most basic building blocks of the syntax are 'variables' and 'constants'. A constant can be either 'true' or 'false'. A variable can accept either a 'true' or 'false' value after evaluation depending on its environment.
The most basic building blocks of the syntax are 'variables' and 'constants'. A constant can be either 'true' or '
false'. A variable can accept either a 'true' or 'false' value after evaluation depending on its environment.

```
true
Expand All @@ -57,7 +61,8 @@ hello_world

### Negation

A variable, constant, or sub-formula can be negated using the negation operator. This operator can be expressed by either `!`, `-`, or `not`.
A variable, constant, or sub-formula can be negated using the negation operator. This operator can be expressed by
either `!`, `-`, or `not`.

```
not true
Expand All @@ -67,7 +72,8 @@ not true

### Binary operators

RsBDD supports the most common, and some uncommon binary operators, such as conjunction, disjunction, implication and bi-implication.
RsBDD supports the most common, and some uncommon binary operators, such as conjunction, disjunction, implication and
bi-implication.

Most operators have a symbolic and textual representation, e.g. `and` or `&`.

Expand Down Expand Up @@ -106,7 +112,8 @@ a | (a & b)

### If-then-else

A simplification of a common expression `(a => b) & ((!a) => c)` can be made using the ternary if-then-else (ite) operator.
A simplification of a common expression `(a => b) & ((!a) => c)` can be made using the ternary if-then-else (ite)
operator.

```
if a then b else c
Expand All @@ -115,7 +122,8 @@ if exists a # a <=> b then b <=> c else false | c

### Quantifiers

The RsBDD supports universal and existential quantification using the `exists` and `forall`/`all` keywords: `{forall|exists} var_1, var_2, .., var_n # {subformula}`
The RsBDD supports universal and existential quantification using the `exists` and `forall`/`all`
keywords: `{forall|exists} var_1, var_2, .., var_n # {subformula}`

```
forall a # true
Expand All @@ -125,13 +133,17 @@ forall a, b # exists c # (c | a) & (c | b)

### Counting

For some problems it can be beneficial to express properties relating to the number of true or false variables, e.g. "at least 2 of the 4 properties must hold".
For some problems it can be beneficial to express properties relating to the number of true or false variables, e.g. "at
least 2 of the 4 properties must hold".

The counting operator (`[]`) in combination with five new equality and inequality operators (`=`, `<=`, `>=`, `<`, `>`) can be used to concisely express these properties.
The counting operator (`[]`) in combination with five new equality and inequality operators (`=`, `<=`, `>=`, `<`, `>`)
can be used to concisely express these properties.

_Note:_ like most operators, the counting operator can be expressed using logic primitives, but this operator simplifies the expression significantly.
_Note:_ like most operators, the counting operator can be expressed using logic primitives, but this operator simplifies
the expression significantly.

A counting comparison can either be made by comparing a set of expressions to a given constant, or an other set of expressions.
A counting comparison can either be made by comparing a set of expressions to a given constant, or an other set of
expressions.

```
"exactly one of a, b, and c holds"
Expand Down Expand Up @@ -167,9 +179,12 @@ forall _a,_b,_c,_d,_e,_f,_g # (

### Fixed points

The rsbdd language supports least-fixpoint (`lfp` / `mu`) and greatest-fixpoint (`gfp` / `nu`) operations to find a respectively minimal or maximal solution by repeatedly applying a given transformer function until the solution is stable.
The rsbdd language supports least-fixpoint (`lfp` / `mu`) and greatest-fixpoint (`gfp` / `nu`) operations to find a
respectively minimal or maximal solution by repeatedly applying a given transformer function until the solution is
stable.

Only monotonic transformer functions are guaranteed to terminate. Termination of fixed point operations are not checked and will run indefinatedly if not handled correctly.
Only monotonic transformer functions are guaranteed to terminate. Termination of fixed point operations are not checked
and will run indefinatedly if not handled correctly.

Its basic properties are defined as follows.

Expand All @@ -187,13 +202,17 @@ gfp/lfp X # false <=> false

### Parse-tree display

Adding the `-p {path}` argument to `rsbdd` constructs a graphviz graph of the parse-tree. This can be used to for introspection of the intended formula, or for reporting purposes. An example of the parse-tree output for `exists b,c # a | (b ^ c)` is displayed below.
Adding the `-p {path}` argument to `rsbdd` constructs a graphviz graph of the parse-tree. This can be used to for
introspection of the intended formula, or for reporting purposes. An example of the parse-tree output
for `exists b,c # a | (b ^ c)` is displayed below.

![parse tree](docs/images/parsetree.svg)

### Experimental and/or upcoming features

Currently the RsBDD language relies heavily on logical primitives. Integer arithmetic could be expressed by manually introducing the primitive 'bits' of a number. Rewrite rules could significantly simplify this process by introducting domains other than boolean variables. Embedding rewrite rules in the BDD could prove to be a challenge.
Currently the RsBDD language relies heavily on logical primitives. Integer arithmetic could be expressed by manually
introducing the primitive 'bits' of a number. Rewrite rules could significantly simplify this process by introducting
domains other than boolean variables. Embedding rewrite rules in the BDD could prove to be a challenge.

## Examples

Expand All @@ -206,9 +225,12 @@ Currently the RsBDD language relies heavily on logical primitives. Integer arith
### Example 2: the 4 queens problem

The famous n-queens problem can be expressed efficiently in the RsBDD language.
The example below shows a 4-queens variant, which can be solved in roughly 15 milliseconds. The library contains a generator for arbitrary n-queens problems.
At this point, the largest verified problem size is n=8, which reports all solutions in less than 20 minutes on modern hardware.
The explosive nature of the problem makes n=9 an infeasable problem. Further optimizations (such as multi-processor parallellism, or vertex ordering) could decrease the run-time in the future.
The example below shows a 4-queens variant, which can be solved in roughly 15 milliseconds. The library contains a
generator for arbitrary n-queens problems.
At this point, the largest verified problem size is n=8, which reports all solutions in less than 20 minutes on modern
hardware.
The explosive nature of the problem makes n=9 an infeasable problem. Further optimizations (such as multi-processor
parallellism, or vertex ordering) could decrease the run-time in the future.

```
"every row must contain exactly one queen"
Expand Down Expand Up @@ -242,17 +264,17 @@ The explosive nature of the problem makes n=9 an infeasable problem. Further opt
[_3x0] <= 1
```

Running this example with the following arguments yields a truth-table showing the queen configuration(s) on a 4x4 chess board.
Running this example with the following arguments yields a truth-table showing the queen configuration(s) on a 4x4 chess
board.

```bash
rsbdd -i examples/4_queens.txt -t -ft
```

| _0x0 | _0x1 | _0x2 | _0x3 | _1x0 | _1x1 | _1x2 | _1x3 | _2x0 | _2x1 | _2x2 | _2x3 | _3x0 | _3x1 | _3x2 | _3x3 | * |
|-------|-------|-------|-------|-------|-------|-------|-------|-------|-------|-------|-------|-------|-------|-------|-------|-------|
| False | False | True | False | True | False | False | False | False | False | False | True | False | True | False | False | True |
| False | True | False | False | False | False | False | True | True | False | False | False | False | False | True | False | True |

| _0x0 | _0x1 | _0x2 | _0x3 | _1x0 | _1x1 | _1x2 | _1x3 | _2x0 | _2x1 | _2x2 | _2x3 | _3x0 | _3x1 | _3x2 | _3x3 | * |
|-------|-------|-------|-------|-------|-------|-------|-------|-------|-------|-------|-------|-------|-------|-------|-------|------|
| False | False | True | False | True | False | False | False | False | False | False | True | False | True | False | False | True |
| False | True | False | False | False | False | False | True | True | False | False | False | False | False | True | False | True |

## CLI Usage

Expand Down
Loading

0 comments on commit 1e7fbf7

Please sign in to comment.