Rules and patterns

This chapter defines all three rule forms, fixed and variadic patterns, rule actions and modifiers, multiplicity constraints, remainder bindings, right-hand-side comprehensions, sequence patterns over n-ary operators, and what makes matching complete over A, C, AC, and ACI operators.

The grammar

Semper has three surface forms for defining rules:

(rewrite lhs rhs [:when (pattern ...)] [:subsume] [:flatten] [:ruleset name])
(birewrite lhs rhs [:when (pattern ...)] [:flatten] [:ruleset name])
(rule (pattern ...) (action ...) [:flatten] [:ruleset name])
(rewrite seq-lhs rhs [:let ((name expr) ...)] [:when (expr ...)]
         [:flatten] [:ruleset name])

action = (union rhs rhs)
       | (set (operator rhs ...) rhs)
       | (operator rhs ...)

Square brackets mark optional syntax. The trailing modifiers may appear in any order, and :flatten at most once. Only an ordinary rewrite accepts :subsume. A general rule puts its query patterns in the first parenthesized list and its actions in the second. Its trailing modifiers are :flatten and :ruleset. The last form is a sequence rewrite, whose left-hand side holds a sequence pattern (Sequence patterns). Its :when holds right-hand-side expressions rather than patterns, and only this form accepts :let.

The set action is part of the surface grammar, but rule application does not implement it. The sort checker rejects a rule that contains it, before any command runs:

sort error: the `set` action (on 'f') is not implemented; write the value as a term and use `union` instead

Annex A gives the complete grammar.

Fixed-arity patterns

A pattern matches the e-graph rather than one syntax tree. Each application must be witnessed by an e-node, but the children of that node are e-classes. A nested pattern may therefore continue through any suitable node in a child class, even when the complete nested term was never inserted.

(sort Expr)
(function a () Expr)
(function b () Expr)
(function f (Expr) Expr)
(function g (Expr) Expr)
(function pair (Expr Expr) Expr)
(function seen (Expr) Expr)
(function same_args (Expr) Expr)

(rewrite (f (g x)) (seen x))
(rewrite (pair x x) (same_args x))

(let outer (f a))
(let inner (g b))
(let pair_term (pair a inner))
(union a inner)
(run 1)

(check-eq outer (seen b))
(check-eq pair_term (same_args a))

The program never inserts (f (g b)). It inserts (f a) and (g b), then places a and (g b) in the same e-class. The pattern (f (g x)) can match outer, binding x to b’s e-class.

Variables bind e-classes, not one spelling of a term. The repeated variable in (pair x x) is non-linear: its first occurrence binds x, and its second requires the same e-class. The union of a and inner therefore lets pair_term match.

For an ordinary fixed-arity operator, each pattern child corresponds to one declared argument position. A literal or nested application constrains that position. A fresh variable binds it, and a variable already bound elsewhere in the query checks equality with it.

rewrite, birewrite, and :subsume

A rewrite is directional in what triggers it, not in the equality it establishes. When the left-hand side matches, Semper builds the right-hand side and merges it with the matched root class. The equality is then symmetric, but an existing right-hand-side shape does not cause the left-hand side to be built.

(sort Expr)
(function a () Expr)
(function b () Expr)
(function c () Expr)
(function f (Expr) Expr)
(function g (Expr) Expr)
(function h (Expr) Expr)

(rewrite (f x) (g x))
(birewrite (f x) (h x))

(let forward (f a))
(let rhs_only (g b))
(let reverse (h c))
(run 3)

(check-eq forward (g a))
(check-eq forward (h a))
(check-neq rhs_only (f b))
(check-eq reverse (f c))

The first rule uses (f a) to build (g a). It does not use (g b) to build (f b). A birewrite installs two rewrites, one in each direction. Thus (f a) builds (h a), and (h c) builds (f c).

Neither form replaces or deletes its input. An ordinary rewrite leaves the matched left-hand-side node available to later rules. A rewrite with :subsume performs the same build and merge, then marks that matched e-node so future pattern indexes skip it. The node remains in its e-class and remains available to (extract term). Extraction under a cost model (Part V) excludes it. Matches already collected for the current application still execute.

birewrite rejects :subsume because subsuming either trigger would disable one direction of the installed pair.

General rules and actions

A general rule separates a conjunctive query from the actions performed for each match. Every pattern in the first list must match under one shared binding environment. A variable used by several patterns is a join key. Unlike rewrite, a general rule has no distinguished root and performs no implicit merge.

(sort Node)
(sort Fact)
(function a () Node)
(function b () Node)
(function c () Node)
(function edge (Node Node) Fact)
(function path (Node Node) Fact)
(function witnessed (Node Node) Fact)
(function group (Node) Node)

(rule ((edge x y) (edge y z))
      ((path x z)
       (union (group x) (group z))))

(rewrite (path x z) (witnessed x z))

(edge a b)
(edge b c)
(run 3)

(check-eq (path a c) (witnessed a c))
(check-eq (group a) (group c))

The shared y requires the destination of the first edge and the source of the second to be in the same e-class. The bare (path x z) action inserts a term. The following rewrite can fire only because that term was inserted. The union action builds both arguments and merges their e-classes.

Actions execute in source order:

Guards

A :when clause adds conjuncts to a rewrite query. Every guard pattern must match under the same binding environment as the left-hand side. The same guards are attached to both directions of a birewrite. A general rule places equivalent conjuncts directly in its query list.

A guard with no shared variables is independent of the left-hand side. One matching fact enables the rewrite. Several matching facts may produce several query rows and apply the same actions more than once.

(sort Expr)
(sort Fact)
(function item () Expr)
(function source (Expr) Expr)
(function result (Expr) Expr)
(function assumption () Fact)
(function num (i64) Expr)
(function small (Expr) Expr)

(rewrite (source x) (result x)
  :when ((assumption)))

(rewrite (num n) (small (num n))
  :when ((i64::< n 5)))

(let waiting (source item))
(num 3)
(num 7)
(run 2)

