#5727

Expose diff function,
expose allchar in Java API
expose op codes for replace/re/all

src/api/api_ast.cpp

@@ -1187,6 +1187,9 @@ extern "C" {
             case OP_SEQ_CONTAINS: return Z3_OP_SEQ_CONTAINS;
             case OP_SEQ_EXTRACT: return Z3_OP_SEQ_EXTRACT;
             case OP_SEQ_REPLACE: return Z3_OP_SEQ_REPLACE;
+            case OP_SEQ_REPLACE_RE: return Z3_OP_SEQ_REPLACE_RE;
+            case OP_SEQ_REPLACE_RE_ALL: return Z3_OP_SEQ_REPLACE_RE_ALL;
+            case OP_SEQ_REPLACE_ALL: return Z3_OP_SEQ_REPLACE_ALL;
             case OP_SEQ_AT: return Z3_OP_SEQ_AT;
             case OP_SEQ_NTH: return Z3_OP_SEQ_NTH;
             case OP_SEQ_LENGTH: return Z3_OP_SEQ_LENGTH;
@@ -1220,9 +1223,11 @@ extern "C" {
             case OP_RE_OPTION: return Z3_OP_RE_OPTION;
             case OP_RE_CONCAT: return Z3_OP_RE_CONCAT;
             case OP_RE_UNION: return Z3_OP_RE_UNION;
+            case OP_RE_DIFF: return Z3_OP_RE_DIFF;
+             case OP_RE_POWER: return Z3_OP_RE_POWER;
             case OP_RE_INTERSECT: return Z3_OP_RE_INTERSECT;
             case OP_RE_LOOP: return Z3_OP_RE_LOOP;
-            case OP_RE_FULL_SEQ_SET: return Z3_OP_RE_FULL_SET;
+             case OP_RE_FULL_SEQ_SET: return Z3_OP_RE_FULL_SET;
             //case OP_RE_FULL_CHAR_SET: return Z3_OP_RE_FULL_SET;
             case OP_RE_EMPTY_SET: return Z3_OP_RE_EMPTY_SET;
             default:

src/api/api_seq.cpp

@@ -308,6 +308,7 @@ extern "C" {
     MK_UNARY(Z3_mk_re_star, mk_c(c)->get_seq_fid(), OP_RE_STAR, SKIP);
     MK_UNARY(Z3_mk_re_option, mk_c(c)->get_seq_fid(), OP_RE_OPTION, SKIP);
     MK_UNARY(Z3_mk_re_complement, mk_c(c)->get_seq_fid(), OP_RE_COMPLEMENT, SKIP);
+    MK_BINARY(Z3_mk_re_diff, mk_c(c)->get_seq_fid(), OP_RE_DIFF, SKIP);
     MK_NARY(Z3_mk_re_union, mk_c(c)->get_seq_fid(), OP_RE_UNION, SKIP);
     MK_NARY(Z3_mk_re_intersect, mk_c(c)->get_seq_fid(), OP_RE_INTERSECT, SKIP);
     MK_NARY(Z3_mk_re_concat, mk_c(c)->get_seq_fid(), OP_RE_CONCAT, SKIP);

src/api/c++/z3++.h

@@ -3797,6 +3797,12 @@ namespace z3 {
         ctx.check_error();
         return expr(ctx, r);
     }
+    inline expr re_diff(expr const& a, expr const& b) {
+        check_context(a, b);
+        Z3_ast r = Z3_mk_re_diff(ctx, a, b);
+        ctx.check_error();
+        return expr(ctx, r);
+    }
     inline expr re_complement(expr const& a) {
         MK_EXPR1(Z3_mk_re_complement, a);
     }

src/api/dotnet/Context.cs

@@ -2667,6 +2667,17 @@ namespace Microsoft.Z3
             return new ReExpr(this, Native.Z3_mk_re_intersect(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
         }
 
+        /// <summary>
+        /// Create a difference regular expression.
+        /// </summary>
+        public ReExpr MkDiff(ReExpr a, ReExpr b) 
+        {
+            Debug.Assert(a != null);
+            Debug.Assert(b != null);
+            CheckContextMatch(a, b);
+            return new ReExpr(this, Native.Z3_mk_re_diff(nCtx, a.NativeObject, b.NativeObject));
+        }
+
         /// <summary>
         /// Create the empty regular expression.
         /// The sort s should be a regular expression.

src/api/java/Context.java

@@ -2246,8 +2246,19 @@ public class Context implements AutoCloseable {
         return (ReExpr<R>) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(t)));
     }
 
+    /**
+     * Create a difference regular expression.
+     */
+    public <R extends Sort> ReExpr<R> mkDiff(Expr<ReSort<R>> a, Expr<ReSort<R>> b)
+    {
+        checkContextMatch(a, b);
+	return (ReExpr<R>) Expr.create(this, Native.mkReDiff(nCtx(), a.getNativeObject(), b.getNativeObject()));
+    }
+
+
     /**
      * Create the empty regular expression.
+     * Coresponds to re.none
      */
     public <R extends Sort> ReExpr<R> mkEmptyRe(R s)
     {
@@ -2256,12 +2267,22 @@ public class Context implements AutoCloseable {
 
     /**
      * Create the full regular expression.
+     * Corresponds to re.all
      */
     public <R extends Sort> ReExpr<R> mkFullRe(R s)
     {
         return (ReExpr<R>) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject()));
     }
 
+    /**
+     * Create regular expression that accepts all characters
+     * Corresponds to re.allchar
+     */
+    public <R extends Sort> ReExpr<R> mkAllcharRe(R s)
+    {
+        return (ReExpr<R>) Expr.create(this, Native.mkReAllchar(nCtx(), s.getNativeObject()));
+    }
+
     /**
      * Create a range expression.
      */

src/api/python/z3/z3.py

@@ -11065,6 +11065,11 @@ def Range(lo, hi, ctx=None):
     hi = _coerce_seq(hi, ctx)
     return ReRef(Z3_mk_re_range(lo.ctx_ref(), lo.ast, hi.ast), lo.ctx)
 
+def Diff(a, b, ctx=None):
+    """Create the difference regular epression
+    """
+    return ReRef(Z3_mk_re_diff(a.ctx_ref(), a.ast, b.ast), a.ctx)
+
 def AllChar(regex_sort, ctx=None):
     """Create a regular expression that accepts all single character strings
     """

src/api/z3_api.h

@@ -1192,6 +1192,9 @@ typedef enum {
     Z3_OP_SEQ_CONTAINS,
     Z3_OP_SEQ_EXTRACT,
     Z3_OP_SEQ_REPLACE,
+    Z3_OP_SEQ_REPLACE_RE,
+    Z3_OP_SEQ_REPLACE_RE_ALL,
+    Z3_OP_SEQ_REPLACE_ALL,
     Z3_OP_SEQ_AT,
     Z3_OP_SEQ_NTH,
     Z3_OP_SEQ_LENGTH,
@@ -1216,7 +1219,9 @@ typedef enum {
     Z3_OP_RE_UNION,
     Z3_OP_RE_RANGE,
     Z3_OP_RE_LOOP,
+    Z3_OP_RE_POWER,
     Z3_OP_RE_INTERSECT,
+    Z3_OP_RE_DIFF,
     Z3_OP_RE_EMPTY_SET,
     Z3_OP_RE_FULL_SET,
     Z3_OP_RE_COMPLEMENT,
@@ -3812,6 +3817,13 @@ extern "C" {
      */
     Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re);
 
+    /**
+       \brief Create the difference of regular expressions.
+
+       def_API('Z3_mk_re_diff', AST ,(_in(CONTEXT), _in(AST), _in(AST)))
+     */
+    Z3_ast Z3_API Z3_mk_re_diff(Z3_context c, Z3_ast re1, Z3_ast re2);
+
     /**
        \brief Create an empty regular expression of sort \c re.