vaelii.impl.asp.edge — com.vaelii/vaelii 0.29.0

edge-solver, the ASP implementation of vaelii.impl.types.solve/Solver. translate renders a Program to ASPIF, and the readers read a backend's answer set back: interpret for edge-solver, kept-of, enumerate-optima and classify-program for the imperatives. A reader runs only on an answer (answered?); the imperative readers refuse any other result with :solver-failed. The encoding, the objective levels, determinism and the no-answer policy: docs/asp.md.

classify-program clj

(classify-program {:keys [assumptions fixed] :as program})

Classify program's assumptions into :true / :supportable / :false by brave/cautious reasoning over its optimal answer sets — in every optimum, in some, in none.

:fixed handles are :true. With no ASP backend every contested assumption is :supportable. An enumeration the backend did not finish is refused (:solver-failed). asp.label re-exports it.

edge-solver clj

The ASP solve-types/Solver, (core/set-solver kb :asp). With no ASP backend reachable it is solve/local-solver; with one it answers from the backend or decides nothing (undecided), and throws only a VirtualMachineError.

enumerate-optima clj

(enumerate-optima {:keys [assumptions] :as program})

Every optimal answer set of program, each as the set of its chosen-true assumption handles, from an :all-optima solve of the tiebreak-off encoding:

• [] — no assumptions, or an :unsat program;
• nil — no ASP backend;
• [#{h} …] — one handle set per optimum otherwise.

An enumeration the backend did not finish is refused (:solver-failed).

kept-of clj

(kept-of {:keys [table assumptions derived]} result)

The chosen-true assumption handles and the true derived atoms of one :label result, read through translation t's atom table; do/label :one and :sat read a labeling with it. An :unsat result keeps #{}, a :best-effort one is read as an answer, and an :interrupted or :unknown one is refused (:solver-failed).

translate clj

(translate program)

(translate {:keys [assumptions contradictions derived derivations] :as program}
           {:keys [tiebreak? keep-belief?]
            :or {tiebreak? true keep-belief? true}})

Render program to ASPIF. Returns

{:aspif      text or nil          ; nil when there is nothing to solve
 :stmts      [statement ...]      ; the structured program the clingo backend injects
 :table      the atom table
 :by-label   {label nogood}       ; violation atom -> the contradiction
 :assumptions [handle ...]        ; in content-key order
 :doomed     [nogood ...]}        ; all-fixed, unsatisfiable without solving

:tiebreak? (default true) emits the level-0 content-keyed objective, which makes the optimum unique; an enumeration turns it off (docs/asp.md, "Two things keep classify from reporting a tie as forced"). :keep-belief? (default true) emits the level-1 objective minimizing defeated assumptions; do/label :sat turns it off (docs/solving.md, "The three modes").