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, 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 and weight bodies — was written out here once and never emitted, so nothing ever called it and no test ever checked it. An encoder nobody has executed is not coverage of a format; it is unverified text generation claiming to be. What the engine needs, it emits and its tests exercise; another type arrives with the caller that wants it.
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)
body literal: +atom for positive, -atom for default-negated
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.
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, 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 and weight bodies — was written out here
once and never emitted, so nothing ever called it and no test ever
checked it. An encoder nobody has executed is not coverage of a
format; it is unverified text generation claiming to be. What the
engine needs, it emits and its tests exercise; another type arrives
with the caller that wants it.
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)
body literal: +atom for positive, -atom for default-negated
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 atom-id)Choice atom {atom-id}. — solver may include it or not.
Choice atom `{atom-id}.` — solver may include it or not.
(constraint body)Integrity constraint :- body. Forbids models in which every body
literal is satisfied.
Integrity constraint `:- body`. Forbids models in which every body literal is satisfied.
(fact atom-id)Unconditional fact: atom-id is true in every model.
Unconditional fact: `atom-id` is true in every model.
(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.
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 statements)Render a sequence of statements as a complete ASPIF program string with header and terminator. The input order is preserved.
Render a sequence of statements as a complete ASPIF program string with header and terminator. The input order is preserved.
(rule head body)Normal rule head :- body. body is a seq of signed literals
(positive atom-id or negative for default negation).
Normal rule `head :- body`. `body` is a seq of signed literals (positive atom-id or negative for default negation).
(show atom-id text)Output mapping atom-id to text in solver output. text must be
ASCII and must not contain newline characters.
Output mapping `atom-id` to `text` in solver output. `text` must be ASCII and must not contain newline characters.
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |