Pure ASPIF text emitter. No vaelii deps, no I/O.

ASPIF is the Potassco Answer Set Programming Intermediate Format, the
ground-program protocol between gringo and clasp.  This emits the
statements the engine's programs use: the rule line (type 1) as facts,
choice atoms, normal rules, integrity constraints, and weight-body rules
and constraints; minimize (2); and output (4).  Projection (3),
externals (5), assumptions (6), heuristics (7), acyclicity edges (8) and
type 1's disjunctive and multi-head choice heads have no encoder
(docs/defenses.md, "The ASPIF emitter encodes only what a program
uses").

Wire format of what is emitted (line-oriented, space-separated):
  Line 1: `asp 1 0 0`
  Rule:     1 <head_type> <head_size> <head...> <body_type> <body_size> <lits...>
              head_type = 0 disjunctive | 1 choice
              body_type = 0 normal (list of signed literals)
                     or = 1 weight  (a cardinality/weight body)
              body literal: +atom for positive, -atom for default-negated
  Weight body: 1 <lower_bound> <n> <lit_1> <w_1> ... <lit_n> <w_n>
              satisfied when the summed weight of the satisfied literals is
              at least <lower_bound>.  A cardinality constraint is the unit-weight
              case: `k+1 <= #count{ ... }` is a weight body of bound k+1 over
              weight-1 literals.  Emitted headless (an integrity constraint that
              excludes any model reaching the bound) or with a head (an atom that
              holds when the bound is reached, for a soft/minimized violation).
  Minimize: 2 <priority> <n> <lit_1> <w_1> ... <lit_n> <w_n>
  Output:   4 <str_len> <str> <n_conditions> <atoms...>
  End:      0

Atom ids are positive integers; 0 is the terminator.  A show
statement's length counts characters, so its text must be ASCII.

The statement constructors return data maps, and `render` turns a
sequence of them into the ASPIF text.

The atom id table `asp.edge/translate` builds.  Two kinds of value are interned under
one counter, so ids are unique across kinds and start at 1 (0 is the ASPIF terminator):

  * a sentex id, an atom the solver decides, labelled `s<sentex-id>`;
  * a contradiction descriptor `(contradiction <head> :involved [[:sentex h] …])`, a
    violation atom the minimize statement weighs, labelled `c<atom-id>`.

A witness reports labels, and each label maps back to its value.  The table is an atom
over a map, and interning is idempotent.

Subprocess wrapper around the clasp ASP solver.

Takes ASPIF text on stdin and reads the JSON `Result` of `--outf=2`.  clasp's exit
codes encode the solve outcome (10 sat, 20 unsat, 30 optimum) and are not errors; a
run throws only when clasp does not run or answers nothing parseable.  The five modes
are `solve`'s.  The search flags are `search-args`, and the limits are docs/asp.md's
"The solve limit" and "The time limit".

`run-clasp` owns the process: it returns only after the process has exited, and kills
it with every descendant at the deadline and on a throw out of the wait.

The in-process ASP backend: a JNA binding to libclingo, with `vaelii.impl.asp.clasp/solve`'s
modes and return shape.  `solve` injects a translated program's `:stmts` through the
`clingo_backend_*` accessors (`backend-load!`); `classify-both` loads the ASPIF text once
over a temp file and runs both enumerations on one control.  The search flags are
`clasp/search-args`, and the time limit is a cancel at the deadline (`drain-models`).
Every native return is checked, and every solve handle and control is freed in a
`finally`.  See docs/asp.md, "Getting a solver" and "The time limit".

`edge-solver`, the ASP implementation of `vaelii.impl.types.solve/Solver`.  `translate`
renders a `Program` to ASPIF, and the readers read a backend's answer set back:
`interpret` for `edge-solver`, `kept-of`, `enumerate-optima` and `classify-program` for
the imperatives.  A reader runs only on an answer (`answered?`); the imperative readers
refuse any other result with `:solver-failed`.  The encoding, the objective levels,
determinism and the no-answer policy: docs/asp.md.

Brave/cautious classification and the two labeling writers.  `classify` reads the
`Program` the KB last recorded; `classify-local` and `classify-datum` classify the
current dilemmas from the JTMS dependency graph with no backend.  `label-context`
records the labeling the engine committed to; `label-dilemmas` (`do/labeling`) commits
one inside a context.  See docs/asp.md and docs/labeling.md.

The `(bravely S)` / `(cautiously S)` prover, opted into with `(add-reasoner kb
:brave-cautious)`: `S` is in some, or every, optimal labeling of the dilemmas the asking
context reads, from `label/classify-datum`.  The read commits nothing.  Ground `S` only;
the answer carries no support, so as a rule antecedent it derives nothing.  See
docs/labeling.md, "Reading brave/cautious without committing".

`(do/label Base Into [mode])` and `(do/classify Into)`: ground the `assumptionRule`s,
solve rules and constraint rules visible from a base context into a `Program`, solve it,
and write each optimal answer set as an inert labeling context under the base; then
aggregate brave/cautious over those contexts.  The labeling and classification extents
are inert, the `(genlCx <labeling> Base)` placement edge is asserted `:monotonic`, and
the grounding is not stored.  See docs/solving.md.

Picks the ASP backend per solve: in-process clingo (`vaelii.impl.asp.clingo`, resolved
on first use so JNA stays optional) or the clasp subprocess.  `asp.edge`, `asp.label` and
`asp.solve-context` call `solve`, `classify-both` and `available?`.  See docs/asp.md,
"Getting a solver".