(check-neq waiting (result item))
(check-eq (small (num 3)) (num 3))
(check-neq (small (num 7)) (num 7))

(assumption)
(run 2)
(check-eq waiting (result item))

Before (assumption) is inserted, the first rewrite cannot fire. Once that unrelated fact exists, it enables the rewrite for waiting. A fact inserted between runs is visible to the next run. A fact produced during a matching round becomes visible after the next index build.

The second guard is a primitive predicate rather than an e-node pattern. (num n) binds an i64 literal value, and i64::< keeps only the match for 3. A primitive predicate must be a top-level query conjunct, may use literal values bound by other query patterns, and must return bool. Matching computes and discards its result without inserting a literal node.

Rulesets

Rulesets partition installed rules into explicitly selected groups. A named ruleset must be declared before a command refers to it. Adding :ruleset name assigns a rewrite, birewrite, or general rule to it. Untagged rules belong to the default ruleset.

(sort Expr)
(function item () Expr)
(function old (Expr) Expr)
(function reduced (Expr) Expr)
(function final (Expr) Expr)
(function stale (Expr) Expr)

(ruleset simplify)

(rewrite (old x) (reduced x) :subsume :ruleset simplify)
(rewrite (old x) (stale x))
(rewrite (reduced x) (final x))

(let value (old item))

(run simplify 2)
(check-eq value (reduced item))
(check-neq value (final item))

(run 2)
(check-eq value (final item))
(check-neq value (stale item))

The first run selects simplify, so only the tagged rewrite fires. It merges value with (reduced item) and subsumes the matched (old item) node. The untagged rewrite to final does not participate.

The bare second run selects the default ruleset. It can rewrite (reduced item) to (final item), but the subsumed (old item) node cannot produce (stale item). A run selects exactly one ruleset. It does not include named rulesets implicitly.

Variadic patterns and remainders

Associative, AC, and ACI declarations produce variadic nodes. Their patterns do not bind a fixed list of declared positions. They select children from an ordered sequence, multiset, or set. A rest variable such as ..rest binds the children not selected by the fixed pattern elements.

The absence of a rest variable makes the pattern exact. Every stored child must then be consumed. With a rest variable, one node may produce several matches as different children satisfy the fixed elements. Splicing ..rest on the right-hand side copies the unmatched collection into the new application.

Chapter 4’s singleton collapse also applies to matching. A one-child pattern such as (Set x) normally has no one-child Set node to match (Patterns that do not match). (Set x ..rest) binds one member while allowing the stored node to contain additional members.

Ordered patterns (:assoc)

An associative-only operator stores an ordered, flattened sequence. Fixed pattern elements match a contiguous window. A rest variable after them binds the suffix, one before them binds the prefix, and rests on both sides bind the prefix and suffix around a sliding window.

(function Front (E) E :assoc)
(function Back (E) E :assoc)
(function First (E) E)
(function Last (E) E)

(rewrite (Front x ..rest) (First x))
(rewrite (Back ..rest x) (Last x))

(let front (Front a b c))
(let back (Back a b c))
(run 1)

(check-eq front (First a))
(check-eq back (Last c))
(check-neq front (First b))
(check-neq back (Last a))

The front rule binds the first child, while the back rule binds the last. Changing source order changes both matches.

(function Window (E) E :assoc)
(function Adjacent (E E) E)
(rewrite (Window ..prefix x y ..suffix) (Adjacent x y))

(let window (Window a b c d))
(run 1)

(check-eq window (Adjacent a b))
(check-eq window (Adjacent b c))
(check-eq window (Adjacent c d))
(check-neq window (Adjacent a c))

The two fixed variables slide across three adjacent pairs in a four-child sequence. They never match the nonadjacent pair a,c. Without either rest variable, the same two-child pattern would match only a sequence with exactly two children.

A repeated variable in a sequence pattern constrains positions. For example, (Seq ..pre x x ..suffix) matches two adjacent children in the same e-class. It does not match equal children separated by another element.

Multiset patterns

An AC operator stores each distinct child with its multiplicity. Every scalar pattern element binds one distinct stored child and consumes that child’s whole multiplicity. A bare element has an implicit exact multiplicity of one. The rest receives all unbound children with their complete multiplicities.

(function Add (E) E :assoc-comm :identity zero)
(function Selected (E E) E)

(rewrite (Add x:count>=2 ..rest)
         (Selected x (Add ..rest)))

(let sum (Add a a a b b))
(run 1)

(check-eq sum (Selected a (Add b b)))
(check-eq sum (Selected b (Add a a a)))

The one node has two matches. Binding x to a also binds k to 3 and gives b:2 to rest. Binding x to b binds k to 2 and gives a:3 to rest. The matcher does not leave two copies of the selected child in the remainder.

Multiplicity annotations have these forms:

The relational form accepts >=, >, <=, <, ==, and !=. Semper collects the constraints on each multiplicity variable and reduces them to a closed interval used during rule installation:

Constraints from repeated uses are intersected. An empty intersection rejects the rule as unsatisfiable. Reusing the same multiplicity variable also makes it non-linear: all occurrences must bind the same count.

(function Mul (E) E :assoc-comm)
(function Twice (E) E)
(rewrite (Mul x:2 ..rest) (Twice x))

(let exact (Mul a a b))
(run 1)
(check-eq exact (Twice a))
(check-neq exact (Twice b))

(function Sum (E) E :assoc-comm)
(function Balanced () E)
(rewrite (Sum x:count y:count ..rest) (Balanced))

(let balanced (Sum c c g g))
(let unbalanced (Sum c c c g g))
(run 1)
(check-eq balanced (Balanced))
(check-neq unbalanced (Balanced))

The exact rule accepts a:2 but not b:1. The non-linear rule accepts the node where two distinct children both have count two and rejects the node whose counts are three and two.

Set patterns

An ACI operator stores a set, so every represented child has multiplicity one. A scalar element binds one distinct member. The remainder receives every unbound member.

