rust z3 版本 >= v 0.10.0 ast.Bool:: 和函数

Question

铁锈z3 当z3的版本为“v.0.4.0”时，我们可以使用Bool::and函数来表示两个bool变量AND的结果。 但在版本> =“v.0.10.0”时，它出错了。 当使用 and 函数“ boolVar1.and(&[&boolVar2])”时，会出现“在当前范围内没有为 struct 'z3::ast::Bool<'_>' 找到名为 'and' 的方法”。 当看到源码的时候，什么时候可以看到这里的‘and’函数

"
varop! {
        and(Z3_mk_and, Self);
        or(Z3_mk_or, Self);
    }
"

我现在如何使用 func 'and'？

z3版本v.0.10.0

varop! {
    and(Z3_mk_and, Self);
    or(Z3_mk_or, Self);
}

Answer 1

在z3-0.4.0中，

Bool::and

的签名如下：

pub fn and(&self, other: &[&Self]) -> Self

但是，在z3-0.6.0中更改为

pub fn and(context: &'ctx Context, values: &[&Self]) -> Self

使用方法如下：

let exp1: Bool = ... ;
let exp2: Bool = ... ;
let and_exp = exp1.and(&[&exp2]);         // for version < z3-0.6.0
let and_exp = Bool::and(&[&exp1, &exp2]); // for version >= z3-0.6.0