mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-07 22:04:53 +00:00
Code Activity

Add missing API functions to Go, OCaml, and TypeScript bindings

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-27 02:55:37 +00:00
parent 3f6acc45ed
commit 282db840de
6 changed files with 100 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

37
src/api/go/array.go
View file

@ -27,3 +27,40 @@ func (c *Context) MkStore(array, index, value *Expr) *Expr {
func (c *Context) MkConstArray(sort *Sort, value *Expr) *Expr {
return newExpr(c, C.Z3_mk_const_array(c.ptr, sort.ptr, value.ptr))
}
// MkSelectN creates a multi-index array read (select) operation.
func (c *Context) MkSelectN(array *Expr, indices []*Expr) *Expr {
idxs := make([]C.Z3_ast, len(indices))
for i, idx := range indices {
idxs[i] = idx.ptr
}
var idxsPtr *C.Z3_ast
if len(idxs) > 0 {
idxsPtr = &idxs[0]
}
return newExpr(c, C.Z3_mk_select_n(c.ptr, array.ptr, C.uint(len(idxs)), idxsPtr))
}
// MkStoreN creates a multi-index array write (store) operation.
func (c *Context) MkStoreN(array *Expr, indices []*Expr, value *Expr) *Expr {
idxs := make([]C.Z3_ast, len(indices))
for i, idx := range indices {
idxs[i] = idx.ptr
}
var idxsPtr *C.Z3_ast
if len(idxs) > 0 {
idxsPtr = &idxs[0]
}
return newExpr(c, C.Z3_mk_store_n(c.ptr, array.ptr, C.uint(len(idxs)), idxsPtr, value.ptr))
}
// MkArrayDefault returns the default value of an array.
func (c *Context) MkArrayDefault(array *Expr) *Expr {
return newExpr(c, C.Z3_mk_array_default(c.ptr, array.ptr))
}
// MkArrayExt returns the extensionality witness for two arrays.
// Two arrays are equal if and only if they are equal on the index returned by MkArrayExt.
func (c *Context) MkArrayExt(a1, a2 *Expr) *Expr {
return newExpr(c, C.Z3_mk_array_ext(c.ptr, a1.ptr, a2.ptr))
}

30
src/api/go/fp.go
View file

@ -137,3 +137,33 @@ func (c *Context) MkFPIsInf(expr *Expr) *Expr {
func (c *Context) MkFPIsZero(expr *Expr) *Expr {
return newExpr(c, C.Z3_mk_fpa_is_zero(c.ptr, expr.ptr))
}
// MkFPIsNormal creates a predicate checking if a floating-point number is normal.
func (c *Context) MkFPIsNormal(expr *Expr) *Expr {
return newExpr(c, C.Z3_mk_fpa_is_normal(c.ptr, expr.ptr))
}
// MkFPIsSubnormal creates a predicate checking if a floating-point number is subnormal.
func (c *Context) MkFPIsSubnormal(expr *Expr) *Expr {
return newExpr(c, C.Z3_mk_fpa_is_subnormal(c.ptr, expr.ptr))
}
// MkFPIsNegative creates a predicate checking if a floating-point number is negative.
func (c *Context) MkFPIsNegative(expr *Expr) *Expr {
return newExpr(c, C.Z3_mk_fpa_is_negative(c.ptr, expr.ptr))
}
// MkFPIsPositive creates a predicate checking if a floating-point number is positive.
func (c *Context) MkFPIsPositive(expr *Expr) *Expr {
return newExpr(c, C.Z3_mk_fpa_is_positive(c.ptr, expr.ptr))
}
// MkFPToIEEEBV converts a floating-point number to its IEEE 754 bit-vector representation.
func (c *Context) MkFPToIEEEBV(expr *Expr) *Expr {
return newExpr(c, C.Z3_mk_fpa_to_ieee_bv(c.ptr, expr.ptr))
}
// MkFPToReal converts a floating-point number to a real number.
func (c *Context) MkFPToReal(expr *Expr) *Expr {
return newExpr(c, C.Z3_mk_fpa_to_real(c.ptr, expr.ptr))
}