mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-26 09:24:36 +00:00
Code Activity

add additional regex operators to API

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-02-20 10:29:18 +02:00
parent 2e00f2f32d
commit 7091b1c856
3 changed files with 17 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/api/api_ast.cpp
View file

@ -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;
}

2
src/api/dotnet/Context.cs
View file

@ -2497,7 +2497,7 @@ namespace Microsoft.Z3
}
/// <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)
{

10
src/api/z3_api.h
View file

@ -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,