[![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