Skip to content

Commit

Permalink
Have distinct take impl Borrow
Browse files Browse the repository at this point in the history
  • Loading branch information
Pat-Lafon committed Oct 13, 2023
1 parent 7a88984 commit 77dcc05
Showing 1 changed file with 5 additions and 2 deletions.
7 changes: 5 additions & 2 deletions z3/src/ast.rs
Original file line number Diff line number Diff line change
Expand Up @@ -264,14 +264,17 @@ pub trait Ast<'ctx>: fmt::Debug {
/// `Ast`s being compared must all be the same type.
//
// Note that we can't use the varop! macro because of the `pub` keyword on it
fn distinct(ctx: &'ctx Context, values: &[&Self]) -> Bool<'ctx>
fn distinct(ctx: &'ctx Context, values: &[impl Borrow<Self>]) -> Bool<'ctx>
where
Self: Sized,
{
unsafe {
Bool::wrap(ctx, {
assert!(values.len() <= 0xffffffff);
let values: Vec<Z3_ast> = values.iter().map(|nodes| nodes.get_z3_ast()).collect();
let values: Vec<Z3_ast> = values
.iter()
.map(|nodes| nodes.borrow().get_z3_ast())
.collect();
Z3_mk_distinct(ctx.z3_ctx, values.len() as u32, values.as_ptr())
})
}
Expand Down

0 comments on commit 77dcc05

Please sign in to comment.