yices2 0.1.2

Rust bindings to the Yices 2 SMT solver
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

# Yices2

Low and high-level Rust bindings to the [Yices2](https://yices.csl.sri.com) SMT solver.

- [Yices2](#yices2)
  - [Example](#example)
    - [Linear Real Arithmetic](#linear-real-arithmetic)
    - [BitVectors](#bitvectors)
  - [Usage](#usage)
  - [Features](#features)
  - [Notes](#notes)

## Example

### Linear Real Arithmetic

```rust,no_run
use yices2::prelude::*;

fn main() -> Result<(), Error> {
  let config = Config::with_defaults_for_logics([Logic::QF_LRA])?;
  let ctx = Context::with_config(&config)?;
  let x = Uninterpreted::with_name(RealType::new()?.into(), "x")?;
  let y = Uninterpreted::with_name(RealType::new()?.into(), "y")?;
  let t1 = Add::new(x.into(), y.into())?;
  let t2 = ArithmeticGreaterThanAtom::new(t1.into(), ArithmeticConstant::zero()?.into())?;
  let t3 = Or::new([
      ArithmeticLessThanAtom::new(x.into(), ArithmeticConstant::zero()?.into())?.into(),
      ArithmeticLessThanAtom::new(y.into(), ArithmeticConstant::zero()?.into())?.into(),
  ])?;
  ctx.assert([t2.into(), t3.into()])?;
  let status = ctx.check()?;
  assert_eq!(status, Status::STATUS_SAT);
  let xv = ctx.model()?.get_double(&x.into())?;
  let yv = ctx.model()?.get_double(&y.into())?;
  assert_eq!(xv, 2.0);
  assert_eq!(yv, -1.0);

  Ok(())
}
```

### BitVectors

```rust,no_run
use yices2::prelude::*;

fn main() -> Result<(), Error> {
  let config = Config::with_defaults_for_logics([Logic::QF_BV])?;
  let ctx = Context::with_config(&config)?;
  let bv = BitVectorType::new(32)?;
  let bvc = BitVectorConstant::from_hex_with_name("00000000", "c")?;
  let x = Uninterpreted::with_name(bv.into(), "x")?;
  let y = Uninterpreted::with_name(bv.into(), "y")?;
  let a1 = BitVectorSignedGreaterThanAtom::new(x.into(), bvc.into())?;
  let a2 = BitVectorSignedGreaterThanAtom::new(y.into(), bvc.into())?;
  let a3 = BitVectorSignedLessThanAtom::new(
      BitVectorAdd::new(x.into(), y.into())?.into(),
      x.into(),
  )?;
  ctx.assert([a1.into(), a2.into(), a3.into()])?;

  assert_eq!(ctx.check()?, Status::STATUS_SAT);

  Ok(())
}
```

## Usage

You can add this crate to your project by running:

```sh
cargo add yices2
```

Or by adding this line to your `Cargo.toml`:

```toml
yices2 = { version = "2.6.4" }
```

## Features

By default, `yices2` enables the `ctor` feature, which calls `yices_init` at program
initialization and `yices_exit` at program exit. If you'd like to disable this behavior,
you can use the `default-features = false` flag in your `Cargo.toml`.

```toml
yices2 = { version = "2.6.4", default-features = false }
```

## Notes

This library is not thread safe, because the underlying `Yices2` library is not thread
safe. Do not use this library in multithreaded code. To use in multi-threaded code,
create a separate process and submit requests to the solver running in that process or
disable the `ctor` feature and manage state yourself.