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 carries --time-limit from config/asp-time-limit (0 lifts it): a
solve that hits it comes back Result: UNKNOWN with TIME LIMIT: 1, read here
as :interrupted.
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 carries `--time-limit` from `config/asp-time-limit` (0 lifts it): a solve that hits it comes back `Result: UNKNOWN` with `TIME LIMIT: 1`, read here as `:interrupted`.
Name (or absolute path) of the clasp executable. Bind to point
solve at a non-default install or a test stub.
Name (or absolute path) of the clasp executable. Bind to point `solve` at a non-default install or a test stub.
(available?)True if the clasp binary can be executed in the current environment. Used by tests to skip cleanly when clasp isn't installed.
True if the clasp binary can be executed in the current environment. Used by tests to skip cleanly when clasp isn't installed.
(solve aspif-text mode)Run clasp on aspif-text in one of the supported modes.
Modes: :label — one minimum-cost witness (for labeling output) :all-optima — every minimum-cost witness (for inspection) :classify-true — atoms in every minimum-cost witness :classify-supportable — atoms in at least one minimum-cost witness
Returns: :status — :optimum | :sat | :best-effort | :unsat | :interrupted | :unknown :atoms — vector of atom-name strings :cost — optimum cost (nil if no minimize statement or unsat) :witnesses — vector of value vectors (only populated for :all-optima) :raw — full parsed JSON (for diagnostics)
:interrupted is the time limit (config/asp-time-limit) or a signal with NO witness
to show for it. A :label run cut off after it had a witness is :best-effort
instead — that model is a valid labeling, its optimality merely unproven — which the
imperative :one caller takes over nothing (asp.edge/kept-of); the enumerating modes
need a finished search, so they stay :interrupted.
Run clasp on `aspif-text` in one of the supported modes. Modes: :label — one minimum-cost witness (for labeling output) :all-optima — every minimum-cost witness (for inspection) :classify-true — atoms in every minimum-cost witness :classify-supportable — atoms in at least one minimum-cost witness Returns: :status — :optimum | :sat | :best-effort | :unsat | :interrupted | :unknown :atoms — vector of atom-name strings :cost — optimum cost (nil if no minimize statement or unsat) :witnesses — vector of value vectors (only populated for :all-optima) :raw — full parsed JSON (for diagnostics) `:interrupted` is the time limit (`config/asp-time-limit`) or a signal with NO witness to show for it. A `:label` run cut off *after* it had a witness is `:best-effort` instead — that model is a valid labeling, its optimality merely unproven — which the imperative `:one` caller takes over nothing (`asp.edge/kept-of`); the enumerating modes need a finished search, so they stay `:interrupted`.
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |