Fix high and medium priority API coherence issues (Go, Java, C++, TypeScript) (#8983)

* Initial plan

* Add missing API functions to Go, Java, C++, and TypeScript bindings

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

@@ -1533,6 +1533,8 @@ namespace z3 {
         
         expr rotate_left(unsigned i) const { Z3_ast r = Z3_mk_rotate_left(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
         expr rotate_right(unsigned i) const { Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
+        expr ext_rotate_left(expr const& n) const { Z3_ast r = Z3_mk_ext_rotate_left(ctx(), *this, n); ctx().check_error(); return expr(ctx(), r); }
+        expr ext_rotate_right(expr const& n) const { Z3_ast r = Z3_mk_ext_rotate_right(ctx(), *this, n); ctx().check_error(); return expr(ctx(), r); }
         expr repeat(unsigned i) const { Z3_ast r = Z3_mk_repeat(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
 
         friend expr bvredor(expr const & a);

src/api/go/arith.go

@@ -124,3 +124,33 @@ func (c *Context) MkGt(lhs, rhs *Expr) *Expr {
 func (c *Context) MkGe(lhs, rhs *Expr) *Expr {
 	return newExpr(c, C.Z3_mk_ge(c.ptr, lhs.ptr, rhs.ptr))
 }
+
+// MkPower creates an exponentiation expression (base^exp).
+func (c *Context) MkPower(base, exp *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_power(c.ptr, base.ptr, exp.ptr))
+}
+
+// MkAbs creates an absolute value expression.
+func (c *Context) MkAbs(arg *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_abs(c.ptr, arg.ptr))
+}
+
+// MkInt2Real coerces an integer expression to a real.
+func (c *Context) MkInt2Real(arg *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_int2real(c.ptr, arg.ptr))
+}
+
+// MkReal2Int converts a real expression to an integer (floor).
+func (c *Context) MkReal2Int(arg *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_real2int(c.ptr, arg.ptr))
+}
+
+// MkIsInt creates a predicate that checks whether a real expression is an integer.
+func (c *Context) MkIsInt(arg *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_is_int(c.ptr, arg.ptr))
+}
+
+// MkDivides creates an integer divisibility predicate (t1 divides t2).
+func (c *Context) MkDivides(t1, t2 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_divides(c.ptr, t1.ptr, t2.ptr))
+}

src/api/go/array.go

@@ -70,3 +70,17 @@ func (c *Context) MkArrayExt(a1, a2 *Expr) *Expr {
 func (c *Context) MkAsArray(f *FuncDecl) *Expr {
 	return newExpr(c, C.Z3_mk_as_array(c.ptr, f.ptr))
 }
+
+// MkMap applies a function to the elements of one or more arrays, returning a new array.
+// The function f is applied element-wise to the given arrays.
+func (c *Context) MkMap(f *FuncDecl, arrays ...*Expr) *Expr {
+	cArrays := make([]C.Z3_ast, len(arrays))
+	for i, a := range arrays {
+		cArrays[i] = a.ptr
+	}
+	var cArraysPtr *C.Z3_ast
+	if len(cArrays) > 0 {
+		cArraysPtr = &cArrays[0]
+	}
+	return newExpr(c, C.Z3_mk_map(c.ptr, f.ptr, C.uint(len(arrays)), cArraysPtr))
+}

src/api/go/bitvec.go

@@ -221,3 +221,25 @@ func (c *Context) MkBVMulNoOverflow(t1, t2 *Expr, isSigned bool) *Expr {
 func (c *Context) MkBVMulNoUnderflow(t1, t2 *Expr) *Expr {
 	return newExpr(c, C.Z3_mk_bvmul_no_underflow(c.ptr, t1.ptr, t2.ptr))
 }
+
+// MkBVRedAnd computes the bitwise AND reduction of a bit-vector, returning a 1-bit vector.
+func (c *Context) MkBVRedAnd(t *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvredand(c.ptr, t.ptr))
+}
+
+// MkBVRedOr computes the bitwise OR reduction of a bit-vector, returning a 1-bit vector.
+func (c *Context) MkBVRedOr(t *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvredor(c.ptr, t.ptr))
+}
+
+// MkBVExtRotateLeft rotates the bits of t1 to the left by the number of bits given by t2.
+// Both t1 and t2 must be bit-vectors of the same width.
+func (c *Context) MkBVExtRotateLeft(t1, t2 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_ext_rotate_left(c.ptr, t1.ptr, t2.ptr))
+}
+
+// MkBVExtRotateRight rotates the bits of t1 to the right by the number of bits given by t2.
+// Both t1 and t2 must be bit-vectors of the same width.
+func (c *Context) MkBVExtRotateRight(t1, t2 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_ext_rotate_right(c.ptr, t1.ptr, t2.ptr))
+}

