The nogood candidate index. Each family keeps its rows of one candidate index
(:nogood-candidates), which the placement detectors read; this namespace runs the
families as one index, holds the forced-monotonic roster, and decides a placed nogood
from its members' classes (verdict). See docs/nmtms.md, "A nogood placed as a
conclusion".
The nogood candidate index. Each family keeps its rows of one candidate index (`:nogood-candidates`), which the placement detectors read; this namespace runs the families as one index, holds the forced-monotonic roster, and decides a placed nogood from its members' classes (`verdict`). See docs/nmtms.md, "A nogood placed as a conclusion".
(arity-held? kb)Does the arity index keep a candidate or the binding of a pair (arity/held?), read
off the index as written, with no sync?
Does the arity index keep a candidate or the binding of a pair (`arity/held?`), read off the index as written, with no sync?
The engine's own roster, {kind #{predicate …}}: every family's :grounds and every
held-members member, held on every KB whether or not it is stated.
The engine's own roster, `{kind #{predicate …}}`: every family's `:grounds` and every
`held-members` member, held on every KB whether or not it is stated.(candidate-handles kb)Every handle some reader can read as a nogood member of a family.
Every handle some reader can read as a nogood member of a family.
(candidate? c h)Is h among candidate-handles of the candidate index c?
Is `h` among `candidate-handles` of the candidate index `c`?
(drop-memos)Empty sync-memo, and return nil. It is process-wide and holds the taxonomy value of
the last KB read, which holds a view of that KB, so it keeps its records and index
reachable until another KB is read; vaelii.core/close! calls this last. A KB still
open recomputes its entry on its next read.
Empty `sync-memo`, and return nil. It is process-wide and holds the taxonomy value of the last KB read, which holds a view of that KB, so it keeps its records and index reachable until another KB is read; `vaelii.core/close!` calls this last. A KB still open recomputes its entry on its next read.
(edge-reach tax since)What the genlCx edges moved after generation since reach, {:under :below}:
:under the contexts at or below a lower end tax/moves-since names, whose ancestor
sets the move changed, and :below, for each lower end and each active edge up from it,
the contexts a context at or below the lower end sees that the upper end does not;
{:all? true} when the relation was rebuilt, which restarts its generation. A
placement the move can create or retire lies in :under, and a common descendant there
is the most general one only when one of its ingredients is stated in :below: one
whose every ingredient the upper end sees has the upper end, above it, as a common
descendant. A removed or inactive edge reaches nothing in :below: the placements
resting on it leave with it, and their nogoods are queued again (negation/take-moved!,
membership/take-moved!, related/take-moved!). Read over the unscoped closures
(write-view), a superset over every reader.
What the `genlCx` edges moved after generation `since` reach, `{:under :below}`:
`:under` the contexts at or below a lower end `tax/moves-since` names, whose ancestor
sets the move changed, and `:below`, for each lower end and each active edge up from it,
the contexts a context at or below the lower end sees that the upper end does not;
`{:all? true}` when the relation was rebuilt, which restarts its generation. A
placement the move can create or retire lies in `:under`, and a common descendant there
is the most general one only when one of its ingredients is stated in `:below`: one
whose every ingredient the upper end sees has the upper end, above it, as a common
descendant. A removed or inactive edge reaches nothing in `:below`: the placements
resting on it leave with it, and their nogoods are queued again (`negation/take-moved!`,
`membership/take-moved!`, `related/take-moved!`). Read over the unscoped closures
(`write-view`), a superset over every reader.(exempt-at? kb ms up hidden?)Does a reader with ancestor set up read no conviction of the placed nogood over the
member handles ms: a membership nogood whose separation a siblingDisjointException
it sees removes (membership/exempt-at?), a contradicted orthogonal whose separation
such an exception removes (related/exempt-at?),
a determinant pair whose fillers it reads as one class (tuple/exempt-at?), or an
arity nogood it reads no binding for (arity/exempt-at?). hidden? names the handles
the reader does not believe or see, or is nil. False for any other nogood.
Does a reader with ancestor set `up` read no conviction of the placed nogood over the member handles `ms`: a membership nogood whose separation a `siblingDisjointException` it sees removes (`membership/exempt-at?`), a contradicted `orthogonal` whose separation such an exception removes (`related/exempt-at?`), a determinant pair whose fillers it reads as one class (`tuple/exempt-at?`), or an arity nogood it reads no binding for (`arity/exempt-at?`). `hidden?` names the handles the reader does not believe or see, or is nil. False for any other nogood.
(handles-at c up)The candidates of c, as synced answers it, stated in a context of the ancestor set
up or in none: every handle a reader with ancestor set up can read as a nogood
member, which a genlCx edge's placement pass reads (edge-reach).
The candidates of `c`, as `synced` answers it, stated in a context of the ancestor set `up` or in none: every handle a reader with ancestor set `up` can read as a nogood member, which a `genlCx` edge's placement pass reads (`edge-reach`).
The roster members no family reads among its grounds, each with the reason it is on the roster (docs/nmtms.md, "The forced-monotonic roster").
The roster members no family reads among its grounds, each with the reason it is on the roster (docs/nmtms.md, "The forced-monotonic roster").
(moves kb since)[c pos moved]: the candidate index as synced answers it, its journal position, and
the handles journaled since the position since (journal/since), which hold every
handle that entered or left the candidates since; nil when the journal does not reach
back to since, and a reader reads the index whole.
`[c pos moved]`: the candidate index as `synced` answers it, its journal position, and the handles journaled since the position `since` (`journal/since`), which hold every handle that entered or left the candidates since; nil when the journal does not reach back to `since`, and a reader reads the index whole.
(note-candidate! kb sx stored?)Keep :nogood-candidates in step with the fact sx arriving (stored? true) or
leaving. Runs at the store primitive and the removal choke point, after the index
write.
Keep `:nogood-candidates` in step with the fact `sx` arriving (`stored?` true) or leaving. Runs at the store primitive and the removal choke point, after the index write.
(note-except-target! kb h)An except of h arrived or left: queue h for the families whose placement reads
what a reader below the placement context hides (arity/note-except-target!).
An `except` of `h` arrived or left: queue `h` for the families whose placement reads what a reader below the placement context hides (`arity/note-except-target!`).
(offer! kb sxs)(offer! kb sxs only)Offer the stored facts sxs to the tuple candidates again (tuple/offer!), with
only :converse to the converse candidates alone.
Offer the stored facts `sxs` to the tuple candidates again (`tuple/offer!`), with `only` `:converse` to the converse candidates alone.
(on-roster? tax kind pred)Does pred carry the roster property kind (:forced-monotonic or
:forced-between-predicates): a baseline-roster member, or declared. The one reader
of the two properties, and a global one: the roster decides what a stored sentex is,
and that does not vary by the reader's visibility.
Does `pred` carry the roster property `kind` (`:forced-monotonic` or `:forced-between-predicates`): a `baseline-roster` member, or declared. The one reader of the two properties, and a global one: the roster decides what a stored sentex is, and that does not vary by the reader's visibility.
(placed-kind kb ms)The kind a nogood over the member handles ms placed as a conclusion reports under,
read off the members' sentences: :negation for a B beside (not B), the membership
family's kind (membership/kind-of), the related-types family's (related/kind-of),
the tuple families' (tuple/kind-of), the arity family's (arity/kind-of),
:inherited for a set the inherited detector found (inherited/inherited-clashes), or
nil for any other set.
The kind a nogood over the member handles `ms` placed as a conclusion reports under, read off the members' sentences: `:negation` for a `B` beside `(not B)`, the membership family's kind (`membership/kind-of`), the related-types family's (`related/kind-of`), the tuple families' (`tuple/kind-of`), the arity family's (`arity/kind-of`), `:inherited` for a set the inherited detector found (`inherited/inherited-clashes`), or nil for any other set.
(placements-owed? c)Is every placement owed: no placement pass has read the edge cursor since the
candidate index c was emptied (rebuild-candidates!, take-edge-cursor!)?
Is every placement owed: no placement pass has read the edge cursor since the candidate index `c` was emptied (`rebuild-candidates!`, `take-edge-cursor!`)?
(rebuild-candidates! kb)Recompute :nogood-candidates from storage, for recover: each family computes its
rows off the store (:recovered), and no record is read for a family that stores no
fact it reads.
Recompute `:nogood-candidates` from storage, for `recover`: each family computes its rows off the store (`:recovered`), and no record is read for a family that stores no fact it reads.
Every family, each a map of the parts the candidate index runs, w a write-view:
:grounds, {kind #{functor}}: the roster literals the family reads as stored
grounds rather than as members, under the roster kind that reads them
(:forced-between-predicates for a functor read only between predicate-spelled
arguments). Absent for a family that reads none.:note! (fn [kb w sx stored?]), at the store and removal choke points; absent for
a family the settle installs.:recovered (fn [kb w]): writes the rows the family computes off the store once
recover has emptied the index.:synced? (fn [tax c]) and :sync (fn [kb w c] c): rows derived from the
taxonomy, read again when it moved.:handles (fn [c]), every handle some reader can read as a member; :holds?
(fn [c h]) answers whether h is among them with a few map reads. Every update that
can move a handle into or out of it journals it (journal/note). Absent for the
negation family, whose members are an index family (reads/as-stored-opposed-in).
Every family places its nogoods as conclusions (chain/place-nogoods!).Every family, each a map of the parts the candidate index runs, `w` a `write-view`:
* `:grounds`, `{kind #{functor}}`: the roster literals the family reads as stored
grounds rather than as members, under the roster kind that reads them
(`:forced-between-predicates` for a functor read only between predicate-spelled
arguments). Absent for a family that reads none.
* `:note!` `(fn [kb w sx stored?])`, at the store and removal choke points; absent for
a family the settle installs.
* `:recovered` `(fn [kb w])`: writes the rows the family computes off the store once
recover has emptied the index.
* `:synced?` `(fn [tax c])` and `:sync` `(fn [kb w c] c)`: rows derived from the
taxonomy, read again when it moved.
* `:handles` `(fn [c])`, every handle some reader can read as a member; `:holds?`
`(fn [c h])` answers whether `h` is among them with a few map reads. Every update that
can move a handle into or out of it journals it (`journal/note`). Absent for the
negation family, whose members are an index family (`reads/as-stored-opposed-in`).
Every family places its nogoods as conclusions (`chain/place-nogoods!`).(roster tax kind)Every predicate on-roster? as kind.
Every predicate `on-roster?` as `kind`.
(roster-literal? tax literal)Is literal on the forced-monotonic roster: its functor is on-roster? as
:forced-monotonic, or as :forced-between-predicates with every argument spelled as a
predicate of arity 2 or more.
Is `literal` on the forced-monotonic roster: its functor is `on-roster?` as `:forced-monotonic`, or as `:forced-between-predicates` with every argument spelled as a predicate of arity 2 or more.
(synced kb)The candidate index after each family's rows derived from the taxonomy are read again
where it moved (:synced?, :sync), and its candidates by the context they are stated
in read again off the journal (journal/indexed, read by handles-at).
The candidate index after each family's rows derived from the taxonomy are read again where it moved (`:synced?`, `:sync`), and its candidates by the context they are stated in read again off the journal (`journal/indexed`, read by `handles-at`).
(take-edge-cursor! kb)[since first?]: the genlCx generation the last call read when it has moved since,
else nil, so tax/moves-since reads the edges moved after it (edge-reach); and
first?, true when no call has read it since the candidate index was emptied
(rebuild-candidates!), so every placement may be owed. The placement pass reads it
once (chain/place-nogoods!).
`[since first?]`: the `genlCx` generation the last call read when it has moved since, else nil, so `tax/moves-since` reads the edges moved after it (`edge-reach`); and `first?`, true when no call has read it since the candidate index was emptied (`rebuild-candidates!`), so every placement may be owed. The placement pass reads it once (`chain/place-nogoods!`).
(verdict class-of roster? members)The verdict on nogood members from class-of (handle -> defeat-class) and
roster? (handle -> boolean, is the member a roster literal): {:defeat h} for a
unique weakest defeasible member off the roster, :dilemma for a defeasible minimum two
such members share, and :hard when no member off the roster is defeasible. A roster
member is never a loser, whatever its class (docs/reference.md, item 7 of "The
function").
The verdict on nogood `members` from `class-of` (`handle -> defeat-class`) and
`roster?` (`handle -> boolean`, is the member a roster literal): `{:defeat h}` for a
unique weakest defeasible member off the roster, `:dilemma` for a defeasible minimum two
such members share, and `:hard` when no member off the roster is defeasible. A roster
member is never a loser, whatever its class (docs/reference.md, item 7 of "The
function").(write-view tax)The unscoped closures of tax, under their tax/…-global names, and tax itself as
:tax: the taxonomy a family keeps its rows through, handed to :note!, :recovered
and :sync. The rows are a superset over every reader, kept where no reader exists,
and each reader scopes what it reads.
The unscoped closures of `tax`, under their `tax/…-global` names, and `tax` itself as `:tax`: the taxonomy a family keeps its rows through, handed to `:note!`, `:recovered` and `:sync`. The rows are a superset over every reader, kept where no reader exists, and each reader scopes what it reads.
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 |