[API Coherence] Report for 2026-07-05 – Full API Surface Re-verification

[github-actions[bot]]

Summary

Re-verification pass of all 14 previously cached issues against the current codebase. No new API families analyzed (cumulative coverage: ~100% of known C API surface).

Metric	Value
APIs analyzed (cumulative)	43 families
Languages covered	8
Cached issues re-verified	14
Newly resolved since 2026-07-04	1 (partial)
Still-unresolved	14 (1 updated scope)

Resolution Updates

• ⚠️ Partial: Rust re_power — prove-rs/z3.rs z3/src/ast/regexp.rs:82 now has re_power(). Rust removed from that issue's "Missing in" list. C++, Python, .NET, OCaml still affected.

---

High Priority

1. Rust missing Simplifier API

z3-sys has Z3_mk_simplifier, Z3_solver_add_simplifier, etc., but the high-level z3 crate has no Simplifier type or Solver::add_simplifier().
Missing in: Rust. Fix: Add Simplifier<'ctx> wrapper and Solver::add_simplifier() in prove-rs/z3.rs.

2. Rust missing FiniteSet API (even in z3-sys)

z3-sys has no Z3_mk_finite_set_* bindings at all. The C API exposes 9 finite-set functions.
Missing in: Rust (both z3-sys and high-level z3 crate). Fix: Add FFI declarations to z3-sys/src/generated/functions.rs, then high-level wrappers.

3. Rust missing polymorphic datatype support

z3-sys has Z3_mk_polymorphic_datatype and Z3_mk_type_variable but DatatypeBuilder has no polymorphic type mechanism.
Missing in: Rust. Fix: Extend z3/src/datatype_builder/mod.rs with type-variable support.

---

Medium Priority

4. C++, Python, .NET, OCaml missing re_power (Z3_mk_re_power)

Creates a regex matching exactly n repetitions. Rust now has it; Java, TypeScript/JS, Go already had it.
Missing in: C++ (z3++.h), Python (z3.py), .NET (Context.cs), OCaml (z3.ml).
Fix: e.g. C++ re_power(expr const& re, unsigned n), Python RePower(re, n), .NET MkRePower(ReExpr re, uint n).

5. OCaml and Rust missing seq functional ops (seq_map, seq_mapi, seq_foldl, seq_foldli)

z3-sys exposes all four C bindings; high-level z3 crate's Seq type does not.
Missing in: OCaml (z3.ml), Rust (z3/src/ast/seq.rs).
Fix: Add mk_seq_map/mapi/foldl/foldli to OCaml; add map/mapi/foldl/foldli methods to Rust Seq.

6. OCaml and Go missing Polynomial Subresultants API

Z3_polynomial_subresultants exposed in C, C++, Python, .NET, Java, TypeScript/JS, Rust but not OCaml or Go.
Fix: Add wrappers to src/api/ml/z3.ml and src/api/go/ (new polynomial.go).

7. Go missing FreshConst / FreshFuncDecl

All other 7 languages provide fresh-name constant creation; Go does not.
Fix: Add MkFreshConst/MkFreshFuncDecl to src/api/go/expr.go.

8. Go missing EnableTrace / DisableTrace

Go has OpenLog/CloseLog but not Z3_enable_trace/Z3_disable_trace wrappers.
Fix: Add EnableTrace(tag string) and DisableTrace(tag string) to src/api/go/log.go.

9. Rust missing logging wrappers (enable_trace, disable_trace, open_log, close_log)

z3-sys exposes these but high-level z3 crate has no public wrappers.
Fix: Add free functions in z3/src/lib.rs or new z3/src/log.rs in prove-rs/z3.rs.

10. C++, Python, Go, Rust missing simplifier enumeration API

Z3_get_num_simplifiers/Z3_get_simplifier_name available in .NET and Java. Go has GetSimplifierDescr only.
Missing in: C++ (z3++.h), Python (z3.py), Go (partial), Rust.
Fix: Add num_simplifiers() + simplifier_name(i) to each language.

11. C++ and Rust missing mk_type_variable

z3-sys exposes the FFI; C++ has no context::type_variable() wrapper.
Missing in: C++ (z3++.h), Rust (high-level z3 crate).

12. Optimize get_lower/upper_as_vector missing in TypeScript/JS, C++, OCaml, Rust

These return an (inf, value, eps) triple needed to correctly read strict-vs-non-strict bounds.
Available in: Python, Java, .NET, Go. Missing in: TypeScript/JS, C++, OCaml, Rust.

---

Low Priority

13. C++ and .NET missing allchar (Z3_mk_re_allchar)

Regex matching any single char. Available in Python (AllChar), Java, TypeScript/JS, OCaml, Go, Rust.
Missing in: C++ (z3++.h), .NET (Context.cs).

14. .NET missing MkLinearOrder, MkPiecewiseLinearOrder, MkTreeOrder

.NET only exposes MkPartialOrder and MkTransitiveClosure of the five special-relation functions.
Missing in: .NET (Context.cs near line 5168). Fix: Add the three missing methods.

15. Go missing AST.Id() method

Go has Hash() but not Id() (wrapping Z3_get_ast_id).
Missing in: Go (src/api/go/z3.go). Fix: Add func (a *Ast) Id() uint { ... }.

---

Issue Count by Language

Language	Open Issues
Rust	8
Go	5
C++	5
OCaml	4
.NET	3
Python	2
TypeScript/JS	1
Java	0

Next Steps

Monitor src/api/z3_api.h for newly added C API functions and prove-rs/z3.rs for Rust fixes to the open issues above.

Generated by API Coherence Checker · 248.4 AIC · ⌖ 13.8 AIC · ⊞ 28.7K · ◷

• expires on Jul 12, 2026, 5:04 AM UTC

[github-actions[bot]]

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

A newer discussion is available at Discussion #10055.