mirror of
https://github.com/Z3Prover/z3
synced 2026-02-09 10:35:36 +00:00
Merge pull request #8499 from Z3Prover/copilot/add-regex-support-typescript-api
Add regex support to TypeScript API
This commit is contained in:
Nikolaj Bjorner
GitHub
commit
384a8e291b
4 changed files with 868 additions and 3 deletions
268
src/api/js/examples/regex-example.md
Normal file
268
src/api/js/examples/regex-example.md
Normal file
|
|
@ -0,0 +1,268 @@
|
|||
# Regular Expression Support in Z3 TypeScript API
|
||||
|
||||
This document demonstrates the new regular expression support added to the Z3 TypeScript API.
|
||||
|
||||
## Basic Usage
|
||||
|
||||
### Creating Regular Expressions
|
||||
|
||||
```typescript
|
||||
const { Re, String: Str, InRe, Solver } = Context('main');
|
||||
|
||||
// Create a regex from a string
|
||||
const hello = Re.toRe('hello');
|
||||
|
||||
// Check if a string matches
|
||||
const solver = new Solver();
|
||||
solver.add(InRe('hello', hello));
|
||||
await solver.check(); // sat
|
||||
```
|
||||
|
||||
### Star Operator (Zero or More)
|
||||
|
||||
```typescript
|
||||
const { Re, InRe, Star } = Context('main');
|
||||
|
||||
const a = Re.toRe('a');
|
||||
const aStar = Star(a);
|
||||
|
||||
// Empty string matches a*
|
||||
InRe('', aStar); // true
|
||||
|
||||
// Multiple 'a's match
|
||||
InRe('aaa', aStar); // true
|
||||
```
|
||||
|
||||
### Plus Operator (One or More)
|
||||
|
||||
```typescript
|
||||
const { Re, InRe, Plus } = Context('main');
|
||||
|
||||
const a = Re.toRe('a');
|
||||
const aPlus = Plus(a);
|
||||
|
||||
// Empty string does NOT match a+
|
||||
InRe('', aPlus); // false
|
||||
|
||||
// One or more 'a's match
|
||||
InRe('aa', aPlus); // true
|
||||
```
|
||||
|
||||
### Option Operator (Zero or One)
|
||||
|
||||
```typescript
|
||||
const { Re, InRe, Option } = Context('main');
|
||||
|
||||
const a = Re.toRe('a');
|
||||
const aOpt = Option(a);
|
||||
|
||||
// Both empty and 'a' match a?
|
||||
InRe('', aOpt); // true
|
||||
InRe('a', aOpt); // true
|
||||
InRe('aa', aOpt); // false
|
||||
```
|
||||
|
||||
### Union (Or)
|
||||
|
||||
```typescript
|
||||
const { Re, InRe, Union } = Context('main');
|
||||
|
||||
const a = Re.toRe('a');
|
||||
const b = Re.toRe('b');
|
||||
const aOrB = Union(a, b);
|
||||
|
||||
// Either 'a' or 'b' match
|
||||
InRe('a', aOrB); // true
|
||||
InRe('b', aOrB); // true
|
||||
InRe('c', aOrB); // false
|
||||
```
|
||||
|
||||
### Intersect (And)
|
||||
|
||||
```typescript
|
||||
const { Re, InRe, Intersect, Star } = Context('main');
|
||||
|
||||
const a = Re.toRe('a');
|
||||
const b = Re.toRe('b');
|
||||
const both = Intersect(Star(a), Star(b));
|
||||
|
||||
// Only empty string matches both a* and b*
|
||||
InRe('', both); // true
|
||||
InRe('a', both); // false
|
||||
```
|
||||
|
||||
### Range
|
||||
|
||||
```typescript
|
||||
const { Range, InRe } = Context('main');
|
||||
|
||||
const azRange = Range('a', 'z');
|
||||
|
||||
// Lowercase letters match
|
||||
InRe('m', azRange); // true
|
||||
|
||||
// Others don't
|
||||
InRe('1', azRange); // false
|
||||
InRe('Z', azRange); // false
|
||||
```
|
||||
|
||||
### Loop (Bounded Repetition)
|
||||
|
||||
```typescript
|
||||
const { Re, InRe, Loop } = Context('main');
|
||||
|
||||
const a = Re.toRe('a');
|
||||
|
||||
// Between 2 and 3 repetitions
|
||||
const a2to3 = Loop(a, 2, 3);
|
||||
InRe('aa', a2to3); // true
|
||||
InRe('aaa', a2to3); // true
|
||||
InRe('a', a2to3); // false
|
||||
InRe('aaaa', a2to3); // false
|
||||
|
||||
// At least 2 repetitions (hi=0 or omitted means unbounded)
|
||||
const a2Plus = Loop(a, 2, 0); // or Loop(a, 2)
|
||||
InRe('aa', a2Plus); // true
|
||||
InRe('aaa', a2Plus); // true
|
||||
InRe('aaaa', a2Plus); // true
|
||||
InRe('a', a2Plus); // false
|
||||
```
|
||||
|
||||
### Power (Exact Repetition)
|
||||
|
||||
```typescript
|
||||
const { Re, InRe, Power } = Context('main');
|
||||
|
||||
const a = Re.toRe('a');
|
||||
const a3 = Power(a, 3);
|
||||
|
||||
// Exactly 3 repetitions match
|
||||
InRe('aaa', a3); // true
|
||||
|
||||
// Others don't
|
||||
InRe('aa', a3); // false
|
||||
InRe('aaaa', a3); // false
|
||||
```
|
||||
|
||||
### Complement (Negation)
|
||||
|
||||
```typescript
|
||||
const { Re, InRe, Complement } = Context('main');
|
||||
|
||||
const a = Re.toRe('a');
|
||||
const notA = Complement(a);
|
||||
|
||||
// Everything except 'a' matches
|
||||
InRe('a', notA); // false
|
||||
InRe('b', notA); // true
|
||||
InRe('', notA); // true
|
||||
```
|
||||
|
||||
### Diff (Set Difference)
|
||||
|
||||
```typescript
|
||||
const { Re, InRe, Diff, Star } = Context('main');
|
||||
|
||||
const a = Re.toRe('a');
|
||||
const b = Re.toRe('b');
|
||||
const diff = Diff(Star(a), b);
|
||||
|
||||
// a* except 'b'
|
||||
InRe('aaa', diff); // true
|
||||
InRe('b', diff); // false
|
||||
```
|
||||
|
||||
### ReConcat (Concatenation)
|
||||
|
||||
```typescript
|
||||
const { Re, InRe, ReConcat } = Context('main');
|
||||
|
||||
const hello = Re.toRe('hello');
|
||||
const world = Re.toRe('world');
|
||||
const helloworld = ReConcat(hello, world);
|
||||
|
||||
// Concatenated strings match
|
||||
InRe('helloworld', helloworld); // true
|
||||
InRe('hello', helloworld); // false
|
||||
```
|
||||
|
||||
## Method Chaining
|
||||
|
||||
Regular expression objects support method chaining:
|
||||
|
||||
```typescript
|
||||
const { Re, InRe } = Context('main');
|
||||
|
||||
const a = Re.toRe('a');
|
||||
|
||||
// Using methods
|
||||
const aStar = a.star();
|
||||
const aPlus = a.plus();
|
||||
const aOpt = a.option();
|
||||
const notA = a.complement();
|
||||
|
||||
// Chaining
|
||||
const complex = a.plus().union(Re.toRe('b').star());
|
||||
```
|
||||
|
||||
## Complex Example: Pattern Matching
|
||||
|
||||
```typescript
|
||||
const { Re, String: Str, InRe, Union, Star, Solver } = Context('main');
|
||||
|
||||
const x = Str.const('x');
|
||||
const a = Re.toRe('a');
|
||||
const b = Re.toRe('b');
|
||||
|
||||
// Pattern: any combination of 'a' and 'b'
|
||||
const pattern = Star(Union(a, b));
|
||||
|
||||
const solver = new Solver();
|
||||
solver.add(InRe(x, pattern));
|
||||
solver.add(x.length().eq(5));
|
||||
|
||||
if (await solver.check() === 'sat') {
|
||||
const model = solver.model();
|
||||
const result = model.eval(x);
|
||||
// Result will be a 5-character string containing only 'a' and 'b'
|
||||
console.log(result.asString()); // e.g., "aabba"
|
||||
}
|
||||
```
|
||||
|
||||
## API Reference
|
||||
|
||||
### Factory Methods
|
||||
|
||||
- `Re.sort(seqSort)` - Create a regex sort
|
||||
- `Re.toRe(seq)` - Convert sequence/string to regex
|
||||
|
||||
### Operators
|
||||
|
||||
- `Star(re)` - Zero or more repetitions (*)
|
||||
- `Plus(re)` - One or more repetitions (+)
|
||||
- `Option(re)` - Zero or one repetition (?)
|
||||
- `Union(...res)` - Or operation (|)
|
||||
- `Intersect(...res)` - And operation (&)
|
||||
- `ReConcat(...res)` - Concatenation
|
||||
- `Complement(re)` - Negation (~)
|
||||
- `Diff(a, b)` - Set difference (a \ b)
|
||||
- `Range(lo, hi)` - Character range
|
||||
- `Loop(re, lo, hi?)` - Bounded repetition {lo,hi} or at least lo if hi=0 or omitted
|
||||
- `Power(re, n)` - Exact repetition {n}
|
||||
|
||||
### Special Patterns
|
||||
|
||||
- `AllChar(reSort)` - Match any single character
|
||||
- `Empty(reSort)` - Empty language
|
||||
- `Full(reSort)` - Match all strings
|
||||
|
||||
### Membership Test
|
||||
|
||||
- `InRe(seq, re)` - Test if sequence matches regex
|
||||
|
||||
## Notes
|
||||
|
||||
- All regex operations are symbolic - they create constraints rather than executing pattern matching
|
||||
- The solver finds strings that satisfy the regex constraints
|
||||
- Regular expressions can be combined with other Z3 constraints (length, containment, etc.)
|
||||
- This implementation follows the SMT-LIB2 regular expression theory
|
||||
|
|
@ -1844,6 +1844,252 @@ describe('high-level', () => {
|
|||
});
|
||||
});
|
||||
|
||||
describe('regular expressions', () => {
|
||||
it('can create regex sort', () => {
|
||||
const { Re, String: Str, eqIdentity } = api.Context('main');
|
||||
|
||||
const reSort = Re.sort(Str.sort());
|
||||
expect(eqIdentity(reSort.basis(), Str.sort())).toBe(true);
|
||||
});
|
||||
|
||||
it('can convert string to regex', async () => {
|
||||
const { Re, String: Str, InRe, Solver } = api.Context('main');
|
||||
|
||||
const hello = Str.val('hello');
|
||||
const re = Re.toRe(hello);
|
||||
|
||||
const solver = new Solver();
|
||||
solver.add(InRe('hello', re));
|
||||
|
||||
const result = await solver.check();
|
||||
expect(result).toBe('sat');
|
||||
});
|
||||
|
||||
it('can use star operator', async () => {
|
||||
const { Re, String: Str, InRe, Star, Solver } = api.Context('main');
|
||||
|
||||
const a = Re.toRe('a');
|
||||
const aStar = Star(a);
|
||||
|
||||
const solver = new Solver();
|
||||
// Empty string matches a*
|
||||
solver.add(InRe('', aStar));
|
||||
|
||||
const result = await solver.check();
|
||||
expect(result).toBe('sat');
|
||||
});
|
||||
|
||||
it('can use plus operator', async () => {
|
||||
const { Re, String: Str, InRe, Plus, Solver } = api.Context('main');
|
||||
|
||||
const a = Re.toRe('a');
|
||||
const aPlus = Plus(a);
|
||||
|
||||
const solver = new Solver();
|
||||
// "aa" matches a+
|
||||
solver.add(InRe('aa', aPlus));
|
||||
|
||||
const result = await solver.check();
|
||||
expect(result).toBe('sat');
|
||||
});
|
||||
|
||||
it('can use option operator', async () => {
|
||||
const { Re, InRe, Option, Solver } = api.Context('main');
|
||||
|
||||
const a = Re.toRe('a');
|
||||
const aOpt = Option(a);
|
||||
|
||||
const solver1 = new Solver();
|
||||
// Empty string matches a?
|
||||
solver1.add(InRe('', aOpt));
|
||||
expect(await solver1.check()).toBe('sat');
|
||||
|
||||
const solver2 = new Solver();
|
||||
// "a" matches a?
|
||||
solver2.add(InRe('a', aOpt));
|
||||
expect(await solver2.check()).toBe('sat');
|
||||
});
|
||||
|
||||
it('can use union operator', async () => {
|
||||
const { Re, InRe, Union, Solver } = api.Context('main');
|
||||
|
||||
const a = Re.toRe('a');
|
||||
const b = Re.toRe('b');
|
||||
const aOrB = Union(a, b);
|
||||
|
||||
const solver1 = new Solver();
|
||||
solver1.add(InRe('a', aOrB));
|
||||
expect(await solver1.check()).toBe('sat');
|
||||
|
||||
const solver2 = new Solver();
|
||||
solver2.add(InRe('b', aOrB));
|
||||
expect(await solver2.check()).toBe('sat');
|
||||
|
||||
const solver3 = new Solver();
|
||||
solver3.add(InRe('c', aOrB));
|
||||
expect(await solver3.check()).toBe('unsat');
|
||||
});
|
||||
|
||||
it('can use intersect operator', async () => {
|
||||
const { Re, InRe, Intersect, Star, Solver } = api.Context('main');
|
||||
|
||||
const a = Re.toRe('a');
|
||||
const b = Re.toRe('b');
|
||||
const aStar = Star(a);
|
||||
const bStar = Star(b);
|
||||
const both = Intersect(aStar, bStar);
|
||||
|
||||
const solver = new Solver();
|
||||
// Only empty string matches both a* and b*
|
||||
solver.add(InRe('', both));
|
||||
expect(await solver.check()).toBe('sat');
|
||||
});
|
||||
|
||||
it('can use range operator', async () => {
|
||||
const { Range, InRe, Solver } = api.Context('main');
|
||||
|
||||
const azRange = Range('a', 'z');
|
||||
|
||||
const solver1 = new Solver();
|
||||
solver1.add(InRe('m', azRange));
|
||||
expect(await solver1.check()).toBe('sat');
|
||||
|
||||
const solver2 = new Solver();
|
||||
solver2.add(InRe('1', azRange));
|
||||
expect(await solver2.check()).toBe('unsat');
|
||||
});
|
||||
|
||||
it('can use loop operator', async () => {
|
||||
const { Re, InRe, Loop, Solver } = api.Context('main');
|
||||
|
||||
const a = Re.toRe('a');
|
||||
const a2to3 = Loop(a, 2, 3);
|
||||
|
||||
const solver1 = new Solver();
|
||||
solver1.add(InRe('aa', a2to3));
|
||||
expect(await solver1.check()).toBe('sat');
|
||||
|
||||
const solver2 = new Solver();
|
||||
solver2.add(InRe('aaa', a2to3));
|
||||
expect(await solver2.check()).toBe('sat');
|
||||
|
||||
const solver3 = new Solver();
|
||||
solver3.add(InRe('a', a2to3));
|
||||
expect(await solver3.check()).toBe('unsat');
|
||||
|
||||
const solver4 = new Solver();
|
||||
solver4.add(InRe('aaaa', a2to3));
|
||||
expect(await solver4.check()).toBe('unsat');
|
||||
});
|
||||
|
||||
it('can use power operator', async () => {
|
||||
const { Re, InRe, Power, Solver } = api.Context('main');
|
||||
|
||||
const a = Re.toRe('a');
|
||||
const a3 = Power(a, 3);
|
||||
|
||||
const solver1 = new Solver();
|
||||
solver1.add(InRe('aaa', a3));
|
||||
expect(await solver1.check()).toBe('sat');
|
||||
|
||||
const solver2 = new Solver();
|
||||
solver2.add(InRe('aa', a3));
|
||||
expect(await solver2.check()).toBe('unsat');
|
||||
});
|
||||
|
||||
it('can use complement operator', async () => {
|
||||
const { Re, InRe, Complement, Solver } = api.Context('main');
|
||||
|
||||
const a = Re.toRe('a');
|
||||
const notA = Complement(a);
|
||||
|
||||
const solver1 = new Solver();
|
||||
solver1.add(InRe('a', notA));
|
||||
expect(await solver1.check()).toBe('unsat');
|
||||
|
||||
const solver2 = new Solver();
|
||||
solver2.add(InRe('b', notA));
|
||||
expect(await solver2.check()).toBe('sat');
|
||||
});
|
||||
|
||||
it('can use diff operator', async () => {
|
||||
const { Re, InRe, Diff, Star, Solver } = api.Context('main');
|
||||
|
||||
const a = Re.toRe('a');
|
||||
const b = Re.toRe('b');
|
||||
const aStar = Star(a);
|
||||
const diff = Diff(aStar, b);
|
||||
|
||||
const solver1 = new Solver();
|
||||
solver1.add(InRe('aaa', diff));
|
||||
expect(await solver1.check()).toBe('sat');
|
||||
|
||||
const solver2 = new Solver();
|
||||
solver2.add(InRe('b', diff));
|
||||
expect(await solver2.check()).toBe('unsat');
|
||||
});
|
||||
|
||||
it('can use ReConcat operator', async () => {
|
||||
const { Re, InRe, ReConcat, Solver } = api.Context('main');
|
||||
|
||||
const hello = Re.toRe('hello');
|
||||
const world = Re.toRe('world');
|
||||
const helloworld = ReConcat(hello, world);
|
||||
|
||||
const solver1 = new Solver();
|
||||
solver1.add(InRe('helloworld', helloworld));
|
||||
expect(await solver1.check()).toBe('sat');
|
||||
|
||||
const solver2 = new Solver();
|
||||
solver2.add(InRe('hello', helloworld));
|
||||
expect(await solver2.check()).toBe('unsat');
|
||||
});
|
||||
|
||||
it('can use method chaining', async () => {
|
||||
const { Re, InRe, Solver } = api.Context('main');
|
||||
|
||||
const a = Re.toRe('a');
|
||||
const aStar = a.star();
|
||||
const aPlus = a.plus();
|
||||
|
||||
const solver1 = new Solver();
|
||||
solver1.add(InRe('', aStar));
|
||||
expect(await solver1.check()).toBe('sat');
|
||||
|
||||
const solver2 = new Solver();
|
||||
solver2.add(InRe('', aPlus));
|
||||
expect(await solver2.check()).toBe('unsat');
|
||||
});
|
||||
|
||||
it('can solve complex regex constraints', async () => {
|
||||
const { Re, String: Str, InRe, Union, Star, Solver } = api.Context('main');
|
||||
|
||||
const x = Str.const('x');
|
||||
const a = Re.toRe('a');
|
||||
const b = Re.toRe('b');
|
||||
const pattern = Star(Union(a, b));
|
||||
|
||||
const solver = new Solver();
|
||||
solver.add(InRe(x, pattern));
|
||||
solver.add(x.length().eq(5));
|
||||
|
||||
const result = await solver.check();
|
||||
expect(result).toBe('sat');
|
||||
|
||||
if (result === 'sat') {
|
||||
const model = solver.model();
|
||||
const xVal = model.eval(x);
|
||||
// Check if it's a string using the isString method if available
|
||||
if ('isString' in xVal && typeof xVal.isString === 'function' && xVal.isString()) {
|
||||
const strVal = (xVal as any).asString();
|
||||
expect(strVal.length).toBe(5);
|
||||
// Verify it only contains 'a' and 'b'
|
||||
expect(/^[ab]+$/.test(strVal)).toBe(true);
|
||||
}
|
||||
}
|
||||
});
|
||||
});
|
||||
|
||||
describe('Params API', () => {
|
||||
it('can create params', () => {
|
||||
const { Params } = api.Context('main');
|
||||
|
|
|
|||
|
|
@ -96,6 +96,9 @@ import {
|
|||
RatNum,
|
||||
RCFNum,
|
||||
RCFNumCreation,
|
||||
Re,
|
||||
ReSort,
|
||||
ReCreation,
|
||||
Seq,
|
||||
SeqSort,
|
||||
Simplifier,
|
||||
|
|
@ -297,6 +300,8 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
|
|||
return new FPRMSortImpl(ast);
|
||||
case Z3_sort_kind.Z3_SEQ_SORT:
|
||||
return new SeqSortImpl(ast);
|
||||
case Z3_sort_kind.Z3_RE_SORT:
|
||||
return new ReSortImpl(ast);
|
||||
case Z3_sort_kind.Z3_ARRAY_SORT:
|
||||
return new ArraySortImpl(ast);
|
||||
default:
|
||||
|
|
@ -340,6 +345,8 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
|
|||
return new FPRMImpl(ast);
|
||||
case Z3_sort_kind.Z3_SEQ_SORT:
|
||||
return new SeqImpl(ast);
|
||||
case Z3_sort_kind.Z3_RE_SORT:
|
||||
return new ReImpl(ast);
|
||||
case Z3_sort_kind.Z3_ARRAY_SORT:
|
||||
return new ArrayImpl(ast);
|
||||
default:
|
||||
|
|
@ -611,6 +618,18 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
|
|||
return r;
|
||||
}
|
||||
|
||||
function isReSort(obj: unknown): obj is ReSort<Name> {
|
||||
const r = obj instanceof ReSortImpl;
|
||||
r && _assertContext(obj);
|
||||
return r;
|
||||
}
|
||||
|
||||
function isRe(obj: unknown): obj is Re<Name> {
|
||||
const r = obj instanceof ReImpl;
|
||||
r && _assertContext(obj);
|
||||
return r;
|
||||
}
|
||||
|
||||
function isStringSort(obj: unknown): obj is SeqSort<Name> {
|
||||
return isSeqSort(obj) && obj.isString();
|
||||
}
|
||||
|
|
@ -1000,6 +1019,17 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
|
|||
},
|
||||
};
|
||||
|
||||
const Re = {
|
||||
sort<SeqSortRef extends SeqSort<Name>>(seqSort: SeqSortRef): ReSort<Name, SeqSortRef> {
|
||||
return new ReSortImpl<SeqSortRef>(Z3.mk_re_sort(contextPtr, seqSort.ptr));
|
||||
},
|
||||
|
||||
toRe(seq: Seq<Name> | string): Re<Name> {
|
||||
const seqExpr = isSeq(seq) ? seq : String.val(seq);
|
||||
return new ReImpl(check(Z3.mk_seq_to_re(contextPtr, seqExpr.ast)));
|
||||
},
|
||||
};
|
||||
|
||||
const Array = {
|
||||
sort<DomainSort extends NonEmptySortArray<Name>, RangeSort extends AnySort<Name>>(
|
||||
...sig: [...DomainSort, RangeSort]
|
||||
|
|
@ -1765,6 +1795,97 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
|
|||
return new BoolImpl(check(Z3.mk_set_subset(contextPtr, a.ast, b.ast)));
|
||||
}
|
||||
|
||||
//////////////////////
|
||||
// Regular Expressions
|
||||
//////////////////////
|
||||
|
||||
function InRe(seq: Seq<Name> | string, re: Re<Name>): Bool<Name> {
|
||||
const seqExpr = isSeq(seq) ? seq : String.val(seq);
|
||||
return new BoolImpl(check(Z3.mk_seq_in_re(contextPtr, seqExpr.ast, re.ast)));
|
||||
}
|
||||
|
||||
function Union<SeqSortRef extends SeqSort<Name>>(...res: Re<Name, SeqSortRef>[]): Re<Name, SeqSortRef> {
|
||||
if (res.length === 0) {
|
||||
throw new Error('Union requires at least one argument');
|
||||
}
|
||||
if (res.length === 1) {
|
||||
return res[0];
|
||||
}
|
||||
return new ReImpl<SeqSortRef>(check(Z3.mk_re_union(contextPtr, res.map(r => r.ast))));
|
||||
}
|
||||
|
||||
function Intersect<SeqSortRef extends SeqSort<Name>>(...res: Re<Name, SeqSortRef>[]): Re<Name, SeqSortRef> {
|
||||
if (res.length === 0) {
|
||||
throw new Error('Intersect requires at least one argument');
|
||||
}
|
||||
if (res.length === 1) {
|
||||
return res[0];
|
||||
}
|
||||
return new ReImpl<SeqSortRef>(check(Z3.mk_re_intersect(contextPtr, res.map(r => r.ast))));
|
||||
}
|
||||
|
||||
function ReConcat<SeqSortRef extends SeqSort<Name>>(...res: Re<Name, SeqSortRef>[]): Re<Name, SeqSortRef> {
|
||||
if (res.length === 0) {
|
||||
throw new Error('ReConcat requires at least one argument');
|
||||
}
|
||||
if (res.length === 1) {
|
||||
return res[0];
|
||||
}
|
||||
return new ReImpl<SeqSortRef>(check(Z3.mk_re_concat(contextPtr, res.map(r => r.ast))));
|
||||
}
|
||||
|
||||
function Plus<SeqSortRef extends SeqSort<Name>>(re: Re<Name, SeqSortRef>): Re<Name, SeqSortRef> {
|
||||
return new ReImpl<SeqSortRef>(check(Z3.mk_re_plus(contextPtr, re.ast)));
|
||||
}
|
||||
|
||||
function Star<SeqSortRef extends SeqSort<Name>>(re: Re<Name, SeqSortRef>): Re<Name, SeqSortRef> {
|
||||
return new ReImpl<SeqSortRef>(check(Z3.mk_re_star(contextPtr, re.ast)));
|
||||
}
|
||||
|
||||
function Option<SeqSortRef extends SeqSort<Name>>(re: Re<Name, SeqSortRef>): Re<Name, SeqSortRef> {
|
||||
return new ReImpl<SeqSortRef>(check(Z3.mk_re_option(contextPtr, re.ast)));
|
||||
}
|
||||
|
||||
function Complement<SeqSortRef extends SeqSort<Name>>(re: Re<Name, SeqSortRef>): Re<Name, SeqSortRef> {
|
||||
return new ReImpl<SeqSortRef>(check(Z3.mk_re_complement(contextPtr, re.ast)));
|
||||
}
|
||||
|
||||
function Diff<SeqSortRef extends SeqSort<Name>>(a: Re<Name, SeqSortRef>, b: Re<Name, SeqSortRef>): Re<Name, SeqSortRef> {
|
||||
return new ReImpl<SeqSortRef>(check(Z3.mk_re_diff(contextPtr, a.ast, b.ast)));
|
||||
}
|
||||
|
||||
function Range<SeqSortRef extends SeqSort<Name>>(lo: Seq<Name, SeqSortRef> | string, hi: Seq<Name, SeqSortRef> | string): Re<Name, SeqSortRef> {
|
||||
const loSeq = isSeq(lo) ? lo : String.val(lo);
|
||||
const hiSeq = isSeq(hi) ? hi : String.val(hi);
|
||||
return new ReImpl<SeqSortRef>(check(Z3.mk_re_range(contextPtr, loSeq.ast, hiSeq.ast)));
|
||||
}
|
||||
|
||||
/**
|
||||
* Create a bounded repetition regex.
|
||||
* @param re The regex to repeat
|
||||
* @param lo Minimum number of repetitions
|
||||
* @param hi Maximum number of repetitions (0 means unbounded, i.e., at least lo)
|
||||
*/
|
||||
function Loop<SeqSortRef extends SeqSort<Name>>(re: Re<Name, SeqSortRef>, lo: number, hi: number = 0): Re<Name, SeqSortRef> {
|
||||
return new ReImpl<SeqSortRef>(check(Z3.mk_re_loop(contextPtr, re.ast, lo, hi)));
|
||||
}
|
||||
|
||||
function Power<SeqSortRef extends SeqSort<Name>>(re: Re<Name, SeqSortRef>, n: number): Re<Name, SeqSortRef> {
|
||||
return new ReImpl<SeqSortRef>(check(Z3.mk_re_power(contextPtr, re.ast, n)));
|
||||
}
|
||||
|
||||
function AllChar<SeqSortRef extends SeqSort<Name>>(reSort: ReSort<Name, SeqSortRef>): Re<Name, SeqSortRef> {
|
||||
return new ReImpl<SeqSortRef>(check(Z3.mk_re_allchar(contextPtr, reSort.ptr)));
|
||||
}
|
||||
|
||||
function Empty<SeqSortRef extends SeqSort<Name>>(reSort: ReSort<Name, SeqSortRef>): Re<Name, SeqSortRef> {
|
||||
return new ReImpl<SeqSortRef>(check(Z3.mk_re_empty(contextPtr, reSort.ptr)));
|
||||
}
|
||||
|
||||
function Full<SeqSortRef extends SeqSort<Name>>(reSort: ReSort<Name, SeqSortRef>): Re<Name, SeqSortRef> {
|
||||
return new ReImpl<SeqSortRef>(check(Z3.mk_re_full(contextPtr, reSort.ptr)));
|
||||
}
|
||||
|
||||
function mkPartialOrder(sort: Sort<Name>, index: number): FuncDecl<Name> {
|
||||
return new FuncDeclImpl(check(Z3.mk_partial_order(contextPtr, sort.ptr, index)));
|
||||
}
|
||||
|
|
@ -4024,6 +4145,76 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
|
|||
}
|
||||
}
|
||||
|
||||
class ReSortImpl<SeqSortRef extends SeqSort<Name> = SeqSort<Name>> extends SortImpl implements ReSort<Name, SeqSortRef> {
|
||||
declare readonly __typename: ReSort['__typename'];
|
||||
|
||||
basis(): SeqSortRef {
|
||||
return _toSort(check(Z3.get_re_sort_basis(contextPtr, this.ptr))) as SeqSortRef;
|
||||
}
|
||||
|
||||
cast(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
|
||||
cast(other: CoercibleToExpr<Name>): Expr<Name>;
|
||||
cast(other: any): any {
|
||||
if (isRe(other)) {
|
||||
_assertContext(other);
|
||||
return other;
|
||||
}
|
||||
throw new Error("Can't cast to ReSort");
|
||||
}
|
||||
}
|
||||
|
||||
class ReImpl<SeqSortRef extends SeqSort<Name> = SeqSort<Name>>
|
||||
extends ExprImpl<Z3_ast, ReSortImpl<SeqSortRef>>
|
||||
implements Re<Name, SeqSortRef>
|
||||
{
|
||||
declare readonly __typename: Re['__typename'];
|
||||
|
||||
plus(): Re<Name, SeqSortRef> {
|
||||
return new ReImpl<SeqSortRef>(check(Z3.mk_re_plus(contextPtr, this.ast)));
|
||||
}
|
||||
|
||||
star(): Re<Name, SeqSortRef> {
|
||||
return new ReImpl<SeqSortRef>(check(Z3.mk_re_star(contextPtr, this.ast)));
|
||||
}
|
||||
|
||||
option(): Re<Name, SeqSortRef> {
|
||||
return new ReImpl<SeqSortRef>(check(Z3.mk_re_option(contextPtr, this.ast)));
|
||||
}
|
||||
|
||||
complement(): Re<Name, SeqSortRef> {
|
||||
return new ReImpl<SeqSortRef>(check(Z3.mk_re_complement(contextPtr, this.ast)));
|
||||
}
|
||||
|
||||
union(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef> {
|
||||
return new ReImpl<SeqSortRef>(check(Z3.mk_re_union(contextPtr, [this.ast, other.ast])));
|
||||
}
|
||||
|
||||
intersect(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef> {
|
||||
return new ReImpl<SeqSortRef>(check(Z3.mk_re_intersect(contextPtr, [this.ast, other.ast])));
|
||||
}
|
||||
|
||||
diff(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef> {
|
||||
return new ReImpl<SeqSortRef>(check(Z3.mk_re_diff(contextPtr, this.ast, other.ast)));
|
||||
}
|
||||
|
||||
concat(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef> {
|
||||
return new ReImpl<SeqSortRef>(check(Z3.mk_re_concat(contextPtr, [this.ast, other.ast])));
|
||||
}
|
||||
|
||||
/**
|
||||
* Create a bounded repetition of this regex
|
||||
* @param lo Minimum number of repetitions
|
||||
* @param hi Maximum number of repetitions (0 means unbounded, i.e., at least lo)
|
||||
*/
|
||||
loop(lo: number, hi: number = 0): Re<Name, SeqSortRef> {
|
||||
return new ReImpl<SeqSortRef>(check(Z3.mk_re_loop(contextPtr, this.ast, lo, hi)));
|
||||
}
|
||||
|
||||
power(n: number): Re<Name, SeqSortRef> {
|
||||
return new ReImpl<SeqSortRef>(check(Z3.mk_re_power(contextPtr, this.ast, n)));
|
||||
}
|
||||
}
|
||||
|
||||
class ArraySortImpl<DomainSort extends NonEmptySortArray<Name>, RangeSort extends Sort<Name>>
|
||||
extends SortImpl
|
||||
implements SMTArraySort<Name, DomainSort, RangeSort>
|
||||
|
|
@ -4731,6 +4922,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
|
|||
FloatRM,
|
||||
String,
|
||||
Seq,
|
||||
Re,
|
||||
Array,
|
||||
Set,
|
||||
Datatype,
|
||||
|
|
@ -4823,6 +5015,23 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
|
|||
FullSet,
|
||||
isMember,
|
||||
isSubset,
|
||||
|
||||
InRe,
|
||||
Union,
|
||||
Intersect,
|
||||
ReConcat,
|
||||
Plus,
|
||||
Star,
|
||||
Option,
|
||||
Complement,
|
||||
Diff,
|
||||
Range,
|
||||
Loop,
|
||||
Power,
|
||||
AllChar,
|
||||
Empty,
|
||||
Full,
|
||||
|
||||
mkPartialOrder,
|
||||
mkTransitiveClosure,
|
||||
polynomialSubresultants,
|
||||
|
|
|
|||
|
|
@ -36,7 +36,8 @@ export type AnySort<Name extends string = 'main'> =
|
|||
| SMTArraySort<Name>
|
||||
| FPSort<Name>
|
||||
| FPRMSort<Name>
|
||||
| SeqSort<Name>;
|
||||
| SeqSort<Name>
|
||||
| ReSort<Name>;
|
||||
/** @hidden */
|
||||
export type AnyExpr<Name extends string = 'main'> =
|
||||
| Expr<Name>
|
||||
|
|
@ -50,7 +51,8 @@ export type AnyExpr<Name extends string = 'main'> =
|
|||
| FP<Name>
|
||||
| FPNum<Name>
|
||||
| FPRM<Name>
|
||||
| Seq<Name>;
|
||||
| Seq<Name>
|
||||
| Re<Name>;
|
||||
/** @hidden */
|
||||
export type AnyAst<Name extends string = 'main'> = AnyExpr<Name> | AnySort<Name> | FuncDecl<Name>;
|
||||
|
||||
|
|
@ -70,6 +72,8 @@ export type SortToExprMap<S extends AnySort<Name>, Name extends string = 'main'>
|
|||
? FPRM<Name>
|
||||
: S extends SeqSort<Name>
|
||||
? Seq<Name>
|
||||
: S extends ReSort<Name>
|
||||
? Re<Name>
|
||||
: S extends Sort<Name>
|
||||
? Expr<Name, S, Z3_ast>
|
||||
: never;
|
||||
|
|
@ -458,6 +462,8 @@ export interface Context<Name extends string = 'main'> {
|
|||
/** @category Expressions */
|
||||
readonly Seq: SeqCreation<Name>;
|
||||
/** @category Expressions */
|
||||
readonly Re: ReCreation<Name>;
|
||||
/** @category Expressions */
|
||||
readonly Array: SMTArrayCreation<Name>;
|
||||
/** @category Expressions */
|
||||
readonly Set: SMTSetCreation<Name>;
|
||||
|
|
@ -846,6 +852,61 @@ export interface Context<Name extends string = 'main'> {
|
|||
/** @category Operations */
|
||||
isSubset<ElemSort extends AnySort<Name>>(a: SMTSet<Name, ElemSort>, b: SMTSet<Name, ElemSort>): Bool<Name>;
|
||||
|
||||
//////////////////////
|
||||
// Regular Expressions
|
||||
//////////////////////
|
||||
|
||||
/** @category RegularExpression */
|
||||
InRe(seq: Seq<Name> | string, re: Re<Name>): Bool<Name>;
|
||||
|
||||
/** @category RegularExpression */
|
||||
Union<SeqSortRef extends SeqSort<Name>>(...res: Re<Name, SeqSortRef>[]): Re<Name, SeqSortRef>;
|
||||
|
||||
/** @category RegularExpression */
|
||||
Intersect<SeqSortRef extends SeqSort<Name>>(...res: Re<Name, SeqSortRef>[]): Re<Name, SeqSortRef>;
|
||||
|
||||
/** @category RegularExpression */
|
||||
ReConcat<SeqSortRef extends SeqSort<Name>>(...res: Re<Name, SeqSortRef>[]): Re<Name, SeqSortRef>;
|
||||
|
||||
/** @category RegularExpression */
|
||||
Plus<SeqSortRef extends SeqSort<Name>>(re: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
|
||||
|
||||
/** @category RegularExpression */
|
||||
Star<SeqSortRef extends SeqSort<Name>>(re: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
|
||||
|
||||
/** @category RegularExpression */
|
||||
Option<SeqSortRef extends SeqSort<Name>>(re: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
|
||||
|
||||
/** @category RegularExpression */
|
||||
Complement<SeqSortRef extends SeqSort<Name>>(re: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
|
||||
|
||||
/** @category RegularExpression */
|
||||
Diff<SeqSortRef extends SeqSort<Name>>(a: Re<Name, SeqSortRef>, b: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
|
||||
|
||||
/** @category RegularExpression */
|
||||
Range<SeqSortRef extends SeqSort<Name>>(lo: Seq<Name, SeqSortRef> | string, hi: Seq<Name, SeqSortRef> | string): Re<Name, SeqSortRef>;
|
||||
|
||||
/**
|
||||
* Create a bounded repetition regex
|
||||
* @param re The regex to repeat
|
||||
* @param lo Minimum number of repetitions
|
||||
* @param hi Maximum number of repetitions (0 means unbounded, i.e., at least lo)
|
||||
* @category RegularExpression
|
||||
*/
|
||||
Loop<SeqSortRef extends SeqSort<Name>>(re: Re<Name, SeqSortRef>, lo: number, hi?: number): Re<Name, SeqSortRef>;
|
||||
|
||||
/** @category RegularExpression */
|
||||
Power<SeqSortRef extends SeqSort<Name>>(re: Re<Name, SeqSortRef>, n: number): Re<Name, SeqSortRef>;
|
||||
|
||||
/** @category RegularExpression */
|
||||
AllChar<SeqSortRef extends SeqSort<Name>>(reSort: ReSort<Name, SeqSortRef>): Re<Name, SeqSortRef>;
|
||||
|
||||
/** @category RegularExpression */
|
||||
Empty<SeqSortRef extends SeqSort<Name>>(reSort: ReSort<Name, SeqSortRef>): Re<Name, SeqSortRef>;
|
||||
|
||||
/** @category RegularExpression */
|
||||
Full<SeqSortRef extends SeqSort<Name>>(reSort: ReSort<Name, SeqSortRef>): Re<Name, SeqSortRef>;
|
||||
|
||||
/**
|
||||
* Create a partial order relation over a sort.
|
||||
* @param sort The sort of the relation
|
||||
|
|
@ -1641,7 +1702,8 @@ export interface Sort<Name extends string = 'main'> extends Ast<Name, Z3_sort> {
|
|||
| DatatypeSort['__typename']
|
||||
| FPSort['__typename']
|
||||
| FPRMSort['__typename']
|
||||
| SeqSort['__typename'];
|
||||
| SeqSort['__typename']
|
||||
| ReSort['__typename'];
|
||||
|
||||
kind(): Z3_sort_kind;
|
||||
|
||||
|
|
@ -1768,6 +1830,7 @@ export interface Expr<Name extends string = 'main', S extends Sort<Name> = AnySo
|
|||
| FP['__typename']
|
||||
| FPRM['__typename']
|
||||
| Seq['__typename']
|
||||
| Re['__typename']
|
||||
| SMTArray['__typename']
|
||||
| DatatypeExpr['__typename'];
|
||||
|
||||
|
|
@ -3129,6 +3192,85 @@ export interface Seq<Name extends string = 'main', ElemSort extends Sort<Name> =
|
|||
replaceAll(src: Seq<Name, ElemSort> | string, dst: Seq<Name, ElemSort> | string): Seq<Name, ElemSort>;
|
||||
}
|
||||
|
||||
///////////////////////
|
||||
// Regular Expressions
|
||||
///////////////////////
|
||||
|
||||
/**
|
||||
* Regular expression sort
|
||||
* @category RegularExpression
|
||||
*/
|
||||
export interface ReSort<Name extends string = 'main', SeqSortRef extends SeqSort<Name> = SeqSort<Name>> extends Sort<Name> {
|
||||
/** @hidden */
|
||||
readonly __typename: 'ReSort';
|
||||
|
||||
/**
|
||||
* Get the basis (underlying sequence sort) of this regular expression sort
|
||||
*/
|
||||
basis(): SeqSortRef;
|
||||
|
||||
cast(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
|
||||
cast(other: CoercibleToExpr<Name>): Expr<Name>;
|
||||
}
|
||||
|
||||
/** @category RegularExpression */
|
||||
export interface ReCreation<Name extends string> {
|
||||
/**
|
||||
* Create a regular expression sort over the given sequence sort
|
||||
*/
|
||||
sort<SeqSortRef extends SeqSort<Name>>(seqSort: SeqSortRef): ReSort<Name, SeqSortRef>;
|
||||
|
||||
/**
|
||||
* Convert a sequence to a regular expression that accepts exactly that sequence
|
||||
*/
|
||||
toRe(seq: Seq<Name> | string): Re<Name>;
|
||||
}
|
||||
|
||||
/**
|
||||
* Regular expression expression
|
||||
* @category RegularExpression
|
||||
*/
|
||||
export interface Re<Name extends string = 'main', SeqSortRef extends SeqSort<Name> = SeqSort<Name>>
|
||||
extends Expr<Name, ReSort<Name, SeqSortRef>, Z3_ast> {
|
||||
/** @hidden */
|
||||
readonly __typename: 'Re';
|
||||
|
||||
/** @category Operations */
|
||||
plus(): Re<Name, SeqSortRef>;
|
||||
|
||||
/** @category Operations */
|
||||
star(): Re<Name, SeqSortRef>;
|
||||
|
||||
/** @category Operations */
|
||||
option(): Re<Name, SeqSortRef>;
|
||||
|
||||
/** @category Operations */
|
||||
complement(): Re<Name, SeqSortRef>;
|
||||
|
||||
/** @category Operations */
|
||||
union(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
|
||||
|
||||
/** @category Operations */
|
||||
intersect(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
|
||||
|
||||
/** @category Operations */
|
||||
diff(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
|
||||
|
||||
/** @category Operations */
|
||||
concat(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
|
||||
|
||||
/**
|
||||
* Create a bounded repetition of this regex
|
||||
* @param lo Minimum number of repetitions
|
||||
* @param hi Maximum number of repetitions (0 means unbounded, i.e., at least lo)
|
||||
* @category Operations
|
||||
*/
|
||||
loop(lo: number, hi?: number): Re<Name, SeqSortRef>;
|
||||
|
||||
/** @category Operations */
|
||||
power(n: number): Re<Name, SeqSortRef>;
|
||||
}
|
||||
|
||||
/**
|
||||
* Defines the expression type of the body of a quantifier expression
|
||||
*
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue