[API Coherence] Report for 2026-07-06 - Re-verification of All Open Issues

[github-actions[bot]]

Summary

Re-verification run confirming all previously identified API coherence issues. No new gaps found.

• C API surface covered: ~573 functions (100%)
• Issues re-verified: 15
• Resolved since last run: 0
• Still open: 15

---

High Priority

1. Rust Missing Simplifier API

z3-sys exposes Z3_mk_simplifier, Z3_simplifier_and_then, Z3_simplifier_using_params, Z3_solver_add_simplifier, but the high-level z3 crate has no Simplifier type and no Solver::add_simplifier().
Available in: C, C++, Python, Java, .NET, Go, TypeScript/JS, OCaml
Fix: Add Simplifier struct and Solver::add_simplifier() to prove-rs/z3.rs
Verified: 2026-07-06

2. Rust Missing FiniteSet API

No Z3_mk_finite_set_* bindings in z3-sys at all, and no FiniteSet support in the high-level crate.
Available in: C, C++, Python, Java, .NET, Go, TypeScript/JS, OCaml
Fix: Add FFI bindings in z3-sys, then expose a high-level FiniteSetSort in z3 crate
Verified: 2026-07-06

3. Rust Missing Polymorphic Datatype Support

z3-sys exposes Z3_mk_polymorphic_datatype and Z3_mk_type_variable, but the high-level DatatypeBuilder has no support for type parameters.
Available in: C, C++, Python, Java, .NET, Go, TypeScript/JS, OCaml
Fix: Extend DatatypeBuilder and add Context::type_variable() in the z3 crate
Verified: 2026-07-06

---

Medium Priority

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

Exact-repetition regex (re.^(n)). C++ has re_loop (range), not exact-count. Python has Loop, not Power. .NET has MkLoop, not MkRePower. OCaml has mk_re_loop, not mk_re_power.
Available in: C, Java, TypeScript/JS, Go, Rust (regexp.rs:82)
Fix: Add re_power/RePower/MkRePower/mk_re_power to each missing language
Verified: 2026-07-06

5. C++ and .NET Missing allchar (Z3_mk_re_allchar)

Regex matching any single character.
Available in: C, Python (AllChar), TypeScript/JS, Java, OCaml (mk_re_allchar), Go (MkReAllchar)
Fix: Add re_allchar(sort) to C++ z3++.h; MkReAllchar(sort) to .NET Context.cs
Verified: 2026-07-06

6. OCaml and Rust Missing Sequence Functional Operations

Z3_mk_seq_map, Z3_mk_seq_mapi, Z3_mk_seq_foldl, Z3_mk_seq_foldli — all missing from OCaml and the Rust high-level crate (z3-sys exposes all four).
Available in: C, C++, Python, Java, .NET, TypeScript/JS, Go
Fix: Add wrappers in OCaml z3.ml; add map/mapi/foldl/foldli to Rust Seq type
Verified: 2026-07-06

7. OCaml and Go Missing Polynomial Subresultants

Z3_polynomial_subresultants — no wrapper in OCaml (z3.ml) or Go.
Available in: C, C++, Python, Java, .NET, TypeScript/JS, Rust (polynomial.rs)
Fix: Add OCaml wrapper in z3.ml; add polynomial.go in src/api/go/
Verified: 2026-07-06

8. Go Missing FreshConst / MkFreshFuncDecl

No MkFreshConst/MkFreshFuncDecl wrappers in src/api/go/.
Available in: All other languages
Fix: Add func (c *Context) MkFreshConst(prefix string, sort *Sort) *Expr and MkFreshFuncDecl to Go
Verified: 2026-07-06

9. Go Missing EnableTrace / DisableTrace

log.go has OpenLog/CloseLog but not EnableTrace/DisableTrace.
Available in: All other languages
Fix: Add to src/api/go/log.go
Verified: 2026-07-06

10. Missing Simplifier Enumeration in C++, Python, Go, Rust

Z3_get_num_simplifiers/Z3_get_simplifier_name allow iterating available simplifiers.
Available in: .NET, Java, OCaml
Missing: C++ (z3++.h), Python (z3.py), Go (simplifier.go has GetSimplifierDescr only), Rust
Fix: Add num_simplifiers() and simplifier_name(i) to each missing binding
Verified: 2026-07-06

11. Rust Missing Logging Wrappers

z3-sys exposes Z3_open_log, Z3_close_log, Z3_enable_trace, Z3_disable_trace but the high-level z3 crate has none.
Fix: Add module-level enable_trace, disable_trace, open_log, close_log to z3 crate
Verified: 2026-07-06

12. C++ and Rust Missing type_variable Wrapper

Z3_mk_type_variable creates a sort variable for polymorphic types.
Available in: C, Python, Java, .NET, Go, TypeScript/JS, OCaml
Fix: Add context::type_variable(symbol) to C++; Context::type_variable(Symbol) to Rust z3 crate
Verified: 2026-07-06

13. Optimize Vector Bounds Missing in TypeScript/JS, C++, OCaml, Rust

Z3_optimize_get_lower_as_vector / Z3_optimize_get_upper_as_vector return a (infeasible, value, eps) triple. Only scalar getLower/getUpper exposed in these four languages.
Available in: C, Python, Java, .NET, Go
Fix: Add getLowerAsVector/getUpperAsVector in each missing language
Verified: 2026-07-06

---

Low Priority

14. .NET Missing MkLinearOrder, MkPiecewiseLinearOrder, MkTreeOrder

Context.cs has MkPartialOrder (line 5168) and MkTransitiveClosure (line 5178) but is missing the other three special relation constructors.
Available in: C, C++, Python, Java, Go, TypeScript/JS, OCaml
Fix: Add MkLinearOrder, MkPiecewiseLinearOrder, MkTreeOrder to src/api/dotnet/Context.cs
Verified: 2026-07-06

15. Go Missing AST.Id() Method

z3.go has Hash() but not Id() (wrapping Z3_get_ast_id).
Available in: All other languages
Fix: Add func (a *AST) Id() uint { return uint(C.Z3_get_ast_id(a.ctx.ptr, a.ptr)) } to z3.go
Verified: 2026-07-06

---

Summary Table

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

Generated by API Coherence Checker · 288.6 AIC · ⌖ 13.7 AIC · ⊞ 28.7K · ◷

• expires on Jul 13, 2026, 5:19 AM UTC

[github-actions[bot]]

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

A newer discussion is available at Discussion #10060.