mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
parent
3f2dafe047
commit
df75792e9c
|
@ -2048,6 +2048,16 @@ public class Context implements AutoCloseable {
|
|||
return (SeqExpr) Expr.create(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
* Retrieve element at index.
|
||||
*/
|
||||
public SeqExpr MkNth(SeqExpr s, Expr index)
|
||||
{
|
||||
checkContextMatch(s, index);
|
||||
return (SeqExpr) Expr.create(this, Native.Z3_mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject()));
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
* Extract subsequence.
|
||||
*/
|
||||
|
|
Loading…
Reference in a new issue