SemanticVerifier.Encoder (semantic_verifier v0.1.2)

Copy Markdown View Source

Encodes Semantic IR constraints, axioms, and branch criteria into SMT-LIB2 s-expressions.

Summary

Functions

build_constraint_refutation(preconditions, target_constraint)
build_reachability_smt(negated_previous_branches, current_criterion)
encode_condition(crit)

Functions

build_constraint_refutation(preconditions, target_constraint)

@spec build_constraint_refutation([String.t()], String.t()) :: String.t()

build_reachability_smt(negated_previous_branches, current_criterion)

@spec build_reachability_smt([String.t()], String.t()) :: String.t()

encode_condition(crit)

@spec encode_condition(String.t()) :: String.t()