SemanticVerifier.ModelParser (semantic_verifier v0.1.0)

Copy Markdown View Source

S-expression tokenizer and parser for Z3 (get-model) outputs. Extracts concrete counter-example variable valuations and function interpretations.

Summary

Types

counter_example()

Functions

parse(raw_output)

Parses a raw Z3 SMT-LIB2 model string into structured counter-example valuations.

Types

counter_example()

@type counter_example() :: %{
  constants: %{required(String.t()) => term()},
  functions: %{required(String.t()) => map()},
  raw_model: String.t()
}

Functions

parse(raw_output)

@spec parse(String.t()) :: counter_example()

Parses a raw Z3 SMT-LIB2 model string into structured counter-example valuations.