diff --git a/src/api/java/Context.java b/src/api/java/Context.java index c6d928de2..e0df3797b 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2106,6 +2106,26 @@ public class Context implements AutoCloseable { return (BoolExpr) Expr.create(this, Native.mkSeqContains(nCtx(), s1.getNativeObject(), s2.getNativeObject())); } + /** + * Check if the string s1 is lexicographically strictly less than s2. + */ + + public BoolExpr MkStringLt(SeqSort s1, SeqSort s2) + { + checkContextMatch(s1, s2); + return new BoolExpr(this, Native.mkStrLt(nCtx(), s1.getNativeObject(), s2.getNativeObject())); + } + + /** + * Check if the string s1 is lexicographically less or equal to s2. + */ + public BoolExpr MkStringLe(SeqSort s1, SeqSort s2) + { + checkContextMatch(s1, s2); + return new BoolExpr(this, Native.mkStrLe(nCtx(), s1.getNativeObject(), s2.getNativeObject())); + } + + /** * Retrieve sequence of length one at index. */