(function Conj (E) E :assoc-comm-idem :identity top)
(function Absorbed (E) E)
(rewrite (Conj (a) (b) ..rest)
         (Absorbed (Conj (d) ..rest)))

(let ordered (Conj a b c))
(let permuted (Conj b a c))
(run 1)
(check-eq ordered permuted)
(check-eq ordered (Absorbed (Conj d c)))

(function Pick (E) E :assoc-comm-idem)
(function Pair (E E) E)
(function RepeatedSet () E)
(rewrite (Pick x y ..rest) (Pair x y))
(rewrite (Pick x x ..rest) (RepeatedSet))

(let pair_source (Pick a c))
(run 1)
(check-eq pair_source (Pair a c))
(check-eq pair_source (Pair c a))
(check-neq pair_source (RepeatedSet))

(function ExactSet (E) E :assoc-comm-idem)
(function Exactly () E)
(rewrite (ExactSet (a) (b)) (Exactly))

(let exact_pair (ExactSet a b))
(let exact_triple (ExactSet a b c))
(run 1)
(check-eq exact_pair (Exactly))
(check-neq exact_triple (Exactly))

The first rule finds a and b in either source order and reconstructs the remainder with d. The second rule’s two variables bind distinct set members. The repeated-variable rule cannot match because one set member cannot satisfy two scalar elements.

Multiplicity annotations on set elements are errors, including x:1.

(sort E)
(function Set (E) E :assoc-comm-idem)
(function Mark (E) E)
(rewrite (Set x:1 ..rest) (Mark x))

Use an AC operator when a rule needs to observe or constrain counts.

Multiplicities on the right-hand side

A multiplicity bound on the left-hand side can be used as an i64 term or as an argument to an i64 primitive. This conversion constructs an ordinary literal term on the right-hand side:

;; A query multiplicity can fill an i64 term or primitive argument.
(function Count (i64) E)
(function CountPair (E E) E)
(function MeasureBag (E) E :assoc-comm)
(function MeasureBox (E E) E)

(rewrite (MeasureBox (Num offset)
                     (MeasureBag element:count ..rest))
         (CountPair
           (Count count)
           (Count (i64::+ count offset))))

(let measured
  (MeasureBox (Num 10) (MeasureBag a a a)))
(run 1)
(check-eq measured (CountPair (Count 3) (Count 13)))

The query binds count to three. (Count count) constructs the literal term Count(3), while the primitive expression constructs Count(13). Multiplicity variables are accepted only where an i64 value is expected.

A child of a variadic right-hand side may also carry an output multiplicity: term:count, term:2, or term:(u64::- count 1). Under an AC operator it is the child’s count; under an associative operator the child is repeated. An ACI operator stores a set, so a count on its child is rejected. Multiplicity expressions use u64::+, u64::-, u64::*, u64::/, u64::%, u64::min, and u64::max, each with two arguments. A sequence rewrite accepts +, -, *, min, and max, with or without the u64:: prefix, and no division or remainder.

Subtraction is accepted only when the collected left-hand-side interval proves that it cannot underflow. Division and remainder require a divisor whose interval excludes zero. Addition and multiplication use checked arithmetic at runtime: an overflow, or a computed count too wide for the configured multiplicity type, stops the run with an error naming the rule and the operands rather than wrapping or aborting the process. An output multiplicity of zero omits the child without evaluating its term.

Occurrences and empty applications

A count is a number of occurrences, so it is at least 1, and an omitted count is 1. A count of 0 says that the element does not occur, so writing x:0 says nothing: it is rejected in a ground term, a pattern, and a right-hand side. A count that a multiplicity expression computes to 0 is different: the child is absent, and it is dropped.

An application of an A, AC, or ACI operator with no children denotes the operator’s identity. It therefore has a meaning only when the operator declares :identity, and then it reduces to the identity element. Without one it means nothing, and Semper never builds it:

• written in a ground term or a right-hand side, it is rejected when the program is checked (“operator ‘Add’ has no :identity, so an application of it with no children is meaningless”);
• written as a pattern, it is rejected because no stored node is empty;
• left empty at run time, because every child’s count was computed to 0 or a rest was empty, the action is not applied, and the run prints warning: N rule action(s) not applied: the right-hand side was an application with no children of an operator without :identity, which has no meaning.

A sequence rule treats a right-hand side with no value the same way: the match does not fire, and the run reports the count.

Splicing and comprehensions

A plain ..rest splice copies a rest binding unchanged. A comprehension maps its elements while splicing the results into the surrounding application:

(sort E)
(function a () E)
(function b () E)
(function c () E)
(function marker () E)
(function F (E) E)

(function Seq (E) E :assoc)
(function Set (E) E :assoc-comm-idem)
(function Bag (E) E :assoc-comm)

(rewrite (Seq first ..rest)
         (Seq (F first) ..[(F element) for element in rest]))
(rewrite (Set chosen ..rest)
         (Set (F chosen) ..{(F element) for element in rest}))
(rewrite (Bag chosen:1 ..rest)
         (Bag (F chosen)
              ..{(F element):count for element:count in rest}))

(let sequence (Seq a b c))
(let set (Set a b c))
(let bag (Bag a b b c c c))
(run 1)

(check-eq sequence (Seq (F a) (F b) (F c)))
(check-eq set (Set (F a) (F b) (F c)))
(check-eq bag (Bag (F a) (F b) (F b) (F c) (F c) (F c)))

A sequence comprehension uses ..[...] and visits its source in order. A set comprehension uses ..{...} and visits each member once. A multiset comprehension also uses braces, but requires both multiplicity annotations: body:output-count and element:source-count. It visits each distinct child once and exposes the child’s complete source count.

In an ordinary rule, the source after in must be an LHS rest binding of the required collection kind. A comprehension cannot iterate an arbitrary right-hand-side term there. Tuple binders and expression sources belong to sequence rewrites (Comprehensions). Its element binder has the source collection’s element sort, and its body must produce the destination operator’s element sort. A comprehension can therefore map between sorts through a declared function. A direct ..rest splice performs no mapping, so its source and destination element sorts must be equal. Splices and comprehensions are rejected under fixed-arity destination operators.

