[API Coherence] API Coherence Report - January 10, 2026: Tactic, Goal, Probe & Quantifier APIs

[github-actions[bot]]

This is the fourth systematic analysis of API coherence across Z3's language bindings, focusing on Tactic APIs, Goal APIs, Probe APIs, and Quantifier APIs.

Executive Summary

APIs Analyzed: 80 C API functions across 4 major API families
Languages: C, C++, Python, Java, .NET (C#), TypeScript/JavaScript
Overall Coherence: C++, Python, Java, and C# have 100% coverage for these APIs
Critical Gap: TypeScript has severe gaps (~30% coverage), with Goal API completely missing

Key Findings

• ✅ C++, Python, Java, C#: Full, mature implementations of all analyzed APIs
• ⚠️ TypeScript: Missing critical components that make tactics system unusable
• 📊 Progress: 16/40 API families analyzed (40% complete)

---

Critical Issues Requiring Action

1. TypeScript: Missing Goal API 🚨 CRITICAL

The Goal API is completely absent from TypeScript bindings, making the entire tactics system unusable.

What's missing: All 17 Goal functions from C API

• Creation: Z3_mk_goal
• Manipulation: Z3_goal_assert, Z3_goal_reset
• Introspection: Z3_goal_size, Z3_goal_depth, Z3_goal_inconsistent
• Status checking: Z3_goal_is_decided_sat, Z3_goal_is_decided_unsat

Available in: Python ✅, Java ✅, C# ✅, C++ ✅
Missing in: TypeScript ❌

Impact: Users cannot create goals, which are the fundamental input to tactics. Even though Tactic and Probe interfaces exist, they cannot be used meaningfully.

Files to modify: src/api/js/src/high-level/types.ts, src/api/js/src/high-level/high-level.ts

---

2. TypeScript: Severely Limited Tactic API 🚨 HIGH

TypeScript has Tactic interface but is missing most methods and combinators.

Missing methods:

• ❌ apply(goal) - Cannot execute tactics
• ❌ solver() - Cannot create solver from tactic
• ❌ help() - No documentation access
• ❌ paramDescrs() - No parameter introspection

Missing combinators:

• ❌ repeat(n), tryFor(ms), when(probe), skip(), fail(), failIf(probe)
• ❌ parOr(), parAndThen() - Parallel combinators

Available: Only Tactic constructor and basic Cond() function

Comparison:

• Python: apply(), solver(), help(), param_descrs() ✅
• Java: apply(), mkSolver(), getHelp(), getParameterDescriptions() ✅
• C++: apply(), mk_solver(), help(), operators &/|, repeat(), try_for() ✅

---

3. TypeScript: Missing ApplyResult API 🚨 HIGH

No way to handle tactic application results.

Missing: All 6 ApplyResult functions

• Z3_apply_result_get_num_subgoals
• Z3_apply_result_get_subgoal
• Z3_apply_result_to_string

Impact: Even if Tactic.apply() existed, users couldn't access the resulting subgoals.

Available in: Python ✅ (ApplyResult class), Java ✅, C# ✅, C++ ✅
Missing in: TypeScript ❌

---

4. TypeScript: Incomplete Quantifier Introspection ⚠️ MEDIUM

Can create quantifiers but cannot inspect them programmatically.

Available:

• ✅ ForAll(), Exists() - Creation works
• ✅ var_name(idx), var_sort(idx) - Basic introspection (found in tests)

Missing introspection:

• ❌ isForall(), isExists() - Type checking
• ❌ weight() - Quantifier weight
• ❌ numPatterns(), pattern(i) - Pattern access
• ❌ body() - Body extraction
• ❌ qid(), skolemId() - Identifiers

Available in other languages:

• Python: Full introspection via QuantifierRef methods ✅
• Java: Quantifier class with all methods ✅
• C#: Quantifier class with properties ✅
• C++: Methods on expr class ✅

---

Detailed Statistics

Coverage by Language (for analyzed APIs)

Language	Tactic	Goal	Probe	Quantifier	Overall
C++	100% ✅	100% ✅	100% ✅	100% ✅	100%
Python	100% ✅	100% ✅	100% ✅	100% ✅	100%
Java	100% ✅	100% ✅	100% ✅	100% ✅	100%
C#	100% ✅	100% ✅	100% ✅	100% ✅	100%
TypeScript	30% ⚠️	0% ❌	40% ⚠️	60% ⚠️	~30%

API Functions Analyzed

• Tactic APIs: 28 functions (creation, combinators, introspection)
• Goal APIs: 17 functions (creation, manipulation, status)
• Probe APIs: 18 functions (creation, comparisons, application)
• Quantifier APIs: 17 functions (creation, introspection)
• Total: 80 C API functions

Issue Breakdown

• Critical: 3 issues (Goal missing, Tactic incomplete, ApplyResult missing)
• High: 4 issues
• Medium: 2 issues (naming inconsistency, probe methods)
• Low: 1 issue (enumeration APIs)

---

Progress Tracking

Cumulative Analysis

Completed: 16 / ~40 API families (40%)

Analyzed so far:

1. Solver APIs ✅
2. Model APIs ✅
3. Context APIs ✅
4. Array Theory APIs ✅
5. BitVector Operations ✅
6. Arithmetic Theory APIs ✅
7. Floating-Point APIs ✅
8. String/Sequence APIs ✅
9. Optimize APIs ✅
10. Datatype APIs ✅
11. Set Theory APIs ✅
12. Proof/Unsat Core APIs ✅
13. Fixedpoint APIs ✅
14. Tactic APIs ✅ (NEW)
15. Goal APIs ✅ (NEW)
16. Probe APIs ✅ (NEW)
17. Quantifier APIs ✅ (NEW)

Next priorities:

• AST Map APIs
• Parameter/ParamDescrs APIs
• Simplifier APIs
• Polynomial APIs
• Special Relations APIs

---

Recommendations

For TypeScript Maintainers (Priority Order)

Critical (Blocks major functionality)

1. Add Goal API - Create Goal interface with all 17 methods
2. Add ApplyResult API - Handle tactic application results
3. Add Tactic.apply() - Make tactics actually usable

High (Significantly limits usability)

4. Add Tactic.solver() - Create solvers from tactics
5. Add tactic combinators - repeat(), tryFor(), when(), skip(), fail()
6. Add Tactic introspection - help(), paramDescrs()

Medium (Improves experience)

7. Add Probe.apply() and probe constructors
8. Add quantifier introspection - isForall(), weight(), pattern(), body()

For All Language Maintainers

• Consider standardizing tactic combinator naming across languages for better consistency

---

File References

Key Files Analyzed

C API Baseline:

• src/api/z3_api.h lines 6224-6818 (Tactic/Goal/Probe/ApplyResult)
• src/api/z3_api.h lines 4265-5406 (Quantifiers)

Python (Complete ✅):

• src/api/python/z3/z3.py lines 5694-5970 (Goal, ApplyResult, Tactic)
• src/api/python/z3/z3.py lines 8470-8900 (Tactic, Probe)
• src/api/python/z3/z3.py lines 2095-2342 (Quantifiers)

Java (Complete ✅):

• src/api/java/Goal.java, Tactic.java, Probe.java, ApplyResult.java, Quantifier.java

C# (Complete ✅):

• src/api/dotnet/Goal.cs, Tactic.cs, Probe.cs, ApplyResult.cs, Quantifier.cs

C++ (Complete ✅):

• src/api/c++/z3++.h lines 3067-3360 (goal, tactic, probe, apply_result classes)
• src/api/c++/z3++.h lines 2350-2397 (quantifier functions)

TypeScript (Incomplete ⚠️):

• src/api/js/src/high-level/types.ts lines 2120-2173 (Tactic/Probe/Quantifier interfaces)
• src/api/js/src/high-level/high-level.ts lines 1091-1122, 2204-2213 (implementations)
• Missing: Goal, ApplyResult interfaces entirely

---

Conclusion

The analysis reveals that TypeScript bindings lag significantly behind other languages in the tactics subsystem. The Goal API is completely missing, making tactics unusable despite having basic Tactic and Probe interfaces.

C++, Python, Java, and C# all provide complete, mature implementations. The TypeScript gaps represent a significant usability issue for JavaScript/TypeScript users who want to use Z3's powerful tactic-based solving framework.

Next analysis: Will cover AST Map, Parameter management, Simplifier, and Polynomial APIs.

---

This is an automated analysis. For detailed findings, see cached report at /tmp/gh-aw/cache-memory/findings_2026-01-10.md.

AI generated by API Coherence Checker