From d82f87ddaaa3982a5fe663ecdfe1f95f3b1c7444 Mon Sep 17 00:00:00 2001 From: RIvance Date: Thu, 5 Sep 2024 17:32:42 +0800 Subject: [PATCH] feat: add Z3Context.mkSeqNth --- src/main/scala/z3/scala/Z3Context.scala | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/main/scala/z3/scala/Z3Context.scala b/src/main/scala/z3/scala/Z3Context.scala index 10f85c6..9051688 100644 --- a/src/main/scala/z3/scala/Z3Context.scala +++ b/src/main/scala/z3/scala/Z3Context.scala @@ -591,6 +591,10 @@ sealed class Z3Context(val config: Map[String, String]) { new Z3AST(Native.mkSeqAt(this.ptr, seq.ptr, i.ptr), this) } + def mkSeqNth(seq: Z3AST, n: Z3AST): Z3AST = { + new Z3AST(Native.mkSeqNth(this.ptr, seq.ptr, n.ptr), this) + } + def mkSeqExtract(seq: Z3AST, start: Z3AST, length: Z3AST): Z3AST = { new Z3AST(Native.mkSeqExtract(this.ptr, seq.ptr, start.ptr, length.ptr), this) }