View Source cure_lsp_smt (cure v0.7.0)

Summary

Functions

check_exhaustiveness(Match_expr)

Check pattern match exhaustiveness

extract_type_constraints(AST)

Extract type constraints from AST

get_cache_stats(Verification_state)

Get cache statistics

init_verification_state()

Initialize verification state with default settings

init_verification_state(Opts)

Initialize verification state with options Options: - solver_type: z3 | cvc5 (default: z3) - timeout: timeout in ms (default: 500) - persistent: keep solver alive (default: true)

invalidate_cache_region(Uri, StartLine, EndLine, Verification_state)

Invalidate cache for a specific region of a document

verify_refinement_types(AST)

Verify refinement types in AST

Functions

check_exhaustiveness(Match_expr)

Check pattern match exhaustiveness

extract_type_constraints(AST)

Extract type constraints from AST

get_cache_stats(Verification_state)

Get cache statistics

init_verification_state()

Initialize verification state with default settings

init_verification_state(Opts)

Initialize verification state with options Options: - solver_type: z3 | cvc5 (default: z3) - timeout: timeout in ms (default: 500) - persistent: keep solver alive (default: true)

invalidate_cache_region(Uri, StartLine, EndLine, Verification_state)

Invalidate cache for a specific region of a document

verify_refinement_types(AST)

Verify refinement types in AST