vaelii.impl.asp.aspif — com.vaelii/vaelii 0.29.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 the statements the engine's programs use: the rule line (type 1) as facts, choice atoms, normal rules, integrity constraints, and weight-body rules and constraints; minimize (2); and output (4). Projection (3), externals (5), assumptions (6), heuristics (7), acyclicity edges (8) and type 1's disjunctive and multi-head choice heads have no encoder (docs/defenses.md, "The ASPIF emitter encodes only what a program uses").

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. A show statement's length counts characters, so its text must be ASCII.

The statement constructors return data maps, and render turns a sequence of them into the ASPIF text.

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.