Low and high-level Rust bindings to the Yices2 SMT solver.
```rust,no_run use yices2::prelude::*;
fn main() -> Result<(), Error> { let config = Config::withdefaultsforlogics([Logic::QFLRA])?; let ctx = Context::withconfig(&config)?; let x = Uninterpreted::withname(RealType::new()?.into(), "x")?; let y = Uninterpreted::withname(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()?; asserteq!(status, Status::STATUSSAT); let xv = ctx.model()?.getdouble(&x.into())?; let yv = ctx.model()?.getdouble(&y.into())?; asserteq!(xv, 2.0); assert_eq!(yv, -1.0);
Ok(()) } ```
```rust,no_run use yices2::prelude::*;
fn main() -> Result<(), Error> { let config = Config::withdefaultsforlogics([Logic::QFBV])?; let ctx = Context::withconfig(&config)?; let bv = BitVectorType::new(32)?; let bvc = BitVectorConstant::fromhexwithname("00000000", "c")?; let x = Uninterpreted::withname(bv.into(), "x")?; let y = Uninterpreted::withname(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()])?;
asserteq!(ctx.check()?, Status::STATUSSAT);
Ok(()) } ```
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" }
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 }
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.