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.
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`.Library name (resolved via jna.library.path) or absolute path to libclingo. A blank
vaelii.clingo.lib is unset, as every switch's blank is (vaelii.impl.config):
-Dvaelii.clingo.lib= names no library, and read as one it would ask JNA for a
library called "".
Library name (resolved via jna.library.path) or absolute path to libclingo. A blank `vaelii.clingo.lib` is unset, as every switch's blank is (`vaelii.impl.config`): `-Dvaelii.clingo.lib=` names no library, and read as one it would ask JNA for a library called "".
(available?)True if libclingo can be loaded and called in this JVM.
True if libclingo can be loaded and called in this JVM.
(classify-both aspif-text)Load aspif-text ONCE and run both classify enumerations over the one control,
switching solve.enum_mode between them — avoiding the second control_new +
load_aspif that two separate solve calls pay. Returns
{:cautious <result> :brave <result>}, each shaped like solve for the
corresponding classify mode.
Load `aspif-text` ONCE and run both classify enumerations over the one control,
switching `solve.enum_mode` between them — avoiding the second control_new +
load_aspif that two separate `solve` calls pay. Returns
`{:cautious <result> :brave <result>}`, each shaped like `solve` for the
corresponding classify mode.(delete-keep-temps! keep)Delete every temp File in a control's :keep vector — the ASPIF file
load-block!/open-control wrote. Call AFTER free-control!. Non-File
keep entries (JNA buffers) are left for GC. Only the classify-both path writes a
temp now (the one-shot solve injects its program through the backend accessors and
writes none); a live control outlives its solve, so classify-both calls this
instead of leaning on deleteOnExit — which in a long-running daemon holds one .aspif
file, and one never-GC'd JVM DeleteOnExitHook entry, per classify.
Delete every temp File in a control's `:keep` vector — the ASPIF file `load-block!`/`open-control` wrote. Call AFTER `free-control!`. Non-File keep entries (JNA buffers) are left for GC. Only the `classify-both` path writes a temp now (the one-shot `solve` injects its program through the backend accessors and writes none); a live control outlives its solve, so `classify-both` calls this instead of leaning on deleteOnExit — which in a long-running daemon holds one .aspif file, and one never-GC'd JVM DeleteOnExitHook entry, per classify.
(free-control! ctl)Free a live control and let its keep-alive buffers/temps be reclaimed. Freeing
twice is a native double free, so a caller frees exactly once — classify-both
does it in a finally.
Free a live control and let its keep-alive buffers/temps be reclaimed. Freeing twice is a native double free, so a caller frees exactly once — `classify-both` does it in a finally.
(open-control arg-strs aspif-text)Create a live Control with arg-strs flags and load the base aspif-text.
Returns {:ctl Pointer :keep [..]} — :keep holds JNA buffers and temp
files that must outlive the control (free it with free-control!).
A load that throws frees the control on the way out: the caller is handed an exception rather than a handle, so nothing else can free it, and a leaked Control is native memory no GC reaches.
Create a live Control with `arg-strs` flags and load the base `aspif-text`.
Returns `{:ctl Pointer :keep [..]}` — `:keep` holds JNA buffers and temp
files that must outlive the control (free it with `free-control!`).
A load that throws frees the control on the way out: the caller is handed an
exception rather than a handle, so nothing else can free it, and a leaked
Control is native memory no GC reaches.(solve {:keys [stmts]} mode)Run clingo in-process on translated program {:aspif <text> :stmts <statements>} in
one of the supported modes, injecting :stmts through the clingo_backend_*
accessors (no ASPIF text, no temp file, no parse). See finalize for the return
contract. A :label solve of a program with no objective runs as :sat: streaming
improving models there would enumerate every model.
Run clingo in-process on translated program `{:aspif <text> :stmts <statements>}` in
one of the supported modes, injecting `:stmts` through the `clingo_backend_*`
accessors (no ASPIF text, no temp file, no parse). See `finalize` for the return
contract. A `:label` solve of a program with no objective runs as `:sat`: streaming
improving models there would enumerate every model.(solve-control ctl assume-lits retain)Solve a live control under assume-lits (signed program literals assumed
for THIS solve only), keeping the models retain keeps. Returns the same drain
shape as the one-shot path. The mode flags are fixed at open-control time; this
is the ASPIF-text path (classify-both loads via load_aspif), so witnesses come off
the output table through the show-shown view model-symbols reads.
Solve a live control under `assume-lits` (signed program literals assumed for THIS solve only), keeping the models `retain` keeps. Returns the same drain shape as the one-shot path. The mode flags are fixed at `open-control` time; this is the ASPIF-text path (`classify-both` loads via load_aspif), so witnesses come off the output table through the `show-shown` view `model-symbols` reads.
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 |