[API Coherence] API Coherence Report - January 12, 2026 (Run 9: Memory, Printing, Conversions, Overflow, PB-SAT)

[github-actions[bot]]

Progress: 36/40 API families analyzed (90% complete)

Summary

Run 9 analyzed 26 functions across 5 API families:

• Memory Management (3 functions)
• Pretty Printing/Formatting (6 functions)
• Type Conversion (5 functions)
• Overflow/Underflow Predicates (7 functions)
• Pseudo-Boolean Constraints (5 functions)

Key Findings

✅ Excellent coherence (100%) in 4 out of 5 families:

• Memory Management: All languages use automatic memory management (Python/Java/TypeScript: GC, C#: GC + thread-safety, C++: RAII)
• Type Conversion: All Int↔Real, Int↔BV, BV↔Int conversions present in all languages
• Overflow/Underflow: All 7 predicates (add/sub/mul/neg) present in all languages
• PB-SAT Constraints: All 5 functions (AtMost, AtLeast, PbLe, PbGe, PbEq) present in all languages

⚠️ Good coherence (75%) in 1 family:

• Pretty Printing: Missing print mode control in Python, C#, TypeScript

Issues Found (3 new)

🔴 High Priority (1 new)

Missing set_ast_print_mode() in Python, C#, TypeScript

• Available in: Java (explicit), C++ (automatic SMT-LIB2)
• Missing in: Python, C#, TypeScript
• Impact: Users cannot control AST output format (SMT-LIB2 vs SMT-LIB1 vs low-level)
• Use cases: Debugging, format compatibility
• Suggested fix: Add wrapper functions to set print mode

🟡 Medium Priority (1 new)

Missing benchmark_to_smtlib_string() in all languages

• Available in: C API only
• Missing in: Python, Java, C#, C++, TypeScript (all 5 languages)
• Impact: Cannot export complete problem as SMTLIB2 benchmark file
• Use cases: Bug reporting, benchmarking, solver comparison
• Workaround: Manually print formulas (not ideal)

⚪ Low Priority (1 new)

Missing pattern_to_string() wrappers

• Missing in: All languages
• Impact: Very low - patterns automatically printed within quantifiers

---

Detailed Analysis

1. Memory Management APIs ✅ 100% Coherent

Assessment: Each language uses appropriate automatic memory management. Manual reference counting (Z3_inc_ref/Z3_dec_ref) is correctly NOT exposed to users.

Language-specific implementations:

• Python/Java/TypeScript: Garbage collection
• C#: GC + automatically enables thread-safe reference counting
• C++: RAII with smart pointer semantics

Verdict: Exemplary design. No changes needed.

---

2. Pretty Printing APIs ⚠️ 75% Coherent

Core printing (toString/str) - ✅ Complete:
All languages provide string conversion for ASTs, sorts, and function declarations via toString() / __str__() methods.

Print mode control - ❌ Gaps:

• ✅ Java: Has Context.setAstPrintMode() - can switch between formats
• ✅ C++: Automatically sets SMT-LIB2 compliant mode
• ❌ Python: No wrapper for Z3_set_ast_print_mode
• ❌ C#: No wrapper for Z3_set_ast_print_mode
• ❌ TypeScript: No wrapper for Z3_set_ast_print_mode

Benchmark export - ❌ Missing everywhere:
Z3_benchmark_to_smtlib_string not exposed in any language binding.

Recommendation:

1. Add print mode control to Python, C#, TypeScript (high priority)
2. Consider adding benchmark export (medium priority)

---

3. Type Conversion APIs ✅ 100% Coherent

All languages provide complete support for:

• Int2Real / Real2Int - Integer ↔ Real conversion
• Int2BV / BV2Int - Integer ↔ Bit-vector conversion
• IntToStr - Integer → String conversion

Each language uses appropriate idioms (global functions, context methods, or automatic coercion).

Verdict: Perfect coherence across all 5 languages.

---

4. Overflow/Underflow Predicates ✅ 100% Coherent

All 7 overflow/underflow predicates present in all languages:

• bvadd_no_overflow / bvadd_no_underflow
• bvsub_no_overflow / bvsub_no_underflow
• bvmul_no_overflow / bvmul_no_underflow
• bvneg_no_overflow

TypeScript stands out with the most ergonomic API - these are methods on BitVec objects (e.g., bv.addNoOverflow(other, isSigned)) rather than global functions.

Verdict: Exemplary API consistency.

---

5. Pseudo-Boolean Constraint APIs ✅ 100% Coherent

All 5 PB-SAT functions present in all languages:

• AtMost / AtLeast - Cardinality constraints
• PbLe / PbGe / PbEq - Weighted pseudo-boolean constraints

Each language uses appropriate parameter types:

• Python: Pythonic tuple syntax
• Java/C#: Array parameters
• C++: expr_vector for efficiency
• TypeScript: Typed tuple arrays for compile-time safety

Verdict: Perfect coherence with language-appropriate syntax.

---

Cumulative Progress (Runs 1-9)

Language Rankings (36/40 families analyzed)

1. Java: 34/36 APIs (94.4%) ⭐⭐⭐ Excellent

   • Has: set_ast_print_mode ✅

2. C++: 34/36 APIs (94.4%) ⭐⭐⭐ Excellent

   • Has: Automatic SMT-LIB2 print mode ✅

3. Python: 33/36 APIs (91.7%) ⭐⭐⭐ Excellent

4. C#: 33/36 APIs (91.7%) ⭐⭐ Very Good

   • Unique: Auto thread-safe reference counting ✅

5. TypeScript: 21/36 APIs (58.3%) ⚠️⚠️ Major Gaps

   • Missing entire theory APIs (FPA, String, Fixedpoint from previous runs)

6. Julia: 0/36 (0%) ❌ External package

Total Issues Tracked: 30

• Critical: 7 (TypeScript theory gaps, RCF/Polynomial missing)
• High: 8 (including 1 new: print mode control)
• Medium: 8 (including 1 new: benchmark export)
• Low: 7 (including 1 new: pattern_to_string)

---

Next Run: Final Sprint to 100%

Remaining API families (4):

1. Deprecated/Legacy APIs
2. Advanced Tactic Combinators (AndThen, OrElse, Repeat, TryFor)
3. Advanced AST Introspection (get_ast_kind, get_decl_kind)
4. Error Handling APIs (error codes, messages, handlers)

Run 10 will achieve 100% API coverage.

---

Recommendations

Immediate Actions (High Priority)

Add print mode control to Python, C#, TypeScript:

Python:

Z3_PRINT_SMTLIB_FULL = 0
Z3_PRINT_LOW_LEVEL = 1
Z3_PRINT_SMTLIB2_COMPLIANT = 2

def set_ast_print_mode(ctx, mode):
    Z3_set_ast_print_mode(ctx.ref(), mode)

C#:

public void SetAstPrintMode(Z3_ast_print_mode mode) {
    Native.Z3_set_ast_print_mode(NativeObject, (uint)mode);
}

TypeScript:

setPrintMode(mode: 'smtlib' | 'smtlib2' | 'low-level'): void {
    const modeMap = { 'smtlib': 0, 'smtlib2': 2, 'low-level': 1 };
    Z3.set_ast_print_mode(this.ptr, modeMap[mode]);
}

Benefit: Better debugging, format control for compatibility
Effort: Low (simple wrapper functions)

Consider (Medium Priority)

Add benchmark export functionality:

• Solver.to_smtlib2() / ToSmtlib2String() / toSmtlib2() methods
• Useful for bug reporting and benchmarking
• Workaround exists (manual printing) but not ideal

---

Positive Highlights

🎉 Memory management is exemplary - Each language uses best practices appropriate to its runtime

🎉 Type conversions are perfect - All conversions consistently available

🎉 Overflow predicates are outstanding - Complete coverage with TypeScript showing best-practice object methods

🎉 PB-SAT constraints are complete - All pseudo-boolean functions properly exposed with type-appropriate syntax

---

Files for Reference

Python: src/api/python/z3/z3.py
Java: src/api/java/Context.java
C#: src/api/dotnet/Context.cs, src/api/dotnet/AST.cs
C++: src/api/c++/z3++.h
TypeScript: src/api/js/src/high-level/high-level.ts, src/api/js/src/high-level/types.ts

AI generated by API Coherence Checker