Add allChar function, fix sosy-lab#281

This function corresponds to `re.allchar` in
http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml.

It is implemented in the Z3 and CVC4 solvers.

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

@@ -128,6 +128,12 @@ default StringFormula concat(StringFormula... parts) {
    */
   RegexFormula all();
 
+ /**
+   * @return formula denoting the set of all strings of length 1, also known as DOT operator which
+   *     represents an arbitrary char. .
+   */
+  RegexFormula allChar();
+
   /**
    * @return formula denoting the range regular expression over two sequences of length 1.
    */

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, noneImpl());
+  }
+
   @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,14 @@ public void testRegexAll3() throws SolverException, InterruptedException {
     assertThatFormula(smgr.in(smgr.makeString(".*"), regex)).isSatisfiable();
   }
 
+  @Test
+  public void testRegexAllChar() throws SolverException, InterruptedException {
+    RegexFormula regexAllChar = smgr.allChar();
+    RegexFormula regexDot = smgr.makeRegex(".");
+    assertThatFormula(smgr.in(smgr.makeString("a"), regexAllChar)).isSatisfiable();
+    assertThatFormula(smgr.in(smgr.makeString("a"), regexDot)).isUnsatisfiable();
+  }
+
   @Test
   public void testStringRegex2() throws SolverException, InterruptedException {
     RegexFormula regex = smgr.concat(smgr.closure(a2z), smgr.makeRegex("ll"), smgr.closure(a2z));