search

epfl-lara / ScalaZ3

DSL in Scala for Constraint Solving with Z3 SMT Solver
Apache License 2.0
123 stars 34 forks source link

feat: add Z3Context.mkSeqNth #89

Open RIvance opened 2 months ago

RIvance commented 2 months ago

Add a missing commonly used Seq operation.

Operation Brief description
(seq.nth s offset) Element at offset in s. If offset is out of bounds the result is under-specified. In other words, it is treated as a fresh variable 
def mkSeqNth(seq: Z3AST, n: Z3AST): Z3AST = {
  new Z3AST(Native.mkSeqNth(this.ptr, seq.ptr, n.ptr), this)
}

reference: https://microsoft.github.io/z3guide/docs/theories/Sequences/