Filters

An optional if computes one concrete literal value per source element. The body is emitted only when the active literal model considers that value truthy.

;; A filter computes a literal value. It is not an e-graph existence query.
(function Num (i64) E)
(function FilterBox (E E) E)
(function FilterBag (E) E :assoc-comm)

(rewrite (FilterBox (Num threshold)
                    (FilterBag marker:1 ..rest))
         (FilterBag
           ..{(F element):count
              for element:count in rest
              if (i64::< threshold count)}))

(let filtered
  (FilterBox (Num 1)
             (FilterBag marker a b b c c c)))
(run 1)
(check-eq filtered
          (FilterBag (F b) (F b) (F c) (F c) (F c)))

The filter combines the LHS-bound threshold with the current source count. It keeps children whose multiplicity is greater than one.

A filter is not an e-graph query. An ordinary application such as (Keep element) would construct an e-node rather than compute a literal, so Semper rejects it:

(sort E)
(function a () E)
(function b () E)
(function Keep (E) E)
(function Seq (E) E :assoc)

(rewrite (Seq first ..rest)
         (Seq first
              ..[element
                 for element in rest
                 if (Keep element)]))

(let term (Seq a b))
(run 1)

To require a graph fact, bind the element on the LHS and add (Keep element) as a rewrite guard or a conjunct of a general rule.

Lexical scope

The source rest variable is resolved in the enclosing environment. The element and optional source-count binders then introduce fresh local names for the body, output multiplicity, and filter. These locals shadow outer names and disappear after the comprehension. Outer query bindings remain unchanged.

;; The local element shadows the query binding only inside the comprehension.
(function Keep (E) E)
(function ScopeBox (E E) E)
(function ScopeSeq (E) E :assoc)

(rewrite (ScopeBox element (ScopeSeq first ..rest))
         (ScopeSeq
           ..[(F element) for element in rest]
           (Keep element)))

(let scoped (ScopeBox a (ScopeSeq b c marker)))
(run 1)
(check-eq scoped (ScopeSeq (F c) (F marker) (Keep a)))

The local element maps c and marker. After the comprehension, the final (Keep element) refers to the unchanged outer binding a. Sibling and nested comprehensions may reuse binder names because each introduces a new scope.

The element and count names of one multiset comprehension must differ. for k:k is rejected as a duplicate declaration in one scope.

(sort E)
(function Bag (E) E :assoc-comm)
(rewrite (Bag selected:1 ..rest)
         (Bag ..{k:k for k:k in rest}))

Computed output counts

A multiset comprehension can transform each source count:

;; A zero output count omits the body. Here a:1 disappears and b:3 becomes b:2.
(function ReducedBag (E) E :assoc-comm)
(rewrite (ReducedBag marker:1 ..rest)
         (ReducedBag
           ..{(F element):(u64::- count 1)
              for element:count in rest}))

(let reduced (ReducedBag marker a b b b))
(run 1)
(check-eq reduced (ReducedBag (F b) (F b)))

Each local source count is at least one, so subtracting one is statically safe. The count-one child maps to zero and is omitted without constructing (F a). The count-three child produces two copies of (F b).

Sequence patterns

A sequence pattern matches a run of children of an n-ary node in one match, and the right-hand side computes over the whole run. It is written at the root of a rewrite over an :assoc, :assoc-comm, or :assoc-comm-idem operator. Three items make up the pattern:

Every variable of a filter’s pattern binds a sequence with one entry per child the filter took, in the same order. A node with no matching child still matches, with the filter empty. The right-hand side, :let, and :when read those sequences.

Merging and factoring under ACI

The example below is the pair of rules the book’s MLTL examples use (MLTL, a temporal logic with interval-bounded operators, is introduced in Chapter 24). The first merges the always-windows of one operand into maximal runs; the second gives all the always-operators of a conjunction one outer window.

(sort IntervalSort)
(function Interval (i64 i64) IntervalSort)
(sort MLTL)
(function Var (String) MLTL)
(function Not (MLTL) MLTL)
(function And (MLTL) MLTL :assoc-comm-idem)
(function Global (IntervalSort MLTL) MLTL)
(function Future (IntervalSort MLTL) MLTL)

; Merge: every G in a conjunction over one operand whose windows form a
; contiguous union becomes one G over that union.
(rewrite (And (..gs (Global (Interval l u) p)) ..rest)
         (And ..{ (Global (Interval a b) q) for (q a b) in (union-by p l u) } ..rest)
  :when ((< (count (union-by p l u)) (count gs))))

; Factor: all G in a conjunction share one outer window.
(rewrite (And (..gs (Global (Interval l u) p)) ..rest)
         (And (Global (Interval K0 K1)
                      (And ..{ (if (and (== l K0) (== u K1)) p (Global (Interval (- l K0) (- u K1)) p))
                               for (l u p) in (zip l u p) }))
              ..rest)
  :let ((K0 (min l)) (K1 (+ K0 (min (- u l)))))
  :when ((>= (count gs) 2) (> K1 0) (== (count (union-by p l u)) (count gs))))

(let a (Var "a")) (let b (Var "b")) (let x (Var "x"))
(let m (And (Global (Interval 0 3) a) (Global (Interval 4 6) a) x))
(let f (And (Global (Interval 2 5) a) (Global (Interval 4 9) b) x))
(run 2)
(check-eq m (And (Global (Interval 0 6) a) x))
(check-eq f (And x (Global (Interval 2 5) (And a (Global (Interval 2 4) b)))))

The first rule merges G[0,3] a and G[4,6] a into G[0,6] a. The second gives the two windows of f the common outer window [2,5] over one inner conjunction. The inner window of a is [0,0], which is a itself.

The expressions available on the right-hand side, in :let, and in :when are:

