From 976fadf7714f6a35528e8b0fbd0d4910e22324b0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 9 Dec 2016 06:21:57 +0100
Subject: [PATCH] add missing complement

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/c++/z3++.h        | 24 ++++++++----------------
 src/api/dotnet/Context.cs | 14 ++++++++++++--
 2 files changed, 20 insertions(+), 18 deletions(-)

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
         /// <summary>
         /// Take the Kleene plus of a regular expression.
         /// </summary>
-        public ReExpr MPlus(ReExpr re)
+        public ReExpr MkPlus(ReExpr re)
         {
             Contract.Requires(re != null);
             Contract.Ensures(Contract.Result<ReExpr>() != null);
@@ -2587,13 +2587,23 @@ namespace Microsoft.Z3
         /// <summary>
         /// Create the optional regular expression.
         /// </summary>
-        public ReExpr MOption(ReExpr re)
+        public ReExpr MkOption(ReExpr re)
         {
             Contract.Requires(re != null);
             Contract.Ensures(Contract.Result<ReExpr>() != null);
             return new ReExpr(this, Native.Z3_mk_re_option(nCtx, re.NativeObject));            
         }
 
+        /// <summary>
+        /// Create the complement regular expression.
+        /// </summary>
+        public ReExpr MkComplement(ReExpr re)
+        {
+            Contract.Requires(re != null);
+            Contract.Ensures(Contract.Result<ReExpr>() != null);
+            return new ReExpr(this, Native.Z3_mk_re_complement(nCtx, re.NativeObject));            
+        }
+
         /// <summary>
         /// Create the concatenation of regular languages.
         /// </summary>