Modules
Top-level facade for Semantic IR formal verification, dead branch analysis, counter-example model parsing, and automated self-healing.
Encodes Semantic IR constraints, axioms, and branch criteria into SMT-LIB2 s-expressions.
Standardized struct representing formal verification violations found by Z3. Includes concrete counter-example models when constraints are violated.
Transforms Semantic IR structures by pruning dead branches and injecting recovery preconditions.
S-expression tokenizer and parser for Z3 (get-model) outputs.
Extracts concrete counter-example variable valuations and function interpretations.
Lightweight connection pool managing persistent Z3 Session workers with non-blocking checkout.
Schema definitions and validators for Semantic IR structures powered by NimbleOptions. Ensures strict structural integrity before passing AST/IR to Z3 formal verifiers.
Stateful GenServer managing a single persistent interactive Z3 Port process (z3 -in -smt2).
Resolves SMT queries via the persistent connection pool or standalone session fallback.