src/api/go/fp.go

@@ -167,3 +167,118 @@ func (c *Context) MkFPToIEEEBV(expr *Expr) *Expr {
 func (c *Context) MkFPToReal(expr *Expr) *Expr {
 	return newExpr(c, C.Z3_mk_fpa_to_real(c.ptr, expr.ptr))
 }
+
+// MkFPRNE creates the round-nearest-ties-to-even rounding mode.
+func (c *Context) MkFPRNE() *Expr {
+	return newExpr(c, C.Z3_mk_fpa_rne(c.ptr))
+}
+
+// MkFPRNA creates the round-nearest-ties-to-away rounding mode.
+func (c *Context) MkFPRNA() *Expr {
+	return newExpr(c, C.Z3_mk_fpa_rna(c.ptr))
+}
+
+// MkFPRTP creates the round-toward-positive rounding mode.
+func (c *Context) MkFPRTP() *Expr {
+	return newExpr(c, C.Z3_mk_fpa_rtp(c.ptr))
+}
+
+// MkFPRTN creates the round-toward-negative rounding mode.
+func (c *Context) MkFPRTN() *Expr {
+	return newExpr(c, C.Z3_mk_fpa_rtn(c.ptr))
+}
+
+// MkFPRTZ creates the round-toward-zero rounding mode.
+func (c *Context) MkFPRTZ() *Expr {
+	return newExpr(c, C.Z3_mk_fpa_rtz(c.ptr))
+}
+
+// MkFPFP creates a floating-point number from a sign bit (1-bit BV), exponent BV, and significand BV.
+func (c *Context) MkFPFP(sgn, exp, sig *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_fp(c.ptr, sgn.ptr, exp.ptr, sig.ptr))
+}
+
+// MkFPNumeralFloat creates a floating-point numeral from a float32 value.
+func (c *Context) MkFPNumeralFloat(v float32, sort *Sort) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_numeral_float(c.ptr, C.float(v), sort.ptr))
+}
+
+// MkFPNumeralDouble creates a floating-point numeral from a float64 value.
+func (c *Context) MkFPNumeralDouble(v float64, sort *Sort) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_numeral_double(c.ptr, C.double(v), sort.ptr))
+}
+
+// MkFPNumeralInt creates a floating-point numeral from a signed integer.
+func (c *Context) MkFPNumeralInt(v int, sort *Sort) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_numeral_int(c.ptr, C.int(v), sort.ptr))
+}
+
+// MkFPNumeralIntUint creates a floating-point numeral from a sign, signed exponent, and unsigned significand.
+func (c *Context) MkFPNumeralIntUint(sgn bool, exp int, sig uint, sort *Sort) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_numeral_int_uint(c.ptr, C.bool(sgn), C.int(exp), C.uint(sig), sort.ptr))
+}
+
+// MkFPNumeralInt64Uint64 creates a floating-point numeral from a sign, int64 exponent, and uint64 significand.
+func (c *Context) MkFPNumeralInt64Uint64(sgn bool, exp int64, sig uint64, sort *Sort) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_numeral_int64_uint64(c.ptr, C.bool(sgn), C.int64_t(exp), C.uint64_t(sig), sort.ptr))
+}
+
+// MkFPFMA creates a floating-point fused multiply-add: rm * (t1 * t2) + t3.
+func (c *Context) MkFPFMA(rm, t1, t2, t3 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_fma(c.ptr, rm.ptr, t1.ptr, t2.ptr, t3.ptr))
+}
+
+// MkFPRem creates a floating-point remainder.
+func (c *Context) MkFPRem(t1, t2 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_rem(c.ptr, t1.ptr, t2.ptr))
+}
+
+// MkFPMin creates the minimum of two floating-point values.
+func (c *Context) MkFPMin(t1, t2 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_min(c.ptr, t1.ptr, t2.ptr))
+}
+
+// MkFPMax creates the maximum of two floating-point values.
+func (c *Context) MkFPMax(t1, t2 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_max(c.ptr, t1.ptr, t2.ptr))
+}
+
+// MkFPRoundToIntegral creates a floating-point round-to-integral operation.
+func (c *Context) MkFPRoundToIntegral(rm, t *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_round_to_integral(c.ptr, rm.ptr, t.ptr))
+}
+
+// MkFPToFPBV converts a bit-vector to a floating-point number (reinterpretation of IEEE 754 bits).
+func (c *Context) MkFPToFPBV(bv *Expr, sort *Sort) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_to_fp_bv(c.ptr, bv.ptr, sort.ptr))
+}
+
+// MkFPToFPFloat converts a floating-point number to another floating-point sort with rounding.
+func (c *Context) MkFPToFPFloat(rm, t *Expr, sort *Sort) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_to_fp_float(c.ptr, rm.ptr, t.ptr, sort.ptr))
+}
+
+// MkFPToFPReal converts a real number to a floating-point number with rounding.
+func (c *Context) MkFPToFPReal(rm, t *Expr, sort *Sort) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_to_fp_real(c.ptr, rm.ptr, t.ptr, sort.ptr))
+}
+
+// MkFPToFPSigned converts a signed bit-vector to a floating-point number with rounding.
+func (c *Context) MkFPToFPSigned(rm, t *Expr, sort *Sort) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_to_fp_signed(c.ptr, rm.ptr, t.ptr, sort.ptr))
+}
+
+// MkFPToFPUnsigned converts an unsigned bit-vector to a floating-point number with rounding.
+func (c *Context) MkFPToFPUnsigned(rm, t *Expr, sort *Sort) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_to_fp_unsigned(c.ptr, rm.ptr, t.ptr, sort.ptr))
+}
+
+// MkFPToSBV converts a floating-point number to a signed bit-vector with rounding.
+func (c *Context) MkFPToSBV(rm, t *Expr, sz uint) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_to_sbv(c.ptr, rm.ptr, t.ptr, C.uint(sz)))
+}
+
+// MkFPToUBV converts a floating-point number to an unsigned bit-vector with rounding.
+func (c *Context) MkFPToUBV(rm, t *Expr, sz uint) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_to_ubv(c.ptr, rm.ptr, t.ptr, C.uint(sz)))
+}

