Add bindings for sequence foldl

z3-sys/src/lib.rs

@@ -3110,6 +3110,9 @@ extern "C" {
     /// The function is under-specified if `offset` is negative or larger than the length of `s`.
     pub fn Z3_mk_seq_index(c: Z3_context, s: Z3_ast, substr: Z3_ast, offset: Z3_ast) -> Z3_ast;
 
+    /// Create a fold of the function `f` over the sequence `s` with accumulator `a`.
+    pub fn Z3_mk_seq_foldl(c: Z3_context, f: Z3_ast, a: Z3_ast, s: Z3_ast) -> Z3_ast;
+
     /// Convert string to integer.
     pub fn Z3_mk_str_to_int(c: Z3_context, s: Z3_ast) -> Z3_ast;
 

z3/src/ast.rs

@@ -1751,6 +1751,37 @@ 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)) }
     }
+
+    /// Create a fold of the function `f` over the sequence with accumulator `a`.
+    ///
+    /// # Examples
+    /// ```
+    /// # use z3::{Config, Context, Solver, Sort};
+    /// # use z3::ast::{Seq, Int, Dynamic, lambda_const};
+    /// #
+    /// # let cfg = Config::new();
+    /// # let ctx = Context::new(&cfg);
+    /// # let solver = Solver::new(&ctx);
+    /// #
+    /// let seq = Seq::new_const(&ctx, "seq", &Sort::int(&ctx));
+    /// let accumulator = Int::new_const(&ctx, "acc");
+    /// let item = Int::new_const(&ctx, "item");
+    /// let sum = lambda_const(
+    ///     &ctx,
+    ///     &[&accumulator, &item],
+    ///     &Dynamic::from_ast(&Int::add(&ctx, &[&accumulator, &item])),
+    /// );
+    ///
+    /// seq.foldl(&sum, &Dynamic::from_ast(&Int::from_u64(&ctx, 0)));
+    /// ```
+    pub fn foldl(&self, f: &Array<'ctx>, a: &Dynamic<'ctx>) -> Dynamic<'ctx> {
+        unsafe {
+            Dynamic::wrap(
+                self.ctx,
+                Z3_mk_seq_foldl(self.ctx.z3_ctx, f.z3_ast, a.z3_ast, self.z3_ast),
+            )
+        }
+    }
 }
 
 impl<'ctx> Dynamic<'ctx> {