A rule is a sentex — same structure (sentence + context), different indexing. Its sentence is an implication:
(implies (and <antecedent> ...) <consequent>) ; single antecedent needs no and
Antecedents and consequent are sentence patterns that may contain variables. Rules are indexed by their antecedent/consequent predicates (see the index store) so forward chaining finds candidate rules without scanning, and — being ordinary sentexes — they get handles, TMS support, and retraction for free.
Rules must be range-restricted: every consequent variable appears in some
antecedent, so a fired consequent is ground. The one exemption is a head
existential (exists ?y C), whose marked variable forward firing skolemizes
(docs/skolem.md). The same closure is required of an exceptWhen exception, which is a
query rather than a conclusion but must be ground for the same reason (checked at the
assert layer via sentex/check-exception-closed).
A rule *is* a sentex — same structure (sentence + context), different indexing. Its sentence is an implication: (implies (and <antecedent> ...) <consequent>) ; single antecedent needs no `and` Antecedents and consequent are sentence patterns that may contain variables. Rules are indexed by their antecedent/consequent predicates (see the index store) so forward chaining finds candidate rules without scanning, and — being ordinary sentexes — they get handles, TMS support, and retraction for free. Rules must be range-restricted: every consequent variable appears in some antecedent, so a fired consequent is ground. The one exemption is a **head existential** `(exists ?y C)`, whose marked variable forward firing skolemizes (docs/skolem.md). The same closure is required of an `exceptWhen` exception, which is a query rather than a conclusion but must be ground for the same reason (checked at the assert layer via `sentex/check-exception-closed`).
nil, or a volatile bound beside *stratification-memo* holding the stored rules'
[:not P] antecedent keys, emptied with it.
nil, or a volatile bound beside `*stratification-memo*` holding the stored rules' `[:not P]` antecedent keys, emptied with it.
nil, or a volatile an assert or a settle binds, holding the stored half of the
stratification graph that checks/stratification-readers builds once and reuses across
the write's or the pass's checks. Every write to the rule indexes below empties it, as
does a rule's engines moving (forget-stratification).
nil, or a volatile an `assert` or a `settle` binds, holding the stored half of the stratification graph that `checks/stratification-readers` builds once and reuses across the write's or the pass's checks. Every write to the rule indexes below empties it, as does a rule's engines moving (`forget-stratification`).
(aggregate-antecedents sentex)The aggregate antecedent literals of a stored rule.
The aggregate antecedent literals of a stored rule.
(aggregate-antecedents-of rule-sentence)The aggregate antecedent literals of a raw rule sentence, for the checks that run before it is stored.
The aggregate antecedent literals of a raw rule *sentence*, for the checks that run before it is stored.
(aggregate-predicates sentex)The predicates a stored rule's aggregate bodies mention.
The predicates a stored rule's aggregate bodies mention.
(aggregate-predicates-of rule-sentence)The predicates a raw rule sentence's aggregate bodies mention, one per conjunct
(watched-literals): the stratification graph's negative-edge keys and the re-check
index's keys.
The predicates a raw rule *sentence*'s aggregate bodies mention, one per conjunct (`watched-literals`): the stratification graph's negative-edge keys and the re-check index's keys.
(aggregate-queries sentex)The body queries of a rule's aggregate antecedents, whole, for the settle-time firing
filter. None is ground, so the filter keeps every firing of an aggregate rule. A
reader that needs the conjuncts peels them with watched-literals.
The body queries of a rule's aggregate antecedents, whole, for the settle-time firing filter. None is ground, so the filter keeps every firing of an aggregate rule. A reader that needs the conjuncts peels them with `watched-literals`.
(antecedent-alternatives antes)The DNF alternatives of an antecedent list, as {:antecedents [...] :choices [...]}
in written order — :antecedents being that alternative's literals and :choices the
disjuncts it took, which is what a refusal names when one alternative is the bad one.
A disjunct that is itself compound contributes its own choices rather than being
named whole, so the innermost disjunct is what a message points at: in
(or (and A (or B C)) D) an alternative's choice is B, C or D, never the and.
The DNF alternatives of an antecedent list, as `{:antecedents [...] :choices [...]}`
in written order — `:antecedents` being that alternative's literals and `:choices` the
disjuncts it took, which is what a refusal names when one alternative is the bad one.
A disjunct that is itself compound contributes its *own* choices rather than being
named whole, so the innermost disjunct is what a message points at: in
`(or (and A (or B C)) D)` an alternative's choice is `B`, `C` or `D`, never the `and`.(antecedent-key literal)The antecedent-index key an antecedent literal files under: its functor, or
[:not f] for a negation whose body has functor f.
Keyed under the bare not every negated antecedent of every rule shares one bucket,
and each arriving negation decodes, and tries to match, every one of them;
keyed by the body's predicate an arriving (not (p a)) reaches the rules with a
negated antecedent on p — and, through trigger-keys' genl walk, those on a genl of
p, which is the direction subsumption runs in under a negation. A vector, so the key
can never collide with a predicate, which is always a symbol. The same spelling on the
index side (antecedent-keys, every writer) and the trigger side
(trigger-keys).
The antecedent-index key an antecedent `literal` files under: its functor, or `[:not f]` for a negation whose body has functor `f`. Keyed under the bare `not` every negated antecedent of every rule shares one bucket, and each arriving negation decodes, and tries to match, every one of them; keyed by the body's predicate an arriving `(not (p a))` reaches the rules with a negated antecedent on `p` — and, through `trigger-keys`' genl walk, those on a genl of `p`, which is the direction subsumption runs in under a negation. A vector, so the key can never collide with a predicate, which is always a symbol. The same spelling on the index side (`antecedent-keys`, every writer) and the trigger side (`trigger-keys`).
(antecedent-keys antes)antecedent-key of each of antes — a rule record's :antecedent, or the antecedents
antecedent-predicates splits off a sentence. Every writer of the antecedent index
passes the record's :antecedent here, the add (special/index-rule-sentex,
reindex) and the removal (special/disintegrate-sentex!) alike, so the two compute
their keys from one input.
`antecedent-key` of each of `antes` — a rule record's `:antecedent`, or the antecedents `antecedent-predicates` splits off a sentence. Every writer of the antecedent index passes the record's `:antecedent` here, the add (`special/index-rule-sentex`, `reindex`) and the removal (`special/disintegrate-sentex!`) alike, so the two compute their keys from one input.
(antecedent-predicates sentence)The antecedent-index keys of a rule sentence — each antecedent's antecedent-key; a
positive literal's key is its predicate, a negated one's is [:not pred].
The antecedent-index keys of a rule `sentence` — each antecedent's `antecedent-key`; a positive literal's key is its predicate, a negated one's is `[:not pred]`.
(antecedents sentence)The antecedent patterns of a rule sentence (unwrapping a leading and).
The antecedent patterns of a rule sentence (unwrapping a leading `and`).
(arrival-releasable? sentex)Can an arriving fact release one of this rule's re-check conditions rather than
only impose one? True for an aggregate and for a nested NAF. Read by the
settle loop, which owes such a rule a re-join, and by the genlCx and equality edge
triggers, which skip their firing-side narrowing for it (docs/exceptions.md,
"Re-chaining what was released, not what was touched").
Can an arriving fact *release* one of this rule's re-check conditions rather than only impose one? True for an **aggregate** and for a **nested** NAF. Read by the settle loop, which owes such a rule a re-join, and by the `genlCx` and equality edge triggers, which skip their firing-side narrowing for it (docs/exceptions.md, "Re-chaining what was released, not what was touched").
(assumption? sentex)Is this stored rule sentex a set/assumptionRule — a choice rule whose head a solve
decides rather than the chainer deriving? Its :effect is :choose
(docs/solving.md).
Is this stored rule sentex a `set/assumptionRule` — a choice rule whose head a solve decides rather than the chainer deriving? Its `:effect` is `:choose` (docs/solving.md).
(backward-sentex? sentex)Does this stored rule sentex backward-chain? Read off the record's :engines, as
forward-sentex? is.
Does this stored rule sentex backward-chain? Read off the record's `:engines`, as `forward-sentex?` is.
The consequent-marker functors a normalized cardinality rule carries, weighted or not.
The consequent-marker functors a normalized cardinality rule carries, weighted or not.
(cardinality-of sentex)The cardinality bound a stored constraint rule expresses — {:op :at-most|:at-least :k int :counted ?v} — read off the consequent marker (cardAtMost k ?v) /
(cardAtLeast k ?v), plus :weight ?w off a weighted (sumAtMost k ?w ?v) /
(sumAtLeast k ?w ?v), or nil for an ordinary constraint rule.
The cardinality bound a stored constraint rule expresses — `{:op :at-most|:at-least
:k int :counted ?v}` — read off the consequent marker `(cardAtMost k ?v)` /
`(cardAtLeast k ?v)`, plus `:weight ?w` off a weighted `(sumAtMost k ?w ?v)` /
`(sumAtLeast k ?w ?v)`, or nil for an ordinary constraint rule.(cardinality-surface? sentence)Is sentence a (asp/atMost …) / (asp/atLeast …) surface form (or a soft twin)?
Is `sentence` a `(asp/atMost …)` / `(asp/atLeast …)` surface form (or a soft twin)?
(chains? sentex)Does either chainer run this stored rule sentex? False for an inert rule and for a choice or constraint rule.
Does either chainer run this stored rule sentex? False for an inert rule and for a choice or constraint rule.
(check-disjunction! sentence)Throw the first disjunction-problems refusal, or return nil. The throwing form both
storage entry points read: core/check-sentence-shape! runs it before anything is stored, and
checks/check-rule! runs it again over what is about to be stored — which is where a
rule the cap refused, and so never expanded, is caught on the mint path.
Throw the first `disjunction-problems` refusal, or return nil. The throwing form both storage entry points read: `core/check-sentence-shape!` runs it before anything is stored, and `checks/check-rule!` runs it again over what is about to be stored — which is where a rule the cap refused, and so never expanded, is caught on the mint path.
(check-indexable-functors sentence)Throw :type :not-indexable when an antecedent literal of the rule sentence puts a
variable in functor position. A variable functor in the consequent is allowed and indexed
(consequent-index-pred).
The rule index is keyed by predicate. Every consequent variable is antecedent-bound
(check-range-restricted), so a consequent (?p ?y ?x) fires through its concrete
antecedent and the var-consequent-key catch-all cell serves backward goals. An antecedent
(?p ?x ?y) names no predicate to key on, so chain/fire-rules-for cannot find the rule from
an arriving fact and the rule would give two answers in two arrival orders. The message
names the instantiated rule, or the generator level to move it to (docs/generators.md): a
functor a level further out binds is ground before its rule is stored. An :inert rule is
exempt at the caller (checks/check-rule!).
Throw `:type :not-indexable` when an antecedent literal of the rule `sentence` puts a variable in functor position. A variable functor in the consequent is allowed and indexed (`consequent-index-pred`). The rule index is keyed by predicate. Every consequent variable is antecedent-bound (`check-range-restricted`), so a consequent `(?p ?y ?x)` fires through its concrete antecedent and the `var-consequent-key` catch-all cell serves backward goals. An antecedent `(?p ?x ?y)` names no predicate to key on, so `chain/fire-rules-for` cannot find the rule from an arriving fact and the rule would give two answers in two arrival orders. The message names the instantiated rule, or the generator level to move it to (docs/generators.md): a functor a level further out binds is ground before its rule is stored. An `:inert` rule is exempt at the caller (`checks/check-rule!`).
(check-range-restricted antecedents consequent)Throw :type :not-range-restricted unless every consequent variable is bound by
some antecedent (and the consequent is a well-formed conclusion).
Uses ex-info, not clojure.core/assert: an elidable check under *assert* false
would store the junk rule silently — the exact failure check-ground exists to
prevent — and an AssertionError carries no :type for callers to discriminate
on.
Throw `:type :not-range-restricted` unless every consequent variable is bound by some antecedent (and the consequent is a well-formed conclusion). Uses `ex-info`, not `clojure.core/assert`: an elidable check under `*assert*` false would store the junk rule *silently* — the exact failure `check-ground` exists to prevent — and an `AssertionError` carries no `:type` for callers to discriminate on.
(closed-extent-antecedents tx antes)The closed negative antecedents of antes whose predicate tx declares a closed
extent (closed-extent-declared?), unscoped. Two set reads and [] when the KB
declares no closed extent.
The closed negative antecedents of `antes` whose predicate `tx` declares a closed extent (`closed-extent-declared?`), unscoped. Two set reads and `[]` when the KB declares no closed extent.
(closed-extent-declared? tx pred)Does tx declare a closed extent on pred in any context, by
closed_extent_predicate or by a closedExtentForArg of any position and value? The
join, the re-check index and the stratification graph read this over-approximation;
derive time decides each selected literal in the conclusion's context.
Does `tx` declare a closed extent on `pred` in any context, by `closed_extent_predicate` or by a `closedExtentForArg` of any position and value? The join, the re-check index and the stratification graph read this over-approximation; derive time decides each selected literal in the conclusion's context.
(closed-extent-predicates-of tx rule-sentence)The predicates inside a raw rule sentence's closed-extent negative antecedents: its re-check keys and its negative edges.
The predicates inside a raw rule *sentence*'s closed-extent negative antecedents: its re-check keys and its negative edges.
(closed-extent-query-predicates tx queries)The predicates of the (not (P …)) literals a re-check watches in queries
(watched-literals) on which tx declares a closed extent (closed-extent-declared?).
These are the extra re-check keys and negative edges of a closed-extent negative inside
an unknown antecedent, an aggregate body or an exceptWhen query: the literal is
posted under not, and
a (P …) arriving or leaving moves it while posting under P alone.
The predicates of the `(not (P …))` literals a re-check watches in `queries` (`watched-literals`) on which `tx` declares a closed extent (`closed-extent-declared?`). These are the extra re-check keys and negative edges of a closed-extent negative inside an `unknown` antecedent, an aggregate body or an `exceptWhen` query: the literal is posted under `not`, and a `(P …)` arriving or leaving moves it while posting under `P` alone.
(closed-extent-recheck-predicates-of tx rule-sentence)The re-check keys a raw rule sentence's closed-extent negatives post it under, and
its negative edges on them: the antecedents' (closed-extent-predicates-of) and those
nested in its unknown antecedents and aggregate bodies (condition-queries-of,
closed-extent-query-predicates).
The re-check keys a raw rule *sentence*'s closed-extent negatives post it under, and its negative edges on them: the antecedents' (`closed-extent-predicates-of`) and those nested in its `unknown` antecedents and aggregate bodies (`condition-queries-of`, `closed-extent-query-predicates`).
(closed-negative-antecedents antes)The (not L) antecedents of antes every variable of which a generator antecedent
binds: the only negative literals a closed extent reads as negation as failure.
The `(not L)` antecedents of `antes` every variable of which a generator antecedent binds: the only negative literals a closed extent reads as negation as failure.
(condition-queries-of rule-sentence)The queries a raw rule sentence's re-check conditions read: every conjunct of its
unknown antecedents, and its aggregate antecedents, which watched-literals peels to
their census bodies. The closed-extent, separation-denial and negates-denial re-check
keys of a rule are read off these.
The queries a raw rule *sentence*'s re-check conditions read: every conjunct of its `unknown` antecedents, and its aggregate antecedents, which `watched-literals` peels to their census bodies. The closed-extent, separation-denial and negates-denial re-check keys of a rule are read off these.
(consequent-index-pred rule-sentex)The key the consequent slot of index-rule files rule-sentex under: its
consequent-predicate, or p/var-consequent-key when that predicate is a variable (a rule
with concrete antecedents concluding (?p …), allowed by check-indexable-functors). The
shared catch-all bucket is unioned into every concrete-goal answer by
resolution/concluding-rule-handles. An :inert rule concludes nothing, so it keeps the
canonical variable, a key nothing reads. special/index-rule-sentex, its unindex twin and
reindex/index-one! share this spelling.
The key the consequent slot of `index-rule` files `rule-sentex` under: its `consequent-predicate`, or `p/var-consequent-key` when that predicate is a variable (a rule with concrete antecedents concluding `(?p …)`, allowed by `check-indexable-functors`). The shared catch-all bucket is unioned into every concrete-goal answer by `resolution/concluding-rule-handles`. An `:inert` rule concludes nothing, so it keeps the canonical variable, a key nothing reads. `special/index-rule-sentex`, its unindex twin and `reindex/index-one!` share this spelling.
(consequent-key c0)consequent-predicate of a rule whose consequent pattern is c0, read off the
consequent itself — which a rule record holds as its :consequent.
`consequent-predicate` of a rule whose consequent pattern is `c0`, read off the consequent itself — which a rule record holds as its `:consequent`.
(consequent-predicate sentence)The predicate a rule concludes.
A generator concludes a rule, so its key is implies — reached by peeling the
set/*Rule wrapper first, because that wrapper belongs to the rule being generated
rather than to the generator (docs/generators.md). Without the peel one generator
files under set/defaultRule and the next under implies, by nothing more than how
its generated rule happened to be written, and the single cell that answers which rules
are generators would answer for some of them.
The predicate a rule concludes. A **generator** concludes a rule, so its key is `implies` — reached by peeling the `set/*Rule` wrapper first, because that wrapper belongs to the rule being generated rather than to the generator (docs/generators.md). Without the peel one generator files under `set/defaultRule` and the next under `implies`, by nothing more than how its generated rule happened to be written, and the single cell that answers *which rules are generators* would answer for some of them.
(constraint-of sentex)The constraint class of this stored rule sentex — :hard / :soft from its
set/hardConstraint / set/softConstraint wrapper (:effect :forbid /
:penalize), or nil for any other rule (docs/solving.md).
The constraint class of this stored rule sentex — `:hard` / `:soft` from its `set/hardConstraint` / `set/softConstraint` wrapper (`:effect` `:forbid` / `:penalize`), or nil for any other rule (docs/solving.md).
(constraint? sentex)Is this stored rule sentex a set/hardConstraint / set/softConstraint — a
contradiction rule whose conjunctive body a solve grounds into a nogood?
Is this stored rule sentex a `set/hardConstraint` / `set/softConstraint` — a contradiction rule whose conjunctive body a solve grounds into a nogood?
(dependency-predicates sentence)The antecedent keys of a rule sentence as consequent-predicate keys: what a rule
reading those antecedents depends on, spelled as the thing that could satisfy it is filed.
An antecedent-key names a negation by its body's predicate ([:not flies]), while a
conclusion (not (flies ?x)) is filed under not. A dependency lookup among concluders
must ask for not, or it reads an empty bucket and checks/check-stratified accepts a
negation cycle. Coarser than the index key on purpose: every negated antecedent depends on
every negated conclusion, the safe direction (checks/stratification-readers).
The antecedent keys of a rule `sentence` as `consequent-predicate` keys: what a rule reading those antecedents depends on, spelled as the thing that could satisfy it is filed. An `antecedent-key` names a negation by its body's predicate (`[:not flies]`), while a conclusion `(not (flies ?x))` is filed under `not`. A dependency lookup among concluders must ask for `not`, or it reads an empty bucket and `checks/check-stratified` accepts a negation cycle. Coarser than the index key on purpose: every negated antecedent depends on every negated conclusion, the safe direction (`checks/stratification-readers`).
(different-antecedents sentex)The (different …) antecedent literals of a stored rule — its unique-name conditions,
which read the equality closure and the indeterminate_term category rather than a fact
the justification names.
The `(different …)` antecedent literals of a stored rule — its unique-name conditions, which read the equality closure and the `indeterminate_term` category rather than a fact the justification names.
The predicates a fact can arrive on that flips a (different …) antecedent. different
is negation as failure over the equality closure and over the indeterminate_term category,
whose members are exempt from the unique-name assumption. A merge ends a difference and
identifying an indeterminate term starts one, so a rule reading different owes a re-check
in both directions. A subkind of the category needs no entry, since
special/recheck-on-predicate fans a predicate up its genls-global closure. genl is here
because the edge makes a kind indeterminate; a skolem is not, since its membership is minted.
This is the set checks/negative-predicates runs the stratification edge to.
The predicates a fact can arrive on that flips a `(different …)` antecedent. `different` is negation as failure over the equality closure and over the `indeterminate_term` category, whose members are exempt from the unique-name assumption. A merge ends a difference and identifying an indeterminate term starts one, so a rule reading `different` owes a re-check in both directions. A subkind of the category needs no entry, since `special/recheck-on-predicate` fans a predicate up its `genls-global` closure. `genl` is here because the edge makes a kind indeterminate; a skolem is not, since its membership is minted. This is the set `checks/negative-predicates` runs the stratification edge to.
(direct-concluders index pred)Rule handles whose consequent predicate is exactly pred, unioned with the
variable-consequent catch-all (p/var-consequent-key): a rule concluding (?p …) could
conclude pred once ?p binds, so any reader answering "which stored rules conclude
pred" must include it or it disagrees with the backward chainer. This is the
stored-graph read — no spec fan, unlike resolution/concluding-rule-handles — shared
by the stratification-cycle check and the blocked-firing explanation.
Rule handles whose consequent predicate is exactly `pred`, unioned with the variable-consequent catch-all (`p/var-consequent-key`): a rule concluding `(?p …)` could conclude `pred` once `?p` binds, so any reader answering "which stored rules conclude `pred`" must include it or it disagrees with the backward chainer. This is the **stored-graph** read — no spec fan, unlike `resolution/concluding-rule-handles` — shared by the stratification-cycle check and the blocked-firing explanation.
(disjunction-problems sentence)Why a sentence's ors cannot be polycanonicalized away, as problem maps; empty when they
can, and empty in one read for a sentence with no or. Four families, in this order: an or
in a position nothing expands (a conclusion, a closed-query body, an exception, under not),
an empty (or), a rule wider than max-alternatives, and an alternative the consequent is
not range-restricted over. A non-rule reads empty (sx/connective-problems refuses a
standalone or). A generator is read level by level: every level's antecedents may
disjoin, only the innermost consequent is a conclusion, and the innermost range check counts
an enclosing level's variables as bound (checks/rule-violation answers for the generated
rule).
Why a sentence's `or`s cannot be polycanonicalized away, as problem maps; empty when they can, and empty in one read for a sentence with no `or`. Four families, in this order: an `or` in a position nothing expands (a conclusion, a closed-query body, an exception, under `not`), an empty `(or)`, a rule wider than `max-alternatives`, and an alternative the consequent is not range-restricted over. A non-rule reads empty (`sx/connective-problems` refuses a standalone `or`). A generator is read level by level: every level's antecedents may disjoin, only the innermost consequent is a conclusion, and the innermost range check counts an enclosing level's variables as bound (`checks/rule-violation` answers for the generated rule).
(exception-arrival-releasable? queries)Can an arriving fact both impose and lift the exception queries (a rule's
provers/rule-exceptions)? An exception blocks while it holds, so a literal it reads
under an even number of unknowns is one an arrival makes hold, and one under an odd
number is one an arrival makes fail. With both, a block one arrival imposed is swept
rather than refused, and a later arrival can lift it with no refusal to read, so the
rule is owed a re-join as arrival-releasable? owes one. An aggregate moves either way
on its own. An exception of one polarity is not: a block an arrival imposes is never
lifted by one, and a block a retraction imposed is re-chained by the sweep.
Can an arriving fact both impose and lift the exception `queries` (a rule's `provers/rule-exceptions`)? An exception blocks while it holds, so a literal it reads under an even number of `unknown`s is one an arrival makes hold, and one under an odd number is one an arrival makes fail. With both, a block one arrival imposed is swept rather than refused, and a later arrival can lift it with no refusal to read, so the rule is owed a re-join as `arrival-releasable?` owes one. An aggregate moves either way on its own. An exception of one polarity is not: a block an arrival imposes is never lifted by one, and a block a retraction imposed is re-chained by the sweep.
(exceptWhen-not-a-rule exc inner)The refusal an inline (exceptWhen <query> X) earns when X is not a rule, as a problem
map, or nil. An exception blocks a rule's conclusions, and a fact has none; assert
throws it, check reports it and an import skips the frame.
The refusal an inline `(exceptWhen <query> X)` earns when X is not a rule, as a problem map, or nil. An exception blocks a rule's conclusions, and a fact has none; `assert` throws it, `check` reports it and an import skips the frame.
(expand-antecedent sentence)Polycanonicalize a rule whose antecedent disjoins into one rule per DNF alternative,
preserving any virtual wrapper. (implies (or A B) C) becomes [(implies A C) (implies B C)] and (implies (and (or A B) D) C) becomes [(implies (and A D) C) (implies (and B D) C)]. Anything else, a non-rule, a rule with no or, or an or in an argument slot, returns
[sentence].
Only the level written here is expanded: a generator's generated rule keeps its or until
chain/mint-rule expands what it stores. A rule the cap refuses and an empty (or) return
[sentence] unexpanded, and disjunction-problems reports both from that form.
Polycanonicalize a rule whose antecedent disjoins into one rule per DNF alternative, preserving any virtual wrapper. `(implies (or A B) C)` becomes `[(implies A C) (implies B C)]` and `(implies (and (or A B) D) C)` becomes `[(implies (and A D) C) (implies (and B D) C)]`. Anything else, a non-rule, a rule with no `or`, or an `or` in an argument slot, returns `[sentence]`. Only the level written here is expanded: a generator's generated rule keeps its `or` until `chain/mint-rule` expands what it stores. A rule the cap refuses and an empty `(or)` return `[sentence]` unexpanded, and `disjunction-problems` reports both from that form.
(expand-consequent sentence)Polycanonicalize a rule that concludes a conjunction into one rule per conjunct,
preserving any virtual wrapper (default / forward / backward / inert / assumptionRule).
A rule (implies A (and C1 C2)) becomes [(implies A C1) (implies A C2)]; anything
else (a non-rule, or a rule with a single consequent) returns [sentence] unchanged.
Runs on a rule whose exceptWhen has already been split off (split-exceptWhen), so
the exception is re-attached once per conjunct by the caller, against each conjunct's
own handle.
Polycanonicalize a rule that concludes a conjunction into one rule per conjunct, preserving any virtual wrapper (default / forward / backward / inert / assumptionRule). A rule `(implies A (and C1 C2))` becomes `[(implies A C1) (implies A C2)]`; anything else (a non-rule, or a rule with a single consequent) returns `[sentence]` unchanged. Runs on a rule whose exceptWhen has already been split off (`split-exceptWhen`), so the exception is re-attached once per conjunct by the caller, against each conjunct's own handle.
(expand-rule sentence)Both polycanonicalizations of a rule, composed: one rule per DNF alternative of the
antecedent, and within each, one per conjunct of the consequent. A rule that does
neither returns [sentence], so every caller can treat the result uniformly.
The product, and in that order — alternatives outermost, conjuncts within — which
is the order assert stores them and therefore the order an exceptWhen is
re-attached along. (implies (or A B) (and C1 C2)) stores four rules.
Both polycanonicalizations of a rule, composed: one rule per DNF alternative of the antecedent, and within each, one per conjunct of the consequent. A rule that does neither returns `[sentence]`, so every caller can treat the result uniformly. The **product**, and in that order — alternatives outermost, conjuncts within — which is the order `assert` stores them and therefore the order an `exceptWhen` is re-attached along. `(implies (or A B) (and C1 C2))` stores four rules.
(forget-stratification)Empty *stratification-memo* and *negated-keys-memo*: a stored rule's graph node moved.
Empty `*stratification-memo*` and `*negated-keys-memo*`: a stored rule's graph node moved.
(forward-sentex? sentex)Does this stored rule sentex forward-chain? Read off the record's :engines, which
its set/*Rule wrapper set. An assumptionRule (a choice head) and a
hard/softConstraint (a contradiction marker) hold #{:solve} — their heads are
decided or forbidden by a solve, not derived — so neither chainer runs them.
Does this stored rule sentex forward-chain? Read off the record's `:engines`, which
its `set/*Rule` wrapper set. An `assumptionRule` (a choice head) and a
`hard`/`softConstraint` (a contradiction marker) hold `#{:solve}` — their heads are
decided or forbidden by a solve, not derived — so neither chainer runs them.(generated-rule consequent)The bare rule form a generator's consequent generates — the (implies …) inside
whatever set/*Rule wrapper the author put on it — or nil when the consequent
concludes a fact, which is every ordinary rule.
The wrapper is peeled here and kept by the caller that mints: it sets the generated rule's direction, which is the only place a direction can be written for a rule nobody types out.
The bare rule form a generator's `consequent` generates — the `(implies …)` inside whatever `set/*Rule` wrapper the author put on it — or nil when the consequent concludes a fact, which is every ordinary rule. The wrapper is peeled here and *kept* by the caller that mints: it sets the **generated** rule's direction, which is the only place a direction can be written for a rule nobody types out.
(generator-sentex? sentex)Is this stored rule sentex a generator? Read off the record's :consequent, which
is where the canonicalized rule kept it.
Is this stored rule sentex a generator? Read off the record's `:consequent`, which is where the canonicalized rule kept it.
(generator? sentence)Is this rule sentence a generator — does it conclude a rule?
Is this rule *sentence* a generator — does it conclude a rule?
(has-aggregate? sentex)Does this rule carry any aggregate antecedent?
Does this rule carry any aggregate antecedent?
(has-different? sentex)Does this rule carry a (different …) antecedent?
Does this rule carry a `(different …)` antecedent?
(has-naf? sentex)Does this rule carry any unknown antecedent?
Does this rule carry any `unknown` antecedent?
(has-nested-naf? sentex)Does an unknown query of this rule carry a nested (unknown …) or an aggregate, so
that an arriving fact can release its block (docs/naf.md, "forall is sugar for a
nested unknown")?
Does an `unknown` query of this rule carry a nested `(unknown …)` or an aggregate, so that an arriving fact can release its block (docs/naf.md, "`forall` is sugar for a nested `unknown`")?
(holes antecedents generated)The variables a generator's generated rule takes from the firing — those its
enclosing antecedents also mention, as a set.
Computed rather than declared, which is the whole reason a generator needs no vocabulary of its own: sharing a variable name with the antecedents is how an author says "fill this in", and the remaining variables are the generated rule's own by the same token. Two spellings cannot disagree, because there is only one.
One level's question. Under nesting each level asks it of the level below, and
nesting carries the answers down as :bound.
The variables a generator's generated rule takes from the firing — those its enclosing `antecedents` also mention, as a set. Computed rather than declared, which is the whole reason a generator needs no vocabulary of its own: sharing a variable name with the antecedents *is* how an author says "fill this in", and the remaining variables are the generated rule's own by the same token. Two spellings cannot disagree, because there is only one. One level's question. Under nesting each level asks it of the level below, and `nesting` carries the answers down as `:bound`.
(index-exception index handle preds)Post rule handle under each predicate of preds in the re-check index, and into the
[:rules] set whatever preds holds.
Post rule `handle` under each predicate of `preds` in the re-check index, and into the `[:rules]` set whatever `preds` holds.
(index-rule index handle ante-keys conseq-key context)Post rule handle, stated in context, under each of ante-keys and under
conseq-key (nil when it has none). antecedent-keys and consequent-index-pred
compute the keys.
Post rule `handle`, stated in `context`, under each of `ante-keys` and under `conseq-key` (nil when it has none). `antecedent-keys` and `consequent-index-pred` compute the keys.
(inner-rule sentence)The bare (implies …) inside any virtual rule wrappers (set/*Rule and
exceptWhen, which may nest in any order — a defeasible forward rule with an
exception). The direction / default / assumption wrappers become record fields and
the exceptWhen becomes a meta-sentex, so the checks and the stored sentence both work
on this.
A forall antecedent is desugared here too (sentex/desugar-forall-rule), so every
pre-storage check — range restriction, closure, quantifier locality, stratification —
reads the nested NAF the constructor will store rather than the sugar it was written
with. A stored rule holds no forall, so this is the identity on one.
The bare `(implies …)` inside any virtual rule wrappers (`set/*Rule` and `exceptWhen`, which may nest in any order — a defeasible forward rule with an exception). The direction / default / assumption wrappers become record fields and the exceptWhen becomes a meta-sentex, so the checks and the stored sentence both work on this. A `forall` antecedent is desugared here too (`sentex/desugar-forall-rule`), so every pre-storage check — range restriction, closure, quantifier locality, stratification — reads the nested NAF the constructor will store rather than the sugar it was written with. A stored rule holds no `forall`, so this is the identity on one.
(innermost-rule sentence)The rule at the bottom of a generator's nesting — the one whose consequent is a
conclusion rather than another rule, and so the only level of a generator that
ever concludes a fact. inner-rule for a rule that generates nothing.
The rule at the bottom of a generator's nesting — the one whose consequent is a **conclusion** rather than another rule, and so the only level of a generator that ever concludes a fact. `inner-rule` for a rule that generates nothing.
The consequent-marker functors the answer-set surfaces normalize into. No authored
sentence spells one: refuse-internal-marker refuses a constraint rule that does.
The consequent-marker functors the answer-set surfaces normalize into. No authored sentence spells one: `refuse-internal-marker` refuses a constraint rule that does.
(lazy-sentex? sentex)Does a forward join prove this stored rule sentex's conclusion on demand
(set/lazyForwardRule)? Read off :engines; a rule that also forward-chains stores
its conclusions, so it is not lazy.
Does a forward join prove this stored rule sentex's conclusion on demand (`set/lazyForwardRule`)? Read off `:engines`; a rule that also forward-chains stores its conclusions, so it is not lazy.
How many alternatives one rule may expand to. A disjunctive antecedent is stored
expanded, so the width is paid in handles, index entries and TMS nodes rather than at
query time — and a nest of ors multiplies, so the cost of a typo is exponential in a
sentence that still reads like one line. Sixteen is the width past which a rule is
better written as a type: assert a genl and one rule on the supertype, which is one
handle however many members it covers.
How many alternatives one rule may expand to. A disjunctive antecedent is *stored* expanded, so the width is paid in handles, index entries and TMS nodes rather than at query time — and a nest of `or`s multiplies, so the cost of a typo is exponential in a sentence that still reads like one line. Sixteen is the width past which a rule is better written as a type: assert a `genl` and one rule on the supertype, which is one handle however many members it covers.
The consequent-marker functor a normalized asp/minimize carries:
(minimizeCost <priority> <weight-var>).
The consequent-marker functor a normalized `asp/minimize` carries: `(minimizeCost <priority> <weight-var>)`.
(minimize-surface? sentence)Is sentence a (asp/minimize priority ?weight body) surface form?
Is `sentence` a `(asp/minimize priority ?weight body)` surface form?
(naf-antecedents sentex)The (unknown S) antecedent literals of a stored rule — its negation-as-failure
conditions.
The `(unknown S)` antecedent literals of a stored rule — its negation-as-failure conditions.
(naf-antecedents-of rule-sentence)The (unknown S) antecedent literals of a raw rule sentence — for the checks
that run before a rule is stored as a sentex (stratification).
The `(unknown S)` antecedent literals of a raw rule *sentence* — for the checks that run before a rule is stored as a sentex (stratification).
(naf-predicates sentex)The predicates a stored rule's unknown antecedents mention: its keys in the
[:exception-index …] re-check index.
The predicates a stored rule's `unknown` antecedents mention: its keys in the `[:exception-index …]` re-check index.
(naf-predicates-of rule-sentence)The predicates a raw rule sentence's unknown antecedents mention, for the
stratification check on a rule not yet stored.
The predicates a raw rule *sentence*'s `unknown` antecedents mention, for the stratification check on a rule not yet stored.
(naf-queries sentex)The inner query literals of a rule's unknown antecedents (naf-queries-of), for
the settle-time firing filter.
The inner query literals of a rule's `unknown` antecedents (`naf-queries-of`), for the settle-time firing filter.
(negates-denial-predicates tx queries)The predicates a negates declaration's denial can move a negated literal of
queries on, as the re-check index's extra keys: for each (not (P …)) a re-check
watches (watched-literals), every predicate declared to negate P or a supertype of
it (tax/negates-over, unscoped, a superset over every reader).
provers/NegatesProver answers (not (P …)) from a believed tuple of such a
predicate's spec subtree, and the trigger fans the tuple up to the predicate
(special/recheck-on-predicate). Empty, off one map read, on a KB declaring no
negates.
The predicates a `negates` declaration's denial can move a negated literal of `queries` on, as the re-check index's extra keys: for each `(not (P …))` a re-check watches (`watched-literals`), every predicate declared to negate `P` or a supertype of it (`tax/negates-over`, unscoped, a superset over every reader). `provers/NegatesProver` answers `(not (P …))` from a believed tuple of such a predicate's spec subtree, and the trigger fans the tuple up to the predicate (`special/recheck-on-predicate`). Empty, off one map read, on a KB declaring no `negates`.
(negates-denial-predicates-of tx rule-sentence)negates-denial-predicates of a raw rule sentence's unknown antecedents and
aggregate bodies, as separation-denial-predicates-of reads them.
`negates-denial-predicates` of a raw rule *sentence*'s `unknown` antecedents and aggregate bodies, as `separation-denial-predicates-of` reads them.
(negative-literal? a)Is a a (not (P …)) literal with a flat, symbol-headed body — the form a closed
extent can be read over?
Is `a` a `(not (P …))` literal with a flat, symbol-headed body — the form a closed extent can be read over?
(nesting sentence)A rule sentence peeled into its levels, outermost first, one map per implies:
{:antecedents … ; that level's antecedent patterns
:consequent … ; what it concludes, wrapper and all
:generated … ; the bare rule it generates, nil at the innermost level
:bound …} ; the variables an *enclosing* level's antecedents bind
An ordinary rule is one level, a generator two, with no cap. :bound is accumulated on the
way down: every enclosing level has fired and substituted its holes before a level's rule is
stored, so those variables are ground there, may stand in functor position, and count as
bound for the innermost rule's range restriction. The holes, the variable functors and the
range restriction are all read off these levels, so they agree about which level owns a
variable.
A rule sentence peeled into its levels, outermost first, one map per `implies`:
{:antecedents … ; that level's antecedent patterns
:consequent … ; what it concludes, wrapper and all
:generated … ; the bare rule it generates, nil at the innermost level
:bound …} ; the variables an *enclosing* level's antecedents bind
An ordinary rule is one level, a generator two, with no cap. `:bound` is accumulated on the
way down: every enclosing level has fired and substituted its holes before a level's rule is
stored, so those variables are ground there, may stand in functor position, and count as
bound for the innermost rule's range restriction. The holes, the variable functors and the
range restriction are all read off these levels, so they agree about which level owns a
variable.(nonempty-recheck-predicates sentex)[nonempty] for a rule with a positive antecedent on nonempty, else nil: the key the
re-check index posts the rule under. NonemptyProver computes the antecedent from the
believed members of its type, so every membership re-checks the rule
(special/recheck-nonempty-readers) and no predicate of the rule names them.
`[nonempty]` for a rule with a positive antecedent on `nonempty`, else nil: the key the re-check index posts the rule under. `NonemptyProver` computes the antecedent from the believed members of its type, so every membership re-checks the rule (`special/recheck-nonempty-readers`) and no predicate of the rule names them.
(normalize-cardinality sentence)Rewrite a (asp/atMost k ?v pattern) surface form into the internal constraint rule
(set/hardConstraint (implies pattern (cardAtMost k ?v))), and a weighted
(asp/atMostSum k ?w ?v body) into (set/hardConstraint (implies body (sumAtMost k ?w ?v))) — the soft twins into set/softConstraint. The identity on anything else, so
assert and check apply it to every sentence.
Refuses a malformed bound here, at the entry point, before storage: k a non-negative
integer, ?v (and ?w, distinct from it) a variable the pattern binds, pattern a
literal or, for a weighted bound, a conjunction. The range check that runs on the
rewritten rule then holds the marker's variables to the antecedent.
Rewrite a `(asp/atMost k ?v pattern)` surface form into the internal constraint rule `(set/hardConstraint (implies pattern (cardAtMost k ?v)))`, and a weighted `(asp/atMostSum k ?w ?v body)` into `(set/hardConstraint (implies body (sumAtMost k ?w ?v)))` — the soft twins into `set/softConstraint`. The identity on anything else, so `assert` and `check` apply it to every sentence. Refuses a malformed bound here, at the entry point, before storage: `k` a non-negative integer, `?v` (and `?w`, distinct from it) a variable the pattern binds, `pattern` a literal or, for a weighted bound, a conjunction. The range check that runs on the rewritten rule then holds the marker's variables to the antecedent.
(normalize-minimize sentence)Rewrite (asp/minimize priority ?weight body) into the internal soft constraint
(set/softConstraint (implies body (minimizeCost priority ?weight))) — a soft whose
choice-head body is penalized by the data weight ?weight at priority, so the
objective at that level sums ?weight over every chosen head. body names a choice
head and binds ?weight off a background fact — the weak-constraint idiom
#minimize{ W@P, head : head-facts, weight-fact }. The identity on anything else.
Refuses a malformed form: the priority a positive integer, ?weight a variable the body
binds, body a literal or conjunction.
Rewrite `(asp/minimize priority ?weight body)` into the internal soft constraint
`(set/softConstraint (implies body (minimizeCost priority ?weight)))` — a soft whose
choice-head body is penalized by the data weight `?weight` at `priority`, so the
objective at that level sums `?weight` over every chosen head. `body` names a choice
head and binds `?weight` off a background fact — the weak-constraint idiom
`#minimize{ W@P, head : head-facts, weight-fact }`. The identity on anything else.
Refuses a malformed form: the priority a positive integer, `?weight` a variable the body
binds, `body` a literal or conjunction.(normalize-soft-priority sentence)Rewrite a priority-tagged (set/softConstraint P (implies body C)) into the internal
(set/softConstraint (implies body (softPriority P C))), moving the priority level onto
the consequent marker so the split, the checks, and the store see an ordinary soft
constraint. The identity on anything else.
Refuses a malformed form here, before storage: the priority a positive integer, the
wrapper set/softConstraint (a hard constraint is an integrity constraint, never
minimized, so a priority on it is meaningless), and the body a rule.
Rewrite a priority-tagged `(set/softConstraint P (implies body C))` into the internal `(set/softConstraint (implies body (softPriority P C)))`, moving the priority level onto the consequent marker so the split, the checks, and the store see an ordinary soft constraint. The identity on anything else. Refuses a malformed form here, before storage: the priority a positive integer, the wrapper `set/softConstraint` (a hard constraint is an integrity constraint, never minimized, so a priority on it is meaningless), and the body a rule.
(normalize-solve-surface sentence)Rewrite the answer-set surface forms — cardinality bounds, priority-tagged soft
constraints, and minimize objectives — into their internal constraint-rule forms, so
the split, the checks, and the store all see ordinary constraint rules. Each rewrite is
the identity off its own surface, and the three surfaces are disjoint, so the order does
not matter; the identity on every other sentence. A constraint rule that spells an
internal marker itself is refused first (refuse-internal-marker).
Rewrite the answer-set surface forms — cardinality bounds, priority-tagged soft constraints, and minimize objectives — into their internal constraint-rule forms, so the split, the checks, and the store all see ordinary constraint rules. Each rewrite is the identity off its own surface, and the three surfaces are disjoint, so the order does not matter; the identity on every other sentence. A constraint rule that spells an internal marker itself is refused first (`refuse-internal-marker`).
(post-join-antecedents sentex)post-join-literals over a stored rule's antecedents.
`post-join-literals` over a stored rule's antecedents.
(post-join-literals antes)The antecedent literals evaluated after the join, in written order: every
aggregate, plus every deferred literal reading a variable an aggregate writes or one
of these writes in turn, so an (evaluate ?d (+ ?n 1)) carries a later (lessThan ?d 9) along. unknown is not here: it binds nothing and is evaluated per placement as
:naf. Asked on every join, so a rule without an aggregate costs one some.
The antecedent literals evaluated **after** the join, in written order: every aggregate, plus every deferred literal reading a variable an aggregate writes or one of these writes in turn, so an `(evaluate ?d (+ ?n 1))` carries a later `(lessThan ?d 9)` along. `unknown` is not here: it binds nothing and is evaluated per placement as `:naf`. Asked on every join, so a rule without an aggregate costs one `some`.
(range-problems antecedents consequent)Why antecedents => consequent is not range-restricted, as a seq of problem strings, empty
when the rule is fine. The value form, like the wff arms. A head existential (exists ?y C)
exempts only its marked variables: the check runs over the inner C (docs/skolem.md).
A generator is checked at its innermost level, with every enclosing level's holes counted as bound; each generator level's own range restriction is vacuous. The refusal therefore reaches the author where the generator is written. Each generator level also owes one claim: it must fill a hole no enclosing level has already filled, since otherwise it generates the same rule at every firing.
Why `antecedents => consequent` is not range-restricted, as a seq of problem strings, empty when the rule is fine. The value form, like the wff arms. A head existential `(exists ?y C)` exempts only its marked variables: the check runs over the inner `C` (docs/skolem.md). A generator is checked at its innermost level, with every enclosing level's holes counted as bound; each generator level's own range restriction is vacuous. The refusal therefore reaches the author where the generator is written. Each generator level also owes one claim: it must fill a hole no enclosing level has already filled, since otherwise it generates the same rule at every firing.
(recheck-predicates sentex)The predicates whose change must re-check this rule for its own re-check conditions: the
predicates its unknown antecedents and aggregate bodies mention, plus
different-flip-predicates where it reads different. A closed-extent negative antecedent
adds its own (closed-extent-predicates-of), since that is a taxonomy read. An exceptWhen
exception is registered under its rule by the meta-sentex's own indexing. This is the key
set the [:exception-index …] index posts a rule under. Each kind reads what the KB
believes at firing time, so a fact arriving on those predicates brings the firing back for
re-decision. A different antecedent holds by the absence of a merge and has no support
handle, so the re-check is the only way to withdraw the firing (docs/predall.md).
The predicates whose change must re-check this rule for its own re-check conditions: the predicates its `unknown` antecedents and aggregate bodies mention, plus `different-flip-predicates` where it reads `different`. A closed-extent negative antecedent adds its own (`closed-extent-predicates-of`), since that is a taxonomy read. An exceptWhen exception is registered under its rule by the meta-sentex's own indexing. This is the key set the `[:exception-index …]` index posts a rule under. Each kind reads what the KB believes at firing time, so a fact arriving on those predicates brings the firing back for re-decision. A `different` antecedent holds by the absence of a merge and has no support handle, so the re-check is the only way to withdraw the firing (docs/predall.md).
(rechecked? sentex)Does this rule carry a re-check condition of its own — an unknown antecedent, an
aggregate, or a different antecedent? The check on registering it in the re-check
index; an exceptWhen exception is registered by its own meta-sentex and is not read off
the rule.
Does this rule carry a re-check condition of its **own** — an `unknown` antecedent, an aggregate, or a `different` antecedent? The check on registering it in the re-check index; an exceptWhen exception is registered by its own meta-sentex and is not read off the rule.
(refuse-internal-marker sentence)Throw :not-well-formed when a constraint rule's authored consequent is one of the
internal-markers; return sentence unchanged otherwise. A hand-written marker skips
the operand checks its surface form runs, and the solve reads each operand as a count or
an objective level, so a symbol operand such as (cardAtMost ?a ?c) would reach
arithmetic and throw a bare ClassCastException out of do/label.
Throw `:not-well-formed` when a constraint rule's authored consequent is one of the `internal-markers`; return `sentence` unchanged otherwise. A hand-written marker skips the operand checks its surface form runs, and the solve reads each operand as a count or an objective level, so a symbol operand such as `(cardAtMost ?a ?c)` would reach arithmetic and throw a bare `ClassCastException` out of `do/label`.
(rewrap sentence direction defeasible assumption constraint)(rewrap sentence direction defeasible assumption constraint solve?)Put the direction / default / assumption / constraint wrappers a rule was written with
back around sentence: the inverse of sx/peel-rule-wrapper, since the wrappers ride the
record and not the stored sentence. The arguments are the wrappers as peel-rule-wrapper
reads them: a polycanonicalized conjunct keeps the mode of its rule, and split-exceptWhen
restores the qualified rule's other wrappers. rewrap-sentex reads them off a stored
record. An exceptWhen is not among them (split-exceptWhen). A cardinality constraint
rule restores its authored surface, (asp/atMost k ?v pattern), instead of the internal
set/hardConstraint (implies …) form (normalize-cardinality). solve? puts
set/solveRule outermost, around the direction wrapper.
Put the direction / default / assumption / constraint wrappers a rule was written with back around `sentence`: the inverse of `sx/peel-rule-wrapper`, since the wrappers ride the record and not the stored sentence. The arguments are the wrappers as `peel-rule-wrapper` reads them: a polycanonicalized conjunct keeps the mode of its rule, and `split-exceptWhen` restores the qualified rule's other wrappers. `rewrap-sentex` reads them off a stored record. An exceptWhen is not among them (`split-exceptWhen`). A cardinality constraint rule restores its authored surface, `(asp/atMost k ?v pattern)`, instead of the internal `set/hardConstraint (implies …)` form (`normalize-cardinality`). `solve?` puts `set/solveRule` outermost, around the direction wrapper.
(rewrap-sentex sentence sx)rewrap with the wrappers read off the stored rule sentex sx — the form its author
wrote, around sentence (its canonical or its originalized sentence). A :derive
rule gets its direction wrapper (none for backward, the default), set/defaultRule
when defeasible and set/solveRule when a solve runs it; a choice or constraint rule gets its head wrapper
alone, since the wrapper stack refuses anything beside it.
`rewrap` with the wrappers read off the stored rule sentex `sx` — the form its author wrote, around `sentence` (its canonical or its originalized sentence). A `:derive` rule gets its direction wrapper (none for backward, the default), `set/defaultRule` when defeasible and `set/solveRule` when a solve runs it; a choice or constraint rule gets its head wrapper alone, since the wrapper stack refuses anything beside it.
(rule-sentence antecedents consequent)Build a rule sentence from antecedent patterns and a consequent pattern.
One spelling for the whole codebase — see sentex/rule-sentence.
Build a rule sentence from antecedent patterns and a consequent pattern. One spelling for the whole codebase — see `sentex/rule-sentence`.
(rule-sentence? sentence)Is sentence a rule form (implies <ante> <conseq>)?
Is `sentence` a rule form `(implies <ante> <conseq>)`?
(rule? sentex)Is sentex a rule — a record with an :antecedent? The field is the discriminant
everywhere; a rule record holds no sentence to test.
Is `sentex` a rule — a record with an `:antecedent`? The field is the discriminant everywhere; a rule record holds no sentence to test.
(separation-denial-predicates tx queries)The types a separation's denial can move a negated literal of queries on, as the
re-check index's extra keys: for each (not (T …)) a re-check watches
(watched-literals) with a unary T, every type a declaration separates T from
(tax/separating-partners, read unscoped with no exception, a superset over every
reader). provers/DisjointnessNegationProver answers (not (T x)) from a membership
(S x) of a type below one of them, and the trigger fans an arriving (S x) out to
S's supertypes (special/recheck-on-predicate), so a rule posted under them is
re-checked when such a membership arrives or leaves. Empty for a T no separation
reaches.
The types a separation's denial can move a negated literal of `queries` on, as the re-check index's extra keys: for each `(not (T …))` a re-check watches (`watched-literals`) with a unary `T`, every type a declaration separates `T` from (`tax/separating-partners`, read unscoped with no exception, a superset over every reader). `provers/DisjointnessNegationProver` answers `(not (T x))` from a membership `(S x)` of a type below one of them, and the trigger fans an arriving `(S x)` out to `S`'s supertypes (`special/recheck-on-predicate`), so a rule posted under them is re-checked when such a membership arrives or leaves. Empty for a `T` no separation reaches.
(separation-denial-predicates-of tx rule-sentence)separation-denial-predicates of a raw rule sentence's unknown antecedents and
aggregate bodies (condition-queries-of): the extra keys the re-check index posts the
rule under beside recheck-predicates (special/index-rule-sentex), a taxonomy read as
closed-extent-predicates-of is.
`separation-denial-predicates` of a raw rule *sentence*'s `unknown` antecedents and aggregate bodies (`condition-queries-of`): the extra keys the re-check index posts the rule under beside `recheck-predicates` (`special/index-rule-sentex`), a taxonomy read as `closed-extent-predicates-of` is.
(signed-reach tax dir p)p's global genl closure in direction dir (:up or :down), together with the
predicates genlInverse edges reach either way round (tax/signed-closure): every
predicate an antecedent or fact on p can meet through the matching fan. The plain
closure itself on a KB declaring no genlInverse.
`p`'s global `genl` closure in direction `dir` (`:up` or `:down`), together with the predicates `genlInverse` edges reach either way round (`tax/signed-closure`): every predicate an antecedent or fact on `p` can meet through the matching fan. The plain closure itself on a KB declaring no `genlInverse`.
(soft-cost-of marker)Read the objective level and per-head weight a ground soft-constraint marker
carries, for solve-context to put on the nogood — the counterpart to cardinality-of
for the minimize/priority surface:
(minimizeCost p w) → {:priority p :weight w :marker marker} — a minimize term over
the chosen head, weighted w at level p;
(softPriority p m) → {:priority p :marker m} — the authored soft m, at level p,
unit weight;
anything else → {:priority 1 :marker marker} — an ordinary soft, level 1.
:marker is the value to name the nogood by (the authored one, unwrapped).
Read the objective level and per-head weight a **ground** soft-constraint marker
carries, for `solve-context` to put on the nogood — the counterpart to `cardinality-of`
for the minimize/priority surface:
`(minimizeCost p w)` → `{:priority p :weight w :marker marker}` — a minimize term over
the chosen head, weighted `w` at level `p`;
`(softPriority p m)` → `{:priority p :marker m}` — the authored soft `m`, at level `p`,
unit weight;
anything else → `{:priority 1 :marker marker}` — an ordinary soft, level 1.
`:marker` is the value to name the nogood by (the authored one, unwrapped).The consequent-marker functor a normalized priority-tagged set/softConstraint
carries: (softPriority <priority> <the authored consequent>).
The consequent-marker functor a normalized priority-tagged `set/softConstraint` carries: `(softPriority <priority> <the authored consequent>)`.
(soft-priority-surface? sentence)Is sentence a priority-tagged constraint wrapper — a leading positive integer before
the rule, (set/softConstraint P (implies …))?
Is `sentence` a priority-tagged constraint wrapper — a leading positive integer before the rule, `(set/softConstraint P (implies …))`?
(solve-sentex? sentex)Does a do/label solve read this stored rule sentex — a choice, constraint or
cardinality rule, or a set/solveRule? Read off :engines, as forward-sentex? is.
Does a `do/label` solve read this stored rule sentex — a choice, constraint or cardinality rule, or a `set/solveRule`? Read off `:engines`, as `forward-sentex?` is.
(split-exceptWhen sentence)Split an (exceptWhen <query> <rule>) assertion into [exception inner].
exception is the flattened conjunction of every exceptWhen wrapper (a vector of
literals in the author's variable names, block-if-all-hold), and inner is what the
exceptWhen qualifies: the wrapped rule with its exceptWhen(s) stripped but its
direction / default / assumption wrappers intact, or the (sentexHandle H) a
bare-handle exceptWhen named. [nil sentence] when there is no exceptWhen.
This is the layer at which an exceptWhen becomes a separate meta-sentex: the assert
layer stores inner as the rule (or resolves the handle) and the exception as
(exceptWhen <aligned-query> (sentexHandle H)) against it.
Split an `(exceptWhen <query> <rule>)` assertion into `[exception inner]`. `exception` is the flattened conjunction of every exceptWhen wrapper (a vector of literals in the author's variable names, block-if-all-hold), and `inner` is what the exceptWhen qualifies: the wrapped rule with its exceptWhen(s) stripped but its direction / default / assumption wrappers intact, or the `(sentexHandle H)` a bare-handle exceptWhen named. `[nil sentence]` when there is no exceptWhen. This is the layer at which an exceptWhen becomes a separate meta-sentex: the assert layer stores `inner` as the rule (or resolves the handle) and the exception as `(exceptWhen <aligned-query> (sentexHandle H))` against it.
(trigger-keys tax sentence index)The antecedent-index keys an arriving fact sentence triggers rules through, and the
trigger side of antecedent-key.
A positive fact triggers its predicate and its supertypes (match1's subsumption). A
negative fact (not (p a)) entails (not (q a)) for every spec q of p, so it triggers
[:not q] for each spec of its body's predicate. Each side is the closure intersected with
the keys some stored rule reads (reads/as-stored-rule-keys), walking the smaller of a
membership test per closure term and one pass over the stored keys. The spec walk stops at
the stored key count (tax/specs-global-within), and (not (thing X)) takes the pass. The
closures are unscoped, a superset that the placement narrows.
The antecedent-index keys an arriving fact `sentence` triggers rules through, and the trigger side of `antecedent-key`. A positive fact triggers its predicate and its supertypes (`match1`'s subsumption). A negative fact `(not (p a))` entails `(not (q a))` for every spec `q` of `p`, so it triggers `[:not q]` for each spec of its body's predicate. Each side is the closure intersected with the keys some stored rule reads (`reads/as-stored-rule-keys`), walking the smaller of a membership test per closure term and one pass over the stored keys. The spec walk stops at the stored key count (`tax/specs-global-within`), and `(not (thing X))` takes the pass. The closures are unscoped, a superset that the placement narrows.
(unindex-exception! index handle preds)Retire rule handle from each predicate of preds in the re-check index and from the
[:rules] set.
Retire rule `handle` from each predicate of `preds` in the re-check index and from the `[:rules]` set.
(unindex-rule! index handle ante-keys conseq-key context)Retire rule handle, stated in context, from the keys index-rule posted it under.
Retire rule `handle`, stated in `context`, from the keys `index-rule` posted it under.
(variable-functor-literals sentence)The [role literal] pairs of a rule whose functor is a variable: (?p ?x ?y) or the dotted
rest (?pred . ?args). Read through naming/applied-literals one level at a time, so the
frames descended into are those the naming check descends: a negated antecedent, a head
existential, an aggregate's body.
Inside a generator's generated rule the question is asked of non-holes only. A generated
rule is a pattern and the mint is what gets stored, checked in its own right when minted. A
variable an enclosing level binds is ground before anything is keyed on it, so one generator
can range over a family of predicates. A variable bound by a literal of the rule being
stored ((implies (and (?tpred ?type ?cap) (?type ?instance)) …)) is refused; written one
level further in it is a hole of the middle level and both functors are concrete. A
generated variable functor no enclosing level binds is refused, naming the generator.
The `[role literal]` pairs of a rule whose functor is a variable: `(?p ?x ?y)` or the dotted rest `(?pred . ?args)`. Read through `naming/applied-literals` one level at a time, so the frames descended into are those the naming check descends: a negated antecedent, a head existential, an aggregate's body. Inside a generator's generated rule the question is asked of non-holes only. A generated rule is a pattern and the mint is what gets stored, checked in its own right when minted. A variable an enclosing level binds is ground before anything is keyed on it, so one generator can range over a family of predicates. A variable bound by a literal of the rule being stored (`(implies (and (?tpred ?type ?cap) (?type ?instance)) …)`) is refused; written one level further in it is a hole of the middle level and both functors are concrete. A generated variable functor no enclosing level binds is refused, naming the generator.
(watched-literals q)The literals a re-check watches for query literal q, an unknown antecedent's query
or an exceptWhen conjunct: each query-operator frame peeled, recursively, to what it
reads (an unknown's conjuncts, a thereExists's body, a forall's desugared NAF, an
aggregate's census body, an and's conjuncts), and anything else as itself. No sentex
is stored under a query operator's functor, so no fact arrives on one. A not frame is
not peeled, because special/recheck-on-sentence keys an arriving (not S) under not
too (docs/naf.md, "S may be a conjunction").
The literals a re-check watches for query literal `q`, an `unknown` antecedent's query or an `exceptWhen` conjunct: each query-operator frame peeled, recursively, to what it reads (an `unknown`'s conjuncts, a `thereExists`'s body, a `forall`'s desugared NAF, an aggregate's census body, an `and`'s conjuncts), and anything else as itself. No sentex is stored under a query operator's functor, so no fact arrives on one. A `not` frame is not peeled, because `special/recheck-on-sentence` keys an arriving `(not S)` under `not` too (docs/naf.md, "`S` may be a conjunction").
(watched-predicates queries)The predicates a re-check keys queries under — watched-literals of each, then its
functor. What exceptWhen's three registration sites and the stratification graph
read of an exception's conjuncts, and what naf-predicates reads of an unknown
antecedent's.
The predicates a re-check keys `queries` under — `watched-literals` of each, then its functor. What `exceptWhen`'s three registration sites and the stratification graph read of an exception's conjuncts, and what `naf-predicates` reads of an `unknown` antecedent's.
(wrap-direction sentence direction)Express direction as the corresponding set/*Rule wrapper around sentence.
:backward needs no wrapper — a bare (implies …) is backward by default.
Express `direction` as the corresponding `set/*Rule` wrapper around `sentence`. `:backward` needs no wrapper — a bare `(implies …)` is backward by default.
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 |