Skip to content

Commit d006891

Browse files
committed
Add bindings for sequence foldl
Signed-off-by: Yage Hu <[email protected]>
1 parent 7b00b99 commit d006891

File tree

2 files changed

+34
-0
lines changed

2 files changed

+34
-0
lines changed

z3-sys/src/lib.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3110,6 +3110,9 @@ extern "C" {
31103110
/// The function is under-specified if `offset` is negative or larger than the length of `s`.
31113111
pub fn Z3_mk_seq_index(c: Z3_context, s: Z3_ast, substr: Z3_ast, offset: Z3_ast) -> Z3_ast;
31123112

3113+
/// Create a fold of the function `f` over the sequence `s` with accumulator `a`.
3114+
pub fn Z3_mk_seq_foldl(c: Z3_context, f: Z3_ast, a: Z3_ast, s: Z3_ast) -> Z3_ast;
3115+
31133116
/// Convert string to integer.
31143117
pub fn Z3_mk_str_to_int(c: Z3_context, s: Z3_ast) -> Z3_ast;
31153118

z3/src/ast.rs

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1746,6 +1746,37 @@ impl<'ctx> Seq<'ctx> {
17461746
pub fn length(&self) -> Int<'ctx> {
17471747
unsafe { Int::wrap(self.ctx, Z3_mk_seq_length(self.ctx.z3_ctx, self.z3_ast)) }
17481748
}
1749+
1750+
/// Create a fold of the function `f` over the sequence with accumulator `a`.
1751+
///
1752+
/// # Examples
1753+
/// ```
1754+
/// # use z3::{Config, Context, Solver, Sort};
1755+
/// # use z3::ast::{Seq, Int, Dynamic, lambda_const};
1756+
/// #
1757+
/// # let cfg = Config::new();
1758+
/// # let ctx = Context::new(&cfg);
1759+
/// # let solver = Solver::new(&ctx);
1760+
/// #
1761+
/// let seq = Seq::new_const(&ctx, "seq", &Sort::int(&ctx));
1762+
/// let accumulator = Int::new_const(&ctx, "acc");
1763+
/// let item = Int::new_const(&ctx, "item");
1764+
/// let sum = lambda_const(
1765+
/// &ctx,
1766+
/// &[&accumulator, &item],
1767+
/// &Dynamic::from_ast(&Int::add(&ctx, &[&accumulator, &item])),
1768+
/// );
1769+
///
1770+
/// seq.foldl(&sum, &Dynamic::from_ast(&Int::from_u64(&ctx, 0)));
1771+
/// ```
1772+
pub fn foldl(&self, f: &Array<'ctx>, a: &Dynamic<'ctx>) -> Dynamic<'ctx> {
1773+
unsafe {
1774+
Dynamic::wrap(
1775+
self.ctx,
1776+
Z3_mk_seq_foldl(self.ctx.z3_ctx, f.z3_ast, a.z3_ast, self.z3_ast),
1777+
)
1778+
}
1779+
}
17491780
}
17501781

17511782
impl<'ctx> Dynamic<'ctx> {

0 commit comments

Comments
 (0)