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 what the engine's programs are built from**, and no more:
the rule line (type 1) as facts, choice atoms, normal rules and
integrity constraints, weight-body rules and constraints (the
cardinality bound a `asp/atMost` / `asp/atLeast` translates to), plus
minimize (2) and output (4).

The rest of the format — projection (3), externals (5), assumptions
(6), heuristics (7), acyclicity edges (8), and type 1's disjunctive
and multi-head choice heads — has no encoder here. An encoder nobody
executes is not coverage of a format; it is unverified text generation
claiming to be. What the engine needs, it emits and its tests
exercise, and nothing else is written here.

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 and must not
appear as an atom. String lengths in show statements count bytes
(equal to character count for ASCII); non-ASCII names need UTF-8
byte counting which we do not currently handle.

The public API has two halves:

  (1) Statement constructors (`fact`, `choice`, `rule`, `constraint`,
      `minimize`, `show`) that return plain data maps. Data form is
      inspectable, easy to assemble programmatically, and trivial to
      unit-test.

  (2) `render` turns a sequence of statements into the full ASPIF
      text with header and terminator.

Bidirectional atom id table for ASPIF translation.

ASPIF atoms are positive integers; every entity referenced in the
emitted program — sentex or contradiction marker — needs a unique id.
Atom 0 is reserved as the ASPIF terminator and is never allocated.

The table maps two kinds of source value to atom ids, sharing a
single counter so ids are unique across kinds:

  (1) sentex ids — the :id field of a vaelii sentex record. These
      become the atoms the ASP solver reasons about.

  (2) contradiction descriptors — nested sentence-shaped Clojure
      values of the form
        (contradiction <head> :involved [[:sentex H1] [:sentex H2] …])
      where `<head>` is a sentence-shaped tag (e.g. `(negation S)`,
      `(disjointTypes ent t-a t-b)`, or a user-named head emitted by
      a grounding rule like `(wrongBulbCount 3 4)`) and `:involved`
      lists the sentex handles that participated. Atoms backed by
      contradiction descriptors get weight in the minimize statement;
      the solver avoids models in which they are true.

Two kinds because two are what the translator emits: every atom in a
program stands for a contested assumption or for a violation. A third
namespace for translator scratch would be an interning path nothing
calls, which is the same unverified machinery `aspif` keeps out of the
emitter.

Labels are short string identifiers that appear in clasp's witness
output; we read them back during result parsing to recover the
originating sentex or contradiction. Format:

  s<sentex-id>   — sentex-backed atoms
  c<atom-id>     — contradiction-backed atoms

Using `s`/`c` prefixes keeps the two namespaces distinct even if a
sentex id happens to numerically match a contradiction atom id.

The table is a clojure.core/atom wrapping a plain map. Intern
operations use swap! for atomicity; lookups are pure derefs. All
intern operations are idempotent.

Subprocess wrapper around the clasp ASP solver.

Consumes ASPIF text on stdin, returns parsed results as Clojure maps.
clasp exit codes encode the solve outcome (10=sat, 20=unsat, 30=optimum,
bitmask combinations) and are NOT error codes — we rely on the JSON
`Result` field from `--outf=2` and only throw when clasp itself fails
to run or produces no parseable output.

The four modes are the ones `vaelii.impl.asp.edge` asks for:
:label, :all-optima, :classify-true, :classify-supportable.

Every run is single-threaded under a fixed seed and carries `--solve-limit` from
`config/asp-solve-limit` when it is positive (`search-args`), so where a search stops
is a function of the program.  `--time-limit` from `config/asp-time-limit` (0 lifts
it) is the backstop, and a process still running at `deadline-ms` is killed.  A
search stopped by either limit is read as `:interrupted` (`stopped-short?`).

Ownership: `run-clasp` starts the process and is its only owner.  It returns only
after the process has exited, and it kills the process and every descendant on the
paths that leave it running: the deadline and a throw out of the wait (an interrupt).

In-process ASP solver: a JNA binding to the native clingo C API (which
embeds clasp). Same solve modes and return shape as
`vaelii.impl.asp.clasp/solve`, but without the subprocess + JSON round-trip.

