diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index f8c1c57dc..86dc77ad5 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -2448,30 +2448,19 @@ namespace z3 {
return expr(s.ctx(), r);
}
inline expr to_re(expr const& s) {
- Z3_ast r = Z3_mk_seq_to_re(s.ctx(), s);
- s.check_error();
- return expr(s.ctx(), r);
+ MK_EXPR1(Z3_mk_seq_to_re, s);
}
inline expr in_re(expr const& s, expr const& re) {
- check_context(s, re);
- Z3_ast r = Z3_mk_seq_in_re(s.ctx(), s, re);
- s.check_error();
- return expr(s.ctx(), r);
+ MK_EXPR2(Z3_mk_seq_in_re, s, re);
}
inline expr plus(expr const& re) {
- Z3_ast r = Z3_mk_re_plus(re.ctx(), re);
- re.check_error();
- return expr(re.ctx(), r);
+ MK_EXPR1(Z3_mk_re_plus, re);
}
inline expr option(expr const& re) {
- Z3_ast r = Z3_mk_re_option(re.ctx(), re);
- re.check_error();
- return expr(re.ctx(), r);
+ MK_EXPR1(Z3_mk_re_option, re);
}
inline expr star(expr const& re) {
- Z3_ast r = Z3_mk_re_star(re.ctx(), re);
- re.check_error();
- return expr(re.ctx(), r);
+ MK_EXPR1(Z3_mk_re_star, re);
}
inline expr re_empty(sort const& s) {
Z3_ast r = Z3_mk_re_empty(s.ctx(), s);
@@ -2491,6 +2480,9 @@ namespace z3 {
ctx.check_error();
return expr(ctx, r);
}
+ inline expr re_complement(expr const& a) {
+ MK_EXPR1(Z3_mk_re_complement, a);
+ }
inline expr range(expr const& lo, expr const& hi) {
check_context(lo, hi);
Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 494b29a00..f12ad58ea 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -2577,7 +2577,7 @@ namespace Microsoft.Z3
///
/// Take the Kleene plus of a regular expression.
///
- public ReExpr MPlus(ReExpr re)
+ public ReExpr MkPlus(ReExpr re)
{
Contract.Requires(re != null);
Contract.Ensures(Contract.Result() != null);
@@ -2587,13 +2587,23 @@ namespace Microsoft.Z3
///
/// Create the optional regular expression.
///
- public ReExpr MOption(ReExpr re)
+ public ReExpr MkOption(ReExpr re)
{
Contract.Requires(re != null);
Contract.Ensures(Contract.Result() != null);
return new ReExpr(this, Native.Z3_mk_re_option(nCtx, re.NativeObject));
}
+ ///
+ /// Create the complement regular expression.
+ ///
+ public ReExpr MkComplement(ReExpr re)
+ {
+ Contract.Requires(re != null);
+ Contract.Ensures(Contract.Result() != null);
+ return new ReExpr(this, Native.Z3_mk_re_complement(nCtx, re.NativeObject));
+ }
+
///
/// Create the concatenation of regular languages.
///