[API Coherence] Report for March 4, 2026 - BitVector, Floating-point, and Array Theory APIs

[github-actions[bot]]

Summary

This run analyzed BitVector operations, Floating-point APIs, and Array theory APIs, building on the previous analysis of Solver and Optimize APIs from February 24, 2026.

Run Statistics

• APIs analyzed in this run: BitVector operations (Z3_mk_bv_, manipulation), Floating-point APIs (Z3_mk_fpa_, Z3_fpa_), Array theory APIs (Z3_mk_select, Z3_mk_store, Z3_mk_array_, Z3_mk_map)
• New functions checked: ~80 functions across 3 API families
• Languages covered: 8 (Python, Java, .NET, C++, TypeScript, Go, OCaml, Rust)
• New inconsistencies found: 8
• Previously cached issues resolved: 5

Progress Tracker

• APIs analyzed so far: 5/~20 API families (25%)
  • ✅ Solver APIs (Z3_solver_*)
  • ✅ Optimize APIs (Z3_optimize_*)
  • ✅ BitVector operations (Z3_mk_bv_*, manipulation)
  • ✅ Floating-point APIs (Z3_mk_fpa_, Z3_fpa_)
  • ✅ Array theory APIs (Z3_mk_select, Z3_mk_store, Z3_mk_array_*, Z3_mk_map)
• Next run will analyze: Quantifier APIs, String/Sequence APIs, or Datatype APIs

Resolution Updates

The following cached issues from the February 24 run have been resolved and are no longer present in the codebase:

✅ Resolved Issues

1. TypeScript Optimize getLower()/getUpper() - RESOLVED

   • TypeScript now has getLower(index: number) and getUpper(index: number) methods in the Optimize class (lines 2388-2392 of high-level.ts)
   • Users can now retrieve optimization objective bounds in TypeScript

2. TypeScript Optimize missing fromFile(), unsatCore(), objectives(), reasonUnknown() - RESOLVED

   • All four methods are now present in TypeScript's Optimize class:
     • fromFile(filename: string) - line 2409
     • unsatCore() - line 2396
     • objectives() - line 2400-2401
     • reasonUnknown() - line 2404

3. Java Solver.addSimplifier() - RESOLVED

   • Java now has public Solver addSimplifier(Simplifier simplifier) at line 575 of Solver.java
   • Java API now supports solver simplification strategies

4. Go Solver.toDimacsString() - RESOLVED

   • Go now has toDimacsString(includeNames bool) at line 398 of solver.go
   • Go users can export SAT problems in DIMACS format

5. TypeScript Optimize.translate() - RESOLVED

   • TypeScript now has translate(target: Context) method at lines 2413-2414
   • Optimization problems can be transferred between contexts in TypeScript

High Priority Issues (New)

1. Go Missing BitVector Rotation and Repeat Operations

What: Go API lacks BitVector rotation and repeat operations
Available in: Python, Java, .NET, C++, OCaml, TypeScript
Missing in: Go
C API functions: Z3_mk_rotate_left, Z3_mk_rotate_right, Z3_mk_ext_rotate_left, Z3_mk_ext_rotate_right, Z3_mk_repeat
Impact: High - These are common operations for cryptographic and hardware verification use cases
Suggested fix: Add the following methods to bitvec.go:

• RotateLeft(n uint) *AST
• RotateRight(n uint) *AST
• ExtRotateLeft(e *AST) *AST
• ExtRotateRight(e *AST) *AST
• Repeat(n uint) *AST

Files to modify: src/api/go/bitvec.go
Verified: 2026-03-04

2. Go Missing Floating-point Operations

What: Go API lacks FPA fused multiply-add (fma), round_to_integral, and to_sbv/to_ubv conversions
Available in: Python, Java, .NET, C++, OCaml
Missing in: Go
C API functions: Z3_mk_fpa_fma, Z3_mk_fpa_round_to_integral, Z3_mk_fpa_to_sbv, Z3_mk_fpa_to_ubv
Impact: High - FMA is important for accurate floating-point computations; conversions are needed for mixed arithmetic
Suggested fix: Add the following methods to fp.go:

