From 7091b1c856e6f85c3b9c0fc9cdb010f2d8ae38e7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 20 Feb 2022 10:29:18 +0200
Subject: [PATCH] add additional regex operators to API

---
 src/api/api_ast.cpp       | 12 +++++++++---
 src/api/dotnet/Context.cs |  2 +-
 src/api/z3_api.h          | 10 +++++++---
 3 files changed, 17 insertions(+), 7 deletions(-)

diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index 87e218d999a..d5de6b5fb32 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -1224,15 +1224,21 @@ extern "C" {
             case OP_RE_PLUS: return Z3_OP_RE_PLUS;
             case OP_RE_STAR: return Z3_OP_RE_STAR;
             case OP_RE_OPTION: return Z3_OP_RE_OPTION;
+            case OP_RE_RANGE: return Z3_OP_RE_RANGE;
             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_CHAR_SET: return Z3_OP_RE_FULL_SET;
+            case OP_RE_POWER: return Z3_OP_RE_POWER;
+            case OP_RE_COMPLEMENT: return Z3_OP_RE_COMPLEMENT;
             case OP_RE_EMPTY_SET: return Z3_OP_RE_EMPTY_SET;
+
+            case OP_RE_FULL_SEQ_SET: return Z3_OP_RE_FULL_SET;
+            case OP_RE_FULL_CHAR_SET: return Z3_OP_RE_FULL_CHAR_SET;
+            case OP_RE_OF_PRED: return Z3_OP_RE_OF_PRED;
+            case OP_RE_REVERSE: return Z3_OP_RE_REVERSE;
+            case OP_RE_DERIVATIVE: return Z3_OP_RE_DERIVATIVE;
             default:
                 return Z3_OP_INTERNAL;
             }
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 214411053aa..94b69d206fe 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -2497,7 +2497,7 @@ public BoolExpr MkStringLt(SeqExpr s1, SeqExpr s2)
         }
 
         /// <summary>
-        /// Check if the string s1 is lexicographically strictly less than s2.
+        /// Check if the string s1 is lexicographically less or equal to s2.
         /// </summary>
         public BoolExpr MkStringLe(SeqExpr s1, SeqExpr s2) 
         {
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 95c04ea1764..d8c817933cf 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1220,13 +1220,17 @@ typedef enum {
     Z3_OP_RE_CONCAT,
     Z3_OP_RE_UNION,
     Z3_OP_RE_RANGE,
+    Z3_OP_RE_DIFF,
+    Z3_OP_RE_INTERSECT,
     Z3_OP_RE_LOOP,
     Z3_OP_RE_POWER,
-    Z3_OP_RE_INTERSECT,
-    Z3_OP_RE_DIFF,
+    Z3_OP_RE_COMPLEMENT,
     Z3_OP_RE_EMPTY_SET,
     Z3_OP_RE_FULL_SET,
-    Z3_OP_RE_COMPLEMENT,
+    Z3_OP_RE_FULL_CHAR_SET,
+    Z3_OP_RE_OF_PRED,
+    Z3_OP_RE_REVERSE,
+    Z3_OP_RE_DERIVATIVE,
 
     // char
     Z3_OP_CHAR_CONST,