From 7a6070506dfe6f05a03e7e9ddf0166640b5d69ab Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 20 Dec 2021 10:17:06 -0800 Subject: [PATCH] #5727 Expose diff function, expose allchar in Java API expose op codes for replace/re/all --- src/api/api_ast.cpp | 7 ++++++- src/api/api_seq.cpp | 1 + src/api/c++/z3++.h | 6 ++++++ src/api/dotnet/Context.cs | 11 +++++++++++ src/api/java/Context.java | 21 +++++++++++++++++++++ src/api/python/z3/z3.py | 5 +++++ src/api/z3_api.h | 12 ++++++++++++ 7 files changed, 62 insertions(+), 1 deletion(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 7f67879bc..d11ce313e 100644 --- a/src/api/api_ast.cpp +++ b/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: diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index a7eb237b3..9dfac4a74 100644 --- a/src/api/api_seq.cpp +++ b/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); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index e323184bf..91ab6d106 100644 --- a/src/api/c++/z3++.h +++ b/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); } diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index c06f58cbd..214411053 100644 --- a/src/api/dotnet/Context.cs +++ b/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))); } + /// + /// Create a difference regular expression. + /// + 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)); + } + /// /// Create the empty regular expression. /// The sort s should be a regular expression. diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 9fcdfb1b5..0a597a6ce 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2246,8 +2246,19 @@ public class Context implements AutoCloseable { return (ReExpr) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(t))); } + /** + * Create a difference regular expression. + */ + public ReExpr mkDiff(Expr> a, Expr> b) + { + checkContextMatch(a, b); + return (ReExpr) Expr.create(this, Native.mkReDiff(nCtx(), a.getNativeObject(), b.getNativeObject())); + } + + /** * Create the empty regular expression. + * Coresponds to re.none */ public ReExpr mkEmptyRe(R s) { @@ -2256,12 +2267,22 @@ public class Context implements AutoCloseable { /** * Create the full regular expression. + * Corresponds to re.all */ public ReExpr mkFullRe(R s) { return (ReExpr) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject())); } + /** + * Create regular expression that accepts all characters + * Corresponds to re.allchar + */ + public ReExpr mkAllcharRe(R s) + { + return (ReExpr) Expr.create(this, Native.mkReAllchar(nCtx(), s.getNativeObject())); + } + /** * Create a range expression. */ diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index ae29a0b01..a11061970 100644 --- a/src/api/python/z3/z3.py +++ b/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 """ diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 0ac70ee98..d5bd1e11c 100644 --- a/src/api/z3_api.h +++ b/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.