diff --git a/src/api/go/solver.go b/src/api/go/solver.go index 74053ad70..6e2a1f019 100644 --- a/src/api/go/solver.go +++ b/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. diff --git a/src/api/go/tactic.go b/src/api/go/tactic.go index 0d9426c7b..8961c2df8 100644 --- a/src/api/go/tactic.go +++ b/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)) diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 9cfbb68d8..71f156557 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/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): Seq { + return new SeqImpl(check(Z3.mk_seq_map(contextPtr, f.ast, this.ast))); + } + + mapi(f: Expr, i: Arith | number | bigint): Seq { + 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, a: Expr): Expr { + return _toExpr(check(Z3.mk_seq_foldl(contextPtr, f.ast, a.ast, this.ast))); + } + + foldli(f: Expr, i: Arith | number | bigint, a: Expr): Expr { + 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 = SeqSort> extends SortImpl implements ReSort { diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index e9c695618..db28c8d16 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -3597,6 +3597,30 @@ export interface Seq = * @category Operations */ le(other: Seq | string): Bool; + + /** + * Apply function f to each element of the sequence (seq.map). + * @category Operations + */ + map(f: Expr): Seq; + + /** + * Apply function f to each element and its index in the sequence (seq.mapi). + * @category Operations + */ + mapi(f: Expr, i: Arith | number | bigint): Seq; + + /** + * Left-fold function f over the sequence with initial accumulator a (seq.foldl). + * @category Operations + */ + foldl(f: Expr, a: Expr): Expr; + + /** + * Left-fold function f with index over the sequence with initial accumulator a (seq.foldli). + * @category Operations + */ + foldli(f: Expr, i: Arith | number | bigint, a: Expr): Expr; } ///////////////////////