Bidirectional atom id table for ASPIF translation.
ASPIF atoms are positive integers; every entity referenced in the emitted program — sentex or contradiction marker — needs a unique id. Atom 0 is reserved as the ASPIF terminator and is never allocated.
The table maps three kinds of source values to atom ids, sharing a single counter so ids are unique across kinds:
(1) sentex ids — the :id field of a vaelii sentex record. These become the atoms the ASP solver reasons about.
(2) contradiction descriptors — nested sentence-shaped Clojure
values of the form
(contradiction <head> :involved [[:sentex H1] [:sentex H2] …])
where <head> is a sentence-shaped tag (e.g. (negation S),
(disjointTypes ent t-a t-b), or a user-named head emitted by
a grounding rule like (wrongBulbCount 3 4)) and :involved
lists the sentex handles that participated. Atoms backed by
contradiction descriptors get weight in the minimize statement;
the solver avoids models in which they are true.
(3) aux descriptors — auxiliary atoms used by translators (e.g. the
count ≥ N heads of cardinality weight rules). They are
distinct from contradictions: the minimize statement does not
weight them, and clasp witnesses ignore them when reconstructing
contradictions for callers.
Labels are short string identifiers that appear in clasp's witness output; we read them back during result parsing to recover the originating sentex or contradiction. Format:
s<sentex-id> — sentex-backed atoms c<atom-id> — contradiction-backed atoms a<atom-id> — aux-backed atoms
Using s/c prefixes keeps the two namespaces distinct even if a
sentex id happens to numerically match a contradiction atom id.
The table is a clojure.core/atom wrapping a plain map. Intern operations use swap! for atomicity; lookups are pure derefs. All intern operations are idempotent.
Bidirectional atom id table for ASPIF translation.
ASPIF atoms are positive integers; every entity referenced in the
emitted program — sentex or contradiction marker — needs a unique id.
Atom 0 is reserved as the ASPIF terminator and is never allocated.
The table maps three kinds of source values to atom ids, sharing a
single counter so ids are unique across kinds:
(1) sentex ids — the :id field of a vaelii sentex record. These
become the atoms the ASP solver reasons about.
(2) contradiction descriptors — nested sentence-shaped Clojure
values of the form
(contradiction <head> :involved [[:sentex H1] [:sentex H2] …])
where `<head>` is a sentence-shaped tag (e.g. `(negation S)`,
`(disjointTypes ent t-a t-b)`, or a user-named head emitted by
a grounding rule like `(wrongBulbCount 3 4)`) and `:involved`
lists the sentex handles that participated. Atoms backed by
contradiction descriptors get weight in the minimize statement;
the solver avoids models in which they are true.
(3) aux descriptors — auxiliary atoms used by translators (e.g. the
`count ≥ N` heads of cardinality weight rules). They are
distinct from contradictions: the minimize statement does not
weight them, and clasp witnesses ignore them when reconstructing
contradictions for callers.
Labels are short string identifiers that appear in clasp's witness
output; we read them back during result parsing to recover the
originating sentex or contradiction. Format:
s<sentex-id> — sentex-backed atoms
c<atom-id> — contradiction-backed atoms
a<atom-id> — aux-backed atoms
Using `s`/`c` prefixes keeps the two namespaces distinct even if a
sentex id happens to numerically match a contradiction atom id.
The table is a clojure.core/atom wrapping a plain map. Intern
operations use swap! for atomicity; lookups are pure derefs. All
intern operations are idempotent.(atom-of-label table label)Reverse: given a label string (from a clasp witness), return the atom id, or nil if the label is unknown.
Reverse: given a label string (from a clasp witness), return the atom id, or nil if the label is unknown.
(atom-of-sentex table sentex-id)Atom id for sentex-id, or nil if not yet interned.
Atom id for `sentex-id`, or nil if not yet interned.
(contradiction-of-atom table atom-id)Contradiction descriptor backing atom-id, or nil.
Contradiction descriptor backing `atom-id`, or nil.
(count-atoms table)Number of atoms allocated so far.
Number of atoms allocated so far.
(intern-aux! table descriptor)Ensure descriptor has an atom id, allocated in the aux namespace
(distinct from contradictions — aux atoms are translator scratch
space and do not appear in the minimize statement). descriptor
must be an equality-comparable Clojure value.
Ensure `descriptor` has an atom id, allocated in the aux namespace (distinct from contradictions — aux atoms are translator scratch space and do not appear in the minimize statement). `descriptor` must be an equality-comparable Clojure value.
(intern-contradiction! table descriptor)Ensure descriptor has an atom id. descriptor is the nested
sentence-shaped value
(contradiction <head> :involved [[:sentex H1] [:sentex H2] …])
so consumers can introspect a witness's contradiction atoms without
secondary queries.
Ensure `descriptor` has an atom id. `descriptor` is the nested sentence-shaped value (contradiction <head> :involved [[:sentex H1] [:sentex H2] …]) so consumers can introspect a witness's contradiction atoms without secondary queries.
(intern-sentex! table sentex-id)Ensure the sentex with id sentex-id has an atom id. Returns the
atom id. Idempotent. Callers that have a sentex record should pass
(sentex/id sentex).
Ensure the sentex with id `sentex-id` has an atom id. Returns the atom id. Idempotent. Callers that have a sentex record should pass `(sentex/id sentex)`.
(label-of-atom table atom-id)Label string for atom-id, or nil.
Label string for `atom-id`, or nil.
(new-table)Return a fresh empty atom table.
Return a fresh empty atom table.
(sentex-id-of-atom table atom-id)The sentex id backing atom-id, or nil if the atom is not sentex-backed.
The sentex id backing `atom-id`, or nil if the atom is not sentex-backed.
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 |