vaelii.impl.asp.aspif — com.vaelii/vaelii 0.18.0

Pure ASPIF text emitter. No vaelii deps, no I/O.

ASPIF is the Potassco Answer Set Programming Intermediate Format, the ground-program protocol between gringo and clasp.

This emits what the engine's programs are built from, and no more: the rule line (type 1) as facts, choice atoms, normal rules and integrity constraints, weight-body rules and constraints (the cardinality bound a asp/atMost / asp/atLeast translates to), plus minimize (2) and output (4).

The rest of the format — projection (3), externals (5), assumptions (6), heuristics (7), acyclicity edges (8), and type 1's disjunctive and multi-head choice heads — has no encoder here. An encoder nobody executes is not coverage of a format; it is unverified text generation claiming to be. What the engine needs, it emits and its tests exercise, and nothing else is written here.

Wire format of what is emitted (line-oriented, space-separated): Line 1: asp 1 0 0 Rule: 1 <head_type> <head_size> <head...> <body_type> <body_size> <lits...> head_type = 0 disjunctive | 1 choice body_type = 0 normal (list of signed literals) or = 1 weight (a cardinality/weight body) body literal: +atom for positive, -atom for default-negated Weight body: 1 <lower_bound> <n> <lit_1> <w_1> ... <lit_n> <w_n> satisfied when the summed weight of the satisfied literals is at least <lower_bound>. A cardinality constraint is the unit-weight case: k+1 <= #count{ ... } is a weight body of bound k+1 over weight-1 literals. Emitted headless (an integrity constraint that excludes any model reaching the bound) or with a head (an atom that holds when the bound is reached, for a soft/minimized violation). Minimize: 2 <priority> <n> <lit_1> <w_1> ... <lit_n> <w_n> Output: 4 <str_len> <str> <n_conditions> <atoms...> End: 0

Atom ids are positive integers; 0 is the terminator and must not appear as an atom. String lengths in show statements count bytes (equal to character count for ASCII); non-ASCII names need UTF-8 byte counting which we do not currently handle.

The public API has two halves:

(1) Statement constructors (fact, choice, rule, constraint, minimize, show) that return plain data maps. Data form is inspectable, easy to assemble programmatically, and trivial to unit-test.

(2) render turns a sequence of statements into the full ASPIF text with header and terminator.

choice clj

(choice atom-id)

Choice atom {atom-id}. — solver may include it or not.

constraint clj

(constraint body)

Integrity constraint :- body. Forbids models in which every body literal is satisfied.

fact clj

(fact atom-id)

Unconditional fact: atom-id is true in every model.

minimize clj

(minimize priority weighted-literals)

Weak constraint (minimize statement). weighted-literals is a seq of [literal weight] pairs. Priorities combine lexicographically when multiple minimize statements are present; within a priority, the cost is the sum of weights of satisfied literals.

render clj

(render statements)

Render a sequence of statements as a complete ASPIF program string with header and terminator. The input order is preserved.

rule clj

(rule head body)

Normal rule head :- body. body is a seq of signed literals (positive atom-id or negative for default negation).

show clj

(show atom-id text)

Output mapping atom-id to text in solver output. text must be ASCII and must not contain newline characters.

weight-constraint clj

(weight-constraint lower-bound weighted-literals)

Integrity constraint with a weight body: :- lower-bound <= #sum{ ... }. Forbids models in which the summed weight of the satisfied body literals reaches lower-bound. weighted-literals is a seq of [literal weight] pairs (a literal is a positive atom-id or negative for default negation).

A cardinality bound is the unit-weight case: at-most-k over atoms M forbids k+1 of them holding — bound k+1 over each [m 1]; at-least-k forbids |M|-k+1 of them absent — bound |M|-k+1 over each [-m 1].

weight-rule clj

(weight-rule head lower-bound weighted-literals)

Normal rule head :- lower-bound <= #sum{ ... } with a weight body: head holds when the summed weight of the satisfied body literals reaches lower-bound. The soft counterpart to weight-constraint — the derived head is a violation atom a minimize then penalizes, so breaching the bound costs rather than excludes.