[API Coherence] Report for 2026-06-06 - Re-verification + Simplifier Enumeration Gap

[github-actions[bot]]

Summary

Re-verified all 7 previously cached issues — all remain open. One new gap found: Simplifier Enumeration API missing in several languages.

• APIs re-verified: 40+ API families (full coverage)
• Previously cached issues resolved: 0
• New inconsistencies found: 1
• Total open issues: 8

Notable: Go gained significant new coverage (finiteset.go, simplifier.go, relations.go) since the previous analysis.

---

High Priority Issues

1. Rust Missing Simplifier API

What: No Simplifier struct or Solver::add_simplifier() in the high-level z3 crate. z3-sys has the raw FFI.
Available in: C, C++, Python, .NET, Java, TypeScript/JS, OCaml, Go
Missing in: Rust z3 crate (/z3/src/ — no simplifier.rs)
Fix: Add simplifier.rs with a Simplifier struct and methods: and_then, using_params, get_help, get_param_descrs; add Solver::add_simplifier.
Verified: 2026-06-06

2. Rust Missing FiniteSet API (both z3 and z3-sys)

What: No FiniteSet bindings at all in z3-sys (only unrelated Z3_mk_finite_domain_sort). Missing: Z3_mk_finite_set_sort, empty, singleton, union, intersect, difference, member, size, subset, map, filter, range.
Available in: C, C++, Python, .NET, Java, OCaml, TypeScript/JS, Go
Missing in: Rust z3-sys (no FFI) and Rust z3 crate
Fix: Add FFI bindings to z3-sys/src/generated/functions.rs, then wrap in z3/src/.
Verified: 2026-06-06

---

Medium Priority Issues

3. Missing Simplifier Enumeration API (New)

What: Z3_get_num_simplifiers, Z3_get_simplifier_name, Z3_simplifier_get_descr allow enumerating available simplifiers.

Language	GetNumSimplifiers	GetSimplifierName	GetSimplifierDescr
.NET	✅	✅	❌
Java	✅	✅	❌
OCaml	✅	✅	❌
Go	❌	❌	✅
C++	❌	❌	❌
Python	❌	❌	❌
TypeScript/JS	❌	❌	❌
Rust z3-sys	✅ (raw FFI)	✅	✅
Rust z3	❌	❌	❌

Fix:

• Go (simplifier.go): Add GetNumSimplifiers() uint and GetSimplifierName(i uint) string
• C++ (z3++.h): Add unsigned num_simplifiers(), std::string simplifier_name(unsigned i) to context; std::string descr() to simplifier class
• Python (z3.py): Add simplifier_names(ctx=None) and simplifier_descr(name, ctx=None) module-level functions
• TypeScript/JS: Add getNumSimplifiers(), getSimplifierName(i), getSimplifierDescr(name) to context API
  Verified: 2026-06-06

4. OCaml and Go Missing Polynomial Subresultants

What: Z3_polynomial_subresultants not wrapped in OCaml or Go.
Available in: C, C++, Python, .NET, Java, TypeScript/JS, Rust z3-sys
Fix: Add src/api/go/polynomial.go; add Polynomial.subresultants to src/api/ml/z3.ml.
Verified: 2026-06-06

5. Go Missing MkFreshConst / MkFreshFuncDecl

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

6. Go and Rust Missing Trace API

What: Z3_enable_trace/Z3_disable_trace not wrapped in Go (log.go only has Open/Close/Append). Rust z3 has no logging at all.
Available in: C, C++, Python, .NET, Java, TypeScript/JS, OCaml
Fix: Add EnableTrace(tag string) / DisableTrace(tag string) to src/api/go/log.go; add module-level trace/log functions to Rust z3.
Verified: 2026-06-06

---

Low Priority Issues

7. .NET Missing MkLinearOrder, MkPiecewiseLinearOrder, MkTreeOrder

What: src/api/dotnet/Context.cs has MkPartialOrder and MkTransitiveClosure but is missing the other three special relation constructors.
Available in: C, C++, Python, Java, TypeScript/JS, OCaml, Go, Rust z3-sys
Fix: Add three methods near MkPartialOrder (line 5168) wrapping Native.Z3_mk_linear_order, Z3_mk_piecewise_linear_order, Z3_mk_tree_order.
Verified: 2026-06-06

8. Go Missing AST.Id() Method

What: AST.Hash() exists in src/api/go/z3.go (line 176) but AST.Id() wrapping Z3_get_ast_id does not.
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 src/api/go/z3.go.
Verified: 2026-06-06

---

Issue Tracker

Issue	Priority	Languages	Status
Rust missing Simplifier API	High	Rust z3 crate	Open
Rust missing FiniteSet API	High	Rust z3, z3-sys	Open
Simplifier enumeration API	Medium	C++, Python, TS/JS, Go, Rust z3	New
Polynomial Subresultants	Medium	OCaml, Go	Open
Go MkFreshConst/FreshFuncDecl	Medium	Go	Open
Trace API (Enable/Disable)	Medium	Go, Rust z3	Open
.NET 3 Special Relations	Low	.NET	Open
Go AST.Id()	Low	Go	Open

Generated by API Coherence Checker · sonnet46 3M · ◷

• expires on Jun 13, 2026, 5:09 AM UTC

[github-actions[bot]]

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

A newer discussion is available at Discussion #9753.