From de9623efe549e36fef7745be00fb84d27f74f64a Mon Sep 17 00:00:00 2001 From: Yage Hu Date: Mon, 30 Sep 2024 23:23:38 -0400 Subject: [PATCH 1/2] Seq init Signed-off-by: Yage Hu --- z3-sys/src/lib.rs | 3 ++ z3/src/ast.rs | 80 +++++++++++++++++++++++++++++++++++++++++++++++ z3/src/sort.rs | 4 +++ 3 files changed, 87 insertions(+) diff --git a/z3-sys/src/lib.rs b/z3-sys/src/lib.rs index e2eacd2b..5a332209 100644 --- a/z3-sys/src/lib.rs +++ b/z3-sys/src/lib.rs @@ -3098,6 +3098,9 @@ extern "C" { /// Retrieve from `s` the unit sequence positioned at position `index`. pub fn Z3_mk_seq_at(c: Z3_context, s: Z3_ast, index: Z3_ast) -> Z3_ast; + /// Retrieve from s the element positioned at position index. The function is under-specified if the index is out of bounds. + pub fn Z3_mk_seq_nth(c: Z3_context, s: Z3_ast, index: Z3_ast) -> Z3_ast; + /// Return the length of the sequence `s`. pub fn Z3_mk_seq_length(c: Z3_context, s: Z3_ast) -> Z3_ast; diff --git a/z3/src/ast.rs b/z3/src/ast.rs index a52de25b..fc51044e 100644 --- a/z3/src/ast.rs +++ b/z3/src/ast.rs @@ -64,6 +64,12 @@ pub struct Set<'ctx> { pub(crate) z3_ast: Z3_ast, } +/// [`Ast`] node representing a sequence value. +pub struct Seq<'ctx> { + pub(crate) ctx: &'ctx Context, + pub(crate) z3_ast: Z3_ast, +} + /// [`Ast`] node representing a datatype or enumeration value. pub struct Datatype<'ctx> { pub(crate) ctx: &'ctx Context, @@ -553,6 +559,8 @@ impl_ast!(Array); impl_from_try_into_dynamic!(Array, as_array); impl_ast!(Set); impl_from_try_into_dynamic!(Set, as_set); +impl_ast!(Seq); +impl_from_try_into_dynamic!(Seq, as_seq); impl_ast!(Regexp); impl<'ctx> Int<'ctx> { @@ -1658,6 +1666,70 @@ impl<'ctx> Set<'ctx> { } } +impl<'ctx> Seq<'ctx> { + pub fn new_const>(ctx: &'ctx Context, name: S, eltype: &Sort<'ctx>) -> Self { + let sort = Sort::seq(ctx, eltype); + unsafe { + Self::wrap(ctx, { + Z3_mk_const(ctx.z3_ctx, name.into().as_z3_symbol(ctx), sort.z3_sort) + }) + } + } + + pub fn fresh_const(ctx: &'ctx Context, prefix: &str, eltype: &Sort<'ctx>) -> Self { + let sort = Sort::seq(ctx, eltype); + unsafe { + Self::wrap(ctx, { + let pp = CString::new(prefix).unwrap(); + let p = pp.as_ptr(); + Z3_mk_fresh_const(ctx.z3_ctx, p, sort.z3_sort) + }) + } + } + + /// Retrieve from s the unit sequence positioned at position index. + 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), + ) + } + } + + /// Retrieve from s the element positioned at position index. + /// + /// # Examples + /// ``` + /// # use z3::{ast, Config, Context, Solver, Sort}; + /// # use z3::ast::{Ast, Bool, Int, Seq}; + /// # let cfg = Config::new(); + /// # let ctx = Context::new(&cfg); + /// # let solver = Solver::new(&ctx); + /// let seq = Seq::fresh_const(&ctx, "", &Sort::bool(&ctx)); + /// + /// solver.assert( + /// &seq.nth(&Int::from_u64(&ctx, 0)) + /// .simplify() + /// .as_bool() + /// .unwrap() + /// ._eq(&Bool::from_bool(&ctx, true)) + /// ); + /// ``` + pub fn nth(&self, index: &Int<'ctx>) -> Dynamic<'ctx> { + unsafe { + Dynamic::wrap( + self.ctx, + Z3_mk_seq_nth(self.ctx.z3_ctx, self.z3_ast, index.z3_ast), + ) + } + } + + pub fn length(&self) -> Int<'ctx> { + unsafe { Int::wrap(self.ctx, Z3_mk_seq_length(self.ctx.z3_ctx, self.z3_ast)) } + } +} + impl<'ctx> Dynamic<'ctx> { pub fn from_ast(ast: &dyn Ast<'ctx>) -> Self { unsafe { Self::wrap(ast.get_ctx(), ast.get_z3_ast()) } @@ -1766,6 +1838,14 @@ impl<'ctx> Dynamic<'ctx> { } } + /// Returns `None` if the `Dynamic` is not actually a `Seq`. + pub fn as_seq(&self) -> Option> { + match self.sort_kind() { + SortKind::Seq => Some(unsafe { Seq::wrap(self.ctx, self.z3_ast) }), + _ => None, + } + } + /// Returns `None` if the `Dynamic` is not actually a `Datatype` pub fn as_datatype(&self) -> Option> { match self.sort_kind() { diff --git a/z3/src/sort.rs b/z3/src/sort.rs index 242ae56e..bf462e0f 100644 --- a/z3/src/sort.rs +++ b/z3/src/sort.rs @@ -70,6 +70,10 @@ impl<'ctx> Sort<'ctx> { unsafe { Self::wrap(ctx, Z3_mk_set_sort(ctx.z3_ctx, elt.z3_sort)) } } + pub fn seq(ctx: &'ctx Context, elt: &Sort<'ctx>) -> Sort<'ctx> { + unsafe { Self::wrap(ctx, Z3_mk_seq_sort(ctx.z3_ctx, elt.z3_sort)) } + } + /// Create an enumeration sort. /// /// Creates a Z3 enumeration sort with the given `name`. From 631986623ec311e505d5d10a81f11565ad70ae8e Mon Sep 17 00:00:00 2001 From: Yage Hu Date: Wed, 2 Oct 2024 12:15:03 -0400 Subject: [PATCH 2/2] Doc fix Signed-off-by: Yage Hu --- z3-sys/src/lib.rs | 3 ++- z3/src/ast.rs | 5 +++-- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/z3-sys/src/lib.rs b/z3-sys/src/lib.rs index 5a332209..72d887bc 100644 --- a/z3-sys/src/lib.rs +++ b/z3-sys/src/lib.rs @@ -3098,7 +3098,8 @@ extern "C" { /// Retrieve from `s` the unit sequence positioned at position `index`. pub fn Z3_mk_seq_at(c: Z3_context, s: Z3_ast, index: Z3_ast) -> Z3_ast; - /// Retrieve from s the element positioned at position index. The function is under-specified if the index is out of bounds. + /// Retrieve from `s` the element positioned at position `index`. + /// The function is under-specified if the index is out of bounds. pub fn Z3_mk_seq_nth(c: Z3_context, s: Z3_ast, index: Z3_ast) -> Z3_ast; /// Return the length of the sequence `s`. diff --git a/z3/src/ast.rs b/z3/src/ast.rs index fc51044e..d2d00f5c 100644 --- a/z3/src/ast.rs +++ b/z3/src/ast.rs @@ -1687,7 +1687,8 @@ impl<'ctx> Seq<'ctx> { } } - /// Retrieve from s the unit sequence positioned at position index. + /// Retrieve the unit sequence positioned at position `index`. + /// Use [`Seq::nth`] to get just the element. pub fn at(&self, index: &Int<'ctx>) -> Self { unsafe { Self::wrap( @@ -1697,7 +1698,7 @@ impl<'ctx> Seq<'ctx> { } } - /// Retrieve from s the element positioned at position index. + /// Retrieve the element positioned at position `index`. /// /// # Examples /// ```