diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 87e218d99..d5de6b5fb 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 214411053..94b69d206 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -2497,7 +2497,7 @@ namespace Microsoft.Z3 } /// - /// Check if the string s1 is lexicographically strictly less than s2. + /// Check if the string s1 is lexicographically less or equal to s2. /// public BoolExpr MkStringLe(SeqExpr s1, SeqExpr s2) { diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 95c04ea17..d8c817933 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,