• reductions of a sequence: min, max, sum, count;
• the scalar primitives of Chapter 3, applied element by element inside a reduction or a comprehension, and if;
• splices ..name, which put a matched sequence back as children;
• comprehensions ..{ body for binders in source }, which build unordered children, and ..[ body for binders in source ], which build ordered ones;
• the sequence primitives (zip s1 ... sn) (positions paired, shortest input wins), (concat s1 ... sn), (union-by p l u) (the windows [l, u] grouped by p and unioned into maximal runs), (narrow ...), and (narrowed ...).

A sequence used where a scalar is expected is rejected when the rule is checked. A min or max of an empty sequence has no value, and the rule does not fire on that node.

Runs under an associative operator

Under :assoc the items cover the children in written order, so a pattern is a regular expression over the child list: one child, a run, or a gap. Any number of gaps is allowed. A run next to a gap is maximal toward it.

(sort E)
(function a () E)
(function b () E)
(function F (E) E)
(function H (E) E)
(function Cat (E) E :assoc)

; Under an associative operator the items cover the children in order:
; `..pre` and `..suf` are gaps, `(..fs (F x))` is a run of F children.
(rewrite (Cat ..pre (..fs (F x)) ..suf) (Cat ..pre (H (Cat ..fs)) ..suf)
  :when ((>= (count fs) 2)))

(let e (Cat a (F a) (F b) b (F a)))
(run 1)
; The run is maximal toward its gaps: both F children before `b` are taken.
; The lone (F a) at the end is a run of length 1, which the guard rejects.
(check-eq e (Cat a (H (Cat (F a) (F b))) b (F a)))

Multiplicities under AC

Under :assoc-comm each child carries a multiplicity. A filter takes the annotation of an ordinary AC element after its name: (..fs:k P) takes any multiplicity and binds it, (..fs:k>=2 P) takes only those at least 2, and :3 takes exactly 3. An unannotated filter takes only children of multiplicity 1, as an unannotated AC element does. Outside the filter, k is a sequence parallel to fs, so (sum k) counts copies and (count fs) counts distinct children.

(sort E)
(function a () E)
(function b () E)
(function c () E)
(function F (E) E)
(function N (i64) E)
(function Only (E) E)
(function All (E) E)
(function Plus (E) E :assoc-comm)
(function Src () E)

; `:k>=2` takes the children of multiplicity at least 2 and binds each one's
; multiplicity in the column `k`; `(sum k)` adds them.
(rewrite (Plus (..fs:k>=2 (F x)) ..rest) (Plus (N (sum k)) ..rest)
  :when ((>= (count fs) 1)))
(let e (Plus (F a) (F a) (F b)))
(run 1)
(check-eq e (Plus (N 2) (F b)))

; An unannotated filter takes only children of multiplicity 1, as an
; unannotated AC element does. `:k` with no bound takes any multiplicity.
(let src (Src))
(rewrite (Src) (Plus (F (a)):3 (F (b)) (c)))
(run 1)
(rewrite (Plus (..fs (F y)) ..rest) (Only (Plus ..fs)))
(rewrite (Plus (..ks:k (F y)) ..rest) (All (Plus ..ks)))
(run 1)
(check-eq src (Only (F b)))
(check-eq src (All (Plus (F a) (F a) (F a) (F b))))

Several filters, and :except

Filters are matched independently. A child that two filters match is given to each in turn, and every assignment is a match. :except other removes from a filter the children other’s pattern matches, for a rule that wants one assignment. :except is accepted under AC and ACI only, since under :assoc order already separates runs, and it must name a sibling filter.

(sort E)
(function a () E)
(function b () E)
(function Not (E) E)
(function Gl (E) E)
(function N (i64) E)
(function Split (E E) E)
(function Kept (E E) E)
(function And (E) E :assoc-comm-idem)
(function Conj (E) E :assoc-comm-idem)
(function Both () E)
(function One () E)

; (Gl (Not a)) matches both `(Gl (Not q))` and `(Gl p)`.
(let both (Both))
(let one (One))
(rewrite (Both) (And (Gl (Not (a))) (Gl (b))))
(rewrite (One) (Conj (Gl (Not (a))) (Gl (b))))
(run 1)

; Without `:except`, a child that two filters match is given to each in turn,
; and every assignment is a match.
(rewrite (And (..ns (Gl (Not q))) (..gs (Gl p)) ..rest)
         (Split (N (count ns)) (N (count gs))))
; With `:except ns`, `gs` keeps only what `ns` does not match: one assignment.
(rewrite (Conj (..ns (Gl (Not q))) (..gs (Gl p) :except ns) ..rest)
         (Kept (N (count ns)) (N (count gs))))
(run 1)
(check-eq both (Split (N 1) (N 1)))
(check-eq both (Split (N 0) (N 2)))
(check-eq one (Kept (N 1) (N 1)))
(check-neq one (Kept (N 0) (N 2)))

Simple items beside filters

A plain pattern beside filters takes one child, and every choice of child is a separate match. The filters then take from the remaining children. The same holds for the member of a class: where several members of a child’s class match, each is a separate match.

(sort E)
(function a () E)
(function b () E)
(function c () E)
(function Not (E) E)
(function F (E) E)
(function N (i64) E)
(function Pick (E E) E)
(function And (E) E :assoc-comm-idem)

; A simple item `(Not x)` beside a filter takes one child; every choice is a
; separate match. The filter then takes every remaining F child.
(rewrite (And (Not x) (..fs (F y)) ..rest) (Pick x (N (count fs))))
(let e (And (Not (a)) (Not (b)) (F (c))))
(run 1)
(check-eq e (Pick (a) (N 1)))
(check-eq e (Pick (b) (N 1)))

Comprehensions

A comprehension’s binders name the columns of its source. An element comprehension for f:k in fs reads each child with its multiplicity, and the body states the output multiplicity after a colon. A column of a multiset sequence must be bound as x:k, or as x:_ to drop the multiplicity; a bare x there is rejected, since whether the count is dropped would be implicit.

