mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 16:27:37 +00:00
Code Activity

Add FiniteSet support to Go, OCaml, and JavaScript APIs

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-20 04:23:26 +00:00
parent 8f6afe3d64
commit 5d93f098fc
5 changed files with 320 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

109
src/api/js/src/high-level/high-level.ts
View file

@ -123,6 +123,9 @@ import {
DatatypeSort,
DatatypeExpr,
DatatypeCreation,
FiniteSet,
FiniteSetSort,
FiniteSetCreation,
} from './types';
import { allSatisfy, assert, assertExhaustive } from './utils';
@ -305,6 +308,9 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
case Z3_sort_kind.Z3_ARRAY_SORT:
return new ArraySortImpl(ast);
default:
if (Z3.is_finite_set_sort(contextPtr, ast)) {
return new FiniteSetSortImpl(ast);
}
return new SortImpl(ast);
}
}
@ -350,6 +356,9 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
case Z3_sort_kind.Z3_ARRAY_SORT:
return new ArrayImpl(ast);
default:
if (Z3.is_finite_set_sort(contextPtr, Z3.get_sort(contextPtr, ast))) {
return new FiniteSetImpl(ast);
}
return new ExprImpl(ast);
}
}
@ -638,6 +647,18 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
return isSeq(obj) && obj.isString();
}
function isFiniteSetSort(obj: unknown): obj is FiniteSetSort<Name> {
const r = obj instanceof FiniteSetSortImpl;
r && _assertContext(obj);
return r;
}
function isFiniteSet(obj: unknown): obj is FiniteSet<Name> {
const r = obj instanceof FiniteSetImpl;
r && _assertContext(obj);
return r;
}
function isProbe(obj: unknown): obj is Probe<Name> {
const r = obj instanceof ProbeImpl;
r && _assertContext(obj);
@ -1104,6 +1125,32 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
},
};
const FiniteSet = {
sort<ElemSort extends Sort<Name>>(elemSort: ElemSort): FiniteSetSort<Name, ElemSort> {
return new FiniteSetSortImpl<ElemSort>(check(Z3.mk_finite_set_sort(contextPtr, elemSort.ptr)));
},
const<ElemSort extends Sort<Name>>(name: string, elemSort: ElemSort): FiniteSet<Name, ElemSort> {
return new FiniteSetImpl<ElemSort>(
check(Z3.mk_const(contextPtr, _toSymbol(name), FiniteSet.sort(elemSort).ptr)),
);
},
consts<ElemSort extends Sort<Name>>(names: string | string[], elemSort: ElemSort): FiniteSet<Name, ElemSort>[] {
if (typeof names === 'string') {
names = names.split(' ');
}
return names.map(name => FiniteSet.const(name, elemSort));
},
empty<ElemSort extends Sort<Name>>(sort: ElemSort): FiniteSet<Name, ElemSort> {
return new FiniteSetImpl<ElemSort>(check(Z3.mk_finite_set_empty(contextPtr, FiniteSet.sort(sort).ptr)));
},
singleton<ElemSort extends Sort<Name>>(elem: Expr<Name>): FiniteSet<Name, ElemSort> {
return new FiniteSetImpl<ElemSort>(check(Z3.mk_finite_set_singleton(contextPtr, elem.ast)));
},
range(low: Expr<Name>, high: Expr<Name>): FiniteSet<Name, Sort<Name>> {
return new FiniteSetImpl(check(Z3.mk_finite_set_range(contextPtr, low.ast, high.ast)));
},
};
const Datatype = Object.assign(
(name: string): DatatypeImpl => {
return new DatatypeImpl(ctx, name);
@ -4310,6 +4357,65 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
}
}
////////////////////////////
// Finite Sets
////////////////////////////
class FiniteSetSortImpl<ElemSort extends Sort<Name> = Sort<Name>>
extends SortImpl
implements FiniteSetSort<Name, ElemSort>
{
declare readonly __typename: 'FiniteSetSort';
elemSort(): ElemSort {
return _toSort(check(Z3.get_finite_set_sort_basis(contextPtr, this.ptr))) as ElemSort;
}
cast(other: Expr<Name>): Expr<Name> {
_assertContext(other);
return other;
}
}
class FiniteSetImpl<ElemSort extends Sort<Name> = Sort<Name>>
extends ExprImpl<Z3_ast, FiniteSetSortImpl<ElemSort>>
implements FiniteSet<Name, ElemSort>
{
declare readonly __typename: 'FiniteSet';
union(other: FiniteSet<Name, ElemSort>): FiniteSet<Name, ElemSort> {
return new FiniteSetImpl<ElemSort>(check(Z3.mk_finite_set_union(contextPtr, this.ast, other.ast)));
}
intersect(other: FiniteSet<Name, ElemSort>): FiniteSet<Name, ElemSort> {
return new FiniteSetImpl<ElemSort>(check(Z3.mk_finite_set_intersect(contextPtr, this.ast, other.ast)));
}
diff(other: FiniteSet<Name, ElemSort>): FiniteSet<Name, ElemSort> {
return new FiniteSetImpl<ElemSort>(check(Z3.mk_finite_set_difference(contextPtr, this.ast, other.ast)));
}
contains(elem: Expr<Name>): Bool<Name> {
return new BoolImpl(check(Z3.mk_finite_set_member(contextPtr, elem.ast, this.ast)));
}
size(): Expr<Name> {
return new ExprImpl(check(Z3.mk_finite_set_size(contextPtr, this.ast)));
}
subsetOf(other: FiniteSet<Name, ElemSort>): Bool<Name> {
return new BoolImpl(check(Z3.mk_finite_set_subset(contextPtr, this.ast, other.ast)));
}
map(f: Expr<Name>): FiniteSet<Name, Sort<Name>> {
return new FiniteSetImpl(check(Z3.mk_finite_set_map(contextPtr, f.ast, this.ast)));
}
filter(f: Expr<Name>): FiniteSet<Name, ElemSort> {
return new FiniteSetImpl<ElemSort>(check(Z3.mk_finite_set_filter(contextPtr, f.ast, this.ast)));
}
}
////////////////////////////
// Datatypes
////////////////////////////
@ -4902,6 +5008,8 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
isSeq,
isStringSort,
isString,
isFiniteSetSort,
isFiniteSet,
isArraySort,
isArray,
isConstArray,
@ -4932,6 +5040,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
Re,
Array,
Set,
FiniteSet,
Datatype,
////////////////

