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

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

add-program! clj

(add-program! session stmts)

Grow session's live program by one backend batch of stmts — control_backend → begin → emit → end on the kept control (backend-batch!) — merging the batch's sym→label into (:syms session) and vid→cid into (:cids session). Because clingo_backend_add_atom is idempotent on a symbol, a vid first seen in an earlier batch re-interns to the SAME cid, so a later batch's rules can reference earlier atoms and the program genuinely grows in place (clasp keeps its learned clauses across the solves between batches). Returns the session.

assign-external! clj

(assign-external! session vid truth)

Set external vid's truth on session's live control to truth (:free | :true | :false) via clingo_control_assign_external. A CONTROL op called BETWEEN solves — no backend bracket, no open solve handle — that re-grounds nothing, so the next solve-session sees the flipped value with clasp's learned clauses intact. The literal is the atom's positive program literal, the clingo_literal_t cid declare-external! recorded. Refuses a vid no batch on this session ever interned — there is no literal to assign. Returns the session.

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.

close-session! clj

(close-session! session)

Free a session's live control (exactly once, like free-control!). Its :keep arg buffers become reclaimable; a session writes no temp file, so there is nothing else to clean up.

declare-external! clj

(declare-external! session vid initial)

(declare-external! session vid initial label)

Declare atom vid an EXTERNAL of session's live control with initial truth initial (:free | :true | :false), inside a backend begin/end bracket (it is a backend op). Interns a(<vid>) → cid (recording vid→cid, and a sym→label from label or (str vid) so the external is observable in model readback), then clingo_backend_external(backend, cid, <type>). Unlike a rule, an external's truth is then toggled between solves by assign-external! with NO re-grounding. Returns the session.

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

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.

open-session clj

(open-session arg-strs)

Open an incremental session: a live control created with arg-strs flags and NO program loaded — the multi-shot analogue of open-control, which base-loads ASPIF text a live control cannot then grow. Returns

{:ctl <Pointer> :syms (atom {}) :cids (atom {}) :keep [argcs]}

:syms accumulates the symbol→label map across every add-program! / declare-external! batch (solve-session's model readback reads through it); :cids accumulates vid→cid so a later batch and assign-external! can name an earlier batch's atoms; :keep holds the JNA arg buffers that must outlive the control. Close with close-session! exactly once (free-control!).

No free-on-throw wrapper, unlike open-control: a failed control_new throws in chk! before a control exists, and nothing between the successful create and the returned map can throw — a session base-loads nothing.

solve clj

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

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; 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-session clj

(solve-session session mode)

Solve session's live control in mode, keeping the models the mode reads and reading their true atoms back through the session's accumulated sym→label map (model-atoms) — the backend analogue of solve-control, but on the kept control and WITHOUT freeing it, so it is callable repeatedly as the program grows and externals toggle. The clingo flags are fixed at open-session; mode selects only the retention and finalize post-processing, so it must agree with those flags. Returns the public finalize contract (:status :atoms :cost :raw).