`solve` takes a translated program map `{:aspif <text> :stmts <statements>}`
and injects the ground `:stmts` straight through the `clingo_backend_*`
accessors — no ASPIF text, no temp file, no parse (`backend-load!`). Each
program atom id is interned as the function symbol `a(<id>)` carrying its s/c
label; a model's true atoms come back through clingo_model_symbols and are
mapped to labels through that symbol association, so no show statement is
emitted. `classify-both` keeps the ASPIF-text path (`clingo_control_load_aspif`
over a temp file), since one live control serves both enumerations.

Why in-process: it drops the per-solve fork and JSON round-trip the
subprocess pays, which is the whole win on the small programs
`vaelii.impl.asp.solver` routes here.

The four modes map to clingo configuration passed as command-line arguments
to clingo_control_new (clingo accepts clasp's flags): --opt-mode=optN so
brave/cautious enumerate over optimal models only, --enum-mode=brave|cautious,
--models=0|1. The lexicographic cost vector comes from clingo_model_cost.

Native lib: a system libclingo (brew install clingo) reachable via
jna.library.path, or an absolute path in -Dvaelii.clingo.lib. Crash isolation
is lost vs the subprocess — every native return is checked, every solve handle
is closed in a finally and every Control is freed in one; a malformed program
throws rather than segfaults.

The search flags are clasp's (`clasp/search-args`): one thread, a fixed seed, and
`--solve-limit` from `config/asp-solve-limit`, which the control takes as a solver
option and applies to each solve.  A search the solve limit stops reports neither
the exhausted bit nor the interrupted one, and `finalize` reads that as
`:interrupted`.

The time limit (`config/asp-time-limit`), the backstop behind it, is not a flag here
— libclingo's control takes solver options only and refuses `--time-limit` — so each
solve runs async and is drained through `clingo_solve_handle_wait` with what remains
of the budget; a solve still running when it runs out is cancelled and reports the
interrupted bit, read as `:interrupted`.

v :- a_h1, a_h2, ...

:- a_h1, a_h2, ...

d :- a_1, ..., not a_k.

:- k+1 <= #count{ a_m1, a_m2, ... }        # at-most-k: never k+1 together

v :- k+1 <= #count{ ... }                  # breaching the bound costs, not excludes

The real ASP backend behind `vaelii.impl.types.solve/Solver` — the edge solver.

`solve.clj` describes *what* an edge solve is: most of the KB is monotonic or
default-true with no conflict, so only the contested defeasible nodes are sent,
known-true content is fixed background, and contradictions are soft and
prioritized so a solve never fails.  This namespace renders that `Program` to
ASPIF and reads an answer set back.

## The encoding

Each contested assumption is a **choice atom**: true means believed, false means
defeated.  Known-true (`:fixed`) members of a contradiction are *not* atoms —
they hold by assumption, which is exactly what makes them background.

A contradiction `#{h1 h2 ...}` becomes a violation atom derived from its
contested members:

    v :- a_h1, a_h2, ...

and a **weak** constraint minimizing `v`.  Weak rather than hard is the whole
point: an unsatisfiable contradiction costs, it does not make the program UNSAT,
so it comes back in `:violated` instead of throwing.

A nogood carrying `:hard true` (a `set/hardConstraint` rule ground by
`solve-context`) is instead a **hard integrity constraint**

    :- a_h1, a_h2, ...

with no violation atom and no minimize term: a model satisfying its whole body is
excluded outright.  That is what makes graph 3-coloring plain satisfaction rather
than optimality-proving over soft violations — an adjacency clash is never
tradeable.  Soft nogoods (the default) keep the minimize path above.

A solve's **normal rules** (`program`'s `:derivations`, ground from `set/solveRule`s by
`solve-context`) are rendered as they are written,

    d :- a_1, ..., not a_k.

over the choice atoms and the **derived** atoms (`:derived`), which get atoms after the
choices and carry no choice rule and no minimize term: the rules alone decide them.  A
hard nogood left with no atom holds in every model and renders as the empty integrity
constraint.

