Strings: Add preconditions for range in CVC4 and improve error handling

Author: daniel-raffler

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4StringFormulaManager.java

@@ -143,10 +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) {
-    // FIXME CVC4 will crash when start > end, even if we add an ITE with preconditions
-    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

src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java

@@ -296,28 +296,19 @@ public void testStringRange() throws SolverException, InterruptedException {
 
     // Check some corner cases:
     // StringFormulaManager.range("b", "a") should be empty
-    if (solver != Solvers.CVC4) {
-      // FIXME CVC4 expects that the lower bound is smaller or equal to the upper bound
-      assertThatFormula(smgr.in(var, smgr.range(smgr.makeString("b"), smgr.makeString("a"))))
-          .isUnsatisfiable();
-      assertThatFormula(smgr.in(var, smgr.range('b', 'a'))).isUnsatisfiable();
-    }
+    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
-    if (solver != Solvers.CVC4) {
-      // FIXME CVC4 expects both bounds to be single character Strings
-      assertThatFormula(smgr.in(var, smgr.range(smgr.makeString(""), smgr.makeString("a"))))
-          .isUnsatisfiable();
-    }
+    assertThatFormula(smgr.in(var, smgr.range(smgr.makeString(""), smgr.makeString("a"))))
+        .isUnsatisfiable();
 
     // Try again with two characters:
     // StringFormulaManager.range("aa", "ab") should be empty
-    if (solver != Solvers.CVC4) {
-      // FIXME CVC4 expects both bounds to be single character Strings
-      assertThatFormula(smgr.in(var, smgr.range(smgr.makeString("aa"), smgr.makeString("ab"))))
-          .isUnsatisfiable();
-    }
+    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