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".
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? kb c h)Is h among candidate-handles of the candidate index c of kb?
Is `h` among `candidate-handles` of the candidate index `c` of `kb`?
(declared tax){[kind pred] {handle context}}: every predicate on the roster by a believed
declaration and off the global roster (global?), with its declarations. Empty on a
KB that declares only baseline members. Read KB-wide, the union over every reader,
which a read walk splits into the declarations its reader sees and misses.
`{[kind pred] {handle context}}`: every predicate on the roster by a believed
declaration and off the global roster (`global?`), with its declarations. Empty on a
KB that declares only baseline members. Read KB-wide, the union over every reader,
which a read walk splits into the declarations its reader sees and misses.(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.
(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?),
or a determinant pair whose fillers it reads as one class (tuple/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?`), or a determinant pair whose fillers it reads as one class (`tuple/exempt-at?`). `hidden?` names the handles the reader does not believe or see, or is nil. False for any other nogood.
(global-reading tax)The roster reading (fn [kind pred]) every reader shares (global?).
The roster reading `(fn [kind pred])` every reader shares (`global?`).
(global? _tax kind pred)Is pred on the global roster as kind: a baseline-roster member. Every reader
reads it on the roster, and no declaration moves it. A declaration in any context,
CxUniverse's included, puts its predicate on the roster at the readers that believe it
(on-roster?, docs/nmtms.md, "The forced-monotonic roster").
Is `pred` on the global roster as `kind`: a `baseline-roster` member. Every reader reads it on the roster, and no declaration moves it. A declaration in any context, CxUniverse's included, puts its predicate on the roster at the readers that believe it (`on-roster?`, docs/nmtms.md, "The forced-monotonic roster").
(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
(special/drain-context-moves!).
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 (`special/drain-context-moves!`).
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").
(literal-declarations tax literal){handle context} of the stored declarations that put literal on the roster and
are not global?: empty when the global roster holds literal or no declaration
does.
`{handle context}` of the stored declarations that put `literal` on the roster and
are not `global?`: empty when the global roster holds `literal` or no declaration
does.(literal-roster tax literal)How literal is on the roster over every reader (roster-literal?), or nil when it is
not: {:predicate f :kind k :global? g :declarations {handle context}}. kind is the
roster property f carries, global? whether baseline-roster holds it, and
declarations the stored declarations giving it, a global? member's included.
How `literal` is on the roster over every reader (`roster-literal?`), or nil when it is
not: `{:predicate f :kind k :global? g :declarations {handle context}}`. `kind` is the
roster property `f` carries, `global?` whether `baseline-roster` holds it, and
`declarations` the stored declarations giving it, a `global?` member's included.(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.
(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)(on-roster? tax kind pred seen?)Does pred carry the roster property kind (:forced-monotonic or
:forced-between-predicates). The 3-arity is the union over every reader: global?,
or a believed declaration in any context. The 4-arity is one reader's: global?, or
a declaration [handle context] seen? holds of.
Does `pred` carry the roster property `kind` (`:forced-monotonic` or `:forced-between-predicates`). The 3-arity is the union over every reader: `global?`, or a believed declaration in any context. The 4-arity is one reader's: `global?`, or a declaration `[handle context]` `seen?` holds of.
(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!`)?
(reader-reading tax seen?)The roster reading (fn [kind pred]) of a reader that sees the declarations [handle context] seen? holds of (on-roster?, 4-arity).
The roster reading `(fn [kind pred])` of a reader that sees the declarations `[handle context]` `seen?` holds of (`on-roster?`, 4-arity).
(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 [kb c]), every handle some reader can read as a member; :holds?
(fn [kb c h]) answers whether h is among them with a few map reads, or off the
index for a member the family reads there (the related-types family's cover pairs). 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 [kb c])`, every handle some reader can read as a member; `:holds?`
`(fn [kb c h])` answers whether `h` is among them with a few map reads, or off the
index for a member the family reads there (the related-types family's cover pairs). 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, over every reader.
Every predicate `on-roster?` as `kind`, over every reader.
(roster-literal? tax literal)(roster-literal? _tax literal on?)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. The 2-arity reads the union over every reader; the
3-arity reads the roster reading on? (global-reading, reader-reading).
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. The 2-arity reads the union over every reader; the 3-arity reads the roster reading `on?` (`global-reading`, `reader-reading`).
(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; and
first?, true when no call has read it since the candidate index was emptied
(rebuild-candidates!), so every placement may be owed. The settle's drain reads it
once a pass (special/drain-context-moves!).
`[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; and `first?`, true when no call has read it since the candidate index was emptied (`rebuild-candidates!`), so every placement may be owed. The settle's drain reads it once a pass (`special/drain-context-moves!`).
(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 |