(sort E)
(function a () E)
(function b () E)
(function F (E) E)
(function G (E) E)
(function K (E E) E)
(function Cat (E) E :assoc)
(function Plus (E) E :assoc-comm)
(function Pairs () E)
(function Twice () E)
(function Both () E)

; `..[ body for binders in source ]` builds an ordered sequence; `zip` pairs
; positions and stops at the shortest input.
(let pairs (Pairs))
(rewrite (Pairs) (Cat (F (a)) (F (b)) (G (b)) (G (a))))
(run 1)
(rewrite (Cat (..fs (F x)) (..gs (G y)))
         (Cat ..[ (K x y) for (x y) in (zip x y) ]))

; An element comprehension `for f:k in fs` reads each child with its
; multiplicity `k`; the body states the output multiplicity.
(let twice (Twice))
(rewrite (Twice) (Plus (F (a)):2 (b)))
(run 1)
(rewrite (Plus (..fs:k>=2 (F x)) ..rest) (Plus ..{ (G x):(* k k) for f:k in fs } ..rest))

; `concat` joins sequences of one element type.
(let both (Both))
(rewrite (Both) (Cat (F (a)) (G (b))))
(run 1)
(rewrite (Cat (..fs (F x)) (..gs (G y))) (Plus ..{ z for z in (concat x y) }))
(run 1)
(check-eq pairs (Cat (K (a) (b)) (K (b) (a))))
(check-eq twice (Plus (G (a)) (G (a)) (G (a)) (G (a)) (b)))
(check-eq both (Plus (a) (b)))

Narrowing

(narrow c d r a b q) reads one eventually-window [c, d] over r per row of its first three columns, and the always-windows [a, b] over q of the last three. For each r it shrinks [c, d] past the windows whose q is r, and gives one row (r c2 d2). (narrowed ...) gives only the rows whose window changed, so a guard on its count keeps the rule from rewriting a node to itself.

(sort IntervalSort)
(function Interval (i64 i64) IntervalSort)
(sort MLTL)
(function Var (String) MLTL)
(function Not (MLTL) MLTL)
(function And (MLTL) MLTL :assoc-comm-idem)
(function Global (IntervalSort MLTL) MLTL)
(function Future (IntervalSort MLTL) MLTL)

; Narrowing: an eventually F[c,d] r beside always-windows G[a,b] (Not r) cannot
; be satisfied inside those windows, so its window shrinks past them.
; `(narrow c d r a b q)` gives one row (r c2 d2) per F; `(narrowed ...)` gives
; only the rows whose window changed, which guards against a no-op rewrite.
(rewrite (And (..ns (Global (Interval a b) (Not q)))
              (..fs (Future (Interval c d) r)) ..rest)
         (And ..ns ..{ (Future (Interval c2 d2) r2) for (r2 c2 d2) in (narrow c d r a b q) } ..rest)
  :when ((> (count (narrowed c d r a b q)) 0)))

(let r (Var "r"))
(let e (And (Global (Interval 0 3) (Not r)) (Future (Interval 2 6) r)))
(run 1)
(check-eq e (And (Global (Interval 0 3) (Not r)) (Future (Interval 4 6) r)))

Splicing across operator kinds

A sequence matched under one kind can be spliced under another. From AC to ACI the multiplicities are dropped. From an unordered match to an ordered operator, the children come in the order the e-graph stores them, which is not a function of the e-graph’s contents, and the checker warns.

(sort E)
(function a () E)
(function b () E)
(function F (E) E)
(function Cat (E) E :assoc)
(function And (E) E :assoc-comm-idem)
(function Plus (E) E :assoc-comm)
(function Src () E)

; A sequence matched under one operator kind can be spliced under another. An
; ordered result from an unordered match takes the children in the order the
; e-graph stores them, which the checker warns about.
(rewrite (And (..fs (F x)) ..rest) (Cat ..fs))
; AC to ACI: multiplicities are dropped, as ACI keeps one copy of each child.
(rewrite (Plus (..fs:k (F x)) ..rest) (And ..fs))
(let e (And (F (a)) (b)))
(let p (Src))
(rewrite (Src) (Plus (F (a)):3 (b)))
(run 2)
(check-eq e (Cat (F (a))))
(check-eq p (F (a)))

Rejected forms

The checker rejects the five shapes below, each with a reason. It also rejects a root that is not A, AC, or ACI, a sequence pattern below the root, a rest or a non-plain operator inside a filter’s pattern, and a name bound twice, by two filters or by a filter and a simple item.

A sequence pattern under a :comm operator. Such a node has exactly two children, and two simple patterns already match it in both orders:

(sort IntervalSort)
(function Interval (i64 i64) IntervalSort)
(sort MLTL)
(function Bool (bool) MLTL)
(function Var (String) MLTL)
(function Not (MLTL) MLTL)
(function And (MLTL) MLTL :assoc-comm-idem :identity (Bool true))
(function Cat (MLTL) MLTL :assoc)
(function Bag (MLTL) MLTL :assoc-comm)
(function Pair (MLTL MLTL) MLTL :comm)
(function Global (IntervalSort MLTL) MLTL)
(rewrite (Pair (..gs (Global (Interval l u) p)) ..rest) (Bool true))

A filter inside a filter:

(sort IntervalSort)
(function Interval (i64 i64) IntervalSort)
(sort MLTL)
(function Bool (bool) MLTL)
(function Var (String) MLTL)
(function Not (MLTL) MLTL)
(function And (MLTL) MLTL :assoc-comm-idem :identity (Bool true))
(function Cat (MLTL) MLTL :assoc)
(function Bag (MLTL) MLTL :assoc-comm)
(function Global (IntervalSort MLTL) MLTL)
(rewrite (And (..gs (Global (Interval l u) (And (..hs p)))) ..rest) (And ..rest))

Two bare sequences under AC or ACI, which would divide the remaining children with nothing to tell them apart:

