From 8fad12fe18bcb00689a39d8437c8b37220a9fec2 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 2 Mar 2026 00:05:23 +0000 Subject: [PATCH 1/3] Initial plan From 28fbe33114378289ea819dc3527bdfb6eed20613 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 2 Mar 2026 00:21:57 +0000 Subject: [PATCH 2/3] Add missing API bindings: Python BvNand/BvNor/BvXnor, Go MkAsArray/MkRecFuncDecl/AddRecDef/Model.Translate, TS Array.fromFunc/Model.translate, OCaml Model.translate Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/api/go/array.go | 6 ++++ src/api/go/solver.go | 6 ++++ src/api/go/z3.go | 27 +++++++++++++++++ src/api/js/src/high-level/high-level.ts | 8 +++++ src/api/js/src/high-level/types.ts | 14 +++++++++ src/api/ml/z3.ml | 2 ++ src/api/ml/z3.mli | 4 +++ src/api/python/z3/z3.py | 39 +++++++++++++++++++++++++ 8 files changed, 106 insertions(+) diff --git a/src/api/go/array.go b/src/api/go/array.go index 25930421f..d3996fb83 100644 --- a/src/api/go/array.go +++ b/src/api/go/array.go @@ -64,3 +64,9 @@ func (c *Context) MkArrayDefault(array *Expr) *Expr { func (c *Context) MkArrayExt(a1, a2 *Expr) *Expr { return newExpr(c, C.Z3_mk_array_ext(c.ptr, a1.ptr, a2.ptr)) } + +// MkAsArray creates an array from a function declaration. +// The resulting array maps each input to the output of the function. +func (c *Context) MkAsArray(f *FuncDecl) *Expr { + return newExpr(c, C.Z3_mk_as_array(c.ptr, f.ptr)) +} diff --git a/src/api/go/solver.go b/src/api/go/solver.go index 7fd8f4586..74053ad70 100644 --- a/src/api/go/solver.go +++ b/src/api/go/solver.go @@ -511,3 +511,9 @@ func (m *Model) SortUniverse(sort *Sort) []*Expr { } return astVectorToExprs(m.ctx, vec) } + +// Translate creates a copy of the model in the target context. +func (m *Model) Translate(target *Context) *Model { + ptr := C.Z3_model_translate(m.ctx.ptr, m.ptr, target.ptr) + return newModel(target, ptr) +} diff --git a/src/api/go/z3.go b/src/api/go/z3.go index 10e3d2a3f..0d1322ea8 100644 --- a/src/api/go/z3.go +++ b/src/api/go/z3.go @@ -471,6 +471,33 @@ func (c *Context) MkFuncDecl(name *Symbol, domain []*Sort, range_ *Sort) *FuncDe return newFuncDecl(c, C.Z3_mk_func_decl(c.ptr, name.ptr, C.uint(len(domain)), domainPtr, range_.ptr)) } +// MkRecFuncDecl creates a recursive function declaration. +// After creating, use AddRecDef to provide the function body. +func (c *Context) MkRecFuncDecl(name *Symbol, domain []*Sort, range_ *Sort) *FuncDecl { + cDomain := make([]C.Z3_sort, len(domain)) + for i, s := range domain { + cDomain[i] = s.ptr + } + var domainPtr *C.Z3_sort + if len(domain) > 0 { + domainPtr = &cDomain[0] + } + return newFuncDecl(c, C.Z3_mk_rec_func_decl(c.ptr, name.ptr, C.uint(len(domain)), domainPtr, range_.ptr)) +} + +// AddRecDef adds the definition (body) for a recursive function created with MkRecFuncDecl. +func (c *Context) AddRecDef(f *FuncDecl, args []*Expr, body *Expr) { + cArgs := make([]C.Z3_ast, len(args)) + for i, a := range args { + cArgs[i] = a.ptr + } + var argsPtr *C.Z3_ast + if len(args) > 0 { + argsPtr = &cArgs[0] + } + C.Z3_add_rec_def(c.ptr, f.ptr, C.uint(len(args)), argsPtr, body.ptr) +} + // MkApp creates a function application. func (c *Context) MkApp(decl *FuncDecl, args ...*Expr) *Expr { cArgs := make([]C.Z3_ast, len(args)) diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 40fa900f5..db2048573 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -1093,6 +1093,9 @@ export function createApi(Z3: Z3Core, em?: any): Z3HighLevel { ): SMTArray { return new ArrayImpl<[DomainSort], RangeSort>(check(Z3.mk_const_array(contextPtr, domain.ptr, value.ptr))); }, + fromFunc(f: FuncDecl): SMTArray { + return new ArrayImpl(check(Z3.mk_as_array(contextPtr, f.ast))); + }, }; const Set = { // reference: https://z3prover.github.io/api/html/namespacez3py.html#a545f894afeb24caa1b88b7f2a324ee7e @@ -2812,6 +2815,11 @@ export function createApi(Z3: Z3Core, em?: any): Z3HighLevel { return this.getUniverse(sort) as AstVector>; } + translate(target: Context): Model { + const ptr = check(Z3.model_translate(contextPtr, this.ptr, target.ptr)); + return new (target.Model as unknown as new (ptr: Z3_model) => Model)(ptr); + } + release() { Z3.model_dec_ref(contextPtr, this.ptr); this._ptr = null; diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index 113dcfd0b..a94b67385 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -1883,6 +1883,14 @@ export interface Model extends Iterable): AstVector>; + /** + * Translate the model to a different context. + * + * @param target - The target context + * @returns A new model in the target context + */ + translate(target: Context): Model; + /** * Manually decrease the reference count of the model * This is automatically done when the model is garbage collected, @@ -2915,6 +2923,12 @@ export interface SMTArrayCreation { domain: DomainSort, value: SortToExprMap, ): SMTArray; + + /** + * Create an array from a function declaration. + * The resulting array maps each input to the output of the function. + */ + fromFunc(f: FuncDecl): SMTArray; } export type NonEmptySortArray = [Sort, ...Array>]; diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 1b60d6678..f1540d1b5 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1692,6 +1692,8 @@ struct let av = Z3native.model_get_sort_universe (gc x) x s in AST.ASTVector.to_expr_list av + let translate (x:model) (to_ctx:context) = Z3native.model_translate (gc x) x to_ctx + let to_string (x:model) = Z3native.model_to_string (gc x) x end diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index cb169b935..689fa088d 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -3057,6 +3057,10 @@ sig @return A list of expressions, where each is an element of the universe of the sort *) val sort_universe : model -> Sort.sort -> Expr.expr list + (** Translate the model to a different context. + @return A new model in the target context *) + val translate : model -> context -> model + (** Conversion of models to strings. @return A string representation of the model. *) val to_string : model -> string diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index df9d7e912..02ed4f166 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -4652,6 +4652,45 @@ def BVRedOr(a): return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx) +def BvNand(a, b): + """Return the bitwise NAND of `a` and `b`. + + >>> x = BitVec('x', 8) + >>> y = BitVec('y', 8) + >>> BvNand(x, y) + bvnand(x, y) + """ + _check_bv_args(a, b) + a, b = _coerce_exprs(a, b) + return BitVecRef(Z3_mk_bvnand(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) + + +def BvNor(a, b): + """Return the bitwise NOR of `a` and `b`. + + >>> x = BitVec('x', 8) + >>> y = BitVec('y', 8) + >>> BvNor(x, y) + bvnor(x, y) + """ + _check_bv_args(a, b) + a, b = _coerce_exprs(a, b) + return BitVecRef(Z3_mk_bvnor(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) + + +def BvXnor(a, b): + """Return the bitwise XNOR of `a` and `b`. + + >>> x = BitVec('x', 8) + >>> y = BitVec('y', 8) + >>> BvXnor(x, y) + bvxnor(x, y) + """ + _check_bv_args(a, b) + a, b = _coerce_exprs(a, b) + return BitVecRef(Z3_mk_bvxnor(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) + + def BVAddNoOverflow(a, b, signed): """A predicate the determines that bit-vector addition does not overflow""" _check_bv_args(a, b) From 1461a53347ce22c38218ad23c86d41d30a6a6bdc Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 2 Mar 2026 16:22:08 +0000 Subject: [PATCH 3/3] Fix TypeScript Array.fromFunc to use f.ptr instead of f.ast for Z3_func_decl type Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/api/js/src/high-level/high-level.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index db2048573..c88929221 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -1094,7 +1094,7 @@ export function createApi(Z3: Z3Core, em?: any): Z3HighLevel { return new ArrayImpl<[DomainSort], RangeSort>(check(Z3.mk_const_array(contextPtr, domain.ptr, value.ptr))); }, fromFunc(f: FuncDecl): SMTArray { - return new ArrayImpl(check(Z3.mk_as_array(contextPtr, f.ast))); + return new ArrayImpl(check(Z3.mk_as_array(contextPtr, f.ptr))); }, }; const Set = {