Add missing Go Goal/FuncEntry/Model APIs and TypeScript Seq higher-order operations (#9006)

* Initial plan

* fix: add missing API bindings from discussion #8992 for Go and TypeScript

- Go tactic.go: add Goal.Depth(), Goal.Precision(), Goal.Translate(), Goal.ConvertModel()
- Go solver.go: add FuncEntry struct, FuncInterp.GetEntry/SetElse/AddEntry, Model.HasInterp
- TypeScript types.ts + high-level.ts: add Seq.map/mapi/foldl/foldli

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/go/solver.go

@@ -501,6 +501,64 @@ func (fi *FuncInterp) GetArity() uint {
 	return uint(C.Z3_func_interp_get_arity(fi.ctx.ptr, fi.ptr))
 }
 
+// FuncEntry represents a single entry in a FuncInterp finite map.
+type FuncEntry struct {
+	ctx *Context
+	ptr C.Z3_func_entry
+}
+
+// newFuncEntry creates a new FuncEntry and manages its reference count.
+func newFuncEntry(ctx *Context, ptr C.Z3_func_entry) *FuncEntry {
+	e := &FuncEntry{ctx: ctx, ptr: ptr}
+	C.Z3_func_entry_inc_ref(ctx.ptr, ptr)
+	runtime.SetFinalizer(e, func(entry *FuncEntry) {
+		C.Z3_func_entry_dec_ref(entry.ctx.ptr, entry.ptr)
+	})
+	return e
+}
+
+// GetEntry returns the i-th entry in the function interpretation.
+func (fi *FuncInterp) GetEntry(i uint) *FuncEntry {
+	return newFuncEntry(fi.ctx, C.Z3_func_interp_get_entry(fi.ctx.ptr, fi.ptr, C.uint(i)))
+}
+
+// SetElse sets the else value of the function interpretation.
+func (fi *FuncInterp) SetElse(val *Expr) {
+	C.Z3_func_interp_set_else(fi.ctx.ptr, fi.ptr, val.ptr)
+}
+
+// AddEntry adds a new entry to the function interpretation.
+// The args slice provides the argument values and val is the return value.
+func (fi *FuncInterp) AddEntry(args []*Expr, val *Expr) {
+	vec := C.Z3_mk_ast_vector(fi.ctx.ptr)
+	C.Z3_ast_vector_inc_ref(fi.ctx.ptr, vec)
+	defer C.Z3_ast_vector_dec_ref(fi.ctx.ptr, vec)
+	for _, a := range args {
+		C.Z3_ast_vector_push(fi.ctx.ptr, vec, a.ptr)
+	}
+	C.Z3_func_interp_add_entry(fi.ctx.ptr, fi.ptr, vec, val.ptr)
+}
+
+// GetValue returns the return value of the function entry.
+func (e *FuncEntry) GetValue() *Expr {
+	return newExpr(e.ctx, C.Z3_func_entry_get_value(e.ctx.ptr, e.ptr))
+}
+
+// GetNumArgs returns the number of arguments in the function entry.
+func (e *FuncEntry) GetNumArgs() uint {
+	return uint(C.Z3_func_entry_get_num_args(e.ctx.ptr, e.ptr))
+}
+
+// GetArg returns the i-th argument of the function entry.
+func (e *FuncEntry) GetArg(i uint) *Expr {
+	return newExpr(e.ctx, C.Z3_func_entry_get_arg(e.ctx.ptr, e.ptr, C.uint(i)))
+}
+
+// HasInterp reports whether the model contains an interpretation for the given declaration.
+func (m *Model) HasInterp(decl *FuncDecl) bool {
+	return bool(C.Z3_model_has_interp(m.ctx.ptr, m.ptr, decl.ptr))
+}
+
 // SortUniverse returns the universe of values for an uninterpreted sort in the model.
 // The universe is represented as a list of distinct expressions.
 // Returns nil if the sort is not an uninterpreted sort in this model.

src/api/go/tactic.go

@@ -200,6 +200,29 @@ func (g *Goal) Reset() {
 	C.Z3_goal_reset(g.ctx.ptr, g.ptr)
 }
 
+// Depth returns the depth of the goal.
+// It tracks how many times the goal was transformed by a tactic.
+func (g *Goal) Depth() uint {
+	return uint(C.Z3_goal_depth(g.ctx.ptr, g.ptr))
+}
+
+// Precision returns the precision of the goal as a uint.
+// Possible values: 0 = precise, 1 = under-approximation, 2 = over-approximation, 3 = under+over.
+func (g *Goal) Precision() uint {
+	return uint(C.Z3_goal_precision(g.ctx.ptr, g.ptr))
+}
+
+// Translate creates a copy of the goal in the target context.
+func (g *Goal) Translate(target *Context) *Goal {
+	return newGoal(target, C.Z3_goal_translate(g.ctx.ptr, g.ptr, target.ptr))
+}
+
+// ConvertModel converts a model from the original goal into a model for this goal.
+// Use this when a tactic has transformed the goal and you need a model for the original.
+func (g *Goal) ConvertModel(m *Model) *Model {
+	return newModel(g.ctx, C.Z3_goal_convert_model(g.ctx.ptr, g.ptr, m.ptr))
+}
+
 // String returns the string representation of the goal.
 func (g *Goal) String() string {
 	return C.GoString(C.Z3_goal_to_string(g.ctx.ptr, g.ptr))

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

@@ -4422,6 +4422,24 @@ export function createApi(Z3: Z3Core, em?: any): Z3HighLevel {
         const otherSeq = isSeq(other) ? other : String.val(other);
         return new BoolImpl(check(Z3.mk_str_le(contextPtr, this.ast, otherSeq.ast)));
       }
+
+      map(f: Expr<Name>): Seq<Name> {
+        return new SeqImpl(check(Z3.mk_seq_map(contextPtr, f.ast, this.ast)));
+      }
+
+      mapi(f: Expr<Name>, i: Arith<Name> | number | bigint): Seq<Name> {
+        const iExpr = isArith(i) ? i : Int.val(i);
+        return new SeqImpl(check(Z3.mk_seq_mapi(contextPtr, f.ast, iExpr.ast, this.ast)));
+      }
+
+      foldl(f: Expr<Name>, a: Expr<Name>): Expr<Name> {
+        return _toExpr(check(Z3.mk_seq_foldl(contextPtr, f.ast, a.ast, this.ast)));
+      }
+
+      foldli(f: Expr<Name>, i: Arith<Name> | number | bigint, a: Expr<Name>): Expr<Name> {
+        const iExpr = isArith(i) ? i : Int.val(i);
+        return _toExpr(check(Z3.mk_seq_foldli(contextPtr, f.ast, iExpr.ast, a.ast, this.ast)));
+      }
     }
 
     class ReSortImpl<SeqSortRef extends SeqSort<Name> = SeqSort<Name>> extends SortImpl implements ReSort<Name, SeqSortRef> {

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

@@ -3597,6 +3597,30 @@ export interface Seq<Name extends string = 'main', ElemSort extends Sort<Name> =
    * @category Operations
    */
   le(other: Seq<Name, ElemSort> | string): Bool<Name>;
+
+  /**
+   * Apply function f to each element of the sequence (seq.map).
+   * @category Operations
+   */
+  map(f: Expr<Name>): Seq<Name>;
+
+  /**
+   * Apply function f to each element and its index in the sequence (seq.mapi).
+   * @category Operations
+   */
+  mapi(f: Expr<Name>, i: Arith<Name> | number | bigint): Seq<Name>;
+
+  /**
+   * Left-fold function f over the sequence with initial accumulator a (seq.foldl).
+   * @category Operations
+   */
+  foldl(f: Expr<Name>, a: Expr<Name>): Expr<Name>;
+
+  /**
+   * Left-fold function f with index over the sequence with initial accumulator a (seq.foldli).
+   * @category Operations
+   */
+  foldli(f: Expr<Name>, i: Arith<Name> | number | bigint, a: Expr<Name>): Expr<Name>;
 }
 
 ///////////////////////