src/api/go/seq.go

@@ -230,3 +230,58 @@ func (c *Context) MkSeqReplaceRe(seq, re, replacement *Expr) *Expr {
 func (c *Context) MkSeqReplaceReAll(seq, re, replacement *Expr) *Expr {
 	return newExpr(c, C.Z3_mk_seq_replace_re_all(c.ptr, seq.ptr, re.ptr, replacement.ptr))
 }
+
+// MkSeqReplaceAll replaces all occurrences of src with dst in seq.
+func (c *Context) MkSeqReplaceAll(seq, src, dst *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_seq_replace_all(c.ptr, seq.ptr, src.ptr, dst.ptr))
+}
+
+// MkSeqNth retrieves the n-th element of a sequence as a single-element expression.
+func (c *Context) MkSeqNth(seq, index *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_seq_nth(c.ptr, seq.ptr, index.ptr))
+}
+
+// MkSeqLastIndex returns the last index of substr in seq.
+func (c *Context) MkSeqLastIndex(seq, substr *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_seq_last_index(c.ptr, seq.ptr, substr.ptr))
+}
+
+// MkSeqMap applies a function to each element of a sequence, returning a new sequence.
+func (c *Context) MkSeqMap(f, seq *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_seq_map(c.ptr, f.ptr, seq.ptr))
+}
+
+// MkSeqMapi applies an indexed function to each element of a sequence, returning a new sequence.
+func (c *Context) MkSeqMapi(f, i, seq *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_seq_mapi(c.ptr, f.ptr, i.ptr, seq.ptr))
+}
+
+// MkSeqFoldl applies a fold-left operation to a sequence.
+func (c *Context) MkSeqFoldl(f, a, seq *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_seq_foldl(c.ptr, f.ptr, a.ptr, seq.ptr))
+}
+
+// MkSeqFoldli applies an indexed fold-left operation to a sequence.
+func (c *Context) MkSeqFoldli(f, i, a, seq *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_seq_foldli(c.ptr, f.ptr, i.ptr, a.ptr, seq.ptr))
+}
+
+// MkStrLt creates a string less-than comparison.
+func (c *Context) MkStrLt(s1, s2 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_str_lt(c.ptr, s1.ptr, s2.ptr))
+}
+
+// MkStrLe creates a string less-than-or-equal comparison.
+func (c *Context) MkStrLe(s1, s2 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_str_le(c.ptr, s1.ptr, s2.ptr))
+}
+
+// MkStringToCode converts a single-character string to its Unicode code point.
+func (c *Context) MkStringToCode(s *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_string_to_code(c.ptr, s.ptr))
+}
+
+// MkStringFromCode converts a Unicode code point to a single-character string.
+func (c *Context) MkStringFromCode(code *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_string_from_code(c.ptr, code.ptr))
+}

