vaelii.impl.asp.aspif — com.vaelii/vaelii 0.1.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. We emit the full set of ground statement types: facts, normal rules, single- and multi-head choice atoms/rules, disjunctive heads, integrity constraints, weight/cardinality bodies, minimize (weak constraints), show output, projection (type 3), externals (type 5), assumptions (type 6), heuristics (type 7), and acyclicity edges (type 8).

Wire format (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 head_size may exceed 1 (disjunction a|b, choice {a;b;c}) body_type = 0 normal (list of signed literals) = 1 weight body — see below body literal: +atom for positive, -atom for default-negated Weight rule: 1 <head_type> <head_size> <head...> 1 <lower_bound> <body_size> <lit_1> <w_1> ... <lit_n> <w_n> head fires when the sum of weights of satisfied body literals is at least <lower_bound>. Cardinality is the all-weights-equal-1 special case. Minimize: 2 <priority> <n> <lit_1> <w_1> ... <lit_n> <w_n> Project: 3 <n> <atoms...> Output: 4 <str_len> <str> <n_conditions> <atoms...> External: 5 <atom> <init> init = 0 free | 1 true | 2 false | 3 release Assume: 6 <n> <signed_lits...> (static assumption block) Heuristic:7 <modifier> <atom> <value> <priority> <body_size> <lits...> modifier = 0 level | 1 sign | 2 factor | 3 init | 4 true | 5 false Edge: 8 <u> <v> <body_size> <lits...> (acyclicity edge u→v) End: 0

ASPIF has no native bound on a choice head (lb {…} ub); a bound is expressed by putting weight-rule + integrity-constraint cardinality enforcement beside a multi-head choice, the same way gringo does.

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, 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.

assume clj

(assume signed-literals)

Static assumption block over signed-literals (positive atom id to assume true, negative to assume false), baked into the loaded program. For per-call assumptions in-process, use the solve-time assumptions argument instead; this line is primarily for the clasp fallback path.

choice clj

(choice atom-id)

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

choice-rule clj

(choice-rule head body)

Choice rule {head} :- body. Solver may include head if the body holds.

choices clj

(choices head-atoms body)

Multi-head choice rule {a; b; c} :- body. The solver may include any subset of head-atoms when body holds. A single-atom head is equivalent to choice-rule.

constraint clj

(constraint body)

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

disjunction clj

(disjunction head-atoms body)

Disjunctive rule a | b | … :- body. head-atoms is a seq of positive atom ids; the solver must make at least one of them true when body holds. A single-atom head is equivalent to rule.

edge clj

(edge u v body)

Acyclicity edge #edge (u, v) : body between node ids u and v. The solver rejects answer sets whose active edges form a cycle. body is a seq of signed literals gating the edge (empty = always).

external clj

(external atom-id & [init])

#external atom-id with initial truth init (:free / :true / :false / :release; default :false). The atom is exempt from the closed-world default and its truth can be assigned at solve time.

fact clj

(fact atom-id)

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

heuristic clj

(heuristic modifier atom-id value priority body)

#heuristic atom-id [value@priority, modifier] : body. Steers the solver's search: modifier is one of :level / :sign / :factor / :init / :true / :false; value and priority are integers; body is a seq of signed literals gating the directive (empty = unconditional).

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.

project clj

(project atoms)

Projection statement #project { atoms }. Restricts enumeration / answer-set output to the listed atoms.

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-rule clj

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

Weight rule head :- LB { L1 = w1 ; L2 = w2 ; … }. The head atom is derived when the sum of weights of satisfied body literals is at least lower-bound. For cardinality use weight 1 on every literal; lower-bound then becomes the cardinality lower bound.

weighted-literals is a seq of [signed-atom-id weight] pairs. Signs work the same as in normal bodies (negative atom id means default negation).