mirror of
https://github.com/Z3Prover/z3
synced 2026-02-10 02:50:55 +00:00
Document Loop function semantics and fix review comments
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot]
parent
910a9c2aa6
commit
de14c0b3ce
3 changed files with 291 additions and 1 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
|
||||
|
|
@ -1860,6 +1860,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
|
|||
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)));
|
||||
}
|
||||
|
|
@ -4195,6 +4201,11 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
|
|||
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)));
|
||||
}
|
||||
|
|
|
|||
|
|
@ -886,7 +886,13 @@ export interface Context<Name extends string = 'main'> {
|
|||
/** @category RegularExpression */
|
||||
Range<SeqSortRef extends SeqSort<Name>>(lo: Seq<Name, SeqSortRef> | string, hi: Seq<Name, SeqSortRef> | string): Re<Name, SeqSortRef>;
|
||||
|
||||
/** @category RegularExpression */
|
||||
/**
|
||||
* 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 */
|
||||
|
|
@ -3254,6 +3260,11 @@ export interface Re<Name extends string = 'main', SeqSortRef extends SeqSort<Nam
|
|||
concat(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
|
||||
|
||||
/** @category Operations */
|
||||
/**
|
||||
* 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): Re<Name, SeqSortRef>;
|
||||
|
||||
/** @category Operations */
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue