mirror of
https://github.com/Z3Prover/z3
synced 2026-02-10 02:50:55 +00:00
Add regex support to TypeScript API - types and implementations
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot]
parent
c8b855fa65
commit
ed111f023a
2 changed files with 332 additions and 3 deletions
|
|
@ -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,91 @@ 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)));
|
||||
}
|
||||
|
||||
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 +4139,71 @@ 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])));
|
||||
}
|
||||
|
||||
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 +4911,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
|
|||
FloatRM,
|
||||
String,
|
||||
Seq,
|
||||
Re,
|
||||
Array,
|
||||
Set,
|
||||
Datatype,
|
||||
|
|
@ -4823,6 +5004,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,55 @@ 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>;
|
||||
|
||||
/** @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 +1696,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 +1824,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 +3186,80 @@ 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>;
|
||||
|
||||
/** @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