mnestic
GitHub

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:

  1. Inline rules are canonicalized into disjunctive normal form; each disjunct becomes its own rule.
  2. Each rule body's atoms are ordered: mnestic's equality pushdown, then its greedy join reorder, then the inherited binding-before-use pass.
  3. The rules are stratified into groups that can be evaluated together, or the query is rejected as unstratifiable.
  4. Within each stratum, magic set rewrites specialize recursive rules to the constants they are called with.
  5. The strata are evaluated bottom-up with the semi-naïve algorithm, stopping early when :limit is 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 m1m8, 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 edges

Here 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:

ColumnMeaning
stratumWhich stratum the rule was assigned to (see Stratification).
rule, rule_idxThe rule this node belongs to, and a running clause counter within the stratum.
atom_idxPosition within the rule's pipeline, counted from the output.
opThe 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).
refWhat a scan or unification refers to: :relation for stored relations, a rule name for in-memory ones, a binding for unify.
joins_onThe binding-to-column equalities a join uses. Empty ({}) means a Cartesian product.
filters/exprPredicates pushed into this node, or a unification's expression.
out_relationThe 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:

  • unify binds *2 to "Postgres" — the constant in *entity{ name: 'Postgres' } was extracted into a generated binding during normalization and is bound first.
  • load_stored :entity + stored_mat_join on {"*2": "**0"}name is a non-key column of entity, so there is no keyed access path: the engine scans the relation and keeps rows whose name matches. When you see stored_mat_join, the joined columns did not form a key prefix.
  • load_stored :mentions + stored_mat_join on {"eid": "**1"}eid is bound, but it matches the second key column of mentions (its key is memory, entity), and key matching is prefix-only. Another scan-and-match. An index whose key starts with entity would restore a keyed path — shown under Evaluating atoms.
  • load_stored :memory with ["gt(importance, 0.5)"] — the importance > 0.5 predicate was pushed into the access of memory, 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_join on {"mid": "**2"}mid is bound and is memory'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.75

The 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 bound

Stratification

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 n
n     d
m3    1
m4    2
m5    1

Replace 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 dependency

mnestic

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
m5

Without 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         out

mnestic

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         out

The 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         out

The (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_rocksdb

mnestic

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         out

Binding 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         out

If 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         out

After ::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         out

Rows 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_out

plus 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.md

The 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 3
id
m1
m2
m3

This 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.