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).
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).
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.
(search-args)The flags under which a solve's search is a function of its program alone: one
thread, clasp's own default seed (1) stated rather than assumed, and
--solve-limit=N for a positive config/asp-solve-limit. The limit counts
conflicts, so it stops a search at the same point on any machine, where
--time-limit stops it wherever the machine has got to. In-process clingo's control
takes the same flags (vaelii.impl.asp.clingo).
The flags under which a solve's search is a function of its program alone: one thread, clasp's own default seed (1) stated rather than assumed, and `--solve-limit=N` for a positive `config/asp-solve-limit`. The limit counts conflicts, so it stops a search at the same point on any machine, where `--time-limit` stops it wherever the machine has got to. In-process clingo's control takes the same flags (`vaelii.impl.asp.clingo`).
(solve aspif-text mode)Run clasp on aspif-text in one of the supported modes.
Modes: :label — one minimum-cost witness (for labeling output) :sat — the first witness, for a program with no objective :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)
A :label solve of a program with no objective runs under :sat's flags: streaming
improving models there would enumerate every model.
:interrupted is the solve limit (config/asp-solve-limit), 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) :sat — the first witness, for a program with no objective :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) A `:label` solve of a program with no objective runs under `:sat`'s flags: streaming improving models there would enumerate every model. `:interrupted` is the solve limit (`config/asp-solve-limit`), 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 |