• FMA(rm, x, y *AST) *AST - Fused multiply-add
• RoundToIntegral(rm *AST) *AST - Round to integer value
• ToSBV(rm *AST, sz uint) *AST - Convert to signed bit-vector
• ToUBV(rm *AST, sz uint) *AST - Convert to unsigned bit-vector

Files to modify: src/api/go/fp.go
Verified: 2026-03-04

Medium Priority Issues (New)

3. Java Missing FPA to_sbv and to_ubv Conversions

What: Java lacks floating-point to signed/unsigned bit-vector conversions
Available in: Python, .NET, C++, OCaml
Missing in: Java, TypeScript, Go, Rust
C API functions: Z3_mk_fpa_to_sbv, Z3_mk_fpa_to_ubv
Suggested fix: Add methods to Context.java:

public BitVecExpr mkFPToSBV(Expr(FPRMSort) rm, Expr(FPSort) t, int sz)
public BitVecExpr mkFPToUBV(Expr(FPRMSort) rm, Expr(FPSort) t, int sz)

Files to modify: src/api/java/Context.java
Verified: 2026-03-04

4. TypeScript Missing FPA round_to_integral

What: TypeScript lacks floating-point round-to-integral operation
Available in: Python, Java, .NET, C++, OCaml
Missing in: TypeScript, Go
C API function: Z3_mk_fpa_round_to_integral
Suggested fix: Add method to high-level Float class in TypeScript:

roundToIntegral(rm: Expr(Name)): Float(Name)

Files to modify: src/api/js/src/high-level/high-level.ts
Verified: 2026-03-04

5. C# Missing MkAsArray Function

What: C# can check if an expression is an as-array (via IsAsArray property) but cannot create one
Available in: Python, Java, C++, OCaml, TypeScript, Go
Missing in: .NET
C API function: Z3_mk_as_array
Note: C# has IsAsArray property to check but no MkAsArray to create
Suggested fix: Add method to Context.cs:

public ArrayExpr(D, R) MkAsArray(D, R)(FuncDecl(R) f) where D : Sort where R : Sort

Files to modify: src/api/dotnet/Context.cs
Verified: 2026-03-04

6. Rust High-level API Missing BitVector Manipulation Methods

What: Rust z3-sys has FFI bindings for BitVector operations, but the high-level z3 crate doesn't expose them
Available in: Python, Java, .NET, C++, OCaml, TypeScript, Go (partially)
Missing in: Rust (high-level z3 crate)
Note: z3-sys has the FFI bindings (Z3_mk_concat, Z3_mk_extract, Z3_mk_rotate_*) but the high-level API doesn't expose them
Impact: Medium - Rust users must use unsafe FFI calls directly
Suggested fix: Add methods to the BV struct in the z3 crate:

• concat(&self, other: &BV) -> BV
• extract(&self, high: u32, low: u32) -> BV
• rotate_left(&self, i: u32) -> BV
• rotate_right(&self, i: u32) -> BV
• repeat(&self, i: u32) -> BV

External repository: https://github.com/prove-rs/z3.rs
Verified: 2026-03-04

Low Priority Issues (New)

7. TypeScript and Go Missing Array Map Function

What: TypeScript and Go lack the array map function (apply function to array elements)
Available in: Python, Java, .NET, C++, OCaml
Missing in: TypeScript, Go
C API function: Z3_mk_map
Suggested fix:

• TypeScript: Add map(f: FuncDecl, ...arrays: Array) method
• Go: Add Map(f *FuncDecl, arrays ...*AST) *AST function

Files to modify: src/api/js/src/high-level/high-level.ts, src/api/go/array.go
Verified: 2026-03-04

Medium Priority Issues (Continuing from Previous Run)

The following issues from the February 24 run remain unresolved (updated with current status):

8. Z3_solver_to_dimacs_string - Partial Coverage

Available in: Python, C++, TypeScript, Go ✅
Missing in: Java, .NET, OCaml, Rust
Verified: 2026-03-04

9. Z3_solver_translate - Limited Coverage

Available in: Python, Java, .NET, C++, OCaml, TypeScript
Missing in: Go, Rust
Verified: 2026-03-04

10. Z3_solver_get_proof - Limited Coverage

Available in: Python, Java, .NET, C++, OCaml, Rust
Missing in: TypeScript, Go
Verified: 2026-03-04

11. Z3_solver_add_simplifier - Good Coverage

Available in: Python, .NET, C++, OCaml, TypeScript, Java ✅
Missing in: Go, Rust
Verified: 2026-03-04

12. Z3_solver_register_on_clause - Very Limited Coverage

Available in: Python, .NET, C++
Missing in: TypeScript, Go, Java, OCaml, Rust
Verified: 2026-03-04

13. Z3_optimize_translate - Good Coverage

Available in: Python, Java, .NET, C++, TypeScript ✅
Missing in: OCaml, Go, Rust
Verified: 2026-03-04

14. Rust z3 Crate - Many Missing Solver/Optimize APIs

Missing: cube, trail, congruence, solve_for, set_initial_value, from_file, dimacs
Note: This is the high-level Rust crate (external repository: https://github.com/prove-rs/z3.rs)
Verified: 2026-03-04

15. Rust z3-sys - Missing FFI Bindings

Priority: Low (affects external crate maintainers, not Z3Prover/z3 directly)
Missing FFI bindings for: solver_to_dimacs_string, solver_add_simplifier, solver_register_on_clause, solver_congruence_*, solver_solve_for, solver_set_initial_value
Note: This is the low-level FFI crate (external repository: https://github.com/prove-rs/z3.rs)
Verified: 2026-03-04

Implementation Guidance for Maintainers

For Go API (Issues #1, #2, #7)

The Go API is missing several important operations across three API families. Recommended approach:

1. BitVector operations (High priority): Add rotation and repeat to src/api/go/bitvec.go following the pattern of existing operations like Extract and Concat
2. Floating-point operations (High priority): Add FMA and conversions to src/api/go/fp.go
3. Array map (Low priority): Add to src/api/go/array.go

All C API functions are already implemented, so this is purely adding Go wrappers.

For Java API (Issue #3)

Add mkFPToSBV and mkFPToUBV methods to Context.java. The C API functions exist (Z3_mk_fpa_to_sbv, Z3_mk_fpa_to_ubv), and the native bindings should already be in place.

For TypeScript API (Issues #4, #7)

1. Add roundToIntegral method to the Float class
2. Add map function for arrays

Both are straightforward additions following existing patterns in high-level.ts.

For C# API (Issue #5)

Add MkAsArray method to Context.cs. Note that the IsAsArray property already exists in Expr.cs, so the infrastructure is in place.

For Rust (Issues #6, #14, #15)

Note: The Rust bindings are maintained in an external repository (https://github.com/prove-rs/z3.rs). These findings should be shared with that project's maintainers.

The high-level z3 crate would benefit from exposing more BitVector manipulation methods and Solver/Optimize APIs that are already available in z3-sys.

Next Steps

The next run will analyze one or more of:

• Quantifier APIs (Z3_mk_forall, Z3_mk_exists, Z3_mk_lambda, patterns)
• String/Sequence APIs (Z3_mk_seq_, Z3_mk_str_)
• Datatype APIs (Z3_mk_datatype, Z3_mk_constructor)
• Set APIs (Z3_mk_set_, Z3_mk_finite_set_)
• Tactic/Probe APIs (Z3_mk_tactic, Z3_mk_probe, Z3_apply_result_*)

Methodology

This analysis:

1. Re-verified all cached issues from the February 24 run before reporting (5 issues found resolved)
2. Systematically checked C API baseline for each API family
3. Verified presence/absence of functions across all 8 language bindings
4. Used automated scripts to scan for function names and patterns
5. Manually verified findings with targeted grep searches
6. Only reports issues confirmed to exist in the current codebase (as of March 4, 2026)

Discussion

Feedback and corrections welcome! If any of these findings are incorrect or if there are specific API families you'd like prioritized in the next run, please comment below.

AI generated by API Coherence Checker

• expires on Mar 11, 2026, 11:25 PM UTC

[github-actions[bot]]

This discussion was automatically closed because it expired on 2026-03-11T23:25:52.360Z.

Closed by Workflow