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

[github-actions[bot]]

Summary

This run re-verified all 14 previously cached issues against the current codebase (commit 7040a74, July 7 2026). All 14 remain unresolved. No new API functions were added to z3_api.h since the last run.

Metric	Value
Previously cached issues	14
Resolved	0
Still unresolved	14
Languages covered	Java, .NET/C#, C++, Python, TS/JS, OCaml, Go, Rust

---

Progress

• APIs analyzed (cumulative): ~45 families (~100%)
• This run: Re-verification only
• Next run: Monitor z3_api.h and prove-rs/z3.rs for new additions

---

High Priority

1. Rust missing Simplifier API

z3-sys has all raw FFI bindings (Z3_mk_simplifier, Z3_solver_add_simplifier, etc.) but the high-level z3 crate has no Simplifier type.
Available in: C++, Python, Java, .NET, TS/JS, Go, OCaml
Fix: Add Simplifier struct and Solver::add_simplifier() in z3/src/ (prove-rs/z3.rs)

2. Rust missing FiniteSet API

Neither z3-sys nor the high-level z3 crate expose any Z3_mk_finite_set_* operations.
Available in: All other languages
Fix: Add Z3_mk_finite_set_* to z3-sys, then wrap in z3/src/ast/

3. Rust missing polymorphic datatype support

DatatypeBuilder in the z3 crate has no support for Z3_mk_type_variable / Z3_mk_polymorphic_datatype. z3-sys has both FFI bindings.
Available in: All other languages
Fix: Add Context::type_variable() and extend DatatypeBuilder in prove-rs/z3.rs

---

Medium Priority

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

Exact-count regex repetition. All four have re_loop/Loop/MkLoop (range-based) but lack the simpler re_power(re, n).
Available in: Java, TS/JS, Go (MkRePower), Rust
Fix: Add one-line wrappers in z3++.h, z3.py, Context.cs, z3.ml

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

Functional map/fold operations on sequences.
Available in: C++, Python, Java, .NET, TS/JS, Go
Fix: OCaml — add let mk_seq_map = Z3native.mk_seq_map etc.; Rust — add methods to Seq in z3/src/ast/seq.rs

6. Optimize get_lower/upper_as_vector missing in TS/JS, C++, OCaml, Rust

Returns epsilon-precise bounds as a triple (inf_coeff, value, eps_coeff).
Available in: Python, Java, .NET (GetLowerAsVector), Go
Fix: Add wrappers in high-level.ts, z3++.h, z3.ml, z3/src/optimize.rs

7. OCaml and Go missing Polynomial Subresultants API

Z3_polynomial_subresultants — exposed in C++, Python, Java, .NET, TS/JS, Rust but not OCaml or Go.
Fix: Add to z3.ml and a new or existing .go file

8. Go missing FreshConst/FreshFuncDecl

No MkFreshConst/MkFreshFuncDecl in any Go file. All other languages have it.
Fix: Add func (c *Context) MkFreshConst(prefix string, sort *Sort) *Expr to Go

9. Go missing EnableTrace/DisableTrace

log.go covers OpenLog/CloseLog/AppendLog but not trace control.
Available in: All other languages
Fix: Add EnableTrace(tag string) / DisableTrace(tag string) to log.go

10. Rust missing logging wrappers

No enable_trace, disable_trace, open_log, close_log in the z3 crate (all in z3-sys).
Fix: Add a log module to z3/src/ in prove-rs/z3.rs

11. Simplifier enumeration missing in C++, Python, Go, Rust

GetNumSimplifiers/GetSimplifierName exist in .NET and Java; absent in C++, Python, Go (has GetSimplifierDescr only), and Rust.
Fix: Mirror the tactic enumeration pattern (num_tactics/tactic_name) in each language

12. C++ and Rust missing mk_type_variable wrapper

C++ z3++.h has no context::type_variable(). Rust z3-sys has the binding but the high-level crate does not wrap it.
Available in: .NET, Java, Python, TS/JS, OCaml, Go
Fix: Add to z3++.h; add to z3/src/ in prove-rs/z3.rs

---

Low Priority

13. .NET missing MkLinearOrder, MkPiecewiseLinearOrder, MkTreeOrder

Only MkPartialOrder and MkTransitiveClosure implemented in Context.cs.
Available in: All other languages (Go has all five in relations.go)
Fix: Add the three missing wrappers to Context.cs

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

Regex that matches any single character.
Available in: Python, TS/JS, Java, OCaml (mk_re_allchar line 1324 of z3.ml), Go, Rust
Fix: Add re_allchar(sort rs) to z3++.h; add MkReAllchar(ReSort rs) to Context.cs

15. Go missing AST Id() method

AST.Hash() exists in z3.go but AST.Id() (wrapping Z3_get_ast_id) is absent.
Fix: One-line addition to z3.go

---

Notes for Maintainers

• Rust issues (Specify python version required in readme #1–3, fp.isSubnormal is buggy #10, Cleanup: avoid defining reserved identifiers #12 partial) should be filed/upstreamed to prove-rs/z3.rs
• Go gaps (Compile error Visual Studio 2010 #8, reserved identifier violation #9, Integrating fixes for #10, #13, #14 #15) are typically one- or two-line wrapper additions
• OCaml bindings often require only let mk_foo = Z3native.mk_foo additions
• C++/.NET gaps are concentrated in newer regex and simplifier APIs

Generated by API Coherence Checker · 315.8 AIC · ⌖ 13.6 AIC · ⊞ 28.7K · ◷

• expires on Jul 15, 2026, 4:52 AM UTC