diff --git a/z3/src/ast.rs b/z3/src/ast.rs index 36955ff3..d58d094e 100644 --- a/z3/src/ast.rs +++ b/z3/src/ast.rs @@ -1829,6 +1829,11 @@ impl<'ctx> Seq<'ctx> { } } + /// Create a unit sequence of `a`. + pub fn unit>(ctx: &'ctx Context, a: &A) -> Self { + unsafe { Self::wrap(ctx, Z3_mk_seq_unit(ctx.z3_ctx, a.get_z3_ast())) } + } + /// Retrieve the unit sequence positioned at position `index`. /// Use [`Seq::nth`] to get just the element. pub fn at(&self, index: &Int<'ctx>) -> Self { @@ -1871,6 +1876,10 @@ impl<'ctx> Seq<'ctx> { pub fn length(&self) -> Int<'ctx> { unsafe { Int::wrap(self.ctx, Z3_mk_seq_length(self.ctx.z3_ctx, self.z3_ast)) } } + + varop! { + concat(Z3_mk_seq_concat, Self); + } } impl<'ctx> Dynamic<'ctx> {