Yices2

Yices 2 SMT求解器的低级和高级Rust绑定。

• Yices2
  • 示例
    • 线性实数算术
    • 位向量
  • 使用
  • 功能

示例

线性实数算术

let config = Config::with_defaults_for_logics([Logic::QF_LRA])?;
let ctx = Context::with_config(&config)?;
let x = Uninterpreted::with_name(Real::new()?.into(), "x")?;
let y = Uninterpreted::with_name(Real::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()?.double(&x.into())?;
let yv = ctx.model()?.double(&y.into())?;
assert_eq!(xv, 2.0);
assert_eq!(yv, -1.0);

位向量

let config = Config::with_defaults_for_logics([Logic::QF_BV])?;
let ctx = Context::with_config(&config)?;
let bv = BitVector::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);

使用

您可以通过运行以下命令将此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 }