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 two kinds of source value 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.
Two kinds because two are what the translator emits: every atom in a
program stands for a contested assumption or for a violation. A third
namespace for translator scratch would be an interning path nothing
calls, which is the same unverified machinery aspif keeps out of the
emitter.
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
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 two kinds of source value 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.
Two kinds because two are what the translator emits: every atom in a
program stands for a contested assumption or for a violation. A third
namespace for translator scratch would be an interning path nothing
calls, which is the same unverified machinery `aspif` keeps out of the
emitter.
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
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-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 |