From 7e4d2b04c63a0a5fbf55c09db7f8c216fb637e5f Mon Sep 17 00:00:00 2001 From: Yage Hu Date: Wed, 6 Nov 2024 09:15:05 -0500 Subject: [PATCH 1/2] Add binding for str.substr Signed-off-by: Yage Hu --- z3/src/ast.rs | 45 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) diff --git a/z3/src/ast.rs b/z3/src/ast.rs index 09bef91d..688faaf2 100644 --- a/z3/src/ast.rs +++ b/z3/src/ast.rs @@ -1231,6 +1231,51 @@ impl<'ctx> String<'ctx> { } } + /// Retrieve the substring of length `length` starting at `offset`. + /// + /// # Examples + /// ``` + /// # use z3::{Config, Context, Solver, SatResult}; + /// # use z3::ast::{Ast as _, Int, String}; + /// # + /// # let cfg = Config::new(); + /// # let ctx = Context::new(&cfg); + /// # let solver = Solver::new(&ctx); + /// # + /// let s = String::from_str(&ctx, "abc").unwrap(); + /// let sub = String::fresh_const(&ctx, ""); + /// + /// solver.assert( + /// &sub._eq( + /// &s.substr( + /// &Int::from_u64(&ctx, 1), + /// &Int::from_u64(&ctx, 2), + /// ) + /// ) + /// ); + /// + /// assert_eq!(solver.check(), SatResult::Sat); + /// assert_eq!( + /// solver + /// .get_model() + /// .unwrap() + /// .eval(&sub, true) + /// .unwrap() + /// .as_string() + /// .unwrap() + /// .as_str(), + /// "bc", + /// ); + /// ``` + pub fn substr(&self, offset: &Int<'ctx>, length: &Int<'ctx>) -> Self { + unsafe { + Self::wrap( + &self.ctx, + Z3_mk_seq_extract(self.ctx.z3_ctx, self.z3_ast, offset.z3_ast, length.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); From f34ee13bbdcaa6de0e2eaff93d104475c58f1c41 Mon Sep 17 00:00:00 2001 From: Yage Hu Date: Wed, 6 Nov 2024 09:56:57 -0500 Subject: [PATCH 2/2] Fix clippy warning Signed-off-by: Yage Hu --- z3/src/ast.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/z3/src/ast.rs b/z3/src/ast.rs index 688faaf2..93caf759 100644 --- a/z3/src/ast.rs +++ b/z3/src/ast.rs @@ -1270,7 +1270,7 @@ impl<'ctx> String<'ctx> { pub fn substr(&self, offset: &Int<'ctx>, length: &Int<'ctx>) -> Self { unsafe { Self::wrap( - &self.ctx, + self.ctx, Z3_mk_seq_extract(self.ctx.z3_ctx, self.z3_ast, offset.z3_ast, length.z3_ast), ) }