Expand description
Yices2
High level bindings to the Yices2 SMT solver.
Examples
Some examples to demonstrate usage of this library.
Linear Real Arithmetic
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()?, "x")?;
let y = Uninterpreted::with_name(RealType::new()?, "y")?;
let t1 = Add::new(x, y)?;
let t2: Term = ArithmeticGreaterThanAtom::new(t1, ArithmeticConstant::zero()?)?.into();
let t3: Term = Or::new([
ArithmeticLessThanAtom::new(x, ArithmeticConstant::zero()?)?,
ArithmeticLessThanAtom::new(y, ArithmeticConstant::zero()?)?,
])?.into();
ctx.assert([t2, t3])?;
let status = ctx.check()?;
assert_eq!(status, Status::STATUS_SAT);
let xv = ctx.model()?.get_double(x)?;
let yv = ctx.model()?.get_double(y)?;
assert_eq!(xv, 2.0);
assert_eq!(yv, -1.0);
Ok(())
}
BitVectors
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, "x")?;
let y = Uninterpreted::with_name(bv, "y")?;
let a1: Term = BitVectorSignedGreaterThanAtom::new(x, bvc)?.into();
let a2: Term = BitVectorSignedGreaterThanAtom::new(y, bvc)?.into();
let a3: Term = BitVectorSignedLessThanAtom::new(
BitVectorAdd::new(x, y)?,
x,
)?.into();
ctx.assert([a1, a2, a3])?;
assert_eq!(ctx.check()?, Status::STATUS_SAT);
Ok(())
}
Usage
You can add this crate to your project by running:
cargo add yices2
Or by adding this line to your Cargo.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
.
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.
Modules
- Use all items at the top level of this module, makes importing easier by just writing
use yices2::prelude::*;
Macros
- Make a call to the Yices2 API. This macro will automatically report any errors that occur as an
Error
, similar toyices_try!
but returns immediately if there is an error. - Make a call to the Yices2 API. This macro will automatically report any errors that occur as an
Error
.