vaelii.impl.dense-jtms — com.vaelii/vaelii 0.1.0

The dense truth-maintenance network — the :tms :dense option, off by default.

The JTMS is always resident, so its footprint is a wall in its own right (measured: ~467 B/node, which is ~43 GB at 100M nodes), and the decomposition (lein bench-jtms) says exactly where the bytes are:

  nodes  71%   <- 310 B/node of it is the per-node MAP OBJECT and its HAMT slot
  in     13%   <- 100% dense; RoaringBitmap measured 384x here
  groundable 13%

Two findings shape everything below. The per-node scalars are already free — stripping :depth, :premise? or :datum from the reference releases nothing, because they are shared cached objects (small Longs, keywords, booleans). So the lever is not "shrink the fields", it is "stop having a map per node": a node here is a bit in a bitmap and, where it has one, an entry in a primitive-keyed map. And belief sets are the opposite regime from the index's postings — bench-postings found RoaringBitmap a loss (1.07-1.45x) on the index's millions of tiny postings, while :in holds nearly every node and compresses 384x. Both measurements are right; density is the variable.

  nodes / premises / in / groundable / defeated / blocked
  touched / touched-in                                       RoaringBitmap
  depths                                    Int2IntOpenHashMap  (absent => 0)
  supports / consequences   Int2ObjectOpenHashMap<IntPostings>  (absent => empty)
  a justification            columns keyed by id, never an object  (see below)
  superseded                             atom of a persistent map  (sparse)

Two of those deserve their reasons. The defeat-classes are one bitmap because the lattice has exactly two elements (vaelii.impl.strength — monotonic > default, and the reference already stores only the entries above the bottom), so "the class map" is precisely "the set of monotonic datums". Adjacency reuses Phase 1's IntPostings (a sorted int[] promoted to a bitmap past 128) rather than a bare int[]: a node's supports are usually one or two, but the consequences of a much-used premise — a rule handle is an antecedent of every justification it licensed — grow without bound, and an array-copy insert would make loading such a rule quadratic.

Why this is a second implementation and not a swap

RoaringBitmap is mutable, and the reference is an atom over one persistent map whose all-or-nothing mutation jtms_atomicity_test pins. A mutable bitmap inside that value would break swap!'s retry semantics and let a reader observe a half-applied relabel — so the dense structures cannot be dropped into the reference, and the two ship side by side behind vaelii.impl.jtms/Tms. That is the same shape the index took (:memory-columnar is a whole second trie beside KvIndexStore), and it carries the same obligation: the algorithms are duplicated here against the dense structures, so jtms_dense_oracle_test proves the two answer identically under randomized operation streams before either is trusted.

Concurrency. Writers are serialized on a monitor, so concurrent mutations compose exactly as the reference's swap! retry does. Readers are not locked: under the engine's one-writer contract (docs/storage.md) there is no reader to protect, and locking in? — the single hottest call in the engine — to buy a guarantee nothing relies on would be a poor trade. A reader racing a writer may therefore see a partially-applied relabel, which is the same latitude the mutable index backends take.

Precondition. ensure-node precedes add-justification, and a justification's antecedents already have nodes — which every engine path does. (The reference tolerates the violation by growing a malformed phantom node; neither implementation is specified there.)

create-dense-tms clj

(create-dense-tms)

A fresh, empty dense truth-maintenance network — vaelii.impl.jtms/create-tms's counterpart, selected by open-kb's {:tms :dense}.