A **cardinality** entry (`program`'s `:cardinalities`, ground from a `asp/atMost` /
`asp/atLeast` rule) is a bound on how many of a set of choice heads may or must hold,
rendered as ONE weight-body statement rather than the `C(n, k+1)` subset nogoods a
hand-written encoding needs.  A hard bound is a weight-body integrity constraint

    :- k+1 <= #count{ a_m1, a_m2, ... }        # at-most-k: never k+1 together

a soft one derives a violation atom the same minimize path penalizes

    v :- k+1 <= #count{ ... }                  # breaching the bound costs, not excludes

and at-least-`k` is the mirror over the default-negated members (`card-encoding`).

In practice `:violated` comes back empty, and that is correct rather than a gap.
An irreducible known-true clash never reaches a solver: `decide/verdict`
classifies it as *hard* and reports it directly, and `solve/program` drops any nogood
with no contested member.  What does arrive always has a contested member, and
defeating that member always satisfies it.
The `:doomed` path below is therefore defensive — it adds no work and stays
correct if nogoods ever grow beyond today's `S` vs `(not S)` pairs.

## The objective, most significant first

Higher ASPIF minimize priorities dominate lower ones, so the levels are:

| level | minimizes | why |
|---|---|---|
| `2 + rank(p)` | violation atoms | satisfy contradictions, caller priority first |
| `1` | defeated assumptions | give up as little belief as possible |
| `0` | a content-keyed weight | break remaining ties *stably* |

Caller priorities are mapped through their ascending rank rather than used as
levels directly, so any integers work and none can collide with the two levels
below.

## Determinism

A tie between equally-good answer sets has no principled winner, but it must not
depend on assertion order — the engine-wide invariant in docs/nmtms.md.  Atom ids
are allocated in `solve/content-key` order, and level 0 weights defeating the
greatest content-key most cheaply, mirroring the stub's choice.  Same knowledge
in any order, same answer set.

## Availability

`edge-solver` degrades rather than fails **when there is no backend at all**: with no
clingo and no clasp reachable it delegates to `solve/local-solver`, so installing it is
always safe.  Degradation is confined to that case on purpose — see below.

## A result that is not an answer

A backend's result is an answer set only at `:optimum` or `:sat`.  `:interrupted`
(the solve limit, `config/asp-solve-limit`; the time limit, `config/asp-time-limit`;
or a signal) and `:unknown` carry **no** witness, and every reader here maps an atom's
absence to *defeated* or *not kept* — so read as an answer, an empty result defeats
every contested assumption and labels every choice head false.  `answered?` gates each reader.

**With a backend present, `edge-solver` decides nothing rather than degrading.**  The
stub and ASP disagree — measured on two nogoods sharing a member, the stub defeats
`{1,3}` where the optimum defeats `{2}` — and the two are not interchangeable halves of
one answer.  A labeling solve that runs out of budget while the classification solve
beside it finishes would pair a stub labeling with an ASP classification, which
`label/check-agrees` reports as `:labeling-inconsistent`, blaming the encoding for a
disagreement the fallback introduced.  A labeling committed from such a pair would
differ run to run on identical knowledge — the order-independence invariant in
docs/nmtms.md is a claim about *knowledge*, and a wall clock is not knowledge.  So `undecided` is
returned instead: no defeat, the contested assumptions all stand, and `:error` names
what went wrong for a caller that can act on it.  With no backend the two degrade
together and stay consistent for free — `classify-program` claims nothing without one —
which is why that case, and only that case, still falls back.

A backend that **throws** — clingo's `:solver-failed`, clasp's `:solver-unavailable`,
a JNA `Error` against a missing libclingo — reads the same way, and the catch is here
rather than at the caller because this is the boundary a native failure crosses.
`undecided` hands the failure back as data, and `label/solved-labeling` raises its
`:error` before the labeling asserts anything.

`:unsat` is different and keeps its own reading: a definite *no model*, the same answer
in every run, so it costs the invariant nothing.  Each reader has a word for it —
`edge-solver` degrades, `kept-of` keeps nothing, `enumerate-optima` is empty.

The imperative readers (`kept-of`, `enumerate-optima`, `classify-program`) refuse an
unanswered result with `:solver-failed` rather than return a world nobody computed.
They are not mid-arbitration, so a throw there adds no work and says more.

