Add bindings for sequence foldl

z3-sys/src/lib.rs

@@ -3100,6 +3100,9 @@ unsafe 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/seq.rs

@@ -1,5 +1,5 @@
+use crate::ast::{Array, Bool, IntoAst};
 use crate::ast::{Ast, Dynamic, Int, varop};
-use crate::ast::{Bool, IntoAst};
 use crate::{Context, Sort, Symbol};
 use std::ffi::CString;
 use z3_sys::*;
@@ -121,6 +121,36 @@ impl Seq {
         }
     }
 
+    /// 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 solver = Solver::new();
+    /// #
+    /// let seq = Seq::new_const("seq", &Sort::int());
+    /// let accumulator = Int::new_const("acc");
+    /// let item = Int::new_const("item");
+    /// let sum = lambda_const(
+    ///     &[&accumulator, &item],
+    ///     &Dynamic::from_ast(&Int::add(&[&accumulator, &item])),
+    /// );
+    ///
+    /// seq.foldl(&sum, &Dynamic::from_ast(&Int::from_u64(0)));
+    /// ```
+    pub fn foldl(&self, f: &Array, a: &Dynamic) -> Dynamic {
+        let ctx = &Context::thread_local();
+
+        unsafe {
+            Dynamic::wrap(
+                ctx,
+                Z3_mk_seq_foldl(self.ctx.z3_ctx.0, f.z3_ast, a.z3_ast, self.z3_ast),
+            )
+        }
+    }
+
     varop! {
         /// Concatenate sequences.
         concat(Z3_mk_seq_concat, Self);