The dense truth-maintenance network, :tms :dense, the default. A node is a bit in a bitmap
and, where it has one, an entry in a primitive-keyed map, instead of a map per node
(docs/density.md, Phase 3).
nodes / premises / in / blocked / forced mono, out, void, held touched / touched-in / touched-new / touched-out RoaringBitmap depths Int2IntOpenHashMap (absent => 0) supports / consequences Int2ObjectOpenHashMap<IntPostings> (absent => empty) a justification columns keyed by id, never an object superseded atom of a persistent map (sparse)
The depths, the two adjacency maps and the three justification columns are reached
through the TmsColumns interface, which HeapColumns implements with the fastutil maps,
so every relabel, sweep and mutation is written once against the interface. The defeat
classes are one bitmap because the lattice has two elements.
Concurrency: a StampedLock gives a reader beside the writer a consistent snapshot.
Writers take the write lock. Point reads (in?) are optimistic, validated after the fact
and redone under the shared read lock if a write intervened; iterating reads take the
shared lock. The lock is non-reentrant, so every protocol method takes it once and calls
only raw-field helpers, and every read body is side-effect-free.
ensure-node precedes add-justification, and a justification's antecedents already have
nodes. Handles and justification ids must fit a 32-bit int; crossing 2^31-1 throws
:type :handle-ceiling with :remedy {:tms :reference} (check-handle!).
jtms_dense_oracle_test proves the two networks answer identically. See docs/nmtms.md,
"Two representations of the same network".
The dense truth-maintenance network, `:tms :dense`, the default. A node is a bit in a bitmap
and, where it has one, an entry in a primitive-keyed map, instead of a map per node
(docs/density.md, Phase 3).
nodes / premises / in / blocked / forced mono, out, void, held
touched / touched-in / touched-new / touched-out RoaringBitmap
depths Int2IntOpenHashMap (absent => 0)
supports / consequences Int2ObjectOpenHashMap<IntPostings> (absent => empty)
a justification columns keyed by id, never an object
superseded atom of a persistent map (sparse)
The depths, the two adjacency maps and the three justification columns are reached
through the `TmsColumns` interface, which `HeapColumns` implements with the fastutil maps,
so every relabel, sweep and mutation is written once against the interface. The defeat
classes are one bitmap because the lattice has two elements.
Concurrency: a `StampedLock` gives a reader beside the writer a consistent snapshot.
Writers take the write lock. Point reads (`in?`) are optimistic, validated after the fact
and redone under the shared read lock if a write intervened; iterating reads take the
shared lock. The lock is non-reentrant, so every protocol method takes it once and calls
only raw-field helpers, and every read body is side-effect-free.
`ensure-node` precedes `add-justification`, and a justification's antecedents already have
nodes. Handles and justification ids must fit a 32-bit int; crossing 2^31-1 throws
`:type :handle-ceiling` with `:remedy {:tms :reference}` (`check-handle!`).
`jtms_dense_oracle_test` proves the two networks answer identically. See docs/nmtms.md,
"Two representations of the same network".(before-network this)this as it stood when the open write record opened its entry for it
(begin-record!), as a read-only Tms, or this itself when the record holds none.
A value no move recorded is read off the live network, which no move since changed.
Answers the reads the read walk makes: labels, classes, premise marks, nodes, the
support and dependent ids, justifications, the blocked and forced sets and the
supersession map. Every other method throws.
`this` as it stood when the open write record opened its entry for it (`begin-record!`), as a read-only `Tms`, or `this` itself when the record holds none. A value no move recorded is read off the live network, which no move since changed. Answers the reads the read walk makes: labels, classes, premise marks, nodes, the support and dependent ids, justifications, the blocked and forced sets and the supersession map. Every other method throws.
(copy-into! target src)Copy every structure of dense network src into target, which must hold no node,
under target's write lock. read-image! reads into a fresh network and this moves
the result into the one a KB already holds: the KB holds its network by identity, so an
image cannot replace the object, and reading into a scratch network first means a
truncated image leaves the KB's network untouched.
Copy every structure of dense network `src` into `target`, which must hold no node, under `target`'s write lock. `read-image!` reads into a fresh network and this moves the result into the one a KB already holds: the KB holds its network by identity, so an image cannot replace the object, and reading into a scratch network first means a truncated image leaves the KB's network untouched.
(create-dense-tms)A fresh, empty dense truth-maintenance network — vaelii.impl.jtms/create-tms's
counterpart, selected by open-kb's {:tms :dense}.
A fresh, empty dense truth-maintenance network — `vaelii.impl.jtms/create-tms`'s
counterpart, selected by `open-kb`'s `{:tms :dense}`.The byte image's layout number. read-image! refuses any other, so an image of
another layout is discarded rather than misread.
The byte image's layout number. `read-image!` refuses any other, so an image of another layout is discarded rather than misread.
(moved-between a b)What replacing dense network a with b moves, as {:moved bitmap :was-in bitmap}.
:moved holds the handles with a node or an IN label in one network and not the other,
and :was-in holds those of them IN in a. Each network is read under its own read
lock.
What replacing dense network `a` with `b` moves, as `{:moved bitmap :was-in bitmap}`.
`:moved` holds the handles with a node or an IN label in one network and not the other,
and `:was-in` holds those of them IN in `a`. Each network is read under its own read
lock.(node-count t)How many nodes dense network t holds — the bitmap's cardinality, read under a read
lock without materializing a handle.
How many nodes dense network `t` holds — the bitmap's cardinality, read under a read lock without materializing a handle.
(read-image! t i)Read an image write-image wrote from i into dense network t, which must hold no
node. Throws IllegalStateException for a populated t and
IllegalArgumentException for bytes that are not an image of image-version; both are
a caller's error rather than a state of the KB, since vaelii.impl.reasoning-image checks
the manifest before it reads a byte.
Read an image `write-image` wrote from `i` into dense network `t`, which must hold no node. Throws `IllegalStateException` for a populated `t` and `IllegalArgumentException` for bytes that are not an image of `image-version`; both are a caller's error rather than a state of the KB, since `vaelii.impl.reasoning-image` checks the manifest before it reads a byte.
(record-mismatch t sentexes justifications premises)Where dense network t and a record store's handle sets disagree, or nil:
[:sentex h] for a node sentexes lacks, [:justification h] for a justification
justifications lacks, and [:premise h] for a node that is a premise in one of t
and premises and not in the other. Each set is a java.util.Set of Long handles, as
p/sentex-ids answers. One pass over t's node, justification and premise bitmaps and
over premises, under a read lock.
Where dense network `t` and a record store's handle sets disagree, or nil: `[:sentex h]` for a node `sentexes` lacks, `[:justification h]` for a justification `justifications` lacks, and `[:premise h]` for a node that is a premise in one of `t` and `premises` and not in the other. Each set is a `java.util.Set` of Long handles, as `p/sentex-ids` answers. One pass over `t`'s node, justification and premise bitmaps and over `premises`, under a read lock.
(unsupported-nodes t)The nodes of dense network t that are no premise and that no justification
concludes, ascending, as Longs: the premise bitmap subtracted from the node bitmap, then
one supports probe per remaining node, under a read lock.
The nodes of dense network `t` that are no premise and that no justification concludes, ascending, as Longs: the premise bitmap subtracted from the node bitmap, then one supports probe per remaining node, under a read lock.
(write-image t o)Write the whole of dense network t to o, under a read lock, so a concurrent reader
is not held up and a writer waits for the image to finish.
Write the whole of dense network `t` to `o`, under a read lock, so a concurrent reader is not held up and a writer waits for the image to finish.
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 |