[API Coherence] Report for 2026-06-08 – Verification Run + Type Variable & Polymorphic Datatype APIs

[github-actions[bot]]

Summary

This run re-verified all 8 previously cached issues (all confirmed still open) and investigated three additional API families.

Metric	Value
APIs verified in this run	Type Variable API, Polymorphic Datatype API, BV Overflow/Underflow API
Total functions checked	~15
Languages covered	8 (C, C++, Java, .NET, Python, TypeScript/JS, OCaml, Go, Rust)
Previously cached issues resolved	0
New issues found	2
Total open issues	10

Resolution Updates

No previously cached issues have been resolved since the last run (2026-06-07). All 8 issues were re-verified as still open in the current codebase (Z3Prover/z3 at 59bb444, prove-rs/z3.rs cloned fresh on 2026-06-08).

Progress

• APIs analyzed to date: ~45+ API families across the entire C API surface (~100% coverage)
• This run: Re-verification + Type Variable API, Polymorphic Datatype API, BV Overflow/Underflow Detection API
• Next runs: Monitor z3_api.h for newly added C API functions; monitor prove-rs/z3.rs for Rust improvements

---

High Priority Issues

1. Rust Missing Simplifier API

What: The Rust high-level z3 crate has no Simplifier type and no Solver::add_simplifier() method. The low-level z3-sys crate exposes the full C FFI, but it is not wrapped.

Available in: C, C++ (simplifier class, solver.add_simplifier()), Python (SimplifierRef, Solver.add_simplifier()), Java (Simplifier, Solver.addSimplifier()), .NET (Simplifier, Solver.AddSimplifier()), TypeScript/JS, OCaml, Go

Missing in: Rust high-level z3 crate (z3/src/)

Suggested fix: Add a Simplifier<'ctx> struct to z3/src/simplifier.rs wrapping Z3_simplifier, with and_then() and using_params() combinators, and a Solver::add_simplifier() method.

Priority: High

---

2. Rust Missing FiniteSet API (also missing from z3-sys FFI layer)

What: z3-sys does not expose Z3_mk_finite_set_sort, Z3_mk_finite_set_empty, Z3_mk_finite_set_singleton, Z3_mk_finite_set_union, Z3_mk_finite_set_inter, Z3_mk_finite_set_subset, Z3_mk_finite_set_member, Z3_mk_finite_set_complement, Z3_mk_set_to_finite_set, or Z3_mk_finite_set_of_seq. (Note: Z3_mk_finite_domain_sort is an unrelated API.) The high-level z3 crate therefore has no FiniteSet support at all.

Available in: C (z3_api.h), C++ (finite_set_sort(), set operations on expr), Python (FiniteSetSort, EmptySet, FullSet, SetUnion, etc.), Java, .NET, TypeScript/JS, OCaml (FiniteSet module), Go (finiteset.go)

Missing in: Both z3-sys (FFI layer) and z3 (high-level) crates in prove-rs/z3.rs

Suggested fix: Add all Z3_mk_finite_set_* functions to z3-sys/src/, then add a FiniteSet<'ctx> type and set operation methods to the high-level z3 crate.

Priority: High (entire API family missing from FFI layer)

---

3. Rust Missing Polymorphic Datatype Support (new this run)

What: The Rust high-level z3 crate's DatatypeBuilder only supports monomorphic datatypes. z3-sys exposes Z3_mk_type_variable and Z3_mk_polymorphic_datatype, but the high-level crate has no API to create type variable sorts or polymorphic datatypes with type parameters.

Available in: C, C++ (context::datatype(name, params, constructors)), Python (CreatePolymorphicDatatype()), Java (Context.mkPolymorphicDatatypeSort()), .NET (Context.MkPolymorphicDatatypeSort()), TypeScript/JS (Datatype.createPolymorphicDatatype()), OCaml (Datatype.mk_polymorphic_sort), Go (Context.MkPolymorphicDatatypeSort())

Missing in: Rust high-level z3 crate (z3/src/lib.rs — DatatypeBuilder has no type-parameter support)

Suggested fix: Add Context::type_variable(name: &str) -> Sort<'ctx> wrapping Z3_mk_type_variable, and extend DatatypeBuilder (or add a PolymorphicDatatypeBuilder) to accept type parameter sorts and call Z3_mk_polymorphic_datatype.

Priority: High (needed for any recursive generic data structure)

---

Medium Priority Issues

4. OCaml and Go Missing Polynomial Subresultants API

What: Z3_polynomial_subresultants(ctx, p, q, x) (in src/api/z3_polynomial.h) is not exposed in OCaml (src/api/ml/) or Go (src/api/go/).

Available in: C, C++ (polynomial_subresultants()), Python (PolynomialSubresultants()), Java, .NET, TypeScript/JS, Rust (z3-sys)

Missing in: OCaml, Go

Suggested fix (OCaml): Add val polynomial_subresultants : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr list to src/api/ml/z3.ml and z3.mli.

Suggested fix (Go): Create src/api/go/polynomial.go with func (c *Context) PolynomialSubresultants(p, q, x *Expr) []*Expr.

Priority: Medium

---

5. Go Missing MkFreshConst / MkFreshFuncDecl

What: The Go API has no wrappers for Z3_mk_fresh_const or Z3_mk_fresh_func_decl, which create uniquely-named constants and function declarations.