(sort IntervalSort)
(function Interval (i64 i64) IntervalSort)
(sort MLTL)
(function Bool (bool) MLTL)
(function Var (String) MLTL)
(function Not (MLTL) MLTL)
(function And (MLTL) MLTL :assoc-comm-idem :identity (Bool true))
(function Cat (MLTL) MLTL :assoc)
(function Bag (MLTL) MLTL :assoc-comm)
(function Global (IntervalSort MLTL) MLTL)
(rewrite (And (..gs (Global (Interval l u) p)) ..a ..b) (And ..gs ..a ..b))

An :except cycle, where a child matching every filter of the cycle would go to none:

(sort IntervalSort)
(function Interval (i64 i64) IntervalSort)
(sort MLTL)
(function Bool (bool) MLTL)
(function Var (String) MLTL)
(function Not (MLTL) MLTL)
(function And (MLTL) MLTL :assoc-comm-idem :identity (Bool true))
(function Cat (MLTL) MLTL :assoc)
(function Bag (MLTL) MLTL :assoc-comm)
(function Pair (MLTL MLTL) MLTL :comm)
(function Global (IntervalSort MLTL) MLTL)
(rewrite (And (..a (Global (Interval l u) p) :except b) (..b (Global (Interval m v) q) :except a) ..rest) (And ..a ..b ..rest))

A sequence pattern anywhere but the left-hand side of a rewrite:

(sort IntervalSort)
(function Interval (i64 i64) IntervalSort)
(sort MLTL)
(function Bool (bool) MLTL)
(function Var (String) MLTL)
(function Not (MLTL) MLTL)
(function And (MLTL) MLTL :assoc-comm-idem :identity (Bool true))
(function Cat (MLTL) MLTL :assoc)
(function Bag (MLTL) MLTL :assoc-comm)
(function Global (IntervalSort MLTL) MLTL)
(rule ((= e (And (..gs (Global (Interval l u) p)) ..rest))) ((union e e)))

When sequence rules run

Sequence rules are matched in each round on the round’s snapshot, together with the ordinary rules, by one Collect step of the compiled query. Under --use-semi-naive they are semi-naive with the ordinary rules: each rule assembles only the nodes whose matches can have changed, when its estimate says that pays, and otherwise matches naively. Without the flag they are naive.

Alternatives considered

The design went through several forms, and four were rejected with a measured reason.

• (each name pattern) and a pass after each round. The first form matched a separate pass after each round of the ordinary rules, over ACI roots only. It was replaced by the filter syntax and the in-round Collect step. The pass survives only as the reference the engine’s differential tests compare against; on the 1,172 MLTL specifications Johannsen and Rozier publish with their FMCAD 2026 paper (Chapter 24) the two build the same e-graph.
• The member of smallest node id. Where a class had several matching members, the first implementation took the one of smallest id. That is sound, but the smallest id depends on insertion and merge order, so two runs building the same e-graph could rewrite differently.
• All matching members in one match. Sound for ACI, but it builds one term holding every window, and the cheaper single-choice terms never enter the e-graph.
• Keeping the pairwise rules as a backstop. Saturation with both would be complete by the ordinary semantics, and it grows the e-graph to 1,505,268 nodes at 4 rounds on one benchmark. The n-ary rules exist to avoid that.

One property is given up by design: a filter takes the maximal set of matching children, never a subset. Enumerating subsets is 2^k firings on a k-ary node, which is the growth sequence patterns exist to avoid.

Matching completeness over A, C, AC, and ACI

An e-graph stores one node per n-ary application, with its children flattened and normalized, and a pattern is matched against those stored children. Four mechanisms decide which matches exist.

Construction flattens. Building (Flat (Flat a b) (Flat c d)) stores one node Flat(a, b, c, d). Every path that builds or recanonizes an n-ary node, and every flattened view below, goes through one normalization function. It coalesces or deduplicates children, drops the identity, applies the nilpotent clamp, and cancels inverse pairs, so all of them agree.

(function Flat (E) E :assoc)
(function Spans (E E) E)
(rewrite (Flat ..prefix x y ..suffix) (Spans x y))

(let flat (Flat (Flat a b) (Flat c d)))
(run 1)
(check-eq flat (Flat a b c d))
(check-eq flat (Spans b c))

Nesting can still appear. A merge after construction can make a child class hold a node of the same operator, and the parent is not rebuilt as flat: with AC completion off, the nested and the flat spelling of one content can both exist. Completion, when on, proves the two spellings equal; it does not build the flat node, so a pattern still sees the stored children.

:flatten matches through nesting. A rule tagged :flatten matches each n-ary node against every view of it. A view opens a child class that holds a node of the same operator, and splices that node’s children in its place. A class is opened only when an item takes an element from inside it, so a view never repeats a match the stored children already give. One node’s enumeration stops at 2^20 views, 2^24 steps, or 2^24 elements. A node over a bound, or one whose view multiplicity exceeds the configured width, is skipped with a warning naming the rule, and the run continues. Under --use-semi-naive, an ordinary rule tagged :flatten is matched naively in every round; a sequence rule tagged :flatten stays semi-naive. On a rule whose query has no A, AC, or ACI operator, :flatten has no effect, and installing the rule prints the warning :flatten has no effect: the rule's pattern has no associative, AC, or ACI operator. A :comm operator does not count.

(sort IntervalSort)
(function Interval (i64 i64) IntervalSort)
(sort MLTL)
(function Var (String) MLTL)
(function And (MLTL) MLTL :assoc-comm-idem)
(function Global (IntervalSort MLTL) MLTL)

(let va (Var "a"))
(let vb (Var "b"))
(let vc (Var "c"))
(let g1 (Global (Interval 1 3) va))
(let g2 (Global (Interval 2 5) vb))
(let g3 (Global (Interval 3 6) vc))
; The node And{g1, cc} is built first. Merging cc with And{g2, g3} afterwards
; leaves it storing two children, one of them a conjunction.
(let cc (Var "cc"))
(let e (And g1 cc))
(union cc (And g2 g3))

