vaelii.impl.asp.clingo — com.vaelii/vaelii 0.11.0

In-process ASP solver: a JNA binding to the native clingo C API (which embeds clasp). Drop-in for vaelii.impl.asp.clasp/solve — same (solve aspif-text mode) contract and return shape — but without the subprocess + JSON round-trip.

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. Shown atoms come back as the s/c/a label strings vaelii emits via ASPIF type-4 show statements; 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 time limit (config/asp-time-limit) 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.

*clingo-lib* clj

Library name (resolved via jna.library.path) or absolute path to libclingo.

available? clj

(available?)

True if libclingo can be loaded and called in this JVM.

classify-both clj

(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.

delete-keep-temps! clj

(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. run-solve .deletes its one-shot temp in its own finally; 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! clj

(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.

open-control clj

(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!).

solve clj

(solve aspif-text mode)

Run clingo in-process on aspif-text (via load_aspif) in one of the supported modes. See finalize for the return contract.

solve-control clj

(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; witness symbols come off the output table, the same show-shown view run-solve reads.