ShotTx.Prover.ModelAgent.Backend.Nitpick (ShotTx v0.0.1)

Copy Markdown View Source

Backend that ships the branch's frontier to a warm Isabelle server and runs nitpick[satisfy] against it.

Pipeline:

  1. Frontier.to_problem/1 turns the branch into a %ShotDs.Data.Problem{}.
  2. ShotDs.Tptp.unparse_problem/1 renders it as THF text with all constants declared and every axiom universally-closed over its free variables.
  3. IsabelleClient.TPTP.isabellize_theory/1 (from isabelle_elixir) converts the THF into Isabelle theory commands.
  4. A theorem "True" nitpick[satisfy, user_axioms=true, …] is appended so Nitpick searches for a model of the axioms rather than a countermodel of a specific goal. user_axioms=true is critical — without it Nitpick ignores the axioms and trivially satisfies the True goal.
  5. ShotTx.IsabelleBridge.probe/2 submits the theory body and returns an async reference. await/2 blocks for the verdict.

Nitpick options

Per-probe options via opts[:nitpick_opts] — merged into the invocation. Common knobs:

  • card: n — cap on cardinality search
  • mono: true|false — assume monotonicity for polymorphic types
  • iter: n — iteration count for coinductive datatypes
  • sat_solver: "…" — override the SAT backend

Timeout is derived from opts[:budget_ms] (converted to seconds). If nitpick_opts explicitly sets timeout, that value wins.

The result of parsing Nitpick's messages is coarse — :sat when Nitpick reports a model, :unknown otherwise. Structured countermodel extraction is left for a follow-up; the model string is stashed in the witness payload as :nitpick_output for display.