yices2-sys

Crates.ioyices2-sys
lib.rsyices2-sys
version2.6.4-patch.1
sourcesrc
created_at2023-08-17 16:33:24.657932
updated_at2023-09-01 07:59:07.350186
descriptionLow level Rust bindings to the Yices 2 SMT solver
homepagehttps://yices.csl.sri.com
repositoryhttps://github.com/novafacing/yices2-rs
max_upload_size
id947223
size6,882,958
Rowan Hart (novafacing)

documentation

README

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.

Commit count: 39

cargo fmt