src/api/java/Context.java

@@ -1152,6 +1152,27 @@ public class Context implements AutoCloseable {
         return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject()));
     }
 
+    /**
+     * Creates the absolute value of an arithmetic expression.
+     * Remarks: The argument must have integer or real sort.
+     **/
+    public <R extends ArithSort> ArithExpr<R> mkAbs(Expr<? extends R> arg)
+    {
+        checkContextMatch(arg);
+        return (ArithExpr<R>) Expr.create(this, Native.mkAbs(nCtx(), arg.getNativeObject()));
+    }
+
+    /**
+     * Creates an integer divisibility predicate (t1 divides t2).
+     * Remarks: Both arguments must have integer sort.
+     **/
+    public BoolExpr mkDivides(Expr<IntSort> t1, Expr<IntSort> t2)
+    {
+        checkContextMatch(t1);
+        checkContextMatch(t2);
+        return new BoolExpr(this, Native.mkDivides(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
+    }
+
     /**
      * Bitwise negation.
      * Remarks: The argument must have a bit-vector

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

@@ -1024,6 +1024,16 @@ export function createApi(Z3: Z3Core, em?: any): Z3HighLevel {
       val(value: string): Seq<Name> {
         return new SeqImpl(check(Z3.mk_string(contextPtr, value)));
       },
+
+      fromCode(code: Arith<Name> | number | bigint): Seq<Name> {
+        const codeExpr = isArith(code) ? code : Int.val(code);
+        return new SeqImpl(check(Z3.mk_string_from_code(contextPtr, codeExpr.ast)));
+      },
+
+      fromInt(n: Arith<Name> | number | bigint): Seq<Name> {
+        const nExpr = isArith(n) ? n : Int.val(n);
+        return new SeqImpl(check(Z3.mk_int_to_str(contextPtr, nExpr.ast)));
+      },
     };
 
     const Seq = {
@@ -4384,6 +4394,34 @@ export function createApi(Z3: Z3Core, em?: any): Z3HighLevel {
         const dstSeq = isSeq(dst) ? dst : String.val(dst);
         return new SeqImpl<ElemSort>(check(Z3.mk_seq_replace_all(contextPtr, this.ast, srcSeq.ast, dstSeq.ast)));
       }
+
+      replaceRe(re: Re<Name>, dst: Seq<Name, ElemSort> | string): Seq<Name, ElemSort> {
+        const dstSeq = isSeq(dst) ? dst : String.val(dst);
+        return new SeqImpl<ElemSort>(check(Z3.mk_seq_replace_re(contextPtr, this.ast, re.ast, dstSeq.ast)));
+      }
+
+      replaceReAll(re: Re<Name>, dst: Seq<Name, ElemSort> | string): Seq<Name, ElemSort> {
+        const dstSeq = isSeq(dst) ? dst : String.val(dst);
+        return new SeqImpl<ElemSort>(check(Z3.mk_seq_replace_re_all(contextPtr, this.ast, re.ast, dstSeq.ast)));
+      }
+
+      toInt(): Arith<Name> {
+        return new ArithImpl(check(Z3.mk_str_to_int(contextPtr, this.ast)));
+      }
+
+      toCode(): Arith<Name> {
+        return new ArithImpl(check(Z3.mk_string_to_code(contextPtr, this.ast)));
+      }
+
+      lt(other: Seq<Name, ElemSort> | string): Bool<Name> {
+        const otherSeq = isSeq(other) ? other : String.val(other);
+        return new BoolImpl(check(Z3.mk_str_lt(contextPtr, this.ast, otherSeq.ast)));
+      }
+
+      le(other: Seq<Name, ElemSort> | string): Bool<Name> {
+        const otherSeq = isSeq(other) ? other : String.val(other);
+        return new BoolImpl(check(Z3.mk_str_le(contextPtr, this.ast, otherSeq.ast)));
+      }
     }
 
     class ReSortImpl<SeqSortRef extends SeqSort<Name> = SeqSort<Name>> extends SortImpl implements ReSort<Name, SeqSortRef> {

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

@@ -3483,6 +3483,16 @@ export interface StringCreation<Name extends string> {
    * Create a string value
    */
   val(value: string): Seq<Name>;
+
+  /**
+   * Create a single-character string from a Unicode code point (str.from_code).
+   */
+  fromCode(code: Arith<Name> | number | bigint): Seq<Name>;
+
+  /**
+   * Convert an integer expression to its string representation (int.to.str).
+   */
+  fromInt(n: Arith<Name> | number | bigint): Seq<Name>;
 }
 
 /** @category String/Sequence */
@@ -3557,6 +3567,36 @@ export interface Seq<Name extends string = 'main', ElemSort extends Sort<Name> =
 
   /** @category Operations */
   replaceAll(src: Seq<Name, ElemSort> | string, dst: Seq<Name, ElemSort> | string): Seq<Name, ElemSort>;
+
+  /** @category Operations */
+  replaceRe(re: Re<Name>, dst: Seq<Name, ElemSort> | string): Seq<Name, ElemSort>;
+
+  /** @category Operations */
+  replaceReAll(re: Re<Name>, dst: Seq<Name, ElemSort> | string): Seq<Name, ElemSort>;
+
+  /**
+   * Convert a string to its integer value (str.to.int).
+   * @category Operations
+   */
+  toInt(): Arith<Name>;
+
+  /**
+   * Convert a single-character string to its Unicode code point (str.to_code).
+   * @category Operations
+   */
+  toCode(): Arith<Name>;
+
+  /**
+   * String less-than comparison (str.lt).
+   * @category Operations
+   */
+  lt(other: Seq<Name, ElemSort> | string): Bool<Name>;
+
+  /**
+   * String less-than-or-equal comparison (str.le).
+   * @category Operations
+   */
+  le(other: Seq<Name, ElemSort> | string): Bool<Name>;
 }
 
 ///////////////////////