You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This is run #15 of the API Coherence Checker. All 24 API families have now been analyzed (100% of the known C API surface). This run focuses on re-verification of all cached open issues to ensure they remain unresolved.
APIs analyzed total: 24 API families (~200+ C functions)
Previously cached issues re-verified: 22 open issues — all confirmed still open
Issues resolved since last run: 0
New issues found: 0 (full surface covered)
Progress
APIs analyzed so far: 24/~24 (100%) — complete coverage of current C API surface
Monitoring: Future runs will monitor new C API additions in src/api/z3_api.h
Next areas: Track upstream changes; monitor prove-rs/z3.rs for Fixedpoint, UserPropagator, and Seq additions
High Priority Issues
1. Z3_enable_concurrent_dec_ref Missing in Python, Java, Go, C++ (z3++.h), TypeScript, Rust
What: Thread-safe reference counting API needed for multi-threaded Z3 usage. Only exposed in .NET (Context.enableConcurrentDecRef()) and OCaml. Available in: .NET, OCaml Missing in: Python, Java, TypeScript, Go, C++ (z3++.h), Rust (high-level) Fix: Add enable_concurrent_dec_ref() method to Context wrappers in each binding. The C API function is Z3_enable_concurrent_dec_ref(ctx). Priority: High — required for safe multi-threaded usage
2. User Propagator API Missing in TypeScript, OCaml, Rust (high-level)
What: The Z3_solver_propagate_* family (12 functions) enables custom theory propagation. Entirely absent in TypeScript/JS, OCaml, and the high-level Rust z3 crate. The Rust z3-sys crate has FFI bindings but no high-level wrappers. Available in: Python (UserPropagator class), Java (UserPropagator class), .NET (UserPropagator class), Go (UserPropagator struct) Missing in: TypeScript/JS (no UserPropagator class), OCaml (no z3native.ml.pre bindings), Rust (no high-level wrapper despite z3-sys having FFI) Fix:
TypeScript: Add UserPropagator class to src/api/js/src/high-level/
OCaml: Add Z3_solver_propagate_* bindings to z3native.ml.pre and a high-level module
Rust: Add UserPropagator struct wrapping z3-sys FFI in z3/src/ Priority: High — enables custom theory integration
3. Pseudo-Boolean / Cardinality APIs Missing in Go and OCaml
What: Z3_mk_atmost, Z3_mk_atleast, Z3_mk_pble, Z3_mk_pbge, Z3_mk_pbeq — five functions for cardinality/pseudo-Boolean constraints. Entirely absent in Go and OCaml. Available in: C, Java (mkAtMost, mkAtLeast, mkPBLe, mkPBGe, mkPBEq), .NET (MkAtMost, MkAtLeast, MkPBLe, MkPBGe, MkPBEq), Python (AtMost, AtLeast, PbLe, PbGe, PbEq), TypeScript, C++, Rust Missing in: Go (no functions in any src/api/go/*.go file), OCaml (no bindings in z3native.ml.pre or z3.mli) Fix:
Go: Add MkAtMost, MkAtLeast, MkPBLe, MkPBGe, MkPBEq to src/api/go/z3.go
OCaml: Add mk_atmost, mk_atleast, mk_pble, mk_pbge, mk_pbeq to z3native.ml.pre and Boolean module in z3.mli Priority: High — commonly used in verification and planning problems
Medium Priority Issues
4. Z3_mk_type_variable Missing in .NET, TypeScript, C++ (z3++.h), Rust
What: Type variable support for polymorphic sorts. Java (mkTypeVariable), Python (Type), OCaml, and Go expose this but four languages do not. Available in: Java, Python, OCaml, Go Missing in: .NET, TypeScript, C++ (z3++.h), Rust Fix: Add wrappers calling Z3_mk_type_variable(ctx, name) in each missing binding. Priority: Medium
5. Z3_mk_polymorphic_datatype Missing in Python, .NET, TypeScript, Go, Rust
What: Creating polymorphic recursive datatypes. Only Java, OCaml, and C++ (z3++.h) expose this. Available in: Java (mkPolymorphicDatatype), OCaml, C++ (z3++.h) Missing in: Python, .NET, TypeScript, Go, Rust Fix: Add wrappers in each missing binding's datatype construction API. Priority: Medium
6. Special Relations API — Partial Gaps in Java, .NET, TypeScript; Full Gap in OCaml and Go
What: Five special relations functions: Z3_mk_linear_order, Z3_mk_partial_order, Z3_mk_piecewise_linear_order, Z3_mk_tree_order, Z3_mk_transitive_closure.
Available in: C (all 5), Python (all 5), C++ (all 5), Rust (all 5 via func_decl.rs) Fix: Complete the implementations in each binding. Priority: Medium
7. Incremental Parser Context API Missing in Java, .NET, Go, TypeScript, Rust, OCaml
What: Z3_parser_context_* functions (add_sort, add_decl, from_string) enable incremental SMTLIB2 parsing with custom sorts/decls. Only Python exposes these. Available in: Python (ParserContext class in z3.py) Missing in: Java, .NET, Go, TypeScript, Rust, OCaml Note: Java, TypeScript have parseSmtlib2String (one-shot parsing) but not the incremental context API Fix: Add ParserContext wrapper classes in each missing binding. Priority: Medium
8. Go Missing SetGlobalParam / GetGlobalParam / ResetAllGlobalParams
What: Global parameter configuration functions (Z3_global_param_set, Z3_global_param_get, Z3_global_param_reset_all). Not exposed in Go. Available in: Python, Java, .NET, TypeScript, OCaml, Rust Missing in: Go Fix: Add SetGlobalParam(id, value string), GetGlobalParam(id string) (string, bool), ResetAllGlobalParams() to src/api/go/z3.go. Priority: Medium
9. Go Missing Standalone parse_smtlib2_string / parse_smtlib2_file (ASTVector return)
What: Go only has Solver.FromString which uses Z3_solver_from_string (directly asserts). The standalone parsing API returning an ASTVector (Z3_parse_smtlib2_string, Z3_parse_smtlib2_file) is missing. Available in: Python, Java, .NET, TypeScript, OCaml, Rust (z3-sys) Missing in: Go, Rust (high-level) Fix: Add ParseSmtlib2String(s string) ASTVector and ParseSmtlib2File(path string) ASTVector to src/api/go/z3.go. Priority: Medium
10. Rust High-Level z3 Crate Missing Several Solver APIs
What: The following Solver methods exist in other languages but not in the Rust high-level z3 crate:
Available in: Python, Java, .NET, C++, OCaml, Go, TypeScript Missing in: Rust (z3 crate) Priority: Medium
11. Rust High-Level Missing Many Seq/String Operations
What: Rust z3/src/ast/seq.rs only exposes at, nth, length, contains. Missing: replace, replace_all, replace_re, replace_re_all, is_prefix, is_suffix, index, last_index, map, mapi, foldl, foldli. All these have FFI bindings in z3-sys. Available in: Python, Java, .NET, C++, OCaml, Go, TypeScript Missing in: Rust (high-level) Priority: Medium
12. Rust High-Level Missing Algebraic Number Operations
What: Rust z3/src/ast/ is missing from the Algebraic API: le, ge, neq comparison, roots, eval. The z3-sys crate has these FFI bindings. Available in: Python (AlgebraicNumRef), C++, OCaml (partial) Missing in: Rust (le/ge/neq/roots/eval), Go, Java, .NET, TypeScript Priority: Medium
13. Rust High-Level Missing Entire Fixedpoint API
What: No Fixedpoint struct in the z3 crate. All Fixedpoint/Datalog reasoning APIs are absent. Available in: Python (Fixedpoint), Java (Fixedpoint), .NET (Fixedpoint), C++ (fixedpoint), OCaml (Fixedpoint), Go (Fixedpoint), TypeScript Missing in: Rust (high-level z3 crate) Priority: Medium
14. Go Missing Entire RCF (Real Closed Field) API
What: None of the ~37 Z3_rcf_* functions are exposed in Go. The RCF API provides exact arithmetic over real closed fields with algebraic, infinitesimal, and transcendental numbers. Available in: C (all), Java (partial), .NET (partial), C++ (partial), OCaml (full), TypeScript (partial) Missing in: Go (entirely), Python (uses AlgebraicNumRef instead), Rust (high-level) Priority: Medium
15. Rust z3-sys Missing 14 of 37 Z3_rcf_* Functions
What: z3-sys is missing FFI bindings for: Z3_rcf_is_rational, Z3_rcf_is_algebraic, Z3_rcf_is_infinitesimal, Z3_rcf_is_transcendental, Z3_rcf_extension_index, Z3_rcf_transcendental_name, Z3_rcf_infinitesimal_name, Z3_rcf_num_coefficients, Z3_rcf_coefficient, Z3_rcf_interval, Z3_rcf_num_sign_conditions, Z3_rcf_sign_condition_sign, Z3_rcf_num_sign_condition_coefficients, Z3_rcf_sign_condition_coefficient. Available in: C API (src/api/z3_rcf.h) Missing in: z3-sys crate (14 functions absent) Priority: Medium
Low Priority Issues
16. Rust z3 Crate Missing BV::repeat
What: Z3_mk_repeat has a FFI binding in z3-sys but is not exposed as pub fn repeat in z3/src/ast/bv.rs. Available in: Python, C++, Java, .NET, OCaml, TypeScript, Go Missing in: Rust (high-level) Priority: Low
What: par_or (parallel OR of tactics) and par_and_then (parallel AND-THEN) are absent in Rust's Tactic wrapper. Available in: Python, Java, .NET, C++, OCaml, Go, TypeScript Missing in: Rust Priority: Low
18. OCaml Algebraic Numbers — Only to_upper / to_lower Exposed
What: Arithmetic.AlgebraicNumber in OCaml only exposes interval bounds. All arithmetic operations (add, sub, mul, div, root, power) and comparisons (lt, gt, eq, neq) are absent from the OCaml high-level API. Available in: Python (AlgebraicNumRef), Rust, C++ Missing in: OCaml Priority: Low
19. Advanced RCF Inspection APIs — Only in OCaml
What: extension_index, transcendental_name, infinitesimal_name, num_coefficients, coefficient, interval, and sign condition queries. Only OCaml exposes these via full Z3_rcf_* bindings. Available in: OCaml (full C API coverage) Missing in: Java, .NET, C++, TypeScript Priority: Low
5 (PB, Special Relations, Global Params, ParseSmtlib2, RCF)
OCaml
4 (Propagator, PB, Special Relations, Algebraic Numbers)
TypeScript
3 (Propagator, Type Variable, Special Relations)
.NET
2 (Type Variable, Special Relations partial)
Java
2 (concurrent_dec_ref, Special Relations partial)
Python
1 (concurrent_dec_ref)
C++ (z3++.h)
2 (concurrent_dec_ref, Type Variable)
Notes for Maintainers
The Rust z3 crate (prove-rs/z3.rs) is an external repository and these findings should ideally be reported as issues there.
The User Propagator API is particularly valuable for researchers building custom theory solvers — extending TypeScript and OCaml bindings would broaden accessibility.
Pseudo-Boolean constraints in Go and OCaml would benefit optimization/planning users on those platforms.
Concurrent dec ref is important for any multi-threaded application; the missing bindings represent a correctness hazard.
reacted with thumbs up emoji reacted with thumbs down emoji reacted with laugh emoji reacted with hooray emoji reacted with confused emoji reacted with heart emoji reacted with rocket emoji reacted with eyes emoji
Uh oh!
There was an error while loading. Please reload this page.
-
Summary
This is run #15 of the API Coherence Checker. All 24 API families have now been analyzed (100% of the known C API surface). This run focuses on re-verification of all cached open issues to ensure they remain unresolved.
Progress
src/api/z3_api.hHigh Priority Issues
1.
Z3_enable_concurrent_dec_refMissing in Python, Java, Go, C++ (z3++.h), TypeScript, RustWhat: Thread-safe reference counting API needed for multi-threaded Z3 usage. Only exposed in .NET (
Context.enableConcurrentDecRef()) and OCaml.Available in: .NET, OCaml
Missing in: Python, Java, TypeScript, Go, C++ (
z3++.h), Rust (high-level)Fix: Add
enable_concurrent_dec_ref()method to Context wrappers in each binding. The C API function isZ3_enable_concurrent_dec_ref(ctx).Priority: High — required for safe multi-threaded usage
2. User Propagator API Missing in TypeScript, OCaml, Rust (high-level)
What: The
Z3_solver_propagate_*family (12 functions) enables custom theory propagation. Entirely absent in TypeScript/JS, OCaml, and the high-level Rustz3crate. The Rustz3-syscrate has FFI bindings but no high-level wrappers.Available in: Python (
UserPropagatorclass), Java (UserPropagatorclass), .NET (UserPropagatorclass), Go (UserPropagatorstruct)Missing in: TypeScript/JS (no
UserPropagatorclass), OCaml (noz3native.ml.prebindings), Rust (no high-level wrapper despitez3-syshaving FFI)Fix:
UserPropagatorclass tosrc/api/js/src/high-level/Z3_solver_propagate_*bindings toz3native.ml.preand a high-level moduleUserPropagatorstruct wrappingz3-sysFFI inz3/src/Priority: High — enables custom theory integration
3. Pseudo-Boolean / Cardinality APIs Missing in Go and OCaml
What:
Z3_mk_atmost,Z3_mk_atleast,Z3_mk_pble,Z3_mk_pbge,Z3_mk_pbeq— five functions for cardinality/pseudo-Boolean constraints. Entirely absent in Go and OCaml.Available in: C, Java (
mkAtMost,mkAtLeast,mkPBLe,mkPBGe,mkPBEq), .NET (MkAtMost,MkAtLeast,MkPBLe,MkPBGe,MkPBEq), Python (AtMost,AtLeast,PbLe,PbGe,PbEq), TypeScript, C++, RustMissing in: Go (no functions in any
src/api/go/*.gofile), OCaml (no bindings inz3native.ml.preorz3.mli)Fix:
MkAtMost,MkAtLeast,MkPBLe,MkPBGe,MkPBEqtosrc/api/go/z3.gomk_atmost,mk_atleast,mk_pble,mk_pbge,mk_pbeqtoz3native.ml.preand Boolean module inz3.mliPriority: High — commonly used in verification and planning problems
Medium Priority Issues
4.
Z3_mk_type_variableMissing in .NET, TypeScript, C++ (z3++.h), RustWhat: Type variable support for polymorphic sorts. Java (
mkTypeVariable), Python (Type), OCaml, and Go expose this but four languages do not.Available in: Java, Python, OCaml, Go
Missing in: .NET, TypeScript, C++ (
z3++.h), RustFix: Add wrappers calling
Z3_mk_type_variable(ctx, name)in each missing binding.Priority: Medium
5.
Z3_mk_polymorphic_datatypeMissing in Python, .NET, TypeScript, Go, RustWhat: Creating polymorphic recursive datatypes. Only Java, OCaml, and C++ (
z3++.h) expose this.Available in: Java (
mkPolymorphicDatatype), OCaml, C++ (z3++.h)Missing in: Python, .NET, TypeScript, Go, Rust
Fix: Add wrappers in each missing binding's datatype construction API.
Priority: Medium
6. Special Relations API — Partial Gaps in Java, .NET, TypeScript; Full Gap in OCaml and Go
What: Five special relations functions:
Z3_mk_linear_order,Z3_mk_partial_order,Z3_mk_piecewise_linear_order,Z3_mk_tree_order,Z3_mk_transitive_closure.mkTreeOrder,mkPiecewiseLinearOrder(has 3/5)MkLinearOrder,MkTreeOrder,MkPiecewiseLinearOrder(has 2/5)linearOrder,treeOrder,piecewiseLinearOrder(has 2/5)Available in: C (all 5), Python (all 5), C++ (all 5), Rust (all 5 via
func_decl.rs)Fix: Complete the implementations in each binding.
Priority: Medium
7. Incremental Parser Context API Missing in Java, .NET, Go, TypeScript, Rust, OCaml
What:
Z3_parser_context_*functions (add_sort, add_decl, from_string) enable incremental SMTLIB2 parsing with custom sorts/decls. Only Python exposes these.Available in: Python (
ParserContextclass inz3.py)Missing in: Java, .NET, Go, TypeScript, Rust, OCaml
Note: Java, TypeScript have
parseSmtlib2String(one-shot parsing) but not the incremental context APIFix: Add
ParserContextwrapper classes in each missing binding.Priority: Medium
8. Go Missing
SetGlobalParam/GetGlobalParam/ResetAllGlobalParamsWhat: Global parameter configuration functions (
Z3_global_param_set,Z3_global_param_get,Z3_global_param_reset_all). Not exposed in Go.Available in: Python, Java, .NET, TypeScript, OCaml, Rust
Missing in: Go
Fix: Add
SetGlobalParam(id, value string),GetGlobalParam(id string) (string, bool),ResetAllGlobalParams()tosrc/api/go/z3.go.Priority: Medium
9. Go Missing Standalone
parse_smtlib2_string/parse_smtlib2_file(ASTVector return)What: Go only has
Solver.FromStringwhich usesZ3_solver_from_string(directly asserts). The standalone parsing API returning anASTVector(Z3_parse_smtlib2_string,Z3_parse_smtlib2_file) is missing.Available in: Python, Java, .NET, TypeScript, OCaml, Rust (z3-sys)
Missing in: Go, Rust (high-level)
Fix: Add
ParseSmtlib2String(s string) ASTVectorandParseSmtlib2File(path string) ASTVectortosrc/api/go/z3.go.Priority: Medium
10. Rust High-Level
z3Crate Missing Several Solver APIsWhat: The following Solver methods exist in other languages but not in the Rust high-level
z3crate:cube/get_trail— incremental solving assistancecongruence_root,congruence_next— congruence closure queriesset_initial_value— hint initializationadd_simplifier— pluggable simplifierregister_on_clause— clause registration callbackto_dimacs_string— DIMACS exportAvailable in: Python, Java, .NET, C++, OCaml, Go, TypeScript
Missing in: Rust (
z3crate)Priority: Medium
11. Rust High-Level Missing Many Seq/String Operations
What: Rust
z3/src/ast/seq.rsonly exposesat,nth,length,contains. Missing:replace,replace_all,replace_re,replace_re_all,is_prefix,is_suffix,index,last_index,map,mapi,foldl,foldli. All these have FFI bindings inz3-sys.Available in: Python, Java, .NET, C++, OCaml, Go, TypeScript
Missing in: Rust (high-level)
Priority: Medium
12. Rust High-Level Missing Algebraic Number Operations
What: Rust
z3/src/ast/is missing from the Algebraic API:le,ge,neqcomparison,roots,eval. Thez3-syscrate has these FFI bindings.Available in: Python (
AlgebraicNumRef), C++, OCaml (partial)Missing in: Rust (
le/ge/neq/roots/eval), Go, Java, .NET, TypeScriptPriority: Medium
13. Rust High-Level Missing Entire Fixedpoint API
What: No
Fixedpointstruct in thez3crate. All Fixedpoint/Datalog reasoning APIs are absent.Available in: Python (
Fixedpoint), Java (Fixedpoint), .NET (Fixedpoint), C++ (fixedpoint), OCaml (Fixedpoint), Go (Fixedpoint), TypeScriptMissing in: Rust (high-level
z3crate)Priority: Medium
14. Go Missing Entire RCF (Real Closed Field) API
What: None of the ~37
Z3_rcf_*functions are exposed in Go. The RCF API provides exact arithmetic over real closed fields with algebraic, infinitesimal, and transcendental numbers.Available in: C (all), Java (partial), .NET (partial), C++ (partial), OCaml (full), TypeScript (partial)
Missing in: Go (entirely), Python (uses
AlgebraicNumRefinstead), Rust (high-level)Priority: Medium
15. Rust
z3-sysMissing 14 of 37Z3_rcf_*FunctionsWhat:
z3-sysis missing FFI bindings for:Z3_rcf_is_rational,Z3_rcf_is_algebraic,Z3_rcf_is_infinitesimal,Z3_rcf_is_transcendental,Z3_rcf_extension_index,Z3_rcf_transcendental_name,Z3_rcf_infinitesimal_name,Z3_rcf_num_coefficients,Z3_rcf_coefficient,Z3_rcf_interval,Z3_rcf_num_sign_conditions,Z3_rcf_sign_condition_sign,Z3_rcf_num_sign_condition_coefficients,Z3_rcf_sign_condition_coefficient.Available in: C API (
src/api/z3_rcf.h)Missing in:
z3-syscrate (14 functions absent)Priority: Medium
Low Priority Issues
16. Rust
z3Crate MissingBV::repeatWhat:
Z3_mk_repeathas a FFI binding inz3-sysbut is not exposed aspub fn repeatinz3/src/ast/bv.rs.Available in: Python, C++, Java, .NET, OCaml, TypeScript, Go
Missing in: Rust (high-level)
Priority: Low
17. Rust
z3Crate Missing Parallel Tactic CombinatorsWhat:
par_or(parallel OR of tactics) andpar_and_then(parallel AND-THEN) are absent in Rust's Tactic wrapper.Available in: Python, Java, .NET, C++, OCaml, Go, TypeScript
Missing in: Rust
Priority: Low
18. OCaml Algebraic Numbers — Only
to_upper/to_lowerExposedWhat:
Arithmetic.AlgebraicNumberin OCaml only exposes interval bounds. All arithmetic operations (add, sub, mul, div, root, power) and comparisons (lt, gt, eq, neq) are absent from the OCaml high-level API.Available in: Python (
AlgebraicNumRef), Rust, C++Missing in: OCaml
Priority: Low
19. Advanced RCF Inspection APIs — Only in OCaml
What:
extension_index,transcendental_name,infinitesimal_name,num_coefficients,coefficient,interval, and sign condition queries. Only OCaml exposes these via fullZ3_rcf_*bindings.Available in: OCaml (full C API coverage)
Missing in: Java, .NET, C++, TypeScript
Priority: Low
Statistics
z3++.h)Notes for Maintainers
z3crate (prove-rs/z3.rs) is an external repository and these findings should ideally be reported as issues there.Beta Was this translation helpful? Give feedback.
All reactions