:true        ⊆ believed        (cautious holds in the committed model)
:false       ∩ believed = ∅    (excluded holds in no model, including that one)
:supportable — either way, by definition

Brave/cautious classification of a settled tie, and materializing one labeling as
a specialization context.

## What this adds over `in?`

The TMS answers *what do I believe*. After `settle` arbitrates a default/default
tie, one side is IN and the other OUT — but that answer flattens two very different
situations. A belief can be IN because every consistent way of resolving the
contradictions keeps it, or because the solver had two equally good options and
picked one. `in?` cannot tell them apart; both read as "believed".

Brave/cautious classification separates them by asking the solver for *all* optimal
answer sets rather than one:

| class | in every optimum | in some optimum | meaning |
|---|---|---|---|
| `:true` | yes | yes | forced — no consistent labeling gives it up |
| `:supportable` | no | yes | arbitrary — the current belief is one of several |
| `:false` | no | no | excluded — no consistent labeling holds it |

`:supportable` is the interesting one, and it is invisible from the TMS alone. In a
Nixon diamond both sides are `:supportable`: whichever the TMS committed to, the
other was equally available.

## Concert with the TMS

Two rules keep these from drifting apart from belief.

**Classification reads the recorded program, never a recomputed one.** Resolving a
tie erases its own evidence — the defeated side stops matching, so the nogood is no
longer derivable from the KB. The `:program` atom on the KB holds what the solver was
actually asked (see the KB record); `vaelii.core/last-program` is the public read of it.

**Labeling reads the TMS, not a fresh solve.** `label-context` materializes the
labeling the engine *committed to*, taken from `jtms/in?`, rather than re-solving
and hoping for the same answer set back. A re-solve would usually agree, and
"usually" is not a property worth building on.

So the invariants hold by construction, and `asp_label_test` pins them:

    :true        ⊆ believed        (cautious holds in the committed model)
    :false       ∩ believed = ∅    (excluded holds in no model, including that one)
    :supportable — either way, by definition

## Requirements

Classifying a `Program` needs a real ASP backend; `local-solver` produces one labeling
and cannot enumerate optima. With no backend reachable, `classify-program` reports every
contested assumption as `:supportable` — correct (each *is* one of several options)
and never overclaims `:true`.  A represented dilemma is classified and labeled off the
dependency graph instead (`classify-local`), on every build.

A query-time prover for `(bravely S)` and `(cautiously S)` — brave/cautious reading
of the dilemmas the KB currently holds, answered as a read and never committed.

## What it answers

`(cautiously S)` holds when `S` is in **every** optimal labeling of the current
dilemmas; `(bravely S)` when `S` is in **some**.  Over a coexisting `P`/`¬P` dilemma the
engine declines to arbitrate (docs/exceptions.md), both sides are IN, and an ordinary
`ask` reports both — so it cannot tell the *forced* belief from the *arbitrary* one.  A
brave/cautious read can: in a Nixon diamond `(bravely (pacifist N))` holds and
`(cautiously (pacifist N))` does not, because the other labeling gives it up.

This is the read-path delivery of the forced/arbitrary signal.  The only prior route to
it, `do/labeling`, **commits** — it re-asserts the kept side at `:monotonic` and defeats
the loser everywhere (docs/labeling.md).  This prover commits nothing: it reads
`label/classify-datum` — the solve-free `label/classify-local`, refined by a backend's
`classify-program` only past its caps — all pure reads over settled belief, so a query
answers and leaves belief, `contradictions` and `last-program` exactly as they were.

## Opting in

Registered like the other optional reasoners — `(add-reasoner kb :brave-cautious)` — so
the ASP stack stays off a KB's load path until a caller asks (docs/asp.md).  **It reads
the solve-free JTMS bracket** (`label/classify-local`) with or without a backend, which
enumerates the dilemmas' optimal resolutions from the dependency graph and classifies
each datum by which resolutions keep it — `:true` in every, `:supportable` in some,
`:false` in none.  Exact for a datum whose
clusters it enumerates: the one cluster its support touches, or several whose product of
resolutions stays within `VAELII_CLASSIFY_MAX_JOINT_OPTIMA`.  A datum past that cap, or
one touching a cluster too large to enumerate, degrades to `:supportable`; a backend
refines a member of such a cluster when no member of it derives from another, where a
`Program` is exact (docs/labeling.md).

