add additional regex operators to API

Z3Prover · Feb 20, 2022 · 7091b1c · 7091b1c
1 parent 2e00f2f
commit 7091b1c
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 7 deletions.
diff --git 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
@@ -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
@@ -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,