diff --git a/src/org/sosy_lab/java_smt/api/StringFormulaManager.java b/src/org/sosy_lab/java_smt/api/StringFormulaManager.java
index 8766c874af..42c4450ab0 100644
--- a/src/org/sosy_lab/java_smt/api/StringFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/api/StringFormulaManager.java
@@ -8,7 +8,6 @@
package org.sosy_lab.java_smt.api;
-import com.google.common.base.Preconditions;
import java.util.Arrays;
import java.util.List;
import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
@@ -155,13 +154,6 @@ default StringFormula concat(StringFormula... parts) {
* @see #range(StringFormula, StringFormula)
*/
default RegexFormula range(char start, char end) {
- Preconditions.checkArgument(
- start <= end,
- "Range from start '%s' (%s) to end '%s' (%s) is empty.",
- start,
- (int) start,
- end,
- (int) end);
return range(makeString(String.valueOf(start)), makeString(String.valueOf(end)));
}
diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4StringFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4StringFormulaManager.java
index 0e167b418a..d61227aa5d 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4StringFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4StringFormulaManager.java
@@ -143,9 +143,33 @@ protected Expr allCharImpl() {
return exprManager.mkExpr(Kind.REGEXP_SIGMA, new vectorExpr());
}
+ /**
+ * Check if the String only contains printable US ASCII characters.
+ *
+ * <p>We use this function to check if the String contains any characters that would have to be
+ * escaped in SMTLIB.
+ */
+ private boolean isAsciiString(String str) {
+ return str.codePoints().allMatch(c -> c >= 0x20 && c <= 0x7E);
+ }
+
@Override
protected Expr range(Expr start, Expr end) {
- return exprManager.mkExpr(Kind.REGEXP_RANGE, start, end);
+ Preconditions.checkArgument(
+ start.isConst() && end.isConst(), "CVC4 does not support variables as bounds");
+
+ String lower = (String) formulaCreator.convertValue(start, start);
+ String upper = (String) formulaCreator.convertValue(end, end);
+
+ Preconditions.checkArgument(
+ isAsciiString(lower) && isAsciiString(upper),
+ "CVC4 only allows printable US ASCII characters as bounds");
+
+ // Return the empty language if the bounds are not single character Strings, or if the upper
+ // bound is smaller than the lower bound
+ return lower.length() != 1 || upper.length() != 1 || upper.compareTo(lower) < 0
+ ? noneImpl()
+ : exprManager.mkExpr(Kind.REGEXP_RANGE, start, end);
}
@Override
diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5StringFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5StringFormulaManager.java
index 500aea06d2..db123b0a57 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5StringFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5StringFormulaManager.java
@@ -140,7 +140,16 @@ protected Term allCharImpl() {
@Override
protected Term range(Term start, Term end) {
- return solver.mkTerm(Kind.REGEXP_RANGE, start, end);
+ // Precondition: Both bounds must be single character Strings
+ // CVC5 already checks that the lower bound is smaller than the upper bound and returns the
+ // empty language otherwise.
+ Term one = solver.mkInteger(1);
+ Term cond =
+ solver.mkTerm(
+ Kind.AND,
+ solver.mkTerm(Kind.EQUAL, length(start), one),
+ solver.mkTerm(Kind.EQUAL, length(end), one));
+ return solver.mkTerm(Kind.ITE, cond, solver.mkTerm(Kind.REGEXP_RANGE, start, end), noneImpl());
}
@Override
diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java
index 29f2032780..61a42339c3 100644
--- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java
+++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java
@@ -605,6 +605,9 @@ static FormulaType<?> getFormulaType(IExpression pFormula) {
* @throws IllegalArgumentException for any other type.
*/
private static FormulaType<?> mergeFormulaTypes(FormulaType<?> type1, FormulaType<?> type2) {
+ if (type1.equals(type2)) {
+ return type1;
+ }
if ((type1.isIntegerType() || type1.isRationalType())
&& (type2.isIntegerType() || type2.isRationalType())) {
return type1.isRationalType() ? type1 : type2;
diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java
index c919679b08..68535404e1 100644
--- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java
@@ -11,11 +11,16 @@
import static com.google.common.base.Preconditions.checkArgument;
import static org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.toITermSeq;
+import ap.basetypes.IdealInt;
import ap.parser.IAtom;
+import ap.parser.IBinFormula;
+import ap.parser.IBinJunctor;
import ap.parser.IExpression;
import ap.parser.IFormula;
import ap.parser.IFunApp;
+import ap.parser.IIntLit;
import ap.parser.ITerm;
+import ap.parser.ITermITE;
import ap.types.Sort;
import com.google.common.collect.ImmutableList;
import java.util.List;
@@ -166,7 +171,17 @@ protected IExpression allCharImpl() {
@Override
protected ITerm range(IExpression start, IExpression end) {
- return new IFunApp(PrincessEnvironment.stringTheory.re_range(), toITermSeq());
+ // Precondition: Both bounds must be single character Strings
+ // Princess already checks that the lower bound is smaller than the upper bound and returns the
+ // empty language otherwise.
+ ITerm one = new IIntLit(IdealInt.apply(1));
+ IFormula cond =
+ new IBinFormula(
+ IBinJunctor.And(), length(start).$eq$eq$eq(one), length(end).$eq$eq$eq(one));
+ return new ITermITE(
+ cond,
+ new IFunApp(PrincessEnvironment.stringTheory.re_range(), toITermSeq(start, end)),
+ noneImpl());
}
@Override
diff --git a/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java
index ca7cfc7985..4c437964f3 100644
--- a/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java
+++ b/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java
@@ -260,6 +260,75 @@ public void testStringConcatEmpty() throws SolverException, InterruptedException
assertEqual(empty, smgr.concat(ImmutableList.of(empty, empty, empty, empty)));
}
+ @Test
+ public void testStringRange() throws SolverException, InterruptedException {
+ StringFormula var = smgr.makeVariable("str");
+
+ // Try something simple:
+ // StringFormulaManager.range("a","b") should not be empty
+ assertThatFormula(smgr.in(var, smgr.range(smgr.makeString("a"), smgr.makeString("b"))))
+ .isSatisfiable();
+ assertThatFormula(smgr.in(var, smgr.range('a', 'b'))).isSatisfiable();
+
+ // Check again with a single element interval:
+ // StringFormulaManager.range("a","a") should not be empty
+ assertThatFormula(smgr.in(var, smgr.range(smgr.makeString("a"), smgr.makeString("a"))))
+ .isSatisfiable();
+ assertThatFormula(smgr.in(var, smgr.range('a', 'a'))).isSatisfiable();
+
+ // Check again for Unicode characters:
+ // StringFormulaManager.range("ꯍ","ꯎ") should not be empty
+ if (solver != Solvers.CVC4) {
+ // FIXME CVC4 only support ASCII characters for range()
+ assertThatFormula(smgr.in(var, smgr.range(smgr.makeString("ꯍ"), smgr.makeString("ꯎ"))))
+ .isSatisfiable();
+ assertThatFormula(smgr.in(var, smgr.range('ꯍ', 'ꯎ'))).isSatisfiable();
+ }
+
+ // And once more with Unicode characters that are not in the BMP:
+ // StringFormulaManager.range("𠃋","𠃋") should not be empty
+ if (solver != Solvers.PRINCESS && solver != Solvers.CVC4) {
+ // FIXME CVC4 only support ASCII characters for range()
+ // FIXME Princess can't handle surrogate pairs
+ assertThatFormula(smgr.in(var, smgr.range(smgr.makeString("𠃋"), smgr.makeString("𠃋"))))
+ .isSatisfiable();
+ }
+
+ // Check some corner cases:
+ // StringFormulaManager.range("b", "a") should be empty
+ assertThatFormula(smgr.in(var, smgr.range(smgr.makeString("b"), smgr.makeString("a"))))
+ .isUnsatisfiable();
+ assertThatFormula(smgr.in(var, smgr.range('b', 'a'))).isUnsatisfiable();
+
+ // Only 'singleton' Strings (= Strings with one character) are allowed:
+ // StringFormulaManager.range("", "a") should be empty
+ assertThatFormula(smgr.in(var, smgr.range(smgr.makeString(""), smgr.makeString("a"))))
+ .isUnsatisfiable();
+
+ // Try again with two characters:
+ // StringFormulaManager.range("aa", "ab") should be empty
+ assertThatFormula(smgr.in(var, smgr.range(smgr.makeString("aa"), smgr.makeString("ab"))))
+ .isUnsatisfiable();
+
+ // Now use variables for the bounds:
+ // StringFormulaManager.range(lower, "b") should be empty iff "b" < lower
+ StringFormula lower = smgr.makeVariable("lower");
+ if (solver != Solvers.PRINCESS && solver != Solvers.CVC4) {
+ // FIXME CVC4 only supports String constants as bounds and will fail for variables
+ // FIXME Princess will crash when using variables as bounds
+ assertThatFormula(
+ bmgr.and(
+ smgr.equal(lower, smgr.makeString("a")),
+ smgr.in(var, smgr.range(lower, smgr.makeString("b")))))
+ .isSatisfiable();
+ assertThatFormula(
+ bmgr.and(
+ smgr.equal(lower, smgr.makeString("c")),
+ smgr.in(var, smgr.range(lower, smgr.makeString("b")))))
+ .isUnsatisfiable();
+ }
+ }
+
@Test
public void testStringPrefixSuffixConcat() throws SolverException, InterruptedException {
// FIXME: Princess will timeout on this test