## Where it stops

**Ground `S` only.**  `(bravely (pacifist N))` is answered; an open `(bravely (pacifist
?x))` is not applicable and no prover answers it, rather than enumerating the contested
atoms — the same restraint `different` takes.

**A query, not a fact and not an antecedent.**  `bravely`/`cautiously` are not
assertible (`wff/brave-cautious-problems`): a stored one would be a computed value with
no way to keep it current, the reason the aggregates and `unknown` are refused too.  As a
rule antecedent the answer carries no support (it is not a `SupportingProver`), so the
forward join drops it and it derives nothing — a read, not something belief rests on.
Threading its support (the dilemma's contested handles) so a rule could rest on it is the
open design point, deferred until a use asks for it.

Solving as a **persistent, inert** artifact: `assumptionRules` define choices, a
solve grounds them (scoped to a base context), enumerates the optimal answer sets,
and materializes **each one as its own labeling context** — a `genlCx` child of
the base holding the chosen truth values as inert sentexes.  `classify` then gathers
brave/cautious over those labelings.

The two imperatives `(do/label Base Into)` and `(do/classify Into)` route here.

## Why inert, and why per-answer-set

Belief in this KB is global (one JTMS, not an ATMS): a *believed* `(not head)` in a
context that sees the base would defeat the base's `head` everywhere — so only one
labeling could ever exist (the `do/labeling` global-commit).  Materializing the truth
values **inert** (`core/assert-inert` — stored and indexed but not a JTMS premise)
sidesteps that entirely: an inert sentex is never IN, so it is invisible to the
belief-filtered nogood scan, forms no contradiction, and moves no belief.  Every
answer set therefore coexists as its own context, the base KB is untouched, and the
result **persists in the records** for inspection.

## What persists, and what does not

The **answer** persists: the labeling contexts and the classification, as inert
sentexes in the records.  The **grounding** — the menu of candidate choice heads —
never does.  A grounding is derived solver working state, recomputable from the
assumptionRules and the base's believed facts; an inert copy would carry no
justification linking it back to what produced it, so it would rot silently the
moment the base moved.  The Program keys on program-local ids (see `build`), and
`label` returns the menu as `:choices` for a caller who wants to see it.

And what persists is **replaced on re-run**, never accreted: `label` clears a
previous run's artifacts under the same `Into` before writing (see `clear-run!`),
and `classify` clears its own previous classification.  Truth values from two
different groundings unioned into one context assert nothing at all.

## What a choice constrains (docs/solving.md)

Constraints reach the ground choice heads and the atoms the solve rules derive from
them: the engine's own contradictions among the choice heads — a `(not X)`/`X` pair, a
`functional` predicate given two values, a `disjoint` type clash — and every
`hardConstraint` / `softConstraint` rule ground over the program's atoms.  A choice
propagates through a `set/solveRule` and through nothing else: the solve rules are
ground into the program's normal rules (`ground-derivations`), and a rule without the
wrapper is not — nothing runs the chainer with a choice held hypothetically.

Backend selector for vaelii's ASP solver. Callers (`asp.edge`, `asp.label` and
`asp.solve-context`) use `solver/solve`/`solver/available?` so the engine can run
the in-process clingo backend (default, when libclingo + JNA are present) or fall
back to the clasp subprocess — without any caller change.

The clingo backend is loaded LAZILY via requiring-resolve so JNA/libclingo
stay optional: a plain build (without the `:with-clingo` profile) has no JNA
on the classpath, the resolve fails cleanly, and the facade falls back to
clasp. clasp is also the deliberate fallback for long-running daemons, since
an in-process native crash takes down the whole JVM.

Select explicitly with -Dvaelii.asp.solver or VAELII_ASP_SOLVER = clingo|clasp.
Default is auto: prefer in-process clingo when it loads, else clasp.