From 495e1f44ba5ce0266dc60b9e7031d2ccfc2425f9 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Fri, 9 Jan 2026 11:26:27 -0800 Subject: [PATCH] Add missing array API functions and fix BitVec method typos (#8132) * 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> --- src/api/c++/z3++.h | 13 +++++++++ src/api/js/src/high-level/high-level.ts | 36 +++++++++++++++++++++++-- src/api/js/src/high-level/types.ts | 17 ++++++++++-- 3 files changed, 62 insertions(+), 4 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index dcc040e56..1a3b7ce8d 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -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(); \ diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 7ac083d29..517bbe50e 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -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, RangeSort extends Sort>( + a: SMTArray, + b: SMTArray, + ): SortToExprMap { + return _toExpr(check(Z3.mk_array_ext(contextPtr, a.ast, b.ast))) as SortToExprMap; + } + function SetUnion>(...args: SMTSet[]): SMTSet { return new SetImpl( 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, isSigned: boolean): Bool { + subNoUnderflow(other: CoercibleToBitVec, isSigned: boolean): Bool { 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): Bool { + mulNoUnderflow(other: CoercibleToBitVec): Bool { 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 { 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 { + return _toExpr(check(Z3.mk_array_default(contextPtr, this.ast))) as SortToExprMap; + } } class SetImpl> @@ -3084,6 +3106,15 @@ export function createApi(Z3: Z3Core): Z3HighLevel { ): SMTArray { 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 { + return _toExpr(check(Z3.mk_array_default(contextPtr, this.ast))) as SortToExprMap; + } } class AstVectorImpl> { @@ -3396,6 +3427,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { Mod, Select, Store, + Ext, Extract, substitute, diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index 3e2094105..c52edf001 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -623,6 +623,12 @@ export interface Context { ] ): SMTArray; + /** @category Operations */ + Ext, RangeSort extends Sort = Sort>( + a: SMTArray, + b: SMTArray, + ): SortToExprMap; + /** @category Operations */ Extract(hi: number, lo: number, val: BitVec): BitVec; @@ -1788,7 +1794,7 @@ export interface BitVec, isSigned: boolean): Bool; /** @category Boolean */ - mulNoUndeflow(other: CoercibleToBitVec): Bool; + mulNoUnderflow(other: CoercibleToBitVec): Bool; /** @category Boolean */ negNoOverflow(): Bool; @@ -1928,6 +1934,13 @@ export interface SMTArray< CoercibleToMap, Name>, ] ): SMTArray; + + /** + * 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; } /**