Available in: C, C++ (context::fresh_const(), context::fresh_func_decl()), Python (FreshConst(), FreshFunction()), Java, .NET, TypeScript/JS, OCaml, Rust (z3-sys)

Missing in: Go (src/api/go/)

Suggested fix: Add func (c *Context) MkFreshConst(prefix string, sort *Sort) *Expr and func (c *Context) MkFreshFuncDecl(prefix string, domain []*Sort, range_ *Sort) *FuncDecl to src/api/go/z3.go.

Priority: Medium

---

6. Go and Rust Missing EnableTrace / DisableTrace

What: Go exposes OpenLog, CloseLog, AppendLog but not EnableTrace / DisableTrace. The Rust high-level z3 crate exposes no logging or tracing wrappers at all (only in z3-sys).

Available in: C, C++ (enable_trace(), disable_trace()), Python, Java (Global.enableTrace()), .NET (Global.EnableTrace()), TypeScript/JS, OCaml (Log.enable_trace)

Missing in: Go (src/api/go/log.go — trace wrappers absent), Rust high-level z3 crate

Suggested fix (Go): Add func EnableTrace(tag string) and func DisableTrace(tag string) to src/api/go/log.go.

Suggested fix (Rust): Add fn enable_trace(tag: &str), fn disable_trace(tag: &str), fn open_log(path: &str) -> bool, fn close_log() as free functions in z3/src/log.rs.

Priority: Medium

---

7. Simplifier Enumeration API Missing in C++, Python, TypeScript/JS, Go, Rust

What: Z3_get_num_simplifiers(ctx), Z3_get_simplifier_name(ctx, i), and Z3_simplifier_get_descr(ctx, name) allow enumerating all available simplifiers. Present in .NET, Java, OCaml; absent elsewhere.

Available in: .NET (Context.NumSimplifiers, Context.SimplifierNames, Context.SimplifierDescription()), Java (Context.getNumSimplifiers(), etc.), OCaml (Context.get_num_simplifiers, etc.)

Missing in: C++ (z3++.h), Python (z3.py), TypeScript/JS, Go (src/api/go/simplifier.go), Rust high-level z3 crate

Suggested fix (C++): Add unsigned num_simplifiers(), symbol simplifier_name(unsigned i), and std::string simplifier_description(char const* name) to the context class.

Suggested fix (Python): Add num_simplifiers(), simplifier_names(), and simplifier_description(name) as free functions in z3.py.

Priority: Medium (tooling / documentation quality)

---

8. C++ and Rust Missing mk_type_variable Wrapper (new this run)

What: Z3_mk_type_variable creates a sort acting as a type parameter for polymorphic datatypes. C++ has no context::type_variable() wrapper — the C++ example (examples/c++/example.cpp:1016) calls Z3_mk_type_variable directly. Rust high-level z3 crate similarly lacks a wrapper (though z3-sys has the FFI binding).

Available in: Java (Context.mkTypeVariable()), .NET (Context.MkTypeVariable()), Python (TypeVarRef / Z3_mk_type_variable), TypeScript/JS (Context.TypeVariable()), OCaml (Sort.mk_type_variable, Sort.mk_type_variable_s), Go (Context.MkTypeVariable())

Missing in: C++ (z3++.h — no context::type_variable() method), Rust high-level z3 crate

Suggested fix (C++):

// in z3++.h, class context:
sort type_variable(symbol const& name) {
    Z3_sort r = Z3_mk_type_variable(*this, name);
    check_error();
    return sort(*this, r);
}
sort type_variable(char const* name) {
    return type_variable(str_symbol(name));
}

Suggested fix (Rust): Add Context::type_variable<'ctx>(&'ctx self, name: &str) -> Sort<'ctx> in z3/src/.

Priority: Medium (required to use polymorphic datatypes without raw C API calls)

---

Low Priority Issues

9. .NET Missing MkLinearOrder, MkPiecewiseLinearOrder, MkTreeOrder

What: .NET exposes only MkPartialOrder and MkTransitiveClosure from the Special Relations API. Three of the five relations are missing.

Available in: C, C++ (linear_order(), piecewise_linear_order(), tree_order()), Python, Java, TypeScript/JS, OCaml, Go, Rust (z3-sys)

Missing in: .NET (src/api/dotnet/Context.cs)

Suggested fix: Add MkLinearOrder(Sort a, uint index), MkPiecewiseLinearOrder(Sort a, uint index), MkTreeOrder(Sort a, uint index) to Context.cs.

Priority: Low

---

10. Go Missing AST.Id() Method

What: Go's AST struct has Hash() (wrapping Z3_get_ast_hash) but lacks Id() (wrapping Z3_get_ast_id).

Available in: All other languages

Missing in: Go (src/api/go/z3.go)

Suggested fix: Add func (a *AST) Id() uint { return uint(C.Z3_get_ast_id(a.ctx.ptr, a.ptr)) }.

Priority: Low

---

Methodology

All issues were verified against:

• Z3Prover/z3 at commit 59bb444
• prove-rs/z3.rs cloned fresh on 2026-06-08

No issues were found to have been resolved since the last run on 2026-06-07.

Generated by API Coherence Checker · sonnet46 4.2M · ◷

• expires on Jun 15, 2026, 5:24 AM UTC

[github-actions[bot]]

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

A newer discussion is available at Discussion #9786.