[API Coherence] Report for 2026-03-14 – Datatype, Model, Tactic/Goal/Probe, Fixedpoint APIs

[github-actions[bot]]

Summary

Run 4 of ongoing API coherence analysis.

Metric	Value
API families analyzed this run	Datatype, Model, Tactic/Goal/Probe, Fixedpoint
Cumulative API families analyzed	12 / ~20 (60%)
Previously cached issues re-verified	14
Cached issues resolved since last run	9 resolved
New issues found this run	4
Total open issues	9

---

✅ Resolution Updates (9 Resolved Since Run 3)

The following previously tracked gaps have been resolved and removed from the open-issues list:

Issue	Resolution
Java missing bvredand / bvredor	Added at Context.java:1195,1207
Go missing bvredand / bvredor	Added at bitvec.go:227,232
C++ and Go missing ext_rotate_left / ext_rotate_right	C++ had it (z3++.h:1536-1537); Go added MkBVExtRotateLeft/Right (bitvec.go:237-243)
Go missing 6 arithmetic functions (MkPower, MkAbs, MkInt2Real, MkReal2Int, MkIsInt, MkDivides)	All added in arith.go:128-155
Go FPA missing rounding mode constants	All added in fp.go:172+
Go FPA missing conversion functions (to_fp_bv, to_fp_float, to_fp_real, to_fp_signed/unsigned, to_sbv, to_ubv, MkFPFP)	All added in fp.go:196-283
Go FPA missing FMA, Rem, Min, Max, RoundToIntegral	All added in fp.go:226-247
Go FPA missing numeral constructors	All added in fp.go:201-223
Go missing seq/string functions (MkSeqReplaceAll, MkSeqNth, MkSeqLastIndex, MkSeqMap, etc.)	All added in seq.go:234+
Go missing array MkMap	Added at array.go:76

The Go bindings have seen substantial improvement since the last run.

---

Progress

• APIs analyzed so far: Solver, Optimize, BitVector, Array, Floating-Point, Quantifier, Arithmetic, Sequence/String/RegExp, Datatype, Model, Tactic/Goal/Probe, Fixedpoint — 12/~20 families (60%)
• Next run: AST Vector/Map APIs, Symbol/Sort/FuncDecl APIs, Context/Config APIs, Statistics APIs, Parser APIs

---

Open Issues

Medium Priority

1. Go Goal Missing Introspection Methods

What's missing: Goal.Depth(), Goal.ConvertModel(), Goal.Translate(), Goal.Precision()
C API: Z3_goal_depth, Z3_goal_convert_model, Z3_goal_translate, Z3_goal_prec / Z3_goal_precision
Available in: Python, Java, .NET, C++, OCaml, TypeScript, Rust (goal.rs has get_depth, get_precision)
Missing in: Go (src/api/go/tactic.go — Goal struct only has Assert, Size, Formula, NumExprs, IsDecidedSat, IsDecidedUnsat, Reset, String)
Suggested fix: Add Depth() uint, Precision() uint, Translate(ctx *Context) *Goal, and ConvertModel(s *Solver) *Model methods to Goal in tactic.go
Priority: Medium

---

2. Go Model / FuncInterp Missing Entry-Level APIs

What's missing: A FuncEntry type and corresponding methods: FuncInterp.GetEntry(i uint) *FuncEntry, FuncInterp.AddEntry(args []*Expr, val *Expr), FuncInterp.SetElse(val *Expr), Model.HasInterp(decl *FuncDecl) bool
C API: Z3_func_interp_get_entry, Z3_func_interp_add_entry, Z3_func_interp_set_else, Z3_func_entry_get_value, Z3_func_entry_get_arg, Z3_func_entry_get_num_args, Z3_model_has_interp
Available in: Python, Java, .NET, C++, OCaml, TypeScript, Rust (func_interp.rs and func_entry.rs expose all these)
Missing in: Go (src/api/go/solver.go — FuncInterp only has NumEntries, GetElse, GetArity)
Suggested fix: Add a FuncEntry struct with GetValue, GetArg, GetNumArgs methods; add GetEntry(i uint) *FuncEntry, AddEntry, SetElse to FuncInterp; add HasInterp to Model
Priority: Medium

---

3. Rust Fixedpoint Missing High-Level Wrappers

What's missing: The Rust high-level Fixedpoint type (in z3/src/fixedpoint.rs) exposes most C API functions but is missing:

• get_rules → Z3_fixedpoint_get_rules (returns the set of rules as an AstVector)
• get_assertions → Z3_fixedpoint_get_assertions (returns asserted axioms as an AstVector)
• get_param_descrs → Z3_fixedpoint_get_param_descrs
• set_predicate_representation → Z3_fixedpoint_set_predicate_representation

