Merge pull request #282 from Swalkyn/master

Add allChar function, fix #281

src/org/sosy_lab/java_smt/api/StringFormulaManager.java

@@ -8,6 +8,7 @@
 
 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;
@@ -124,10 +125,20 @@ default StringFormula concat(StringFormula... parts) {
   RegexFormula none();
 
   /**
+   * Note: The size of the used alphabet depends on the underlying SMT solver.
+   *
    * @return formula denoting the set of all strings, also known as Regex <code>".*"</code>.
    */
   RegexFormula all();
 
+  /**
+   * Note: The size of the used alphabet depends on the underlying SMT solver.
+   *
+   * @return formula denoting the set of all strings of length 1, also known as DOT operator which
+   *     represents one arbitrary char, or as Regex <code>"."</code>.
+   */
+  RegexFormula allChar();
+
   /**
    * @return formula denoting the range regular expression over two sequences of length 1.
    */
@@ -138,6 +149,13 @@ 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)));
   }
 

src/org/sosy_lab/java_smt/basicimpl/AbstractStringFormulaManager.java

@@ -205,6 +205,13 @@ public RegexFormula all() {
 
   protected abstract TFormulaInfo allImpl();
 
+  @Override
+  public RegexFormula allChar() {
+    return wrapRegex(allCharImpl());
+  }
+
+  protected abstract TFormulaInfo allCharImpl();
+
   @Override
   public RegexFormula range(StringFormula start, StringFormula end) {
     return wrapRegex(range(extractInfo(start), extractInfo(end)));

src/org/sosy_lab/java_smt/delegate/statistics/StatisticsStringFormulaManager.java

@@ -156,6 +156,12 @@ public RegexFormula all() {
     return delegate.all();
   }
 
+  @Override
+  public RegexFormula allChar() {
+    stats.stringOperations.getAndIncrement();
+    return delegate.allChar();
+  }
+
   @Override
   public RegexFormula range(StringFormula start, StringFormula end) {
     stats.stringOperations.getAndIncrement();

src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedStringFormulaManager.java

@@ -178,6 +178,13 @@ public RegexFormula all() {
     }
   }
 
+  @Override
+  public RegexFormula allChar() {
+    synchronized (sync) {
+      return delegate.allChar();
+    }
+  }
+
   @Override
   public RegexFormula range(StringFormula start, StringFormula end) {
     synchronized (sync) {

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

@@ -138,6 +138,11 @@ protected Expr allImpl() {
     return exprManager.mkExpr(Kind.REGEXP_COMPLEMENT, noneImpl());
   }
 
+  @Override
+  protected Expr allCharImpl() {
+    return exprManager.mkExpr(Kind.REGEXP_SIGMA, new vectorExpr());
+  }
+
   @Override
   protected Expr range(Expr start, Expr end) {
     return exprManager.mkExpr(Kind.REGEXP_RANGE, start, end);

src/org/sosy_lab/java_smt/solvers/z3/Z3StringFormulaManager.java

@@ -131,6 +131,11 @@ protected Long allImpl() {
     return Native.mkReFull(z3context, formulaCreator.getRegexType());
   }
 
+  @Override
+  protected Long allCharImpl() {
+    return Native.mkReAllchar(z3context, formulaCreator.getRegexType());
+  }
+
   @Override
   protected Long range(Long start, Long end) {
     return Native.mkReRange(z3context, start, end);

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

@@ -128,6 +128,47 @@ public void testRegexAll3() throws SolverException, InterruptedException {
     assertThatFormula(smgr.in(smgr.makeString(".*"), regex)).isSatisfiable();
   }
 
+  @Test
+  public void testRegexAllChar() throws SolverException, InterruptedException {
+    RegexFormula regexAllChar = smgr.allChar();
+
+    assertThatFormula(smgr.in(smgr.makeString("a"), regexAllChar)).isSatisfiable();
+    assertThatFormula(smgr.in(smgr.makeString("ab"), regexAllChar)).isUnsatisfiable();
+    assertThatFormula(smgr.in(smgr.makeString(""), regexAllChar)).isUnsatisfiable();
+    assertThatFormula(smgr.in(smgr.makeString("ab"), smgr.times(regexAllChar, 2))).isSatisfiable();
+    assertThatFormula(
+            smgr.in(smgr.makeVariable("x"), smgr.intersection(smgr.range('9', 'a'), regexAllChar)))
+        .isSatisfiable();
+
+    RegexFormula regexDot = smgr.makeRegex(".");
+    assertThatFormula(smgr.in(smgr.makeString("a"), regexDot)).isUnsatisfiable();
+  }
+
+  @Test
+  public void testRegexAllCharUnicode() throws SolverException, InterruptedException {
+    RegexFormula regexAllChar = smgr.allChar();
+
+    // Single characters.
+    assertThatFormula(smgr.in(smgr.makeString("\\u0394"), regexAllChar)).isSatisfiable();
+    assertThatFormula(smgr.in(smgr.makeString("\\u{1fa6a}"), regexAllChar)).isSatisfiable();
+
+    // Combining characters are not matched as one character.
+    assertThatFormula(smgr.in(smgr.makeString("a\\u0336"), regexAllChar)).isUnsatisfiable();
+    assertThatFormula(smgr.in(smgr.makeString("\\n"), regexAllChar)).isUnsatisfiable();
+
+    if (solverUnderTest != Solvers.CVC4) {
+      // CVC4 does not support Unicode characters.
+      // Z3 and other solvers support Unicode characters in the theory of strings.
+      assertThatFormula(
+              smgr.in(
+                  smgr.makeVariable("x"), smgr.intersection(smgr.range('a', 'Δ'), regexAllChar)))
+          .isSatisfiable();
+      // Combining characters are not matched as one character.
+      // Non-ascii non-printable characters should use the codepoint representation
+      assertThatFormula(smgr.in(smgr.makeString("Δ"), regexAllChar)).isUnsatisfiable();
+    }
+  }
+
   @Test
   public void testStringRegex2() throws SolverException, InterruptedException {
     RegexFormula regex = smgr.concat(smgr.closure(a2z), smgr.makeRegex("ll"), smgr.closure(a2z));