Yices2

对 Yices2 SMT 求解器的高级绑定。

示例

一些示例，展示该库的使用。

线性实数算术

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(())
}

位向量

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(())
}

使用方法

您可以通过运行以下命令将此 crate 添加到您的项目中

cargo add yices2

或者通过将此行添加到您的 Cargo.toml

yices2 = { version = "2.6.4" }

特性

默认情况下，yices2 启用了 ctor 特性，该特性在程序初始化时调用 yices_init，在程序退出时调用 yices_exit。如果您想禁用此行为，可以在您的 Cargo.toml 中使用 default-features = false 标志。

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

注意

由于底层 Yices2 库不是线程安全的，因此此库不是线程安全的。不要在多线程代码中使用此库。要在多线程代码中使用，请创建一个单独的进程，并向在该进程中运行的求解器提交请求，或者禁用 ctor 特性并自行管理状态。