All four bindings exist in z3-sys (verified at z3-sys/src/lib.rs:6559,6568,6571,6595).
Available in: Python, Java, .NET, C++, Go (fixedpoint.go has GetRules, GetAssertions, GetParamDescrs, SetPredicateRepresentation)
Missing in: Rust (z3/src/fixedpoint.rs)
Suggested fix: Add four methods to the Fixedpoint struct in z3.rs; the z3-sys bindings are already in place
Priority: Medium

---

4. Rust Seq Missing Most Sequence Operations

What's missing: The Rust Seq type (z3/src/ast/seq.rs) only implements: new_const, fresh_const, empty, unit, at, nth, length, contains, concat

Missing operations with C API equivalents available in z3-sys:

• extract / Z3_mk_seq_extract (subsequence by offset+length)
• replace / Z3_mk_seq_replace
• replace_all / Z3_mk_seq_replace_all
• replace_re / Z3_mk_seq_replace_re
• replace_re_all / Z3_mk_seq_replace_re_all
• is_prefix / Z3_mk_seq_prefix
• is_suffix / Z3_mk_seq_suffix
• index_of / Z3_mk_seq_index
• last_index_of / Z3_mk_seq_last_index
• map / Z3_mk_seq_map
• mapi / Z3_mk_seq_mapi
• foldl / Z3_mk_seq_foldl
• foldli / Z3_mk_seq_foldli

Available in: Python, Java, .NET, C++, Go, TypeScript (except map/mapi/foldl/foldli)
Missing in: Rust
Suggested fix: Expand z3/src/ast/seq.rs with the above methods; all underlying z3-sys bindings already exist
Priority: Medium

---

5. TypeScript Missing Sequence Higher-Order Operations

What's missing: TypeScript (src/api/js/src/high-level/high-level.ts) is missing:

• seqMap / Z3_mk_seq_map
• seqMapi / Z3_mk_seq_mapi
• seqFoldl / Z3_mk_seq_foldl
• seqFoldli / Z3_mk_seq_foldli

Note: Most other previously-missing seq functions (replace_re, str_to_int, string_to_code, str_lt, str_le, etc.) have been added and are no longer missing.
Available in: Python, Java, .NET, C++, Go, OCaml
Missing in: TypeScript
Suggested fix: Add wrapper methods to the SeqImpl class in high-level.ts
Priority: Medium

---

Low Priority

6. Rust BV Missing repeat Operation

What's missing: BV::repeat(n) wrapping Z3_mk_repeat
z3-sys binding exists at z3-sys/src/lib.rs:2760
Available in: Python, C++, Java, .NET, OCaml, TypeScript, Go
Missing in: Rust (z3/src/ast/bv.rs — all other BV unary/binary/shift ops use the macro pattern, but repeat is missing)
Suggested fix: Add pub fn repeat(&self, i: u32) -> Self to BV in bv.rs
Priority: Low

---

7. Rust Tactic Missing Parallel Combinators

What's missing: Tactic::par_or (run tactics in parallel, return first success), Tactic::par_and_then (parallel composition), and Tactic::fail_if_not_decided
C API: Z3_tactic_par_or, Z3_tactic_par_and_then, Z3_tactic_fail_if_not_decided
Available in: Python, Java, .NET, C++, Go (tactic.go:114-124), TypeScript
Missing in: Rust (z3/src/tactic.rs — has or_else, and_then, cond, fail_if, but no parallel variants)
Suggested fix: Add par_or, par_and_then, fail_if_not_decided to Tactic in tactic.rs; z3-sys bindings exist
Priority: Low

---

8. Rust Solver Missing Advanced APIs (Ongoing)

What's missing: The Rust Solver (z3/src/solver.rs) is missing newer APIs:

• cube / Z3_solver_cube
• get_trail / Z3_solver_get_trail
• congruence_root / Z3_solver_congruence_root
• congruence_next / Z3_solver_congruence_next
• solve_for / Z3_solver_solve_for
• set_initial_value / Z3_solver_set_initial_value
• add_simplifier / Z3_solver_add_simplifier
• register_on_clause / Z3_solver_register_on_clause
• to_dimacs / Z3_solver_to_dimacs_string

Several of these are also missing from z3-sys FFI bindings, blocking the Rust high-level from implementing them.
Available in: Python, Java, .NET, C++, Go
Missing in: Rust
Priority: Low (some of these are niche/advanced features)

---

Notes for Maintainers

1. The Go bindings have improved dramatically since the previous run — many previously missing FP, arithmetic, sequence, and array APIs have been added. The remaining gaps are relatively small.
2. The Rust external crate (prove-rs/z3.rs) remains the most incomplete binding, particularly for sequence operations and newer solver features.
3. Issues Specify python version required in readme #1, Fixed exponentiation in examples/python/complex/complex.py. #2 (Go Goal/Model) are straightforward to implement since the z3-sys–equivalent C API wrappers are already established patterns in Go.

AI generated by API Coherence Checker · history

• expires on Mar 21, 2026, 11:22 PM UTC

[github-actions[bot]]

This discussion has been marked as outdated by API Coherence Checker.

A newer discussion is available at Discussion #9021.