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".
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".
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 the cautious and the brave enumeration on one control,
switching solve.enum_mode between them. Returns {:cautious <result> :brave <result>}, each shaped like solve's.
Load `aspif-text` once and run the cautious and the brave enumeration on one control,
switching `solve.enum_mode` between them. Returns `{:cautious <result> :brave
<result>}`, each shaped like `solve`'s.(delete-keep-temps! keep)Delete every temp File in a control's :keep vector, after free-control!. JNA
buffers are left for the GC.
Delete every temp File in a control's `:keep` vector, after `free-control!`. JNA buffers are left for the GC.
(free-control! ctl)Free a live control, exactly once: a second free is a native double free.
Free a live control, exactly once: a second free is a native double free.
(open-control arg-strs aspif-text)Create a live Control with arg-strs flags and load aspif-text. Returns {:ctl Pointer :keep [..]}, :keep holding the JNA buffers and temp file that must outlive
the control (free-control!). A load that throws frees the control first.
Create a live Control with `arg-strs` flags and load `aspif-text`. Returns `{:ctl
Pointer :keep [..]}`, `:keep` holding the JNA buffers and temp file that must outlive
the control (`free-control!`). A load that throws frees the control first.(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 literals assumed for this solve only),
keeping the models retain keeps; the drain shape of backend-solve. The control was
loaded from ASPIF text, so witnesses are read through the show statements
(model-symbols).
Solve a live control under `assume-lits` (signed literals assumed for this solve only), keeping the models `retain` keeps; the drain shape of `backend-solve`. The control was loaded from ASPIF text, so witnesses are read through the show statements (`model-symbols`).
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 |