Rules
Rule statements have form
$$1␣H␣B$$
in which head $H$ has form
$$h␣m␣a_1␣ . . . ␣a_m$$
where $h ∈ {0, 1}$ determines whether the head is a disjunction or a choice, $m ≥ 0$ is the number of head elements, and each $a_i$ is an atom. Body $B$ has one of two forms:
Normal bodies have form
$$0␣n␣l_1␣ . . . ␣l_n$$
where $n ≥ 0$ is the length of the rule body, and each $l_i$ is a literal.
Weight bodies have form
$$1␣l␣n␣l_1␣w_1␣ . . . ␣l_n␣w_n$$
where $l$ is a positive integer to denote the lower bound, $n ≥ 0$ is the number of literals in the rule body, and each $l_i$ and $w_i$ are a literal and a positive integer.
Minimize Statements
Minimize statements have form
$$2␣p␣n␣l_1␣w_1␣\ldots␣l_n␣w_n$$
where $p$ is an integer priority, $n ≥ 0$ is the number of weighted literals, each $l_i$ is a literal,
and each $w_i$ is an integer weight.
Projection Statements
Projection statements have form
$$3␣n␣a_1␣ . . . ␣a_n$$
where $n ≥ 0$ is the number of atoms, and each $a_i$ is an atom.
Output Statements
Output statements have form
$$4␣m␣s␣n␣l_1␣ . . . ␣l_n$$
where $n ≥ 0$ is the length of the condition, each $l_i$ is a literal, and $m ≥ 0$ is an integer indicating the length in bytes of string s (where s excludes byte zero and newline).
External Statements
External statements result from #external directives and have form
$$5␣a␣v$$
where a is an atom, and $v ∈ {0, 1, 2, 3}$ indicates free, true, false, and release.
Assumptions Statements
Assumption statements have form
$$6␣n␣l_1␣ . . . ␣l_n$$
where $n ≥ 0$ is the number of literals, and each $l_i$ is a literal.
Heuristic Statements
Heuristic statements have form
$$7␣m␣a␣k␣p␣n␣l_1␣ . . . ␣l_n$$
where $m ∈ {0, \ldots, 5}$ stands for the $(m+1)\text{th}$ heuristic modifier among level, sign, factor, init, true, and false, $a$ is an atom, $k$ is an integer, $p$ is a non-negative integer priority, $n ≥ 0$ is the number of literals in the condition, and the literals $l_i$ are the condition under which the heuristic modification should be applied.
Edge Statements
Edge statements have form
$$8␣u␣v␣n␣l_1␣ . . . ␣l_n$$
where $u$ and $v$ are integers representing an edge from node $u$ to node $v$, $n ≥ 0$ is the length of the condition, and the literals $l_i$ are the condition for the edge to be present.
Theory Terms
Numeric theory terms, symbolic theory terms, and compound theory terms (including tuples, lists, and sets), are represented using the following statements:
$$9␣0␣u␣w$$
$$9␣1␣u␣n␣s$$
$$9␣2␣u␣t␣n␣u_1␣ . . . ␣u_n$$
where $n ≥ 0$ is a length, index $u$ is a non-negative integer, integer $w$ represents a numeric term, string s of length $n$ represents a symbolic term (including functions) or an operator, integer t is either $-1$, $-2$, or $-3$ for tuple terms in parentheses, braces, or brackets, respectively, or an index of a symbolic term or operator, and each $u_i$ is an integer for a theory term.
Theory Atoms
Theory elements, atoms without guards, and atoms with guards are represented using the following statements:
$$9␣4␣v␣n␣u_1␣ . . . ␣u_n␣m␣l_1␣ . . . ␣l_m$$
$$9␣5␣a␣p␣n␣v_1␣ . . . ␣v_n$$
$$9␣6␣a␣p␣n␣v_1␣ . . . ␣v_n␣g␣u_1$$
where $n ≥ 0$ and $m ≥ 0$ are lengths, index $v$ is a non-negative integer, $a$ is an atom or $0$ for directives, each $u_i$ is an integer for a theory term, each $l_i$ is an integer for a literal, integer $p$ refers to a symbolic term, each $v_i$ is an integer for a theory atom element, and integer $g$ refers to a theory operator.
Comment Statements
Comments have form
$$10␣s$$
where $s$ is a string not containing a newline.
