rust z3 version >= v 0.10.0 ast.Bool::and function

Question

Rust z3 When the version of z3 is "v.0.4.0", we could use Bool::and function to represents the result of the AND of two bool variables. But in version >= "v.0.10.0",it went wrong. "no method named 'and' found for struct 'z3::ast::Bool<'_>' in the current scope" occurs when used and function " boolVar1.and(&[&boolVar2])". When see the source code, when can see the 'and' func in here

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

How can i use the func 'and' now?

z3 version v.0.10.0

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

Answer 1

In z3-0.4.0, the signature of Bool::and was as follows:

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

However, it was changed in z3-0.6.0 to

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

The usage is as follows:

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