vaelii.impl.asp.solve-context — com.vaelii/vaelii 0.29.0

(do/label Base Into [mode]) and (do/classify Into): ground the assumptionRules, solve rules and constraint rules visible from a base context into a Program, solve it, and write each optimal answer set as an inert labeling context under the base; then aggregate brave/cautious over those contexts. The labeling and classification extents are inert, the (genlCx <labeling> Base) placement edge is asserted :monotonic, and the grounding is not stored. See docs/solving.md.

classify clj

(classify kb into-cx)

do/classify: aggregate the labelings a prior (do/label _ Into) wrote and write (forced H) (true in every labeling), (excluded H) (false in every one) or (supportable H) per head, with its classificationOf marker, into <Into>Class, replacing the previous classification. Refuses :labeling-run-blocked when class-blocked finds anything. Returns {:into :class-context :count :forced [..] :supportable [..] :excluded [..]}, or :count 0 :reason :no-labelings. See docs/solving.md, "(do/classify Into)".

label clj

(label kb base into-cx)

(label kb base into-cx mode)

do/label: ground and solve the program build makes in base. mode is :all (the default), :one or :sat:

• :all writes each optimal answer set as an inert labeling context <Into><i> under base, holding (head) per true atom, (not head) per false one and its labelingOf marker, after clearing the previous run (clear-run!);
• :one returns one optimal answer set and writes nothing;
• :sat is :one without the keep-belief objective.

An :all run refuses :labeling-run-blocked before grounding when the previous run cannot be replaced (blocked-artifacts). A run grounding no choice clears too; a run with no backend leaves the previous run standing.

Returns {:base :into :choices [..] :derived [..] :labelings [{:context :true [..] :false [..]}] :count n :ground-ms :translate-ms :solve-ms}, :context nil under :one / :sat, :best-effort? true when a stopped solve held a model. :count 0 carries a :reason: :no-choices, :no-backend, or :unsatisfiable under :one / :sat. See docs/solving.md, "(do/label Base Into [mode])".