mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-18 16:28:56 +00:00
Code Activity

Add missing array API functions and fix BitVec method typos (#8132)

Browse source 
* Initial plan

* Add missing API functions: array_default, array_ext, and fix BitVec typos

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add documentation for new array API functions

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix WebAssembly build: Add default() method to LambdaImpl

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2026-01-09 11:26:27 -08:00 • committed by GitHub
parent 3881b6845b
commit 495e1f44ba
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 62 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/api/c++/z3++.h
View file

@ -4085,6 +4085,19 @@ namespace z3 {
return expr(f.ctx(), r);
}
inline expr array_default(expr const & a) {
Z3_ast r = Z3_mk_array_default(a.ctx(), a);
a.check_error();
return expr(a.ctx(), r);
}
inline expr array_ext(expr const & a, expr const & b) {
check_context(a, b);
Z3_ast r = Z3_mk_array_ext(a.ctx(), a, b);
a.check_error();
return expr(a.ctx(), r);
}
#define MK_EXPR1(_fn, _arg) \
Z3_ast r = _fn(_arg.ctx(), _arg); \
_arg.check_error(); \

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

@ -1324,6 +1324,19 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
>;
}
/**
* Create array extensionality index given two arrays with the same sort.
* The meaning is given by the axiom:
* (=> (= (select A (array-ext A B)) (select B (array-ext A B))) (= A B))
* Two arrays are equal if and only if they are equal on the index returned by this function.
*/
function Ext<DomainSort extends NonEmptySortArray<Name>, RangeSort extends Sort<Name>>(
a: SMTArray<Name, DomainSort, RangeSort>,
b: SMTArray<Name, DomainSort, RangeSort>,
): SortToExprMap<DomainSort[0], Name> {
return _toExpr(check(Z3.mk_array_ext(contextPtr, a.ast, b.ast))) as SortToExprMap<DomainSort[0], Name>;
}
function SetUnion<ElemSort extends AnySort<Name>>(...args: SMTSet<Name, ElemSort>[]): SMTSet<Name, ElemSort> {
return new SetImpl<ElemSort>(
check(
@ -2644,7 +2657,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
return new BoolImpl(check(Z3.mk_bvsub_no_overflow(contextPtr, this.ast, this.sort.cast(other).ast)));
}
subNoUndeflow(other: CoercibleToBitVec<Bits, Name>, isSigned: boolean): Bool<Name> {
subNoUnderflow(other: CoercibleToBitVec<Bits, Name>, isSigned: boolean): Bool<Name> {
return new BoolImpl(check(Z3.mk_bvsub_no_underflow(contextPtr, this.ast, this.sort.cast(other).ast, isSigned)));
}
@ -2656,7 +2669,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
return new BoolImpl(check(Z3.mk_bvmul_no_overflow(contextPtr, this.ast, this.sort.cast(other).ast, isSigned)));
}
mulNoUndeflow(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
mulNoUnderflow(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
return new BoolImpl(check(Z3.mk_bvmul_no_underflow(contextPtr, this.ast, this.sort.cast(other).ast)));
}
@ -2742,6 +2755,15 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
): SMTArray<Name, DomainSort, RangeSort> {
return Store(this, ...indicesAndValue);
}
/**
* Access the array default value.
* Produces the default range value, for arrays that can be represented as
* finite maps with a default range value.
*/
default(): SortToExprMap<RangeSort, Name> {
return _toExpr(check(Z3.mk_array_default(contextPtr, this.ast))) as SortToExprMap<RangeSort, Name>;
}
}
class SetImpl<ElemSort extends Sort<Name>>
@ -3084,6 +3106,15 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
): SMTArray<Name, DomainSort, RangeSort> {
return Store(this, ...indicesAndValue);
}
/**
* Access the array default value.
* Produces the default range value, for arrays that can be represented as
* finite maps with a default range value.
*/
default(): SortToExprMap<RangeSort, Name> {
return _toExpr(check(Z3.mk_array_default(contextPtr, this.ast))) as SortToExprMap<RangeSort, Name>;
}
}
class AstVectorImpl<Item extends AnyAst<Name>> {
@ -3396,6 +3427,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
Mod,
Select,
Store,
Ext,
Extract,
substitute,

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

@ -623,6 +623,12 @@ export interface Context<Name extends string = 'main'> {
]
): SMTArray<Name, DomainSort, RangeSort>;
/** @category Operations */
Ext<DomainSort extends NonEmptySortArray<Name>, RangeSort extends Sort<Name> = Sort<Name>>(
a: SMTArray<Name, DomainSort, RangeSort>,
b: SMTArray<Name, DomainSort, RangeSort>,
): SortToExprMap<DomainSort[0], Name>;
/** @category Operations */
Extract<Bits extends number>(hi: number, lo: number, val: BitVec<Bits, Name>): BitVec<number, Name>;
@ -1788,7 +1794,7 @@ export interface BitVec<Bits extends number = number, Name extends string = 'mai
subNoOverflow(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
/** @category Boolean */
subNoUndeflow(other: CoercibleToBitVec<Bits, Name>, isSigned: boolean): Bool<Name>;
subNoUnderflow(other: CoercibleToBitVec<Bits, Name>, isSigned: boolean): Bool<Name>;
/** @category Boolean */
sdivNoOverflow(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
@ -1797,7 +1803,7 @@ export interface BitVec<Bits extends number = number, Name extends string = 'mai
mulNoOverflow(other: CoercibleToBitVec<Bits, Name>, isSigned: boolean): Bool<Name>;
/** @category Boolean */
mulNoUndeflow(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
mulNoUnderflow(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
/** @category Boolean */
negNoOverflow(): Bool<Name>;
@ -1928,6 +1934,13 @@ export interface SMTArray<
CoercibleToMap<SortToExprMap<RangeSort, Name>, Name>,
]
): SMTArray<Name, DomainSort, RangeSort>;
/**
* Access the array default value.
* Produces the default range value, for arrays that can be represented as
* finite maps with a default range value.
*/
default(): SortToExprMap<RangeSort, Name>;
}
/**