71
src/api/js/src/high-level/types.ts
View file

@ -52,7 +52,8 @@ export type AnyExpr<Name extends string = 'main'> =
| FPNum<Name>
| FPRM<Name>
| Seq<Name>
| Re<Name>;
| Re<Name>
| FiniteSet<Name>;
/** @hidden */
export type AnyAst<Name extends string = 'main'> = AnyExpr<Name> | AnySort<Name> | FuncDecl<Name>;
@ -330,6 +331,12 @@ export interface Context<Name extends string = 'main'> {
/** @category Functions */
isString(obj: unknown): obj is Seq<Name>;
/** @category Functions */
isFiniteSetSort(obj: unknown): obj is FiniteSetSort<Name>;
/** @category Functions */
isFiniteSet(obj: unknown): obj is FiniteSet<Name>;
/** @category Functions */
isProbe(obj: unknown): obj is Probe<Name>;
@ -468,6 +475,8 @@ export interface Context<Name extends string = 'main'> {
/** @category Expressions */
readonly Set: SMTSetCreation<Name>;
/** @category Expressions */
readonly FiniteSet: FiniteSetCreation<Name>;
/** @category Expressions */
readonly Datatype: DatatypeCreation<Name>;
////////////////
@ -1706,7 +1715,8 @@ export interface Sort<Name extends string = 'main'> extends Ast<Name, Z3_sort> {
| FPSort['__typename']
| FPRMSort['__typename']
| SeqSort['__typename']
| ReSort['__typename'];
| ReSort['__typename']
| FiniteSetSort['__typename'];
kind(): Z3_sort_kind;
@ -1835,7 +1845,8 @@ export interface Expr<Name extends string = 'main', S extends Sort<Name> = AnySo
| Seq['__typename']
| Re['__typename']
| SMTArray['__typename']
| DatatypeExpr['__typename'];
| DatatypeExpr['__typename']
| FiniteSet['__typename'];
get sort(): S;
@ -2739,6 +2750,60 @@ export interface SMTSet<Name extends string = 'main', ElemSort extends AnySort<N
contains(elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>): Bool<Name>;
subsetOf(b: SMTSet<Name, ElemSort>): Bool<Name>;
}
//////////////////////////////////////////
//
// Finite Sets
//
//////////////////////////////////////////
/**
* Represents a finite set sort
*
* @typeParam ElemSort The sort of elements in the finite set
* @category Finite Sets
*/
export interface FiniteSetSort<Name extends string = 'main', ElemSort extends Sort<Name> = Sort<Name>>
extends Sort<Name> {
readonly __typename: 'FiniteSetSort';
/** Returns the element sort of this finite set sort */
elemSort(): ElemSort;
}
/** @category Finite Sets */
export interface FiniteSetCreation<Name extends string> {
sort<ElemSort extends Sort<Name>>(elemSort: ElemSort): FiniteSetSort<Name, ElemSort>;
const<ElemSort extends Sort<Name>>(name: string, elemSort: ElemSort): FiniteSet<Name, ElemSort>;
consts<ElemSort extends Sort<Name>>(names: string | string[], elemSort: ElemSort): FiniteSet<Name, ElemSort>[];
empty<ElemSort extends Sort<Name>>(sort: ElemSort): FiniteSet<Name, ElemSort>;
singleton<ElemSort extends Sort<Name>>(elem: Expr<Name>): FiniteSet<Name, ElemSort>;
range(low: Expr<Name>, high: Expr<Name>): FiniteSet<Name, Sort<Name>>;
}
/**
* Represents a finite set expression
*
* @typeParam ElemSort The sort of elements in the finite set
* @category Finite Sets
*/
export interface FiniteSet<Name extends string = 'main', ElemSort extends Sort<Name> = Sort<Name>>
extends Expr<Name, FiniteSetSort<Name, ElemSort>, Z3_ast> {
readonly __typename: 'FiniteSet';
union(other: FiniteSet<Name, ElemSort>): FiniteSet<Name, ElemSort>;
intersect(other: FiniteSet<Name, ElemSort>): FiniteSet<Name, ElemSort>;
diff(other: FiniteSet<Name, ElemSort>): FiniteSet<Name, ElemSort>;
contains(elem: Expr<Name>): Bool<Name>;
size(): Expr<Name>;
subsetOf(other: FiniteSet<Name, ElemSort>): Bool<Name>;
map(f: Expr<Name>): FiniteSet<Name, Sort<Name>>;
filter(f: Expr<Name>): FiniteSet<Name, ElemSort>;
}
//////////////////////////////////////////
//
// Datatypes