From 1a1e734228b96e96e77f61264683d2225eff0486 Mon Sep 17 00:00:00 2001
From: Yage Hu <me@huyage.dev>
Date: Sun, 27 Oct 2024 12:28:40 -0400
Subject: [PATCH] Add binding to get unit string at index (#319)

Signed-off-by: Yage Hu <me@huyage.dev>
---
 z3/src/ast.rs | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/z3/src/ast.rs b/z3/src/ast.rs
index c2fdc3ad..ea3b2838 100644
--- a/z3/src/ast.rs
+++ b/z3/src/ast.rs
@@ -1161,6 +1161,34 @@ impl<'ctx> String<'ctx> {
         }
     }
 
+    /// Retrieve the substring of length 1 positioned at `index`.
+    ///
+    /// # Examples
+    /// ```
+    /// # use z3::{Config, Context, Solver};
+    /// # use z3::ast::{Ast as _, Int};
+    /// #
+    /// # let cfg = Config::new();
+    /// # let ctx = Context::new(&cfg);
+    /// # let solver = Solver::new(&ctx);
+    /// #
+    /// let s = z3::ast::String::fresh_const(&ctx, "");
+    ///
+    /// solver.assert(
+    ///     &s.at(&Int::from_u64(&ctx, 0))
+    ///         ._eq(&z3::ast::String::from_str(&ctx, "a").unwrap())
+    /// );
+    /// assert_eq!(solver.check(), z3::SatResult::Sat);
+    /// ```
+    pub fn at(&self, index: &Int<'ctx>) -> Self {
+        unsafe {
+            Self::wrap(
+                self.ctx,
+                Z3_mk_seq_at(self.ctx.z3_ctx, self.z3_ast, index.z3_ast),
+            )
+        }
+    }
+
     /// Checks if this string matches a `z3::ast::Regexp`
     pub fn regex_matches(&self, regex: &Regexp) -> Bool<'ctx> {
         assert!(self.ctx == regex.ctx);