; Factoring: all G of a conjunction share the outer window [K0, K1].
(rewrite (And (..gs (Global (Interval l u) p)) ..rest)
         (And (Global (Interval K0 K1)
                      (And ..{ (if (and (== l K0) (== u K1)) p (Global (Interval (- l K0) (- u K1)) p))
                               for (l u p) in (zip l u p) }))
              ..rest)
  :let ((K0 (min l)) (K1 (+ K0 (min (- u l)))))
  :when ((>= (count gs) 2) (> K1 0) (== (count (union-by p l u)) (count gs)))
  :flatten)
(run 1)
(check-eq e (Global (Interval 1 3) (And va (Global (Interval 1 2) vb) (Global (Interval 2 3) vc))))

Without the tag, the same rule reads the stored children {g1, cc}, which hold one Global, and the factoring does not fire:

(sort IntervalSort)
(function Interval (i64 i64) IntervalSort)
(sort MLTL)
(function Var (String) MLTL)
(function And (MLTL) MLTL :assoc-comm-idem)
(function Global (IntervalSort MLTL) MLTL)

(let va (Var "a"))
(let vb (Var "b"))
(let vc (Var "c"))
(let g1 (Global (Interval 1 3) va))
(let g2 (Global (Interval 2 5) vb))
(let g3 (Global (Interval 3 6) vc))
; The node And{g1, cc} is built first. Merging cc with And{g2, g3} afterwards
; leaves it storing two children, one of them a conjunction.
(let cc (Var "cc"))
(let e (And g1 cc))
(union cc (And g2 g3))

; Factoring: all G of a conjunction share the outer window [K0, K1].
(rewrite (And (..gs (Global (Interval l u) p)) ..rest)
         (And (Global (Interval K0 K1)
                      (And ..{ (if (and (== l K0) (== u K1)) p (Global (Interval (- l K0) (- u K1)) p))
                               for (l u p) in (zip l u p) }))
              ..rest)
  :let ((K0 (min l)) (K1 (+ K0 (min (- u l)))))
  :when ((>= (count gs) 2) (> K1 0) (== (count (union-by p l u)) (count gs)))
)
(run 1)
(check-eq e (Global (Interval 1 3) (And va (Global (Interval 1 2) vb) (Global (Interval 2 3) vc))))

Commutative pairs match in both orders. A :comm operator has exactly two children; a pattern over it matches both argument orders, and :flatten leaves it untouched. With neither child bound, (c x y) matches a stored c(a, a) twice, once per order.

What is not complete, by design: scalar variables range over existing classes, not over unmaterialized sub-sums such as Add(a,b) inside Add(a,b,c) (below); a sequence filter takes the maximal set, never a subset; and an untagged rule reads only the stored children.

Patterns that do not match

Patterns are matched as written. No stage normalizes a pattern by the declared laws, and none warns about one that construction would store in another form. Each pattern below loses matches:

• An identity child. (Plus x (Zero)) with :identity (Zero) matches no node, since construction, rebuild, and views drop the unit.
• An element past a nilpotent order. x:2 under :nilpotent 2 never binds, since counts are reduced modulo the order.
• An inverse pair. (Plus x (Neg x)) with :inverse Neg never matches, since pairs cancel at build and rebuild.
• A repeated element. (Or x x) under ACI never matches, since a stored set holds distinct classes. (Add x x) under AC never matches either; x:2 is the form that does.
• A nested same-operator application. (Plus (Plus a b) x) matches only where a child class holds a Plus{a, b} node. A flat stored Plus{a, b, c} gives no match, with or without :flatten, since views open classes, not sub-multisets.
• A single element. (Plus x) matches only a degenerate stored node, such as an And{K} that rebuild can leave in K’s class, and never under :flatten.

An application with no element, (Plus), is rejected when the rule is checked.

Two cases lose matches under :flatten itself. If inverse cancellation or the nilpotent clamp removes every element an opened class contributes, the view is dropped. For example, Add{a, d, e, f, K} with K equal to Add{(Neg a), (Neg d)} has the view {e, f}, which (Add x y) :flatten should match and does not. A degenerate node such as And{K} has only a single-class view, which is not matched, so a tagged rule misses the match an untagged one finds there.

Limits of variadic matching

Semper’s AC matcher implements maximum-partition matching, not unrestricted classical AC matching. Scalar elements bind distinct stored children and take their complete multiplicities. The rest variable takes all remaining stored children.

(sort E)
(function a () E)
(function b () E)
(function c () E)
(function Add (E) E :assoc-comm)
(function PairFound () E)
(function Repeated (E) E)

;; Two scalar elements require exactly two distinct multiset children.
(rewrite (Add x:1 y:1) (PairFound))

;; A multiplicity annotation handles one child repeated two or more times.
(rewrite (Add x:k>=2 ..rest) (Repeated x))

(let repeated (Add a a))
(let triple (Add a b c))
(run 1)

;; The binary-shaped pattern cannot split a:2 between x and y.
(check-neq repeated (PairFound))
(check-eq repeated (Repeated a))

;; Without a rest variable, two scalar elements cannot absorb a third child or
;; bind an implicit sub-sum such as Add(a,b).
(check-neq triple (PairFound))

The exact pattern (Add x:1 y:1) does not match Add{a:2}. The subject has one distinct child with multiplicity two, not two children for x and y. The variant (Add x:k>=2 ..rest) handles that representation.

A pattern also cannot split a:5, consume two copies, and leave three in rest. It must bind the complete count and reconstruct the desired number on the right-hand side, for example with (u64::- k 2).

Scalar variables range over existing e-classes. They do not range over implicit sums or arbitrary subsets of one flattened node. A pattern cannot bind x to an unmaterialized Add(a,b) inside Add(a,b,c). Another command must first construct that subterm, or the pattern must name its children separately.

An ordinary pattern under :assoc permits one prefix and one suffix rest, because its fixed elements describe a contiguous window; a sequence pattern permits any number of gaps. AC and ACI patterns are unordered and permit one remainder.

The pattern-matching design chapter defines the matching relations and their limits. The rule-application design chapter specifies right-hand-side evaluation and actions.