LSP Performance Optimization

This module provides performance optimizations for real-time LSP verification:

Optimizations

1. Query Batching

• Batch multiple constraints into a single SMT query
• Use multiple (assert ...) before (check-sat)
• Reduces SMT solver startup overhead

2. Timeout Tuning

• Short timeout (500ms) for LSP interactive use
• Long timeout (5000ms) for full compilation
• Configurable per-context timeouts

3. Background Verification

• Queue verification tasks
• Process in background worker gen_server
• Return cached results immediately
• Cancel verification on file close

4. Hot Path Optimization

• Fast constraint extraction (<50ms)
• Optimized SMT-LIB generation
• AST caching to avoid re-parsing

Performance Targets

• Constraint extraction: <50ms
• SMT query (simple): <100ms
• SMT query (complex): <500ms
• Full document verification: <1s
• Cache hit rate: >80%

Architecture

LSP Request
    ↓
Fast Path: Cache Hit → Return immediately (<10ms)
    ↓
Slow Path: Cache Miss
    ↓
Background Worker: Queue task
    ↓
Batch Constraints → Single SMT Query
    ↓
Return result + Update cache