Add str.<= and str.< to Java API

Z3Prover · Feb 20, 2022 · 9a1a728 · 9a1a728
1 parent 7091b1c
commit 9a1a728
Showing 1 changed file with 20 additions and 0 deletions.
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
@@ -2106,6 +2106,26 @@ public <R extends Sort> BoolExpr mkContains(Expr<SeqSort<R>> s1, Expr<SeqSort<R>
         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<CharSort> s1, SeqSort<CharSort> 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<CharSort> s1, SeqSort<CharSort> s2)
+    {
+	checkContextMatch(s1, s2);
+	return new BoolExpr(this, Native.mkStrLe(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
+    }
+
+
     /**
      * Retrieve sequence of length one at index.
      */