m2cSMT

m2cSMT is a solver of non-linear (in)equations encoded in a subset of the SMT-Lib format. 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:

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

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

[dependencies]
m2csmt = "0"

and to .cargo/config.toml:

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

Usage

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

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

Run it with :

cargo run -- path/to/demo.smt2

You should get:

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:

    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:

    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.

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.

License

MIT