# SemanticVerifier demo pipeline: happy path + violation with counter-example.
#
# Run it with:
#
#     mix run examples/demo_pipeline.exs
#
# The same calls can be stepped through interactively with `iex -S mix`.

# --- Example 1: happy path — a valid IR verifies cleanly ---------------
#
# The frame declares the preconditions its safety constraint needs, so
# verification returns `{:ok, verified}` with no errors and no recovery
# candidates. Note the enriched IR: every frame gains a "branches" key and
# the top level gains "errors"/"recovery_candidates" alongside their
# atom-keyed counterparts.

ir = %{
  "intent" => "sample_pipeline",
  "frames" => [
    %{
      "id" => "f1",
      "frame" => "Reading",
      "FE" => %{"Source" => "file.txt"},
      "Preconditions" => ["Exists(file.txt)", "Readable(file.txt)"]
    }
  ],
  "constraints" => ["Readable(file.txt)"]
}

case SemanticVerifier.verify(ir) do
  {:ok, verified} ->
    IO.puts("\n[1] {:ok, verified}")
    IO.inspect(verified, pretty: true, limit: :infinity)

  other ->
    IO.puts("[1] unexpected result: #{inspect(other)}")
end

# --- Example 2: violated invariant — counter-example + recovery --------
#
# The frame reads protected.txt but declares no preconditions, so
# `Readable(protected.txt)` cannot be formally proven. Verification returns
# `{:error, [error | _], enriched_ir}` where:
#
#   * the error carries the violated constraint and a concrete Z3
#     counter-example model (SAT interpretation: `Readable -> false`);
#   * `enriched_ir[:recovery_candidates]` proposes adding the missing
#     precondition — exactly what `SemanticVerifier.auto_heal/1` applies.

invalid_ir = %{
  "intent" => "violation_test",
  "frames" => [
    %{
      "id" => "f1",
      "frame" => "Reading",
      "FE" => %{"Source" => "protected.txt"},
      "Preconditions" => []
    }
  ],
  "constraints" => ["Readable(protected.txt)"]
}

case SemanticVerifier.verify(invalid_ir) do
  {:error, [error | _], enriched_ir} ->
    IO.puts("\n[2] error (id #{error.id})")
    IO.inspect(error, pretty: true, limit: :infinity)
    IO.puts("\n[2] recovery candidates")
    IO.inspect(enriched_ir[:recovery_candidates], pretty: true, limit: :infinity)

  other ->
    IO.puts("[2] unexpected result: #{inspect(other)}")
end