From 256e4c075eed2f1c137701565fedb7ae05e078da Mon Sep 17 00:00:00 2001 From: Davvos11 Date: Wed, 16 Oct 2024 11:06:59 +0200 Subject: [PATCH] Add bindings for mk_seq_nth --- src/Z3/Base.hs | 8 ++++++++ src/Z3/Monad.hs | 8 ++++++++ 2 files changed, 16 insertions(+) diff --git a/src/Z3/Base.hs b/src/Z3/Base.hs index 63c675f..1f7de5b 100644 --- a/src/Z3/Base.hs +++ b/src/Z3/Base.hs @@ -310,6 +310,7 @@ module Z3.Base ( , mkSeqExtract , mkSeqReplace , mkSeqAt + , mkSeqNth , mkSeqLength , mkSeqIndex , mkStrToInt @@ -2050,6 +2051,13 @@ mkSeqAt :: Context -> IO AST mkSeqAt = liftFun2 z3_mk_seq_at +-- | Retrieve from s the element positioned at position index. +mkSeqNth :: Context + -> AST -- ^ s + -> AST -- ^ index + -> IO AST +mkSeqNth = liftFun2 z3_mk_seq_nth + -- | Return the length of the sequence s. mkSeqLength :: Context -> AST -- ^ s diff --git a/src/Z3/Monad.hs b/src/Z3/Monad.hs index b6b280b..d1bc2fe 100644 --- a/src/Z3/Monad.hs +++ b/src/Z3/Monad.hs @@ -231,6 +231,7 @@ module Z3.Monad , mkSeqExtract , mkSeqReplace , mkSeqAt + , mkSeqNth , mkSeqLength , mkSeqIndex , mkStrToInt @@ -1822,6 +1823,13 @@ mkSeqAt :: MonadZ3 z3 -> z3 AST mkSeqAt = liftFun2 Base.mkSeqAt +-- | Retrieve from s the element positioned at position index. +mkSeqNth :: MonadZ3 z3 + => AST -- ^ s + -> AST -- ^ index + -> z3 AST +mkSeqNth = liftFun2 Base.mkSeqNth + -- | Return the length of the sequence s. mkSeqLength :: MonadZ3 z3 => AST -> z3 AST mkSeqLength = liftFun1 Base.mkSeqLength