Merge pull request #8793 from Z3Prover/copilot/fix-missing-api-functions

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

src/api/go/array.go

@@ -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))
+}

src/api/go/fp.go

@@ -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))
+}

src/api/js/src/high-level/high-level.ts

@@ -4251,6 +4251,14 @@ export function createApi(Z3: Z3Core, em?: any): Z3HighLevel {
       isPositive(): Bool<Name> {
         return new BoolImpl(check(Z3.mk_fpa_is_positive(contextPtr, this.ast)));
       }
+
+      toIEEEBV(): BitVec<number, Name> {
+        return new BitVecImpl(check(Z3.mk_fpa_to_ieee_bv(contextPtr, this.ast)));
+      }
+
+      toReal(): Arith<Name> {
+        return new ArithImpl(check(Z3.mk_fpa_to_real(contextPtr, this.ast)));
+      }
     }
 
     class FPNumImpl extends FPImpl implements FPNum<Name> {

src/api/js/src/high-level/types.ts

@@ -3398,6 +3398,12 @@ export interface FP<Name extends string = 'main'> extends Expr<Name, FPSort<Name
 
   /** @category Predicates */
   isPositive(): Bool<Name>;
+
+  /** @category Conversion */
+  toIEEEBV(): BitVec<number, Name>;
+
+  /** @category Conversion */
+  toReal(): Arith<Name>;
 }
 
 /**

src/api/ml/z3.ml

@@ -770,6 +770,12 @@ struct
   let mk_store = Z3native.mk_store
   let mk_const_array = Z3native.mk_const_array
 
+  let mk_select_n ctx a idxs =
+    Z3native.mk_select_n ctx a (List.length idxs) idxs
+
+  let mk_store_n ctx a idxs v =
+    Z3native.mk_store_n ctx a (List.length idxs) idxs v
+
   let mk_map ctx f args =
     Z3native.mk_map ctx f (List.length args) args
 

src/api/ml/z3.mli

@@ -869,6 +869,19 @@ sig
       {!mk_select} *)
   val mk_const_array : context -> Sort.sort -> Expr.expr -> Expr.expr
 
+  (** Multi-index array read.
+
+      The node [a] must have a multi-dimensional array sort, and [idxs] is the list of indices.
+      {!mk_select} *)
+  val mk_select_n : context -> Expr.expr -> Expr.expr list -> Expr.expr
+
+  (** Multi-index array update.
+
+      The node [a] must have a multi-dimensional array sort, [idxs] is the list of indices,
+      and [v] is the value to store.
+      {!mk_store} *)
+  val mk_store_n : context -> Expr.expr -> Expr.expr list -> Expr.expr -> Expr.expr
+
   (** Maps f on the argument arrays.
 
       Each element of [args] must be of an array sort [[domain_i -> range_i]].