Query execution
Most databases treat query execution as an implementation detail behind a
cost-based optimizer. That abstraction leaks: when the optimizer picks a bad
plan, you end up reverse-engineering it anyway, and graph queries, which are
join-heavy by nature, hit that wall soonest. This engine takes the opposite
approach: there is no cost-based optimizer, and plans are deterministic.
The plan follows from how the query is written and how the data is stored, so
once you know the rules in this chapter you can predict exactly what will run,
and read it with ::explain.
mnestic
Deterministic does not have to mean naive. mnestic adds three deterministic
rewrites on top of the inherited pipeline: an
equality pushdown that compiles ==
post-filters on stored relations into keyed lookups (0.8.0), a stat-free
greedy join reorder that fixes
naively-ordered conjunctions, default on (0.10.5), and an opt-in
factorized count() rewrite whose
detector annotates ::explain even when the rewrite is off (0.10.5). All
three leave result sets unchanged, and all three are visible in the plan.
The pipeline
A query goes through these stages, each described in a section below:
- Inline rules are canonicalized into disjunctive normal form; each disjunct becomes its own rule.
- Each rule body's atoms are ordered: mnestic's equality pushdown, then its greedy join reorder, then the inherited binding-before-use pass.
- The rules are stratified into groups that can be evaluated together, or the query is rejected as unstratifiable.
- Within each stratum, magic set rewrites specialize recursive rules to the constants they are called with.
- The strata are evaluated bottom-up with the semi-naïve algorithm,
stopping early when
:limitis satisfied.
::explain { <query> } runs everything except the final evaluation stage and
returns the compiled plan instead of results.
Reading a plan with ::explain
The examples on this page use the small agent-memory graph shared across these
docs: episodic memory rows m1–m8, an entity catalog, mentions links
between them, and weighted recalls edges between memories. Keys sit to the
left of => — key order is what decides access paths below.
memory { id => kind, text, importance, at, v } # notes, decisions, insights
entity { id => name, kind } # people, tools, projects
mentions { memory, entity } # which memories involve whom
recalls { from, to => strength } # association edgesHere is a three-way join — important memories that mention Postgres — and its real plan:
::explain {
?[text, importance] := *entity{ name: 'Postgres', id: eid },
*mentions{ memory: mid, entity: eid },
*memory{ id: mid, text, importance },
importance > 0.5
}stratum rule_idx rule atom_idx op ref joins_on filters/expr out_relation
0 0 ? 7 unify *2 "Postgres" ["*2"]
0 0 ? 6 load_stored :entity [] ["eid", "**0", "~1"]
0 0 ? 5 stored_mat_join {"*2": "**0"} ["eid"]
0 0 ? 4 load_stored :mentions [] ["mid", "**1"]
0 0 ? 3 stored_mat_join {"eid": "**1"} ["mid"]
0 0 ? 2 load_stored :memory ["gt(importance, 0.5)"] ["**2", "~3", "text", "importance", "~4", "~5"]
0 0 ? 1 stored_prefix_join {"mid": "**2"} ["text", "importance"]
0 0 ? 0 out ["text", "importance"]One row per plan node, printed in execution order; atom_idx 0 is always the
rule's output node. The columns:
| Column | Meaning |
|---|---|
stratum | Which stratum the rule was assigned to (see Stratification). |
rule, rule_idx | The rule this node belongs to, and a running clause counter within the stratum. |
atom_idx | Position within the rule's pipeline, counted from the output. |
op | The operator: scans (load_stored, load_mem), joins (stored_prefix_join, stored_mat_join, mem_prefix_join, …), unify, filter, reorder, and the output nodes out / aggr_out (meet aggregations show meet_aggr_out, bounded meets bounded_meet_aggr_out; fixed-rule strata show fixed). |
ref | What a scan or unification refers to: :relation for stored relations, a rule name for in-memory ones, a binding for unify. |
joins_on | The binding-to-column equalities a join uses. Empty ({}) means a Cartesian product. |
filters/expr | Predicates pushed into this node, or a unification's expression. |
out_relation | The bindings flowing out of the node. |
Generated names in the bindings follow a convention: *N is a binding the
normalizer invented for an inline constant or parameter, ~N is a column you
did not bind (ignored), and **N is a compile-time alias for a join key.
Reading this plan top to bottom:
unifybinds*2to"Postgres"— the constant in*entity{ name: 'Postgres' }was extracted into a generated binding during normalization and is bound first.load_stored :entity+stored_mat_joinon{"*2": "**0"}—nameis a non-key column ofentity, so there is no keyed access path: the engine scans the relation and keeps rows whosenamematches. When you seestored_mat_join, the joined columns did not form a key prefix.load_stored :mentions+stored_mat_joinon{"eid": "**1"}—eidis bound, but it matches the second key column ofmentions(its key ismemory, entity), and key matching is prefix-only. Another scan-and-match. An index whose key starts withentitywould restore a keyed path — shown under Evaluating atoms.load_stored :memorywith["gt(importance, 0.5)"]— theimportance > 0.5predicate was pushed into the access ofmemory, the first node where all of its variables are bound. Failing rows are dropped as the relation is read and never enter a join.stored_prefix_joinon{"mid": "**2"}—midis bound and ismemory's full primary key, so each probe is a keyed point lookup, logarithmic in the relation size. This is the operator you want to see on large relations.
Running the query:
text importance
Slow connector queries trace to a missing tenant_id index 0.75The rest of this page explains where each part of that plan comes from.
Disjunctive normal form
Evaluation starts by canonicalizing inline rules into disjunctive normal form, i.e., a disjunction of conjunctions, with any negation pushed to the innermost level. Each clause of the outermost disjunction is then treated as a separate rule. The consequence is that the safety rule may be violated even though textually every variable in the head occurs in the body:
?[a, b] := *memory{ id: a } or *entity{ id: b }This is rewritten into two rules, each missing one of the two head bindings, and the engine rejects it:
eval::unbound_symb_in_head
× Symbol 'b' in rule head is unbound
help: Note that symbols occurring only in negated positions are not
considered boundStratification
The next step is stratification. The engine builds a graph with the named rules as nodes, adding a link whenever one rule applies another — through body atoms for inline rules, and through input relations for fixed rules.
Some links are labelled stratifying:
- when an inline rule applies another rule through negation,
- when an inline rule that contains aggregations applies any rule other than itself,
- when an inline rule applies itself and it has aggregations that are not semi-lattice aggregations,
- when an inline rule applies another rule whose aggregations are all semi-lattice aggregations,
- when an inline rule applies a fixed rule,
- when a fixed rule has another rule as an input relation.
The strongly connected components of this graph are then computed. If any strongly connected component contains a stratifying link, the query is unstratifiable and execution aborts. Otherwise the components are topologically sorted into strata: rules in the same stratum are logically executed together, and no stratifying link exists within a stratum. The engine merges components into as few strata as possible while preserving that restriction.
The semi-lattice exception in the third bullet is what lets recursion carry an
aggregate. min is a semi-lattice aggregation, so a shortest-distance rule
may apply itself:
dist[n, min(d)] := *recalls{ from: 'm2', to: n }, d = 1
dist[n, min(d)] := dist[c, d0], *recalls{ from: c, to: n }, d = d0 + 1
?[n, d] := dist[n, d]
:order nn d
m3 1
m4 2
m5 1Replace min with sum, which is not a semi-lattice aggregation, and the
self-application becomes a stratifying link inside a strongly connected
component:
dist[n, sum(d)] := *recalls{ from: 'm2', to: n }, d = 1
dist[n, sum(d)] := dist[c, d0], *recalls{ from: c, to: n }, d = d0 + 1
?[n, d] := dist[n, d]eval::unstratifiable
× Query is unstratifiable
help: The rule 'dist' is in the strongly connected component ["dist"],
and is involved in at least one forbidden dependencymnestic
Since mnestic 0.10.0, bounded-meet aggregates ride the same self-recursion
permit as semi-lattice aggregations: min_cost_k (k best derivations with
evidence, 0.10.0), host-registered dominance meets (0.10.1), and the built-in
pareto_min/pareto_max skyline aggregates (0.11.1) may all sit in
recursive rules. See Aggregations.
::explain shows the stratum assigned to every rule. Negation is the
easiest way to see two strata:
::explain {
linked[m] := *mentions{ memory: m }
?[id] := *memory{ id }, not linked[id]
}stratum rule atom_idx op ref joins_on
0 linked 1 load_stored :mentions
0 linked 0 out
1 ? 3 load_stored :memory
1 ? 2 load_mem linked
1 ? 1 mem_neg_prefix_join {"id": "**0"}
1 ? 0 out(Columns are trimmed here and below; the full output has the same nine columns
as the walkthrough above.) linked is fully computed in stratum 0; only then
does stratum 1 run the negated join against it.
Magic set rewrites
Within each stratum, inline rules are rewritten using magic sets, so that
recursive rules do not compute results that are immediately discarded.
Consider reachability along recalls edges, asked from a single seed:
reachable[a, b] := *recalls{ from: a, to: b }
reachable[a, b] := reachable[a, c], *recalls{ from: c, to: b }
?[r] := reachable['m2', r]r
m3
m4
m5Without the rewrite, the whole reachable relation — the transitive closure
from every memory — would be generated first, and everything not starting at
'm2' thrown away. The rewrite specializes reachable to the constant it is
called with. You can see it in the plan; the first rows are:
rule atom_idx op ref joins_on filters/expr
? 3 load_mem ?|S.0.0
? 2 load_mem reachable|Mbf
? 1 mem_prefix_join {"*1": "**0"}
? 0 out
reachable|Mbf 3 load_mem reachable|S.0.0bf
reachable|Mbf 2 load_stored :recalls
reachable|Mbf 1 stored_prefix_join {"a": "**0"}
reachable|Mbf 0 out
...
?|S.0.0 1 unify *1 "m2"
?|S.0.0 0 out(16 further rows compile the recursive clause and the rest of the plumbing.)
The naming convention: reachable|Mbf is the magic-rewritten version of
reachable with adornment bf — first argument bound, second free;
|I rules seed those bound arguments (here, from the ?|S.0.0 supplementary
relation that holds the constant 'm2'); |S.i.j relations thread the bound
set through clause i. The derivation is driven from 'm2' outward instead
of computing the full closure.
The rewritten query is guaranteed to yield the same relation for ?, and in
general yields fewer intermediate rows. The rewrite currently applies only to
inline rules without aggregations; the entry rule ? is never itself
rewritten.
Semi-naïve evaluation
After the rewrites, each stratum contains either a single fixed rule or a set of inline rules. Fixed rules run their specific implementations. For inline rules, each rule is assigned an output relation, and the semi-naïve algorithm evaluates them: a bottom-up strategy that deduces all facts derivable from the given facts, but in each iteration only joins against the delta — the facts newly derived in the previous iteration — until a fixpoint is reached.
Note
By contrast, top-down strategies start with stated goals and try to find proof for the goals. Bottom-up strategies have many advantages when the whole output of each rule is needed, but may waste time generating unused facts if only some of the output is kept. Magic set rewrites exist to eliminate precisely this weakness.
Ordering of atoms
After conversion to disjunctive normal form, each atom in a rule body is one of the following:
- an explicit unification,
- an application of a rule or a stored relation,
- an expression, which must evaluate to a boolean,
- a negation of an application.
The first two can introduce fresh bindings; the last two cannot. Atoms that
introduce bindings compile to joins; atoms that do not are applied as filters.
The inherited ordering pass keeps the generator atoms in their given order and
floats every filter to the earliest position where all of its variables are
bound — that is why gt(importance, 0.5) ended up attached to the :memory
access in the walkthrough above: filtering before joining minimizes the rows
that reach the next join.
That leaves one question the inherited engine never answered: who orders the generators? Upstream, the answer was "you do" — the join order is exactly the written order. When hand-tuning (or opting out of the reorder below), the strategy that works almost always is to put the most restrictive atoms that introduce new bindings first.
Equality pushdown
There are two ways to pin a key to a value, and upstream they compiled very
differently: k = 'm3', *memory{ id: k, .. } was a keyed lookup, while
*memory{ id: k, .. }, k == 'm3' was a full scan followed by a filter.
mnestic rewrites the second form into the first. Both now produce this
identical plan:
::explain { ?[kind, text] := *memory{ id, kind, text }, id == 'm3' }atom_idx op ref joins_on filters/expr
3 unify id "m3"
2 load_stored :memory
1 stored_prefix_join {"id": "**0"}
0 outmnestic
Specific to mnestic 0.8.0 — measured ~28–29× on single-row primary-key
lookups at 5,000 rows. The conversion is gated to non-numeric ground
values: op_eq treats 1 == 1.0 as true across Int/Float, but a keyed
lookup compares strictly, so numeric == keeps its post-filter semantics.
Details and benchmarks: Equality pushdown.
Greedy join reorder
Since 0.10.5, mnestic also orders the generator atoms themselves. A
deterministic, stat-free pre-pass reorders the positive stored-relation atoms
of an eligible conjunction — fewest new variables first, preferring a
fully-bound primary key on ties, falling back to written position — which is
exactly the fix for a conjunction written in schema order rather than join
order (the shape LLM agents produce). Here the two mentions atoms are
written adjacent, sharing no variable:
::explain {
?[e1, e2] := *mentions{ memory: a, entity: e1 },
*mentions{ memory: b, entity: e2 },
*recalls{ from: a, to: b }
}atom_idx op ref joins_on
5 load_stored :mentions
4 load_stored :recalls
3 stored_prefix_join {"a": "**0"}
2 load_stored :mentions
1 stored_prefix_join {"b": "**1"}
0 outThe pass moved recalls between them: each mentions scan is immediately
constrained by an edge, and the intermediate never exceeds the join frontier.
Opting out with :reorder written compiles the authored order verbatim:
::explain {
?[e1, e2] := *mentions{ memory: a, entity: e1 },
*mentions{ memory: b, entity: e2 },
*recalls{ from: a, to: b }
:reorder written
}atom_idx op ref joins_on
5 load_stored :mentions
4 load_stored :mentions
3 stored_prefix_join (cartesian) {}
2 load_stored :recalls
1 stored_prefix_join {"a": "**0", "b": "**1"}
0 outThe (cartesian) annotation marks a join with no shared bound variables —
joins_on is {} — so this plan pairs every mentions row with every
mentions row (81 intermediate rows from this 9-row relation, N² in general)
before recalls prunes. Both plans return the same seven rows:
e1 e2
e_maya e_rocksdb
e_pg e_pg
e_pg e_rocksdb
e_rocksdb e_rocksdb
e_rocksdb e_search
e_sam e_pg
e_search e_rocksdbmnestic
Specific to mnestic 0.10.5 (default on; tie-break fix in 0.10.7) —
measured 54.5× on the motivating triangle-join repro. The pass is the
identity on any already-greedy order, so hand-tuned queries compile
byte-identically; it declines rules with fewer than three stored-relation
atoms, derived-rule or index-search atoms, or multi-valued in
unifications; and a residual Cartesian step is both annotated in
::explain and reported via log::warn. A bare :limit without :order
also forces the written order, keeping the returned subset stable. It
consults no statistics — when a bad order is bad for a reason structure
cannot reveal, you are still the optimizer. Full design:
Greedy join reorder.
Evaluating atoms
How a single binding-introducing atom executes:
For unifications, the right-hand side — an expression with all variables
bound — is evaluated, and the result joined to the current relation (as in a
map-cat operation in functional languages).
Rules and stored relations are conceptually trees with composite keys sorted
lexicographically, so the cost of applying one is determined by whether the
bound variables and constants form a key prefix. recalls has key
(from, to); binding the first key column gives a prefix scan:
::explain { ?[to, s] := *recalls['m2', to, s] }atom_idx op ref joins_on filters/expr
3 unify *1 "m2"
2 load_stored :recalls
1 stored_prefix_join {"*1": "**0"}
0 outBinding only the second key column is not a prefix, so the whole relation must be scanned and matched:
::explain { ?[f, s] := *recalls[f, 'm5', s] }atom_idx op ref joins_on filters/expr
3 unify *1 "m5"
2 load_stored :recalls
1 stored_mat_join {"*1": "**0"}
0 outIf every key column is bound, the application matches at most one stored
tuple — a logarithmic-time existence check. For stored relations, check the
schema for the order of the keys to deduce the complexity; ::explain tells
you which access path you actually got.
A stored_mat_join on a large relation is the cue to add an index. The engine
selects one automatically when its key order fits. Querying mentions by its
second key column is a scan-and-match:
::explain { ?[mid] := *mentions{ memory: mid, entity: 'e_pg' } }atom_idx op ref joins_on filters/expr
3 unify *1 "e_pg"
2 load_stored :mentions
1 stored_mat_join {"*1": "**0"}
0 outAfter ::index create mentions:by_entity { entity, memory }, the same query
compiles to a prefix join against the index — no query change required:
atom_idx op ref joins_on filters/expr
3 unify *1 "e_pg"
2 load_stored :mentions:by_entity
1 stored_prefix_join {"*1": "**0"}
0 outRows are generated in a streaming fashion: joins proceed as soon as one row is available and do not wait for whole intermediate relations to materialize.
The factorized-counting advisory
One shape deterministic plans handle badly is count() over a join: the
naive plan enumerates every match only to increment a counter. mnestic ships
an opt-in rewrite that counts eligible acyclic joins without materializing
them, and — independent of whether the rewrite is enabled — an always-on
detector flags eligible queries directly in ::explain:
::explain {
?[count(m)] := *mentions{ memory: m, entity: e },
*recalls{ from: m, to: m2 },
*mentions{ memory: m2, entity: e2 }
}atom_idx op ref joins_on
5 load_stored :mentions
4 load_stored :recalls
3 stored_prefix_join {"m": "**0"}
2 load_stored :mentions
1 stored_prefix_join {"m2": "**1"}
0 aggr_outplus one extra row, carrying its message in the filters/expr column:
op filters/expr
factorize_advisory rule `?`: count over a materialized join; factorizes over separator {m, m2} into 2 components — see docs/specs/cardinality-algebra.mdThe advisory row means the detector recognized this count as factorizable —
worth measuring with factorization enabled (set_query_factorization(true)
from Rust, or db.set_query_factorization(True) from Python since 0.10.7).
No advisory on a count query is itself a signal: the body has a shape the
rewrite declines — a cycle, a !=, a count_unique — and will be counted
naively.
mnestic
Specific to mnestic 0.10.5. The rewrite is off by default and produces bit-identical, exact-integer answers when enabled (measured 4–342× on the motivating benchmark). Eligibility rules and the exact-counting design: Factorized counting.
Early stopping
For the entry rule ?, if :limit is specified as a query option, a counter
monitors how many valid rows have been generated, and the query stops as soon
as enough rows exist:
?[id] := *memory{ id }
:limit 3id
m1
m2
m3This only works when the entry rule is an inline rule and you do not specify
:order — with a sort, all rows must be generated before the limit can be
applied. As noted above, a bare :limit without :order also pins the
written atom order, so the subset you get back is deterministic.
mnestic
Early stopping bounds rows; a wall-clock budget bounds time. Since
mnestic 0.10.5, :timeout and ::kill actually interrupt a running query
mid-join (upstream, a ::kill could queue behind the very query it targeted,
and a :timeout was only honoured between rule applications),
and a Db-wide default timeout can be set from Rust or Python. See
Interruptibility & query budgets.
Adapted from the CozoDB documentation by Ziyang Hu and the Cozo Project Authors, used under CC‑BY‑SA‑4.0. Adaptations for mnestic are released under the same license. mnestic is an independent fork and is not affiliated with or endorsed by the original authors.