m2csmt 0.1.2

A solver for systems of non-linear (in)equations
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121

[![crates.io](https://img.shields.io/crates/v/m2csmt.svg)](https://crates.io/crates/m2csmt)
[![docs](https://img.shields.io/docsrs/m2csmt)](https://docs.rs/m2csmt)

# m2cSMT

m2cSMT is a solver of non-linear (in)equations encoded in a subset of the [SMT-Lib format](https://smt-lib.org/language.shtml).  One possible use is to solve trigonometric configuration problems.

m2cSMT uses Interval Constraint Propagation on floating point intervals, with outward-directed rounding of computations.

## Installation

To run a file from the command line, install rust, download this repository and, in the root of the folder:

```bash
cargo run -- path/to/your/file.smt2
```

To include the library in a rust project, add to `cargo.toml`:

```toml
[dependencies]
m2csmt = "0"
```

and to `.cargo/config.toml`:

```toml
[build]
rustflags = ["-C", "target-cpu=haswell"]
rustdocflags = ["-C", "target-cpu=haswell"]
```

## Usage

To solve `x²-2x+1 = 0`, create file `demo.smt2`:

```smt2
(declare-const x Real)
(assert (= (+ (** x 2) (* -2.0 x) 1.0) 0.0))
(check-sat)
(get-model)
```

Run it with :

```bash
cargo run -- path/to/demo.smt2
```

You should get:

```text
delta_sat with absolute precision 0.0005027206300594056
x = [0.998001,0.998252]
```

The equation is indeed satisfied with a precision of `0.0005`.

You can obtain the same results in rust:

```rust
    use m2csmt::solver::Solver;
    let source = "
        (declare-const x Real)
        (assert (= (+ (** x 2) (* -2.0 x) 1.0) 0.0))
        (check-sat)
        (get-model)";

    let mut solver = Solver::default();
    for result in solver.parse_and_execute(source) {
        println!("{}", result)
    }
```

Or, using the Command API:

```rust
    use m2csmt::solver::Solver;
    use m2csmt::api::{{Command, Term}};
    use m2csmt::*;

    let source = vec![
        DeclareConst!("x", "Real"),
        Assert!(F!("=",
                    F!("**", Symbol!("x"), Integer!(2))
                        + Real!(-2.0) * Symbol!("x")
                        + Real!(1.0),
                    Real!(0.0))),
        CheckSat!(),
        GetModel!()
        ];
    let mut solver = Solver::default();
    for result in solver.execute(source) {
        println!("{}", result.unwrap())
    }
```

## Support

Please report errors and suggestions via issues in [the Gitlab repository](https://gitlab.com/pierre.carbonnelle/m2csmt).

## Roadmap

Future developments include:

* improve performance, e.g., by using the derivative of the formula.
* extend it with a boolean satisifiability solver.

## Contributing

Contributions are welcome: issues and suggestions, rust code, realistic benchmarks, ...  In particular, we welcome benchmarks inspired by real-life problems.

The technical documentation is available in the `src/_technical_doc.md` file.

## Authors and acknowledgment

Many thanks to the rust community and, in particular, to the authors of the interval arithmetic library called [inari](https://crates.io/crates/inari).

## License

MIT