Introduction

What this is

Semper is a term rewriting and equality saturation engine. Programs can snapshot and restore its state with semi-persistent (push) and (pop), and can issue anti-unification queries over e-classes. Semper is a command-line program that reads a text file of S-expression commands in order. Every program in this book is one such file.

Semper lets a program tag operators with algebraic properties such as associativity, commutativity, idempotence, an identity element, or a declared nilpotence order. The engine enforces those properties through automatic term canonization instead of rewrite rules. For an associative and commutative operator, children are represented as a sorted multiset. One e-node therefore represents every reassociation and permutation of that multiset, compressing a whole family of AC-equivalent terms without enumerating its members.

The engine also answers more than equality questions. An anti-unification query returns a term that preserves shared structure and marks the remaining disagreements with Variants nodes.

The five parts

In Part I, we build the binary, write and run a program, declare operators with algebraic properties, and write rules over ordinary, sequence, multiset, and set operators.

In Part II, we explain what the e-graph stores, how saturation runs, how canonization implements declared algebraic properties, and how the three congruence modes differ.

In Part III, we explain what anti-unification computes, how exact search, graph search, and their hybrid work, and what an optimal result is optimal over.

In Part IV, we apply the engine to autoformalization. We sample a formalizer several times, cluster the samples by equality saturation, and anti-unify across clusters to explain the remaining differences.

In Part V, we extract terms under cost models: costs written as scripts, in Rust, as answer-set programs, or in MiniZinc, solved by an internal or an external solver. Chapter 24 opens the part.

What you need to know already

We assume that you are familiar with first-order terms and rewrite rules. We do not assume any experience with Semper or with e-graphs, equality saturation, AC canonization, or anti-unification; we introduce each of them from scratch.

The examples

Every program shown in this book lives in doc/book/examples/ and is included in its chapter directly from that file. The book_examples test executes every .egg file at the top level of that directory. The book_cost_model_examples test runs the Part V programs in examples/cost-models/ and compares each output with its .out file. It skips a program whose external solver is not installed.

Each example states the behavior the chapter relies on, either with check or checkau assertions or, for a program the book shows being rejected, with an EXPECT directive naming the failure. A change in engine behavior therefore fails a test instead of silently invalidating the book. Every number, size, ratio, and error message quoted in the book was captured by running the corresponding file.

What this book is not

This book is not the design documentation. It states what a user needs to run and understand the engine. The design chapters are the source of truth for storage, algorithms, and implementation invariants. When more detail is needed, this book links to the relevant design chapter instead of restating its specification.

This book is also not a paper. It proves no theorems. When an implementation claim rests on a prose argument rather than a machine-checked proof, the book states that boundary and links to the design chapter containing the argument.

Install and build

Build from source

git clone https://github.com/yaspar-org/semi-persistent.git
cd semi-persistent
cargo build --release

The workspace requires Rust 1.98.1, pinned in rust-toolchain.toml. rustup selects this compiler when Cargo runs in the checkout. A normal build does not require Verus; the proof annotations compile away under rustc.

The build also requires a C++ compiler: the extractor’s internal SAT solver is CaDiCaL, which Cargo compiles from source (crate cadical-sys). Xcode’s command-line tools provide one on macOS (xcode-select --install), and g++ or clang++ does on Linux (Debian and Ubuntu: apt install build-essential). The external solvers that cost models can use (RoundingSat, clingo, MiniZinc) are optional and found on the PATH at run time; Part V lists them.

Cargo writes the command-line program to target/release/semi-persistent. Run its help command to confirm the build:

./target/release/semi-persistent --help

Equality saturation engine

Usage: semi-persistent [OPTIONS] <FILE>

Re-running the Verus proofs

Verus is required only to re-check the proofs in abstract-domains, containers-verus, and au-verus. All three crates pin the same Verus release in their .verus-version files.

The following installs the pinned release on x86-64 Linux or Apple Silicon macOS. The release archive includes Verus, cargo-verus, and Z3.

version=$(cat containers-verus/.verus-version)

case "$(uname -s)-$(uname -m)" in
  Linux-x86_64) asset=x86-linux ;;
  Darwin-arm64) asset=arm64-macos ;;
  *) echo "Download the matching asset from the Verus release page"; exit 1 ;;
esac

tmp=$(mktemp -d)
curl -fL \
  "https://github.com/verus-lang/verus/releases/download/release%2F${version}/verus-${version}-${asset}.zip" \
  -o "$tmp/verus.zip"
unzip -q "$tmp/verus.zip" -d "$tmp"

verus_home="$HOME/.local/verus-$version"
mkdir -p "$HOME/.local"
mv "$tmp"/verus-* "$verus_home"
export PATH="$verus_home:$PATH"

On macOS, allow the downloaded binaries through Gatekeeper:

bash "$verus_home/macos_allow_gatekeeper.sh"

Add the PATH export to your shell startup file to retain it in later shells. Confirm the installation with verus --version, then run the proof suites:

(cd abstract-domains && cargo verus verify)
(cd containers-verus && cargo verus verify)
(cd containers-verus && cargo verus verify --features literal-types)
(cd au-verus && cargo verus verify)

The crates in the workspace

Running Semper does not require working with these crates individually. Cargo prints their package names during builds, and the corresponding Rust crate names appear in stack traces. This table maps those names to their source paths.

Run the test suite

From the workspace root, run:

cargo test --workspace

At the time of writing, Cargo discovers 1,782 tests. The default run executes 1,731 and reports 51 as ignored. On the machine used to prepare this chapter, the command completed in 6 minutes 2 seconds.

The interpreter’s file-based integration fixtures live under egraph/tests/egg/. The harness in egraph/tests/egg_tests.rs sends each registered .egg program through the parser, sort checker, and interpreter. Unless overridden by a fixture directive, it runs the program with both naive and semi-naive evaluation, each under the static and the runtime atom-scheduling modes.

The same harness defines book_examples. It scans the top level of doc/book/examples/ for every file with the .egg extension and sends each one through the same checker. Chapters include those files directly, so every book example is a test. Adding an example to that directory does not require separate Rust test registration.

The ignored count includes manual diagnostics and measurements rather than one unfinished suite. Six entries are child-process cases for hasher configuration; their non-ignored driver tests already execute them in fresh processes. The slow ignored groups are:

• the completion_* diagnostics and the ac_vs_rules comparison;
• the bench_acgen_* fixtures in egg_tests;
• the AU measurement and stress tests in the au_* test binaries; and
• the feature-gated, 100-million-element compat_vec_stress tests.

List ignored tests without running them:

cargo test --workspace -- --ignored --list

Run slow tests by naming their harness rather than running every ignored test together. For example:

cargo test -p semi-persistent-egraph --release --test egg_tests \
  bench_acgen -- --ignored --nocapture

cargo test -p semi-persistent-egraph --release --test ac_vs_rules \
  -- --ignored --nocapture

cargo test -p semi-persistent-egraph --release --test au_hardness \
  hardness_map -- --ignored --nocapture

cargo test -p semi-persistent-containers-verus --features compat-all \
  --test compat_vec_stress -- --ignored --test-threads 1 --nocapture

The repository’s reproduction guide gives the commands and expected durations for the individual AU measurements.

Running a program

Invocation

The command line takes one positional argument: the path to an .egg program. We write any options after that path:

./target/release/semi-persistent PROGRAM.egg [OPTIONS]

Here is the program used in Chapter 3:

;; EXPECT: ok
;; TYPES: bignum
;; Book chapter 3: sorts, operators, ground terms, and what congruence gives you
;; for free. Nothing here declares a rule, so every equality below is either one
;; the program asserted or one congruence closure derived from those.

;; ANCHOR: literal-model-declarations
(sort Expr)
(sort Name)

;; IBig is supplied by the selected bignum literal model.
(function f (Name) Expr)
(function Lit (IBig) Expr)
;; ANCHOR_END: literal-model-declarations

;; An operator declares its argument sorts, then its result sort. Arity is fixed
;; by that list unless an algebraic attribute makes the operator variadic
;; (chapter 4).
;; ANCHOR: operator-declarations
(function add (Expr Expr) Expr)
(function neg (Expr) Expr)

;; Nullary operators are the leaves. They take an empty argument list.
(constructor x () Name)
(constructor y () Name)
(constructor z () Name)
;; ANCHOR_END: operator-declarations

;; `let` builds the term, inserts it, and binds the name to its e-class. The name
;; is then usable wherever a term is expected.
(let fx (f (x)))
(let fy (f (y)))
(let sum (add fx fy))

;; A bare term at top level is inserted without being named. This is how you
;; populate the e-graph with terms a rule should fire on.
(neg (add (f (z)) (f (z))))

;; Structural identity is free: the same term built twice is the same e-class,
;; because every term is hash-consed on insertion.
(let sum_again (add (f (x)) (f (y))))
(check-eq sum sum_again)

;; `union` asserts an equality the program did not derive.
(union fx fy)

;; Congruence closure is the one inference that runs without any rule: equal
;; arguments make equal applications. Nothing declared `add` to be commutative or
;; anything else, yet `add(fx, fy) = add(fy, fx)` now holds, because `fx` and
;; `fy` are the same class and so both terms are the same node.
(check-eq (add fx fy) (add fy fx))
;; It propagates upward through any number of layers.
(check-eq (neg (add fx fx)) (neg (add fy fy)))

;; What congruence does NOT give you: it never equates terms with different
;; operators or different arity at the root.
(check-neq (add fx fx) (neg fx))

;; `check-eq` and `check-neq` build their terms before comparing them, so a term
;; the program never derived does not make them fail: they add it. A presence test
;; is `check`, egglog's check, which builds nothing and succeeds only if the graph
;; already holds a match. `(add fx fx)` was built above, so this check passes;
;; `(check (add fx fy))` would fail, because no command built that term.
(check (add fx fx))

Run it from the repository root:

./target/release/semi-persistent doc/book/examples/03-terms.egg

ok — 11 nodes

All its checks pass, and the engine finishes with 11 e-nodes.

What a program file is

A Semper program is a text file containing S-expression commands. The .egg extension is a convention rather than a requirement. A semicolon starts a comment that continues to the end of the line.

Semper parses the complete file, sort-checks its commands in source order, and then executes the checked commands in that same order. Declarations are not hoisted: a sort must precede operators that use it, and an operator must precede terms or rules that use it. A declaration later in the file cannot satisfy an earlier reference.

The example above follows this order: it declares its sorts, declares its operators, builds and names terms, and finally checks equalities.

Output streams

Commands that return data, including extract, antiunify, print-size, and print-stats, write their results to standard output. Successful checks print nothing. After the program finishes, Semper writes its closing status to standard error:

ok — N nodes

The example above therefore has no standard output; its only visible line is the closing status. Warnings also go to standard error, one line each, prefixed with warning:.

Redirecting standard output gives a script only the query results while leaving the status visible on the terminal:

./target/release/semi-persistent PROGRAM.egg > answers.txt

To capture both streams separately:

./target/release/semi-persistent PROGRAM.egg \
  > answers.txt 2> status.txt

Exit status

Semper exits with status 0 only after the complete program runs successfully. Syntax, sort-checking, failed-check, and other run-time errors exit with status

1. A command-line error exits with status 2.

A failed check stops the program immediately. Its nonzero status lets an example file act as a regression test: a script or test runner fails when the behavior asserted by the file no longer holds. Query output may have been written before a later check failed, so callers should use the exit status rather than the presence of output to decide whether the run succeeded.

Running the book’s examples

Every program displayed in this book lives under doc/book/examples/. The chapters include those files directly, so the displayed source and the tested source are identical.

Run one example from the repository root:

./target/release/semi-persistent doc/book/examples/03-terms.egg

Run all book examples through their test harness:

cargo test -p semi-persistent-egraph --test egg_tests book_examples

The book_examples test scans every .egg file at the top level of the directory. The first eight lines of a file, the two header lines and six more, may contain directives such as ;; EXPECT: ok or ;; TYPES: machine. These lines are comments to the engine binary; the test harness reads them to select settings and the expected outcome.

Annex C lists every directive and its corresponding command-line option. When running an example manually, pass the matching option for any nondefault directive. An EXPECT directive can also state that a parse, sort, check, or run-time failure is the expected test result.

Sorts and terms

Literal models

Before declarations are sort-checked, --types selects the concrete sorts and primitive operations available to the program. The default is bignum.

Programs use these sort names directly in declarations. The running example uses the default model:

(sort Expr)
(sort Name)

;; IBig is supplied by the selected bignum literal model.
(function f (Name) Expr)
(function Lit (IBig) Expr)

Expr and Name are introduced by the program, while IBig is supplied by the selected literal model. Running the same declaration with only --types machine rejects IBig as an unknown sort.

Annex C gives the full --types flag reference.

The grammar

The declaration and ground-term fragment of a Semper program has this grammar. Braces mean zero or more repetitions, brackets mark an optional item, and | separates alternatives.

program       = { command }

command       = declaration
              | insertion
              | "(" "let" name term ")"
              | "(" "union" term term ")"

declaration   = "(" "sort" name ")"
              | "(" decl-kind name "(" { name } ")" name
                    { decl-option } ")"
              | "(" "datatype" name { variant } ")"

decl-kind     = "function" | "constructor"
variant       = "(" name { name } { decl-option } ")"

term          = literal | name | application
application   = "(" operator { term-child } ")"
term-child    = term [ ":" unsigned-integer ]
insertion     = "(" name { term } ")"

decl-option   = ":cost" unsigned-integer
              | ":unextractable"
              | ":assoc" | ":comm" | ":assoc-comm"
              | ":assoc-comm-idem"
              | ":assoc-left" | ":assoc-right"
              | ":idempotent"
              | ":nilpotent" [ unsigned-integer ]
              | ":identity" term
              | ":cancellative"
              | ":inverse" name

An operator may be an ordinary name or a qualified builtin such as IBig::+. Whitespace and ; comments may appear between tokens. A nullary application can be written explicitly with parentheses, as in (x). Ground terms contain no pattern variables; a bare name must resolve to a literal, a nullary operator, or a name introduced by an earlier let. A term-child count follows its term with no space before the colon.

Chapter 4 defines the algebraic declaration options listed above. Annex A collects the complete surface grammar, including patterns, rule actions, query and control commands, and every command option.

Sorts

(sort S) registers an uninterpreted sort named S. It introduces only the sort; it does not create any constants or other terms. The running example declares Expr and Name as separate sorts. Semper has no subtyping or implicit coercions between them.

An operator declaration fixes the sort of every term it builds. In the example, (constructor x () Name) makes (x) a Name, while (function f (Name) Expr) accepts a Name and returns an Expr. Therefore (f (x)) has sort Expr. Each child must have exactly the argument sort declared for its position, and the outermost operator determines the term’s result sort.

(datatype T (C S1 ... Sn) ...) combines a sort declaration with constructor declarations. It first registers T, then treats each variant as (constructor C (S1 ... Sn) T). Registering T first permits recursive variants that use T as an argument. Every other argument sort must already exist.

Operators

An operator declaration lists its argument sorts before its result sort:

(function add (Expr Expr) Expr)
(function neg (Expr) Expr)

;; Nullary operators are the leaves. They take an empty argument list.
(constructor x () Name)
(constructor y () Name)
(constructor z () Name)

add is binary, neg is unary, and the empty argument lists make x, y, and z nullary operators. For an ordinary operator, the number of declared argument sorts fixes its arity.

function and constructor have the same sortchecking, congruence, matching, and canonization behavior. constructor additionally marks the operator as a term former. Every variant of a datatype receives the same marker. The current extractor does not otherwise prefer constructors over functions.

Two declaration tags control extraction. :cost n assigns each node of the operator a cost of n, with a default of 1. :unextractable excludes those nodes from extraction while leaving them in the e-graph and available for matching. Both tags are accepted on functions and constructors. They affect which representative extract selects, not which terms are equal. Chapter 8 defines the extraction cost model.

The remaining declaration tags assign algebraic properties. Semper enforces them through automatic term canonization rather than rewrite rules. Chapter 4 defines those properties and their legal combinations.

Building a term

A ground term enters the e-graph through one of three top-level forms. A bare application inserts it without naming it. (let name term) inserts the term and binds name to its e-class. (union left right) inserts both terms and merges their e-classes.

(sort Expr)
(constructor x () Expr)
(function f (Expr) Expr)
(function g (Expr) Expr)
(function h (Expr) Expr)

;; A bare application inserts a term without naming its e-class.
(f (x))
(print-size)

;; `let` inserts a term and binds a name to its e-class.
(let named (g (f (x))))
(print-size)

;; `union` inserts both terms and merges their e-classes.
(union named (h (f (x))))
(print-size)

(check-eq named (h (f (x))))

The three print-size commands report:

x: 1
f: 1
total: 2
x: 1
f: 1
g: 1
total: 3
x: 1
f: 1
g: 1
h: 1
total: 4

The bare (f (x)) inserts two e-nodes. The let reuses both and inserts only (g (f (x))), raising the total to three. The union likewise reuses (f (x)), inserts (h (f (x))), and raises the total to four. print-size counts e-nodes, so merging the last two nodes into one e-class does not reduce the total.

A child of an AC application may carry a count: (Add a:3 b) is (Add a a a b), stored as one entry a:3, never expanded. A child of an associative (:assoc) application may carry one too, and it is then repeated that many times, since a sequence is positional. The count must be at least 1. An ACI operator stores a set, which holds each element once, so a count under it is rejected, as it is under any other kind of operator. A count is accepted wherever a term is: in a top-level insertion such as (Add a:3 b), and inside let, check, and nested applications.

named is an e-class binding, not an alias for the syntax (g (f (x))). After the union, the same binding denotes the class containing both (g (f (x))) and (h (f (x))). Later commands may use named wherever a ground term is accepted.

Sortchecking

Semper sort-checks the complete program before executing any command. Declarations are processed in source order. An operator declaration is rejected if an argument or result sort is unknown. Registration also validates the supported shapes and combinations of algebraic tags, including identity sorts and inverse signatures. Chapter 4 gives those requirements.

Before a ground term is built, Semper resolves its operator and checks its arity. It then checks the children from the leaves upward, requiring each child to have exactly the sort declared for its position. Names must resolve to an earlier let binding, a literal, or a nullary operator.

(sort E)
(sort N)
(function f (N) E)
(constructor x () N)

(f (f (x)))

(x) has sort N, so the inner (f (x)) has sort E. The outer application of f requires an N, not an E. The program is rejected before execution:

sort error at line 12 column 4: argument 1 of 'f': expected sort 'N', got 'E'

These checks establish that declarations have supported forms and terms are well-sorted. Algebraic tags remain assertions about the intended interpretation. Sortchecking can validate that a tag combination is supported, but it does not prove that the intended operator satisfies the declared laws. Once accepted, Semper enforces those laws through canonization. Chapter 23 collects this and the other obligations left to the program author.

Literals

Literal tokens are typed during sortchecking. When a token appears as an operator argument, the declaration supplies its expected sort and the selected literal model tries to parse the token at that sort. The example selects both literal models so it can use machine and arbitrary-precision sorts together.

(sort Expr)
(constructor Lit (bool) Expr)
(constructor Big (IBig) Expr)
(constructor Machine (i64) Expr)
(constructor Real (f64) Expr)
(constructor Text (String) Expr)

(let truth (Lit true))
(let big (Big 42))
(let machine (Machine 42))
(let real (Real 3.5))
(let text (Text "Semper"))

(check-eq truth (Lit true))
(check-eq big (Big 42))
(check-eq machine (Machine 42))
(check-eq real (Real 3.5))
(check-eq text (Text "Semper"))
(check-neq big machine)

The two occurrences of 42 have the same spelling, but Big requires an IBig while Machine requires an i64. Similarly, true is parsed as bool, 3.5 as f64, and the quoted token "Semper" as String.

Concrete literal sorts are separate from user-declared sorts. There is no implicit coercion from bool to Expr; (Lit true) explicitly constructs an Expr containing the Boolean value. An algebraic operator returning Expr can therefore use (Lit true) as its identity term, while bare true would have the wrong sort.

During term construction, Semper interns the concrete value in an internal literal node beneath the user-declared constructor. These internal operators do not appear in surface syntax. The literal-model design chapter specifies their representation and the primitive-operation interface.

Declaring algebraic operators

Chapter 3 established which declarations Semper accepts. This chapter defines the semantic contract those declarations create. Chapter 10 later explains how the corresponding canonical representations are implemented.

Semper lets you tag operators with algebraic properties. Once declared, these properties are enforced through automatic term canonization rather than rewrite rules. The most familiar example is associativity and commutativity:

(sort Math)
(function a () Math)
(function b () Math)
(function c () Math)
(function Add (Math) Math :assoc-comm)

(let nested (Add a (Add b c)))
(check-eq nested (Add c a b))

Applications of Add are flattened and stored as sorted multisets. Reassociation and permutation therefore disappear from the representation: a whole family of AC-equivalent terms is compressed into a single e-node rather than stored as separate nodes connected by rewrite rules.

Operators declared with :assoc, :assoc-left, :assoc-right, or an AC alias are variadic. Their declaration contains one argument sort, and an application may contain one or more children. An application with no children is also valid when the operator declares an identity.

The attributes

Compatible attributes may be combined and written in any order. :assoc-comm is an alias for :assoc :comm, while :assoc-comm-idem expands to :assoc :comm :idempotent.

:nilpotent must be accompanied by :identity. The identity is a ground term of the result sort, built from declarations available at that point. Reducing child multiplicities modulo the nilpotence order can empty the multiset. When that happens, Semper canonizes the result directly to the identity’s e-class. The same rule applies to an explicitly empty application such as (Xor); there is no separate empty Xor node connected to the identity by a rewrite.

(sort E)
(function Zero () E)
(function A () E)
(function Xor (E) E :assoc :comm :nilpotent 2 :identity (Zero))

(check-eq (Xor) (Zero))
(check-eq (Xor (A) (A)) (Zero))

Semper rejects both a :nilpotent declaration without an identity and an empty variadic application whose operator has no identity. A nullary operator declared with an empty argument list remains an ordinary constant; this restriction applies only to empty applications of variadic operators.

:assoc-left and :assoc-right specify fold direction rather than full associativity. For a left fold,

f(f(a,b),c) = f(a,b,c)

but f(a,f(b,c)) retains its grouped right child. A right fold is the mirror image. Bare :assoc flattens both nestings, so all three terms have the same canonical representation.

The three sequence tags are mutually exclusive. A directional fold also cannot be combined with :comm; an AC declaration uses :assoc :comm.

These effects are applied when ground terms are inserted and when rewrite rules construct their right-hand sides. They require neither rewrite rules nor AC completion. Not every other combination is legal; the legality table later in this chapter lists the supported combinations.

Inverse-pair cancellation and cancellativity

Semper supports two additional algebraic attributes with deliberately narrow contracts. They provide inverse-pair cancellation and cancellative inference, not general group reasoning.

The inverse attribute names a previously declared unary operator:

(sort E)
(function Zero () E)
(function A () E)
(function Neg (E) E)
(function Add (E) E
  :assoc-comm
  :identity (Zero)
  :inverse Neg)

(check-eq (Add A A (Neg A)) A)

Neg must have signature E -> E, and Add must declare an identity. This declaration asserts that Add(x, Neg(x)) = Zero. Semper cancels such explicit pairs while constructing terms, even in plain mode. For example, Add(a, a, Neg(a)) canonizes to a.

In plain mode, :cancellative performs no inference because AC completion does not run. It participates both in eager completion ((set-option :completion eager)) and in checks with check completion ((set-option :check-completion on)). Given an asserted equality Add(a,c) = Add(b,c), completion may therefore derive a = b.

These transformations are sound relative to the laws declared by the user: each removed inverse pair equals the declared identity, and common summands are removed only from equations for an operator declared cancellative. This soundness argument is backed by focused tests but is not yet machine-checked end to end.

The boundary is completeness. Semper recognizes an inverse pair only when the corresponding Neg(x) node exists, and pairs exposed only by later merges may require AC completion. The tags alone do not derive general Abelian-group laws such as Neg(Neg(x)) = x, distribute Neg over Add, or normalize sums to signed coefficients. In particular, :inverse means a group inverse, not a Boolean complement: Not(x) is not an inverse for And, because And(x, Not(x)) is False while And’s identity is True.

Arity: one child, and none

A variadic application denotes a fold of its binary operator. Folding one child returns that child; folding no children returns the identity, when one has been declared. Semper performs these reductions during term construction rather than storing nodes that later need rewriting.

For an AC or ACI operator without an identity, the last case reports that the empty monomial has no meaning without an identity. An associative-only operator cannot declare an identity, so its empty application requires at least one argument.

Associative operators must therefore be closed over one sort. Their argument and result sorts must coincide, both because nested applications feed results back as arguments and because singleton collapse returns the child’s e-class directly. Semper enforces this invariant. For example,

(sort A)
(sort B)
(function Bad (A) B :assoc-comm)

Which combinations are legal

Semper validates algebraic attributes when an operator is declared.

A commutative-only operator’s return sort may differ from its shared argument sort. For example, (function Same (E E) R :comm) is legal.

One important implementation restriction follows from the table: an identity requires a full AC operator. Semper cannot currently attach an identity to an associative-but-noncommutative operator.

Canonization carries the declared laws, rewrite rules carry the rest

An algebraic declaration places its listed laws in term canonization. An AC operator therefore needs no rules for reassociation or permutation, and an ACI operator needs no additional rule for duplicate removal. Identity, nilpotence, and represented inverse pairs are handled by the same construction path when their attributes are present.

Every other equation in the modeled domain remains an explicit rule. For a Boolean language, distributivity, De Morgan’s laws, absorption, and double negation are not declaration attributes. A program that needs those equations must install the corresponding rewrite or birewrite forms. Omitting a domain rule leaves its equality underived even when all operators have accurate AC or ACI declarations.

This separation lets a program choose its equational theory. The declared laws always determine how terms are represented. The installed rules determine which additional domain equalities saturation can derive. Part IV uses this distinction when adding a domain rewrite changes a reported difference between two autoformalizations.

The algebraic-properties design chapter specifies the canonical representations and completion interactions in detail.

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.

E-nodes, e-classes, congruence

This chapter defines e-nodes and e-classes, measures structural sharing, and explains union-find, congruence closure, rebuild, and equality checks.

E-nodes and e-classes

An e-node is an operator together with references to its argument e-classes. An e-class is a set of e-nodes that Semper currently knows to be equal.

(sort E)
(function a () E)
(function b () E)
(function f (E E) E)

(let left (f (a) (b)))
(print-size)

The print-size command reports:

a: 1
b: 1
f: 1
total: 3

The term contributes three e-nodes: a(), b(), and f(Ca, Cb), where Ca and Cb are the classes containing the two leaves. All three nodes are new in this example and initially belong to separate e-classes.

The parent stores class arguments, not pointers to fixed syntax-tree children. Once a child class acquires additional members, the same parent e-node represents applications using any equal member of that child class. After insertion, left names an e-class rather than one retained syntax tree.

The node arena and the e-class relation are separate structures. Adding a new e-node creates a singleton e-class. Later equalities can merge classes without deleting their member nodes. This is why print-size counts nodes rather than equivalence classes.

Hash-consing

At insertion time, hash-consing maps an operator and canonical argument tuple to an existing e-node’s class. Inserting the same key again therefore reuses that class instead of allocating another node.

;; Repeating the same term reuses all three existing e-nodes.
(f (a) (b))
(print-size)

The second print-size has the same output as the first:

a: 1
b: 1
f: 1
total: 3

Reinserting (f (a) (b)) reuses both leaves and their parent, so the measured node total remains three. The identity test uses e-class representatives for the children. If those representatives change after a merge, rebuild updates the affected parent keys.

Union-find

Semper maintains e-class membership with union-find. Every e-node has a class identifier. find follows parent links to the class’s canonical representative. In the same pass it applies path halving: each visited node is pointed at its grandparent, which shortens later lookups. A union between two representatives makes one the survivor and the other a child of it.

The survivor is an implementation choice, not a preferred term. A merge does not rewrite or delete either side, and choosing a different survivor does not change the asserted equality. The --union-by flag changes the survivor heuristic and can change operational work and printed representatives, but it does not change which input equality was asserted. Annex C lists the available policies.

Path-halving writes and union updates are both undone by a pop. Chapter 7 describes that semi-persistent storage.

Congruence

Congruence adds the rule that applications of the same operator to equal arguments are equal. The example first creates a second parent and confirms that it is distinct from left. It then merges only the leaf classes:

;; This parent is distinct until its two argument classes are merged.
(let right (f (b) (b)))
(check-neq left right)

;; No rewrite runs. Congruence alone merges the parent classes.
(union (a) (b))
(check-eq left right)
(print-size)

After (union (a) (b)), both parent nodes have the canonical key f(Cab, Cab). Rebuild detects that collision and merges the parent classes, so (check-eq left right) passes without a rewrite rule.

The final print-size reports:

a: 1
b: 1
f: 2
total: 4

The graph still stores four e-nodes. The two leaves now occupy one e-class, and the two parents occupy another. Congruence changes class membership, not the node count. Hash-consing prevents duplicate allocation for a key when it is inserted; rebuild can later make historical nodes collide, in which case it merges their classes and retains both arena entries.

A rewrite that merges two classes therefore also affects every application whose child points into those classes. Rules match and extend these shared classes instead of enumerating a separate rewritten tree for every equivalent term.

Rebuild

A class merge immediately updates union-find, but parent e-nodes can still contain the absorbed representative in their stored keys. Rebuild restores a congruence-closed state. It visits parents from the absorbed class’s use-list, replaces child identifiers with current representatives, canonizes the children, and probes the hash-consing cache again. A collision schedules another class merge, so the process continues until no pending merges remain. Rebuild then runs a repair round that cancels inverse pairs formed by later merges, and it alternates the two passes until neither changes the graph.

The union and equality-check commands rebuild before returning their result. Saturation also rebuilds before constructing each round’s matching indexes. Rules therefore match against a congruence-closed graph rather than an intermediate state with stale parent keys. print-size itself only reads the node arenas; it does not trigger rebuild.

Chapter 10 describes the operator-specific canonization performed during term construction and parent recanonization. The e-graph design chapter specifies the rebuild worklist and use-list algorithm.

What an equality check asks

(check-eq t1 t2) builds both ground terms, rebuilds the e-graph, and asks whether their e-nodes have the same union-find representative. It does not compare two extracted syntax trees.

A passing check means the asserted unions, fired rules, declared algebraic canonization, and active congruence procedure derived the equality. A failing check means the terms remain in different classes in the graph as currently computed. It is not a proof that the terms are unequal in every model of the declared laws.

Likewise, (check-neq t1 t2) accepts when the two current representatives are different. Chapter 11 explains how plain, eager, and lazy congruence modes change the work performed before that decision.

(check fact ...) asks a different question, egglog’s: does the e-graph already contain a match for these facts? A check builds nothing. (check (= t1 t2)) succeeds only if both terms exist and share a class, so it fails on a term that no command built, where check-eq would build it and possibly join it by congruence. Names that are not globals are variables of the one check: (check (= e (f x))) asks whether some class contains an f node, and (check (= e (f x)) (= x (a))) whether one has the class of (a) as its child. (!= p q) requires different classes, and :count k, :min k and :none count the matches. Equivalence is decided with check-eq; check tests what the graph holds.

The storage structures are specified in the design chapters for nodes, e-classes, and hash-consing.

Semi-persistence: push and pop

This chapter defines push and pop, explains their sparse restoration mechanism and capacity behavior, and shows nesting, scoped names, and speculative use.

Opening and discarding a scope

(push) rebuilds the e-graph and records the resulting logical state. (pop) restores the most recent recorded state and closes its scope in one step, discarding insertions, unions, and rule effects performed inside the scope.

(sort E)
(function a () E)
(function b () E)
(function f (E) E)
(function g (E) E)

(let left (f (a)))
(let right (f (b)))
(print-size)

(push)
(union (a) (b))
(check-eq left right)

(push)
(let nested (g left))
(print-size)
(pop)

;; The inner pop keeps the equality from the outer scope.
(check-eq left right)
(pop)

(check-neq left right)
(print-size)

Before the first push, a, b, f(a), and f(b) account for four e-nodes. The union inside the outer scope makes left and right equal. The nested scope then adds one g node, so its print-size reports five nodes:

a: 1
b: 1
f: 2
g: 1
total: 5

Popping the nested scope removes the g node but preserves the outer scope’s union. Popping the outer scope removes that union. The final disequality check passes, and the last print-size reports the original four nodes:

a: 1
b: 1
f: 2
total: 4

Rules installed inside a scope and let bindings created there are also discarded. Output is not reversible: text printed before a pop remains in the process output.

Why the pop is cheap

Semper uses semi-persistent containers instead of copying the complete e-graph at every push. Append-only arenas record their logical lengths and truncate new suffixes on restore. Mutable arrays, including union-find parent arrays, capture a slot’s previous value the first time that slot changes in a scope. Restore replays those sparse differences and restores the saved lengths.

Hash-consing tables and other derived indexes are not themselves the logical state. Each node cache keeps a hint index from content fingerprints to node ids, and a restore does no work on it. A lookup compares every hint against the restored node arena, so hints for discarded content are skipped. The literal interning table is a verified semi-persistent map that unwinds the discarded suffix of its index, and rebuilds the index instead when that is cheaper. Saturation’s matching indexes have round-local lifetimes and are built again when needed.

Push therefore records one stamp in a single history rather than cloning all nodes and classes. The history drives nine synchronized members, which carry no tokens of their own. Push marks the members sequentially. A pop runs the seven large members in parallel once the graph holds at least 2^14 live nodes. Push work includes the rebuild and frame bookkeeping. Pop work depends on the changes made since the mark and on the discarded suffixes. The project name refers to this semi-persistent representation.

The command-line mode is --push-pop diff, and it is the default.

push :shrink

Plain (push) preserves allocation capacity even though a later (pop) restores the logical lengths. Reusing that capacity avoids reallocating when the next branch grows to a similar size. print-size reports logical e-nodes, so it cannot show retained capacity.

(push :shrink) conditionally reclaims excess container capacity at the mark. The current interpreter passes a factor of 4 and a headroom of 2. A container shrinks when its capacity exceeds four times its logical length. The append-only arenas add the headroom to that threshold, and some stores ignore the request. Shrinking can move live storage and add work to push; pop does not perform another shrink. The option does not promise that every allocation is returned.

(push :shrink)
(check-neq left right)
(pop)

Nesting and lifetime

Scopes nest in last-in, first-out order. In the main example, the first pop discards only nested; the equality created in the outer scope remains until the second pop.

A pop with no matching push is a runtime error:

(pop)

The interpreter reports pop without matching push.

let introduces a runtime global name. A binding created inside a pushed scope is unavailable after its matching pop:

(sort E)
(function a () E)
(push)
(let scoped (a))
(pop)
(check-eq scoped (a))

This program is rejected during whole-program sortchecking because scoped is no longer in the global-name environment at the final check. If an inner let shadows an outer name, popping restores the outer binding:

(let chosen (a))
(push)
(let chosen (b))
(check-eq chosen (b))
(pop)
(check-eq chosen (a))

Sort and operator declarations are different. Semper sortchecks the complete program before interpretation and registers declarations in source order, so push and pop do not give declarations a runtime lifetime. Installed rules, runtime let bindings, e-nodes, and equalities are scoped.

Speculative assertion

Scopes support repeated speculative checks over one shared background graph. A program can saturate its background facts, push, assert one candidate formalization, inspect the equalities it implies, and pop before trying the next candidate. Chapter 19 applies this sequence to alternative explanations of differences between autoformalization clusters.

The exact restore order and the cache protocol are specified in the design chapters for the e-graph and interpreter.

Equality saturation

Equality saturation repeatedly matches and applies rules, rebuilds the e-graph, and stops at an operational fixpoint, a goal, or an iteration bound. This chapter defines that round order, the forms of run, extraction, and run statistics.

A round

Before a run with an :until goal starts, Semper builds the two ground goal terms. Each iteration then performs these operations in order:

1. Rebuild the e-graph, then test the goal against the current union-find. A multiplicity past the configured width stops the run with an error here.
2. Build an immutable full index and its scheduling statistics.
3. Process the selected ordinary rules in declaration order. For each rule, schedule and collect its matches against the index, then apply its actions. The selected sequence rules then run as one batch on the same index.
4. Recycle the index and test whether the action counter is zero.

The index represents the graph immediately after step 1. Nodes and canonical forms produced by rule actions are therefore available to matching in the next iteration, after another rebuild and index construction. A rule’s matches are collected before any of that rule’s actions run.

The first example needs several rounds because each recursive rewrite creates the next dbl application that can match.

(sort N) (function z () N) (function s (N) N) (function dbl (N) N)

(rewrite (dbl (z)) (z)) (rewrite (dbl (s x)) (s (s (dbl x))))

(let two (s (s z))) (let four (s (s (s (s z))))) (let d2 (dbl two))

;; The first iteration exposes another recursive dbl application. (run 1) (check-neq d2 four)

;; Two more iterations finish this input. (run 2) (check-eq d2 four)

;; This run reaches an action-counter fixpoint before its bound. (let d4 (dbl four)) (let eight (s (s (s (s (s (s (s (s z))))))))) (run 10) (check-eq d4 eight) (print-stats)

The first one-round run cannot finish d2. Two more rounds derive d2 = four. The final run requests ten iterations but reaches its operational fixpoint after three.

The complete rule-application procedure is specified in design §7.7.

Saturation

A run reports saturation when an iteration’s action counter is zero. A union counts only when it merges two previously distinct classes. An insert counts whenever its action is applied, even when hash-consing finds an existing node, and a subsume action also counts whenever it is applied. A repeatedly matching insert or subsume rule can therefore keep saturated false without increasing the graph.

This is an operational fixpoint of the selected declared rules and the current driver. It is not a completeness result for an unstated theory. A law that was neither declared as an algebraic property nor encoded by a rule is absent. Likewise, a successful (check-neq a b) says only that a and b currently belong to different classes.

If the iteration bound is reached first, the run stops with saturated: false. The e-graph retains everything derived so far, and subsequent checks inspect that partial result.

The forms of run

The four common forms select a budget, an optional ruleset, and an optional goal:

A named run may also carry either :until goal. Each run selects exactly one ruleset. It does not combine the named ruleset with untagged rules.

(sort E) (constructor a () E) (constructor b () E) (constructor c () E) (constructor f (E) E)

(ruleset selected) (rewrite (f x) (a)) (rewrite (f x) (b) :ruleset selected)

(let term (f (c)))

;; A named run selects only rules tagged with that ruleset. (run selected 2) (check-eq term (b)) (check-neq term (a))

;; A bare run selects only untagged rules. (run 2) (check-eq term (a))

;; Distinct classes satisfy an inequality goal before the first iteration. (run 10 :goal (!= (a) (c))) (check-neq (a) (c))

;; Equal classes cannot become distinct during saturation. (run 1 :goal (!= term (a))) (check-eq term (a))

The goal is tested after rebuild and before matching in the first and every later iteration. It is rebuilt and tested once more after the final permitted round. A goal that already holds still costs zero iterations. An equality goal can become true as classes merge. An inequality goal either succeeds initially or cannot become true during that run: saturation merges classes and never splits them. :goal (!= ...) records no permanent disequality constraint.

Runs that do not saturate

Some rules generate a fresh term at every iteration. The up rewrite below can keep extending its argument, so increasing the iteration bound keeps exposing more work. An equality goal stops this run as soon as the requested depth has joined the starting term.

(function up (N) N) (rewrite (up x) (up (s x)))

;; The rewrite can keep producing larger terms. The equality goal stops this ;; run before the iteration bound. (run 100 :goal (= (up z) (up (s (s (s z)))))) (check-eq (up z) (up (s (s (s z))))) (print-stats)

The practical control is always a finite iteration bound, optionally combined with an equality goal, followed by checks for the facts the program requires. A run that repeatedly reaches its budget should be treated as a property of the rule set, not as evidence that Semper will eventually choose to stop.

Extraction

(extract t) rebuilds the graph and prints a lowest-cost ground term from t’s e-class. It uses the per-operator costs and exclusions introduced in Chapter 3. Costs are additive over the root and children, including each occurrence represented by a multiplicity.

(sort E) (constructor unit () E) (constructor wrap (E) E) (constructor expensive () E :cost 5) (constructor hidden () E :unextractable)

(union (expensive) (wrap (unit))) (union (expensive) (hidden))

;; Prints (wrap (unit)), whose cost is 2. (extract (expensive)) (check-eq (expensive) (wrap (unit)))

The class in this example contains (expensive), (hidden), and (wrap (unit)). Extraction prints (wrap (unit)): its cost is 2, (expensive) costs 5, and (hidden) is not a candidate.

Among nodes of equal cost, extraction takes the one whose term is lowest, and then the one whose content colour (a hash of its structure, the name dump-egraph gives it, Chapter 24) is smallest. The choice therefore depends only on the e-graph’s contents, not on the order nodes were created in: two runs that build the same e-graph extract the same term. Height comes before colour because, with operators of cost 0, a class can reach itself at equal cost, and a choice by colour alone could pick the cycle. An AC, ACI, or commutative node’s operands print sorted by their text.

A cycle is not itself an error when its class also has an extractable grounded member. Extraction fails when no candidate has a fully extractable child set. It reports a more specific error when every node in the requested class is marked :unextractable.

(sort E) (constructor hidden () E :unextractable) (let value (hidden)) (extract value)

A cost that is not additive, or that depends on how an AC operator’s operands are grouped, is a cost model: Chapter 24.

Extraction chooses one representative of one e-class. Anti-unification compares two e-classes and is introduced in Part III. The extraction algorithm and its failure cases are specified in design §11.1.

Statistics

(print-stats) prints the current node and class counts followed by the most recent run’s iteration count, match-step count, wall time, saturation flag, and goal flag. (print-stats :file "path.json") writes the same fields as JSON. The match-step count includes executed lowered matching steps and emitted matches. It is an implementation work measure, not a semantic match count.

print-stats does not rebuild the e-graph. Its node and class fields describe the graph when the command executes, while the remaining fields still describe the last run. The presence of a print-stats command enables match-step counting for that program.

Under the naive strategy selected by the saturation fixture, the first printed reading is 23 nodes, 9 classes, 3 iterations, and 111 match steps, with saturation true. The goal-directed run then reports 30 nodes, 10 classes, 3 iterations, and 144 match steps, with goal-met true and saturation false. Wall time depends on the machine and run.

The interpreter’s command behavior and statistics fields are specified in design §9.1.

Naive and semi-naive evaluation

Chapter 8 defines the saturation round. This chapter compares only how the naive and semi-naive strategies schedule matches within that round: full recomputation, delta variants, and the cases that retain a full-index fallback.

Naive evaluation

Given the post-rebuild snapshot defined in Chapter 8, naive evaluation matches every selected rule against all indexed nodes. A match found in iteration 3 can be found and acted on again in iterations 4 and 5. There is no cross-iteration set of previously applied matches.

This strategy repeats matching work as the graph grows. Its advantage is a simple execution path with no delta bookkeeping, so it serves as the reference strategy in differential tests.

Semi-naive evaluation

Semi-naive evaluation uses a full match in its first iteration because the entire initial graph is new. In later iterations it builds both the full index and a delta index. The delta contains nodes touched since the previous full index was built:

• nodes created by rule actions;
• nodes recanonicalized during rebuild;
• members recorded when one e-class is absorbed into another.

The delta is not merely a suffix of newly allocated node IDs. A merge can change a stored node’s canonical children or enlarge a class without allocating a node, and either event can enable a match.

For an eligible rule with k relation-scanning atoms, Semper evaluates k variants. Variant i restricts atoms before i to full minus delta, restricts atom i to delta, and leaves later atoms on full. Every selected match belongs to the variant containing its first delta atom, so the variants do not duplicate one another.

Equality constraints, primitive predicates, and global comparisons are filters, not relation-scanning atoms. Some rule shapes can become enabled by a merge that no scanning atom represents. Semper evaluates those rules against the full index in every iteration rather than applying an unsafe delta restriction. These shapes are a rule with no scanning atom, a rule tagged :flatten, an equality constraint on an atom’s node variable, and a global in a child or element position.

Delta boundaries

Rule actions performed during an iteration are outside its delta and become visible in the next iteration. The four indexed relations, by operator, class representative, child position, and variadic containment, all obey each atom’s full, delta, or full minus delta mode.

Variadic matching requires all four relations to share that boundary. An associative, AC, or ACI parent can acquire a new canonical representation after a child merge, and a class merge can expose new membership without changing the surviving representative. Recanonicalized parents and absorbed class members are therefore recorded in the touched log. Restricting only the operator scan would miss or duplicate matches reached through child and containment indexes.

Sequence rules and :flatten rules

A sequence rule (Chapter 5) is one query over a whole node, so it has no per-atom variants. Under --use-semi-naive it is evaluated against the round’s delta instead. A root node’s matches can change only if the node is in the delta or one of its child classes is affected: the root class of a delta row of one of the rule’s item patterns, or the class of a node subsumed this round. For each rule and round, Semper estimates from index sizes, before doing the work, whether testing that condition pays. When it does, the rule assembles only the nodes that pass, either filtering naive’s candidates or listing the nodes directly when their parents are few; otherwise it is matched naively. On the 1,172 MLTL specifications Johannsen and Rozier publish with their FMCAD 2026 paper (Chapter 24) the estimate chooses naive in all 11,555 rule rounds, since a test costs more than the assembly it can save on graphs that small, and naive and semi-naive saturation build identical e-graphs.

An ordinary rule tagged :flatten is matched naively in every iteration: a view changes when a class below the node gains a member of the same operator, and no variant’s delta holds the root then.

These rules implement the delta decomposition described in design §9.2. The index relations are specified in design §8.1.

Equivalent outcomes

The user-facing contract is equivalent derivable equalities and check outcomes, not identical execution traces. Naive evaluation emits old matches again. Semi-naive evaluation emits delta-involving matches and uses full matching for the exceptional rule shapes above. The strategies can consequently report different emitted matches, node counts, iteration counts, and match-step counts.

The Chapter 9 fixture 09-eval-strategies.egg runs a variant of the dbl program from Chapter 8, with z and s declared as constructors and an input of three. It selects both strategies with the harness directive:

;; EVAL: both

The harness executes the multi-round program under each strategy. Its equality and disequality checks must pass in every execution.

The repository also differentially compares the resulting equality partition over shared input nodes and exercises fresh nodes, recanonicalization, class growth, variadic atoms, subsumption, globals, and equality constraints. These executable tests support the implementation contract; they are not a machine-checked proof of semi-naive completeness.

Selecting a strategy

Naive evaluation is the default. --use-naive selects it explicitly, and --use-semi-naive selects semi-naive evaluation. The flags are mutually exclusive.

EVAL is a directive understood by the .egg test harness, not a Semper language command. ;; EVAL: naive and ;; EVAL: semi select one strategy. ;; EVAL: both runs the fixture separately under both strategies and checks the expected program outcome in each run.

Canonization and the node kinds

Chapter 4 defines the algebraic declaration contract. This chapter describes the physical child representations selected by those declarations and the canonization pipeline that prepares an e-node for hash-consing.

The five child representations

Each operator selects one of five representations for its children. Literal nodes are a separate leaf kind that carries a concrete value.

Ordinary operators use ordered tuples. Tuples of up to three children have dedicated storage, while wider tuples use a pooled slice. :comm selects the unordered pair. The associative declarations select a sequence, :assoc-comm selects a multiset, and :assoc-comm-idem selects a set.

The missing information in the last column cannot distinguish two e-nodes. Chapter 4 defines the corresponding equations and Chapter 5 defines how patterns inspect each representation.

The canonization pipeline

Term construction performs these operations before inserting an e-node:

1. Replace every child id with its current e-class representative.
2. Flatten eligible nested applications of the same variadic operator.
3. Normalize the resulting child representation.
4. Resolve an empty or singleton variadic result when its declaration permits it.
5. Look up the operator and normalized children in the hash-cons table.

Normalization sorts an unordered pair. It preserves sequence order. For a multiset it sorts children, coalesces equal entries, and applies the configured unit, count, and inverse transforms. For a set it sorts and deduplicates children and removes a configured unit. The legality and meaning of those transforms belong to Chapter 4.

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

;; A binary commutative operator stores a sorted pair. Building the swapped
;; spelling reuses the same node, so both size reports have total 3.
(function eq (E E) E :comm)
(let eq_ab (eq a b))
(print-size)
(let eq_ba (eq b a))
(print-size)
(check-eq eq_ab eq_ba)

Both print-size commands report total: 3. The second spelling replaces its children by the same representatives, sorts them to the same pair, and finds the existing eq node.

Ground-term insertion and rewrite right-hand-side evaluation use this same pipeline. The full procedure is specified in design §5.2.

Recanonization during rebuild

A class merge can make a stored child id noncanonical or make two direct children equal. Rebuild revisits affected parents, replaces their direct children with current representatives, and reapplies the representation’s sorting, coalescing, deduplication, unit removal, and multiplicity clamp. A hash-cons collision then triggers the generic congruence merge described in Chapter 6. Recanonization does not cancel inverse pairs. A separate repair round in every rebuild cancels the pairs that later merges form. A coalesced multiplicity past the configured width leaves the node unchanged, and the command or run reports the overflow as an error.

Multisets retain the original multiplicities until the configured clamp runs. Nilpotent operators therefore remain MSet nodes even at order two. Sets store no explicit counts because every represented count is one.

Sequence nodes have a narrower rebuild boundary. Rebuild recanonizes the ids already present in a sequence span, but it cannot enlarge that span when a child class later acquires a same-operator sequence. Chapter 11 describes the optional associative inter-reduction work that can add further equalities, and a rule tagged :flatten matches through such nesting without changing what is stored (Chapter 5).

The boundary

Canonization normalizes one node under its selected representation. It does not derive consequences that require equations between separate stored nodes. Generic congruence belongs to Chapter 6, domain equations belong to the rules of Chapter 5, and optional completion belongs to Chapter 11.

Three congruence closures

Chapters 6 and 10 define generic congruence and local canonization. This chapter compares the additional equalities obtained in plain mode, eager completion, and lazy completion.

The selected mode does not change the maximum-partition matching relation defined in Chapter 5. Completion derives equalities between stored terms; it does not broaden rule matching into classical AC matching.

A consequence plain mode misses

Consider the asserted equations add(a,b) = c and add(a,b,d) = n. The declared AC theory entails add(c,d) = n, but flattening means that the larger stored sum has direct children a, b, and d. The class for add(a,b) is not one of those direct children.

(sort E)
(function add (E) E :assoc :comm)
(function a () E)
(function b () E)
(function c () E)
(function d () E)
(function n () E)

(union (add a b) c)
(union (add a b d) n)

;; Ordinary congruence follows a direct class reference.
(function f (E) E)
(check-eq (f (add a b)) (f c))

;; Plain rebuild does not substitute the known sub-sum into the larger sum.
(print-size)
(check-eq n (add c d))

The first check demonstrates ordinary congruence through a direct child-class reference. The final check fails because plain mode performs no sub-sum substitution. Its preceding print-size reports 8 e-nodes.

The modes side by side

For multiset and set operators, eager completion treats asserted ground equations as an oriented basis and closes implemented inter-reduction, superposition, and cancellative consequences during rebuild. It also performs a narrower inter-reduction pass over associative sequences, closing some equalities hidden when construction flattened an intermediate sequence. Lazy completion runs the same work only to answer equality and disequality checks, inside a transaction that is later restored.

The modes are two settings. :completion decides whether rebuild completes, which is what rules, extraction and anti-unification see. :check-completion decides whether a check completes temporarily to answer, and matters only while :completion is off: lazy mode is graph completion off with check completion on. A set-option takes effect from its command on, and overrides the starting flag, so a program states its own mode. Turning :completion eager on rebuilds at once; turning it off keeps what eager completion derived. A single check can override the setting with :complete or :no-complete, for example (check-eq a b :complete) in a plain program.

The eager and lazy fixtures use the same declarations, equations, and decisive check as the displayed program. Immediately before that check, the measured node counts are 8 in plain mode, 9 in eager mode, and 8 in lazy mode. Plain fails the equality check. Eager and lazy pass it, but only eager retains the additional node.

Eager work runs on every rebuild and is visible to rules, extraction, and anti-unification. Lazy work is visible to consecutive equality or disequality checks in the shared transaction. The first other command closes that transaction, so other graph readers see the restored plain graph.

Choosing a mode

Use plain mode when the program needs no consequences of asserted equations over associative, AC, or ACI nodes. Use lazy mode for a limited sequence of equality questions. Use eager mode when rules, extraction, anti-unification, or another graph reader must observe completion-derived classes.

One practical point when choosing plain mode: because plain mode derives no AC consequences, its answer to an equality query over AC or ACI nodes can depend on the order the statements appear in. Flattening a nested same-operator argument is declined once that argument’s class is referenced as a child anywhere else, and that condition never becomes false again, so building an unrelated term earlier can change how a later term is spelled:

(let t0 (Add (Mul D D) A))    ; delete this line, or move it below, and
(let t1 (Mul D D A D))        ; the following check passes instead of failing
(let t2 (Mul A D (Mul D D)))
(check-eq t1 t2)

Both readings are sound. A reordering never makes a false equality provable, only a true one unprovable. Within a single term the order is fixed, so the effect appears only across statements. If a program depends on equalities like this one, that is the signal to turn on eager completion or check completion, which decide it in either order. Operators declared associative-only (:assoc) are not affected: their flattening is decided from the written form of the application, so it does not depend on what else the program has built.

Chapter 23 collects the limits and qualifications of these modes. The procedures are specified in design chapter 6, Part III, with the scope of the completeness argument in design chapter 6.

What anti-unification is

The definition

Unification finds a most general substitution that makes two terms identical. Anti-unification is the dual: it finds a most specific term of which both operands are instances. The common operators form a skeleton, and the positions where the operands differ are generalized.

How a disagreement is reported

For f(a,a) and f(a,b), the first child belongs to the skeleton and the second child differs:

(sort E)
(function a () E)
(function b () E)
(function f (E E) E)

(let left (f (a) (a)))
(let right (f (a) (b)))

(antiunify left right :algorithm exact)
(checkau left right :max_size 4 :algorithm exact)

The antiunify command prints:

(anti-unify :size 4 :cr 0.3333 :completion exact
  (f a (Variants a b)))

Textbook anti-unification would usually put a fresh variable in that position. Semper instead writes (Variants a b). Selecting the first child of each Variants node reconstructs the left operand; selecting the second reconstructs the right operand. The output therefore carries the two readings that produced each disagreement.

The commands

antiunify computes and prints an anti-unifier. checkau computes the same result and fails when its size exceeds :max_size; it prints no anti-unifier on success. Its bound is an upper bound, so :max_size 4 accepts any result of size four or less.

Both commands accept inline terms or names introduced by let. Book examples use checkau to make the measured size an executable regression. The antiunify and checkau command signatures are collected in Annex B, and Annex A gives their complete grammar. Chapters 14 and 15 define the algorithm and cycle options.

Reading the output

If a and b are the smaller and larger operand sizes, respectively, the reported ratio is

(result_size - a) / b

For a fixed pair of ground terms, zero denotes full agreement and one is the no-sharing result that holds both terms in one Variants node. The example’s result has size four over two size-three operands, hence (4 - 3) / 3 = 0.3333.

For e-classes, a and b are the independently smallest representatives. Search may choose larger represented terms to obtain a common skeleton, so :cr is not clamped and can exceed one.

The objective

Both solvers minimize (size, variant_mass) lexicographically. Size is compared first. If two results have the same size, the solver chooses the one with fewer concrete nodes below Variants nodes, leaving more of the result in the common skeleton. variant_mass is not printed by the surface command.

The exact definitions and the separate floating-point reward used only for UCT selection are in design chapter 12, section 2.5.

What it does not do

Anti-unification localizes a disagreement; it does not decide which side is correct. That decision requires a type checker, a schema, a test, or a person. Part IV uses the shared skeleton and its Variants nodes to direct that review.

Anti-unification modulo the declared algebra

Chapter 4 defines the algebraic declarations, and Chapter 10 shows their child representations. This chapter measures their effect on anti-unification. Order and repetition can disappear during term canonization. A declared identity also lets the anti-unifier align collection nodes with different cardinalities.

Order, absorbed by commutativity

The two pairs below differ only in whether their operator is declared commutative:

(sort E)
(function a () E)
(function b () E)
(function Pair (E E) E)
(function PairC (E E) E :comm)

(let ordered_left (Pair (a) (b)))
(let ordered_right (Pair (b) (a)))
(antiunify ordered_left ordered_right :algorithm exact)
(checkau ordered_left ordered_right :max_size 5 :algorithm exact)

(let commutative_left (PairC (a) (b)))
(let commutative_right (PairC (b) (a)))
(antiunify commutative_left commutative_right :algorithm exact)
(checkau commutative_left commutative_right :max_size 3 :algorithm exact)

The order-sensitive pair reports both positional disagreements. The commutative pair was already one canonical e-node before the query:

(anti-unify :size 5 :cr 0.6667 :completion exact
  (Pair (Variants a b) (Variants b a)))
(anti-unify :size 3 :cr 0.0000 :completion exact
  (PairC a b))

Declaring commutativity changes the measured result from size 5 and ratio 0.6667 to size 3 and ratio 0.

Repetition, absorbed by idempotence

The next comparison gives the left operand two copies of a and the right operand two copies of b. Bag preserves those multiplicities, while SetI is idempotent:

(sort E)
(function a () E)
(function b () E)
(function c () E)
(function Bag (E) E :assoc-comm)
(function SetI (E) E :assoc-comm-idem)

(let bag_left (Bag (a) (a) (b)))
(let bag_right (Bag (a) (b) (b)))
(antiunify bag_left bag_right :algorithm exact)
(checkau bag_left bag_right :max_size 5 :algorithm exact)

(let set_left (SetI (a) (a) (b)))
(let set_right (SetI (a) (b) (b)))
(antiunify set_left set_right :algorithm exact)
(checkau set_left set_right :max_size 3 :algorithm exact)

(let changed_left (SetI (a) (b)))
(let changed_right (SetI (a) (c)))
(antiunify changed_left changed_right :algorithm exact)
(checkau changed_left changed_right :max_size 4 :algorithm exact)

The multiset result shares one a and one b, then reports the unmatched copies. Canonization removes the duplicate members from both SetI terms:

(anti-unify :size 5 :cr 0.2500 :completion exact
  (Bag a b (Variants a b)))
(anti-unify :size 3 :cr 0.0000 :completion exact
  (SetI a b))

Idempotence changes the measured result from size 5 and ratio 0.25 to size 3 and ratio 0.

Arity, aligned by an identity element

Order and duplicate removal happen while Semper constructs the operands. Different cardinalities require an additional AU operation: when an AC or ACI operator has an identity, the solver can pad the shorter collection with that identity before aligning children.

The next fixture compares a three-condition conjunction with the same conjunction missing one condition. AndU declares (Lit true) as its identity; AndN has the same ACI properties but no identity:

(sort Formula)
(sort Bucket)
(sort Region)

(function Lit (bool) Formula)
(function AndU (Formula) Formula :assoc-comm-idem :identity (Lit true))
(function AndN (Formula) Formula :assoc-comm-idem)

(function src () Bucket)
(function dst () Bucket)
(function regionOf (Bucket) Region)
(function versioningOn (Bucket) Formula)
(function encrypted (Bucket) Formula)
(function approvedRegion (Region) Formula)

(let fullU
  (AndU
    (versioningOn (src))
    (encrypted (src))
    (approvedRegion (regionOf (dst)))))
(let droppedU
  (AndU
    (versioningOn (src))
    (encrypted (src))))
(antiunify fullU droppedU :algorithm exact)
(checkau fullU droppedU :max_size 10 :algorithm exact)

(let fullN
  (AndN
    (versioningOn (src))
    (encrypted (src))
    (approvedRegion (regionOf (dst)))))
(let droppedN
  (AndN
    (versioningOn (src))
    (encrypted (src))))
(antiunify fullN droppedN :algorithm exact)
(checkau fullN droppedN :max_size 13 :algorithm exact)

The two measured results are:

(anti-unify :size 10 :cr 0.6250 :completion exact
  (AndU
    (versioningOn src)
    (encrypted src)
    (Variants (approvedRegion (regionOf dst)) (Lit true))))
(anti-unify :size 13 :cr 1.0000 :completion exact
  (Variants
    (AndN (versioningOn src) (encrypted src) (approvedRegion (regionOf dst)))
    (AndN (versioningOn src) (encrypted src))))

With the identity, the absent condition is paired with true, while the two shared conditions remain in the skeleton. Without it, the unequal-cardinality nodes have no structural alignment and both conjunctions are generalized whole. Identity padding changes the measured result from size 13 and ratio 1 to size 10 and ratio 0.625.

Where absorption stops

The final query in the repetition fixture compares (SetI a b) with (SetI a c). ACI canonization absorbs order and repetition, but it does not equate b with c:

(anti-unify :size 4 :cr 0.3333 :completion exact
  (SetI a (Variants b c)))

This is a genuine replacement under the declared algebra: a remains shared and the replacement remains visible. A domain equality can still be established by a Chapter 5 rule before the query. Part IV covers cases that require a reviewer rather than another equality.

The exact algorithm

The exact solver searches the finite action graph induced by two e-classes. Its answer is exact for a selected cycle policy, the objective from Chapter 12, and the e-graph snapshot supplied to it.

The search space

A search state asks how to anti-unify two e-classes. It is an OR node because the solver may choose among several compatible representations of those classes. Each choice is an AND node because all child-class pairs induced by that representation must be solved.

The same ordered class pair can be reached from several parents, so the search space is a graph rather than a tree. The graph has finitely many ordered pairs even when cyclic e-classes represent infinitely many finite terms.

The actions at a state

Every unequal state has a generalize action: Variants(best(left), best(right)). It provides an achieved result before any structural action is examined. Compatible e-nodes provide the other actions:

The transport formulation materializes child-pair cells rather than all complete AC pairings. Multiplicity supplies and demands select how many copies of each child pair the composed result contains.

The complete action-generation rules are in design chapter 12, section 3.4.

The recursion

Let G(q) be the achieved baseline for state q: the smallest admissible term when the classes agree, and the generalize result otherwise. Pair-mode Exact starts with G and repeatedly evaluates every structural action from the previous round:

V0(q)     = G(q)
Vd+1(q)   = min(Vd(q), compose(a, Vd(children(a))) for each action a)

The minimum uses (size, variant_mass). Pair mode interns each reachable ordered pair once and performs synchronous rounds until the values stop changing. Side-policy Exact instead memoizes contextual states because its cycle filter depends on retained left and right ancestors.

Cycles

Saturation can merge a class with one of its descendants. Recursion must then exclude infinite descent without excluding every finite derivation that crosses the cycle.

The side policies are provenance choices. They prevent search from using some rewrite-created cyclic structure, and an exact result under either policy is optimal only in the graph that policy retains. Pair mode admits a side revisit when the other side changes; its pair-cycle-erasure argument says that blocking a repeated ordered pair still retains a minimum finite derivation.

The fixture below creates the recursive class cycle = {f(a), h(a, cycle)} and queries the same operands under all three policies:

(sort E)
(function a () E)
(function f (E) E)
(function h (E E) E)

(let cycle (f (a)))
(union cycle (h (a) cycle))

(let left (h (a) (h (f (a)) (f (a)))))
(let right (h (a) (h (a) (f (a)))))

(antiunify left right :algorithm exact :cycles sides)
(checkau left right :max_size 9 :algorithm exact :cycles sides)

(antiunify left right :algorithm exact :cycles sides-current)
(checkau left right :max_size 9 :algorithm exact :cycles sides-current)

(antiunify left right :algorithm exact :cycles pair)
(checkau left right :max_size 8 :algorithm exact :cycles pair)

It prints:

(anti-unify :size 9 :cr 1.0000 :completion exact
  (h a (Variants (h (f a) (f a)) (f a))))
(anti-unify :size 9 :cr 1.0000 :completion exact
  (Variants (h a (h (f a) (f a))) (f a)))
(anti-unify :size 8 :cr 0.8571 :completion exact
  (h a (h (Variants (f a) a) (f a))))

The hidden qualities are (9,7) for sides, (9,9) for sides-current, and (8,3) for pair. The size-eight derivation revisits one side class while its partner changes, then reaches a finite terminal pair. Both side policies filter that route.

Pruning

The solver can compute a size lower bound for a structural action by summing child-pair bounds, or by solving a transport problem over those bounds. Two implemented comparisons use it:

1. If the bound is greater than the achieved generalize size, the action cannot improve the state.
2. If the bound is greater than the current achieved incumbent, the action cannot improve that incumbent.

Both comparisons are opt-in Rust-API settings, off by default. The first is dominance_pruning in UCT; the second is exact_pruning in Exact and live_incumbent_pruning in UCT. The surface commands run with all three off.

Both comparisons are strict and inspect size only. Equality cannot discard an action because an equal-size result may still have smaller variant mass. A discarded structural action loses no achieved term and cannot contain the lexicographic optimum.

The bound and pruning arguments are in design chapter 12, sections 9.1-9.4.

What :completion exact means

For this algorithm, :completion exact says that the returned term is optimal:

1. under Chapter 12’s (size, variant_mass) objective;
2. among derivations admitted by the selected cycle policy; and
3. over the admissible e-nodes and equalities in the current snapshot.

Chapter 16 measures the consequences of these qualifiers. The pair-mode cycle-erasure and round-bound argument is a prose argument supported by regressions and a finite oracle, not a machine-checked theorem for the Rust solver. The current proof boundary is stated in design chapter 12, section 9.6.

Graph search, and the hybrid

UCT searches the same action graph defined in Chapter 14, but it can return an achieved result before the graph has been exhausted. A playout budget controls how much of the graph it explores.

When to use it

The surface default is :algorithm uct with 1,000 playouts and :cycles sides. Select exact when an exhaustive result is required and its search completes within the available resources. Select UCT when a fixed playout budget is required. Neither algorithm is generally faster; their costs depend on the action graph.

Unless the root state is already terminal, UCT performs a deterministic initial rollout before its first playout. A budget of :playouts 0 therefore returns that initial achieved result rather than no result. Further playouts can improve it or exhaust the graph. The output reports :completion budget in the first case and :completion exact in the second.

The following query reuses Chapter 14’s cyclic construction. With 10,000 playouts and pair-cycle filtering, UCT exhausts this small graph and returns the same size-eight term:

(antiunify left right :algorithm uct :playouts 10000 :cycles pair)
(checkau left right :max_size 8 :algorithm uct :playouts 10000 :cycles pair)

(anti-unify :size 8 :cr 0.8571 :completion exact
  (h a (h (Variants (f a) a) (f a))))

One playout

A playout performs four operations:

1. Select from the root, using UCT at OR nodes and an effort selector at AND nodes.
2. Expand the first unhandled action reached.
3. Run a deterministic rollout to initialize newly reached states.
4. Walk back along that path, recomputing values and composing stored child terms into achieved candidates for their parents.

Composition during the final step is how later playouts improve on the initial rollout. The full procedure is specified in design chapter 12, section 3.3.

The same subproblem, reached many ways

Several paths may reach the same contextual class-pair state. They share that state’s current value and achieved term. Selection counts remain local to the parent-action edge, however, so traffic arriving through another parent does not pretend that this parent selected the shared child.

Chapter 14 defines the cycle contexts that distinguish states. The shared-state and local-edge bookkeeping is detailed in design chapter 12, section 2.6.

Values are recomputed, not accumulated

Ordinary tree-MCTS bookkeeping would mix unrelated traffic at a shared child. A child visit count includes visits from parents that the current parent never selected, and propagating every child update into every parent would count work outside each parent’s selected distribution.

Semper keeps N(n,a) on the edge from state n to action a, and recomputes values from current child values:

Q(n)   = (U(n) + sum N(n,a) * Q(a)) / (1 + sum N(n,a))
Q(a)   = 1 + sum count(i) * Q(child(i))

U(n) is the initial rollout estimate. AC and ACI actions replace the second sum with the current minimum-cost transport. An off-path parent can temporarily hold a stale value, changing what a finite budget explores, but a published candidate is still composed from achieved child terms rather than estimates.

Closure

A structural completion check asks whether every reachable action has been handled and every realized child has completed. If so, a children-first pass recomposes all shared parents before the root is reported exact.

The opt-in closed_bit setting of the Rust API, off by default, maintains closure incrementally. A completed shared state then notifies every parent through reverse edges, selection skips its closed subgraph, and a closed root stops the run early. Without that setting, including every surface command, the run spends its full playout budget. Closure means that no unresolved action remains. It cannot be inferred merely because a size lower bound equals the incumbent size: an equal-size action could still improve variant mass. Chapter 14 gives the pruning rule; the closure argument is in design chapter 12, section 9.5.

The hybrid

Hybrid search hands an admitted UCT state to Exact. A completed call marks that state exact and terminal, so subsequent selection need not enter its subgraph. The call receives the same class pair, cycle context, and cycle mode as the UCT state and therefore solves the same contextual problem.

Admission uses estimates of the reachable class-pair rectangle and entry-state action count. These estimates are not complexity bounds on descendant contextual states. A separate Rust configuration can impose a node-entry budget on one delegated call. Hybrid correctness has finite differential evidence and an implementation argument, not a machine-checked solver proof.

Hybrid selection is available only through the Rust API. The implementation and argument are in mcgs.rs.

Configuration

The surface language exposes :algorithm, :playouts, and :cycles. Chapter 14 defines the cycle options. Incremental closure, hybrid calls, their admission settings, and the other search-policy controls are Rust-API configuration. The complete configuration table is in design chapter 12, section 7.

What the result is optimal with respect to

An exact result minimizes the Chapter 12 objective over the derivations admitted by its cycle policy and the equalities present in its e-graph snapshot. Each qualification can change the returned term.

Optimal over the e-graph, not over the theory

Chapter 11’s containment example asserts add(a,b) = c and add(a,b,d) = n. The AC theory entails add(c,d) = n, but plain congruence does not derive it. Chapter 16 wraps n and add(c,d) in a common unary operator g and runs this query:

(antiunify l r :algorithm exact)
(checkau l r :max_size 2 :algorithm exact)

The same program is executed in three completion modes:

The size-two checkau bound deliberately fails in the plain and lazy fixtures and succeeds in the eager fixture.

Plain mode reports an exact optimum over its snapshot. The snapshot lacks one AC consequence, so it contains a disagreement where the theory does not. Eager completion adds that equality before the snapshot is taken, and the disagreement disappears.

Lazy completion does not help the anti-unifier

The lazy result has size 5, the same as plain, rather than the eager result’s size 2. As Chapter 11 explains, lazy completion is scoped to equality and disequality checks. Anti-unification reads the restored graph.

When an AU query must observe consequences of asserted AC equations, turn on eager completion with (set-option :completion eager) or --derive-ac-eqs. Lazy completion is suitable for isolated equality questions, not for preparing an anti-unification snapshot.

Optimal within the cycle policy

Chapter 14’s cyclic fixture measures size 9 under the default sides policy and size 8 under pair. Both outputs say :completion exact; they optimize different admitted derivations. A quoted cyclic result must therefore name its cycle policy. Chapter 14 defines those policies and gives the measured terms.

Optimal under this objective

The objective is a definition of which valid anti-unifier is best. It does not encode domain terminology or a reader’s preferred presentation.

In the next fixture, the two initial classes contain only domain-facing Approved and Rejected terms. Each class is then merged with an equivalent Wire representation:

(sort E)
(function common () E)
(function Approved (E bool) E)
(function Rejected (E bool) E)
(function Wire (E bool) E)

(let left (Approved (common) false))
(let right (Rejected (common) true))

(antiunify left right :algorithm exact)
(checkau left right :max_size 6 :algorithm exact)

(union left (Wire (common) false))
(union right (Wire (common) true))

(antiunify left right :algorithm exact)
(checkau left right :max_size 4 :algorithm exact)

Before the unions, the only result is the explicit domain distinction:

(anti-unify :size 6 :cr 1.0000 :completion exact
  (Variants (Approved common false) (Rejected common true)))

After the unions, the solver finds a smaller common representation:

(anti-unify :size 4 :cr 0.3333 :completion exact
  (Wire common (Variants false true)))

The size-four result is optimal under (size, variant_mass), but the size-six result preserves the labels Approved and Rejected. Applications that prefer those labels need a different output objective or a presentation layer; the exact certificate does not claim readability.

What is argued rather than proved

The au-verus crate proves objective-order and representation lemmas. It also proves a lower bound for any function that satisfies two recurrence inequalities. It does not prove that the solver’s recurrence value equals the optimum, and it does not verify the production Rust solver end to end. A small exhaustive oracle supplies finite evidence for pair-mode Exact on enumerable fixtures.

Pair-cycle erasure and global optimality remain prose arguments supported by regressions. Hybrid calls have finite differential evidence. Chapters 14 and 15 state the operational claims, and design chapter 12, section 9.6 states the current proof boundary.

Using e-graphs and anti-unification for semantic comparison in autoformalization

Autoformalization turns a natural-language requirement into a formal artifact. This chapter defines the review problem, explains what ordinary checks leave unsettled, and introduces comparison across several generated samples.

From a sentence to an enforced artifact

A formalization pipeline may produce a policy, specification, formula, or proof obligation. The sentence records what somebody requested. The generated artifact is what another system will enforce, check, or prove.

Consider this requirement:

The agent may POST to /deploy, but only if a health check has already come back 200 in the last 15 minutes.

Its policy must represent the request method, path, event kind, response status, and time window. A reviewer who knows the formal language may not know the intended policy, while the author of the sentence may not know the formal language. Comparing syntax does not resolve that division.

What the ordinary checks leave open

Compare against a reference. A correct reference would settle the question, but many autoformalization tasks have no such artifact. Accuracy against a gold answer and a diff against expected output are unavailable in that case.

Validate the artifact. Validation remains required. It rejects malformed terms, unknown fields, and sort errors. It also accepts a well-formed artifact that expresses the wrong condition.

Test the artifact. Tests remain required as well. A replay exposes a missing condition only when its trace exercises the behavior that condition would have excluded. The test author must first identify the behavior to test.

Read the artifact. Direct review can find every category of error, but a large formula gives no ordering over its possible error locations. The reviewer reads agreed structure and disputed structure with equal attention.

Validation and testing answer questions that comparison cannot. The method in this part supplements them by identifying where samples disagree.

Sample it several times

Generate three to five formalizations of the same sentence, or obtain them from several formalizers. The comparison does not treat any sample as a reference. It produces two intermediate results:

1. a partition whose members are equal under the declared algebra and asserted domain facts;
2. an anti-unifier for each pair of clusters, with both readings attached at every localized difference.

Agreement means that this comparison localized no disagreement at that position. It does not establish that the agreed reading is correct. Chapters 18 and 19 construct the partition and the pairwise explanations.

Presentational noise

Several syntactic differences may preserve the intended meaning: reordered or repeated conjuncts, reversed equality operands, >= 1 versus 1 <=, 15 minutes versus 900 seconds, or a named predicate versus its expansion. A text diff reports these beside changes to event kinds, connectives, and guards.

Different mechanisms remove or localize different kinds of noise:

Identity alignment does not make the samples equal. It keeps their shared children in the skeleton and localizes the missing child.

Correlated errors

Samples from one model under one prompt can repeat the same interpretation. Agreement among those samples is therefore weaker than agreement among independent sources. The repository’s formalizer pilot uses one system and explicitly treats its result as an optimistic bound, not a population study.

This method directs review toward uncorrelated differences. It is not a soundness argument, and Chapter 23 retains that boundary among the engine’s other limits.

Clustering samples by equality saturation

Clustering composes the declarations, saturation, and equality checks from Parts I and II. This chapter builds a partition of four samples, shows how one domain fact changes it, and gives checks for diagnosing an unexpected partition.

The procedure

For one set of samples:

1. Declare the shared signature and only the algebraic properties valid in the domain.
2. Insert every sample with a distinct let name.
3. Assert the domain equalities that the comparison may use.
4. Run the selected rules to saturation.
5. Check every pair of sample names for equality or non-equality.

The fixture performs the checks both before and after its domain rule:

(sort Formula)
(sort Region)

(function Lit (bool) Formula)
(function And (Formula) Formula :assoc-comm-idem :identity (Lit true))
(function Or (Formula) Formula :assoc-comm-idem :identity (Lit false))

(function core () Formula)
(function destination () Region)
(function approvedRegion (Region) Formula)
(function usEast (Region) Formula)
(function euWest (Region) Formula)
(function apSouth (Region) Formula)

(let s1
  (And
    (core)
    (approvedRegion (destination))))

;; Reordered, with a duplicate that idempotence removes.
(let s2
  (And
    (approvedRegion (destination))
    (core)
    (core)))

(let s3
  (And
    (core)
    (Or
      (usEast (destination))
      (euWest (destination)))))

(let s4
  (And
    (core)
    (Or
      (usEast (destination))
      (apSouth (destination)))))

;; Initial partition: {s1, s2}, {s3}, {s4}.
(extract s1)
(extract s2)
(extract s3)
(extract s4)
(check-eq s1 s2)
(check-neq s1 s3)
(check-neq s1 s4)
(check-neq s2 s3)
(check-neq s2 s4)
(check-neq s3 s4)

;; This deployment defines the named predicate by two concrete regions.
(rewrite
  (approvedRegion r)
  (Or (usEast r) (euWest r)))
(run 3)

;; Saturation moves the partition to {s1, s2, s3}, {s4}.
(extract s1)
(extract s2)
(extract s3)
(extract s4)
(check-eq s1 s2)
(check-eq s1 s3)
(check-neq s1 s4)
(check-eq s2 s3)
(check-neq s2 s4)
(check-neq s3 s4)

All samples enter one e-graph. s1 and s2 canonize to the same node, so no later proof is needed to join them. A rewrite can merge other sample classes without discarding either representation.

Reading the partition

Semper has no surface command that prints a partition. For four samples, the six pairwise checks record it directly. Before the rewrite, the checks assert

{s1, s2}  {s3}  {s4}

s1 and s2 differ only by conjunct order and a duplicate core. The ACI declaration for And absorbs both. s3 expands approvedRegion into two specific regions, and s4 names a different second region.

The four initial extractions print:

(And (approvedRegion (destination)) (core))
(And (approvedRegion (destination)) (core))
(And (Or (euWest (destination)) (usEast (destination))) (core))
(And (Or (apSouth (destination)) (usEast (destination))) (core))

The rule states that this deployment’s approved regions are usEast and euWest. After three rounds, the partition is

{s1, s2, s3}  {s4}

Extraction now prints the approvedRegion representative for the first three samples. It still prints the apSouth disjunction for s4.

The check grid uses n(n - 1) / 2 checks for n samples. For a larger corpus, host code can group the class identifiers returned through the Rust API. There is no separate clustering API.

What the partition depends on

A cluster means that Semper proved its members equal under this program. It does not assert semantic equivalence independently of the program.

The first and second partitions differ only because the rewrite was installed and run. The samples themselves did not change.

When a cluster is too fine

First inspect the unresolved syntax. If it is order or repetition, check the Chapter 4 declaration. If it is a domain equation, check that Chapter 8 ran the relevant ruleset to saturation. If it is an equality hidden by flattened AC structure, Chapter 11 explains when eager completion is required.

When a cluster is too coarse

A rule or union may have asserted more than the domain permits. With --proofs --dump-proofs FILE, the proof dump records one path from each node to its representative, including rewrite identifiers along that path. It can identify which merge joined a class, but it does not directly produce a named sample-to-sample explanation or enumerate alternative proofs. The proof-logging design chapter defines that output and its verification boundary.

Explaining the differences between clusters

After clustering, one anti-unification query per cluster pair locates the remaining differences. This chapter reads one such result and tests a proposed domain resolution inside a temporary scope.

One query per pair of clusters

For k clusters, choose one representative from each and run k(k - 1) / 2 queries. After Chapter 18’s rewrite there are two clusters, so its fixture needs one query:

(antiunify s1 s4 :algorithm exact)
(checkau s1 s4 :max_size 9 :algorithm exact)

It prints:

(anti-unify :size 9 :cr 0.7143 :completion exact
  (And
    (Or
      (usEast destination)
      (Variants (euWest destination) (apSouth destination)))
    core))

Any of s1, s2, or s3 can represent the first cluster. An antiunify operand resolves to its e-class, so all three names present the same search state to the solver.

Reading the explanation

The skeleton says that both clusters require core, use a disjunction of regions, and include usEast. The marked position carries the remaining alternatives:

(Variants (euWest destination) (apSouth destination))

A reviewer must determine which region belongs in the deployment policy. A configuration source, deployment test, or domain owner can settle that question. Semper reports the alternatives but does not choose one.

A Variants node is a syntactic marker in the selected anti-unifier, not necessarily one independent semantic decision. Chapter 22 shows one connective change represented by two markers through identity elements.

Ordering several differences

Semper reports :cr for each pair and the terms under each Variants node. It does not rank review questions or aggregate them across queries. A review can use three observable quantities as a convention:

1. inspect pairs with lower :cr first because their disagreement is more localized relative to their operands;
2. inspect smaller alternative subterms before alternatives that replace a complete formula;
3. group the same field and alternatives when they recur across cluster pairs.

Chapter 21 applies the third convention. These steps organize review; they are not part of the AU objective from Chapter 12.

Testing a resolution

A suspected domain equality can be tested without retaining it:

(push)
(union (euWest (destination)) (apSouth (destination)))
(check-eq s1 s4)
(check-eq s2 s4)
(check-eq s3 s4)
(pop)

;; Pop restores the two-cluster partition.
(check-eq s1 s3)
(check-neq s1 s4)
(check-neq s3 s4)

Inside the scope, equating the two region predicates merges s4 with all three members of the other cluster. pop restores the two-cluster partition. The scope behavior is the mechanism from Chapter 7; the union is only a hypothesis being tested.

Even a one-cluster result establishes agreement only under the asserted facts. Chapter 17’s correlated-error warning still applies.

Repair by disagreement

This chapter computes a diff between two candidate Dogwood policies produced from the same natural-language requirement. The diff ignores known language equivalences, locates the remaining variation points, and presents the alternatives at each point. These localized alternatives drive clarification of the original intent.

Dogwood and temporal policies

Dogwood is a Cedar-derived policy language for authorization over event histories. Its temporal sublanguage is a bounded, past-only fragment of Metric First-Order Temporal Logic (MFOTL). It provides event predicates, formerly, previous, since, and the count and sum aggregations. Every temporal operator has a bounded look-back window.

A when temporal { phi } clause evaluates phi at the current decision timepoint against the recorded event history. The event schema determines the fields carried by each action and event kind. Request events carry inputs. Response events can additionally carry outputs such as an HTTP status code.

The original requirement is:

The agent may POST to /deploy, but only if a health check has already come back 200 in the last 15 minutes.

There is no reference policy against which to compare a generated answer. We instead compare two independently produced candidates and use their localized differences to formulate review questions.

The two candidates

Candidate A retains both current-request guards. Its temporal predicate, however, reads output.status_code from a request event:

@id("deploy_after_health_check")
permit (
    principal,
    action == Strands::Action::"http:request",
    resource
)
when { context.input.method == "POST" && context.input.path == "/deploy" }
when temporal {
    (count for (t: Timepoint). where (
        formerly within 15m (
            Strands::Action::"http:request"::request{
                callerPrincipal: principal,
                output.status_code: 200
            }
            && tp(t)
        )
    )) >= 1
};

Candidate B uses the response event kind but omits the /deploy guard:

@id("deploy_after_health_check")
permit (
    principal,
    action == Strands::Action::"http:request",
    resource
)
when { "POST" == context.input.method }
when temporal {
    1 <= (count for (t: Timepoint). where (
        formerly within 900s (
            tp(t)
            && Strands::Action::"http:request"::response{
                 output.status_code: 200,
                 callerPrincipal:    principal
               }
        )
    ))
};

The missing guard is a fail-open behavior. After a matching 200 response, candidate B permits a POST to /admin/purge-all as well as a POST to /deploy.

The candidates also contain six presentational differences:

Encoding Dogwood in Semper

Semper does not evaluate Dogwood policies. It represents their abstract syntax as sorted first-order terms so that policies can be compared modulo the declared algebraic properties of the language operators and rewrite rules encoding known identities in the language. Dogwood remains responsible for validating and replaying completed policies.

The model retains the policy head, Cedar conditions, temporal conditions, aggregation binders, field paths, and request and response event kinds. The main correspondences are:

Here is the complete executable model:

;; EXPECT: ok
;; EVAL: both

;; ANCHOR: dogwood-signature
(sort PolicySet)
(sort Effect)
(sort Scope)
(sort PScope)
(sort AScope)
(sort RScope)
(sort Action)
(sort Expr)
(sort SVal)
(sort TCond)
(sort TTerm)
(sort TAgg)
(sort ArgSet)
(sort Path)
(sort FSeg)
(sort Win)
(sort Ty)
(sort Binders)
(sort Kind)

(function noPolicies () PolicySet)
(function rule (Effect Scope Expr) PolicySet)
(function policies (PolicySet) PolicySet :assoc-comm-idem :identity (noPolicies))
(function permit () Effect)
(function forbid () Effect)

(function head (PScope AScope RScope) Scope)
(function anyPrincipal () PScope)
(function anyResource () RScope)
(function actionEq (Action) AScope)

(function eTrue () Expr)
(function eFalse () Expr)
(function eAnd (Expr) Expr :assoc-comm-idem :identity (eTrue))
(function eOr (Expr) Expr :assoc-comm-idem :identity (eFalse))
(function eEq (Expr Expr) Expr :comm)
(function eCtx (Path) Expr)
(function eStr (SVal) Expr)
(function temporal (TCond) Expr)

(function tTrue () TCond)
(function tAnd (TCond) TCond :assoc-comm-idem :identity (tTrue))
(function formerly (Win TCond) TCond)
(function tp (TTerm) TCond)
(function pred (Action Kind ArgSet) TCond)
(function tGte (TTerm TTerm) TCond)
(function tLte (TTerm TTerm) TCond)

(function bvar (IBig) TTerm)
(function scopePrincipal () TTerm)
(function tInt (IBig) TTerm)
(function agg (TAgg) TTerm)
(function count (Binders TCond) TAgg)
(function bnil () Binders)
(function bcons (Ty Binders) Binders)
(function tyTimepoint () Ty)

(function noArgs () ArgSet)
(function arg (Path TTerm) ArgSet)
(function args (ArgSet) ArgSet :assoc-comm-idem :identity (noArgs))
(function fnil () Path)
(function fld (FSeg Path) Path)
(function secs (IBig) Win)
(function mins (IBig) Win)
(function secsTimes (IBig IBig) Win)

(function request () Kind)
(function response () Kind)
(function aHttpRequest () Action)
(function fInput () FSeg)
(function fOutput () FSeg)
(function fMethod () FSeg)
(function fPath () FSeg)
(function fCallerPrincipal () FSeg)
(function fStatusCode () FSeg)
(function vPOST () SVal)
(function vDeploy () SVal)
;; ANCHOR_END: dogwood-signature

(let methodIsPost
  (eEq (eCtx (fld (fInput) (fld (fMethod) (fnil)))) (eStr (vPOST))))

(let methodIsPostFlipped
  (eEq (eStr (vPOST)) (eCtx (fld (fInput) (fld (fMethod) (fnil))))))

(let pathIsDeploy
  (eEq (eCtx (fld (fInput) (fld (fPath) (fnil)))) (eStr (vDeploy))))

(let healthArgs
  (args
    (arg (fld (fCallerPrincipal) (fnil)) (scopePrincipal))
    (arg (fld (fOutput) (fld (fStatusCode) (fnil))) (tInt 200))))

(let healthArgsFlipped
  (args
    (arg (fld (fOutput) (fld (fStatusCode) (fnil))) (tInt 200))
    (arg (fld (fCallerPrincipal) (fnil)) (scopePrincipal))))

;; ANCHOR: dogwood-candidates
(let candA
  (rule (permit)
    (head (anyPrincipal) (actionEq (aHttpRequest)) (anyResource))
    (eAnd
      methodIsPost
      pathIsDeploy
      (temporal
        (tGte
          (agg (count (bcons (tyTimepoint) (bnil))
                 (formerly (mins 15)
                   (tAnd
                     (pred (aHttpRequest) (request) healthArgs)
                     (tp (bvar 0))))))
          (tInt 1))))))

(let candB
  (rule (permit)
    (head (anyPrincipal) (actionEq (aHttpRequest)) (anyResource))
    (eAnd
      (temporal
        (tLte
          (tInt 1)
          (agg (count (bcons (tyTimepoint) (bnil))
                 (formerly (secs 900)
                   (tAnd
                     (tp (bvar 0))
                     (pred (aHttpRequest) (response) healthArgsFlipped)))))))
      methodIsPostFlipped)))
;; ANCHOR_END: dogwood-candidates

(let pickWorst
  (rule (permit)
    (head (anyPrincipal) (actionEq (aHttpRequest)) (anyResource))
    (eAnd
      (temporal
        (tGte
          (agg (count (bcons (tyTimepoint) (bnil))
                 (formerly (secs 900)
                   (tAnd
                     (pred (aHttpRequest) (request) healthArgs)
                     (tp (bvar 0))))))
          (tInt 1)))
      methodIsPost)))

(let repaired
  (rule (permit)
    (head (anyPrincipal) (actionEq (aHttpRequest)) (anyResource))
    (eAnd
      (temporal
        (tGte
          (agg (count (bcons (tyTimepoint) (bnil))
                 (formerly (secs 900)
                   (tAnd
                     (pred (aHttpRequest) (response) healthArgs)
                     (tp (bvar 0))))))
          (tInt 1)))
      methodIsPost
      pathIsDeploy)))

;; ANCHOR: dogwood-identity
(rewrite (mins x) (secsTimes x 60))
(rewrite (secsTimes x y) (secs (IBig::* x y)))
(birewrite (tLte a b) (tGte b a))
(run 4)
(check-eq (mins 15) (secs 900))
;; ANCHOR_END: dogwood-identity

(check-neq candA candB)
(check-neq repaired candA)
(check-neq repaired candB)
(check-neq pickWorst candA)
(check-neq pickWorst candB)
(check-neq repaired pickWorst)

;; ANCHOR: dogwood-main-query
(antiunify candA candB :algorithm exact)
(checkau candA candB :max_size 61 :algorithm exact)
;; ANCHOR_END: dogwood-main-query

(antiunify repaired candA :algorithm exact)
(checkau repaired candA :max_size 60 :algorithm exact)
(antiunify repaired candB :algorithm exact)
(checkau repaired candB :max_size 60 :algorithm exact)
(antiunify pickWorst candA :algorithm exact)
(checkau pickWorst candA :max_size 60 :algorithm exact)
(antiunify pickWorst candB :algorithm exact)
(checkau pickWorst candB :max_size 51 :algorithm exact)

The encoding retains each candidate’s original time unit. The rewrite from mins to secs states the conversion inside the comparison theory:

(rewrite (mins x) (secsTimes x 60))
(rewrite (secsTimes x y) (secs (IBig::* x y)))
(birewrite (tLte a b) (tGte b a))
(run 4)
(check-eq (mins 15) (secs 900))

The first rule builds (secsTimes 15 60). The second rule binds both operands as IBig literal values and evaluates the eager IBig::* primitive, reducing the intermediate term to (secs 900). The equality is therefore derived by visible rewrite rules rather than imposed while translating the policies.

The identity of eAnd represents an omitted condition. It lets the anti-unifier align candidate A’s path guard with eTrue instead of replacing the complete condition with one large variation. Treating Cedar conjunction as commutative assumes its operands have passed validation and cannot produce order-dependent errors. Temporal conjunction is set intersection and does not have that short-circuiting qualification.

The policy diff

The model runs the exact anti-unifier after applying the comparison identity:

(antiunify candA candB :algorithm exact)
(checkau candA candB :max_size 61 :algorithm exact)

The measured result has size 61, compression ratio 0.1864, and two variation points:

(anti-unify :size 61 :cr 0.1864 :completion exact
  (rule
    permit
    (head anyPrincipal (actionEq aHttpRequest) anyResource)
    (eAnd
      (eEq (eCtx (fld fInput (fld fMethod fnil))) (eStr vPOST))
      (temporal
        (tGte
          (agg
            (count
              (bcons tyTimepoint bnil)
              (formerly
                (mins 15)
                (tAnd
                  (tp (bvar 0))
                  (pred
                    aHttpRequest
                    (Variants request response)
                    (args
                      (arg (fld fCallerPrincipal fnil) scopePrincipal)
                      (arg (fld fOutput (fld fStatusCode fnil)) (tInt 200))))))))
          (tInt 1)))
      (Variants (eEq (eCtx (fld fInput (fld fPath fnil))) (eStr vDeploy)) eTrue))))

The first variation asks whether the historical event is a request or a response. The second asks whether the current request must target /deploy or whether the corresponding conjunction slot is eTrue.

All six presentational differences have disappeared. No rewrite equates either of the two reported alternatives.

Checking the four completions

Two binary variation points produce four complete policies:

Dogwood validation rejects both request completions:

predicate `Strands::Action::"http:request"::request` mentions field
`output.status_code`, which is not declared on that event

The event schema therefore settles the first variation without a policy reviewer. Request events contain inputs but do not contain response outputs.

Both response completions validate. A replay contains a 200 response, POST /deploy, and then POST /admin/purge-all:

--- candB ---
@60 (time point 0): ALLOW
@120 (time point 1): ALLOW
--- repaired ---
@60 (time point 0): ALLOW
@120 (time point 1): DENY

The validator cannot infer whether /deploy was intended. The requirement settles that variation: retain the path guard. Combining candidate B’s event kind with candidate A’s guard produces a policy written by neither candidate:

@id("deploy_after_health_check")
permit (
    principal,
    action == Strands::Action::"http:request",
    resource
)
when { context.input.method == "POST" && context.input.path == "/deploy" }
when temporal {
    1 <= (count for (t: Timepoint). where (
        formerly within 900s (
            tp(t)
            && Strands::Action::"http:request"::response{
                 output.status_code: 200,
                 callerPrincipal:    principal
               }
        )
    ))
};

Anti-unification localizes the decisions but does not adjudicate them. Dogwood’s schema settles one decision mechanically; the original statement and replay settle the other. A mistake shared by both candidates would remain in their common skeleton, so the correlated-error limitation from Chapter 17 still applies.

A larger Dogwood policy

Five samples produce three clusters and three representative-pair queries. This chapter groups recurring alternatives across those queries so the review list grows with distinct decisions rather than with cluster pairs.

The expanded model

The fixture abstracts Chapter 20’s deploy and health-check conditions into the atoms methodPost, pathDeploy, and successfulHealth. It adds Lte, Ite, directCopy, and multipartCopy for a shared ground conditional. All five samples contain (Ite (Lte 100 100) (directCopy) (multipartCopy)). It supplies more shared structure but creates no disagreement.

The samples vary along two dimensions:

Three clusters

The complete pair grid records the partition:

;; Partition: {sampleA1, sampleA2}, {sampleB}, {sampleC1, sampleC2}.
(check-eq sampleA1 sampleA2)
(check-neq sampleA1 sampleB)
(check-neq sampleA1 sampleC1)
(check-neq sampleA1 sampleC2)
(check-neq sampleA2 sampleB)
(check-neq sampleA2 sampleC1)
(check-neq sampleA2 sampleC2)
(check-neq sampleB sampleC1)
(check-neq sampleB sampleC2)
(check-eq sampleC1 sampleC2)

Its result is

{sampleA1, sampleA2}  {sampleB}  {sampleC1, sampleC2}

The two presentation-only variants join their corresponding classes during construction. Event kind and the missing guard remain separate.

Three pairwise explanations

One representative from each cluster gives these queries:

(antiunify sampleA1 sampleB :algorithm exact)
(checkau sampleA1 sampleB :max_size 14 :algorithm exact)

(antiunify sampleA1 sampleC1 :algorithm exact)
(checkau sampleA1 sampleC1 :max_size 15 :algorithm exact)

(antiunify sampleB sampleC1 :algorithm exact)
(checkau sampleB sampleC1 :max_size 16 :algorithm exact)

The measured results are:

The identity in the second row means that cluster C omitted one conjunct. It does not mean that pathDeploy and true are equal.

Deduplicating recurring decisions

Reading each query independently would present four marker occurrences across the table. Grouping the same position and alternatives produces two review items:

Semper does not compute this aggregate table. The fixture executes all three queries, and the reader groups repeated alternative pairs by their position in the shared skeleton. Chapter 19’s speculative scope can test either resolution; this chapter only reduces the repeated outputs to the distinct decisions.

General policy conditions

The final example contains nested conditions, two Boolean connectives, and a numeric boundary. It shows one connective error represented through two identity elements, removes a domain-specific difference, and cross-checks the result under UCT.

The sentence

A cross-region replication request is permitted only if the source bucket has versioning enabled and the destination bucket lies in an approved region. If the object is tagged confidential, the destination and source accounts must be the same and server-side encryption with a customer-managed key must be in effect. Objects up to the multipart threshold are copied directly; larger objects require a multipart copy.

The self-contained fixture models one ground request. And and Or are ACI with their Boolean identities, and Eq is commutative. No other Boolean law is implicit.

The selected disagreement

formulaA follows the sentence. formulaB seeds two policy errors: it uses Or instead of And for the confidential-object requirements, and Lt instead of Lte at the multipart threshold. It also reorders conjuncts, reverses the account equality, and expands approvedRegion.

The first selected query is:

(antiunify formulaA formulaB :algorithm exact)
(checkau formulaA formulaB :max_size 42 :algorithm exact)

It prints:

(anti-unify :size 42 :cr 0.5862 :completion exact
  (Implies
    permit
    (And
      (Implies
        (taggedConfidential obj)
        (And
          (Or (Eq (accountOf dst) (accountOf src)) (Variants (Lit false) sseCmk))
          (Variants sseCmk (Lit true))))
      (Ite
        (Variants
          (Lte (sizeOf obj) multipartThreshold)
          (Lt (sizeOf obj) multipartThreshold))
        directCopy
        multipartCopy)
      (versioningOn src)
      (Variants
        (approvedRegion (regionOf dst))
        (Or (usEast1 (regionOf dst)) (euWest1 (regionOf dst)))))))

Conjunct order and equality-operand order have disappeared. Four Variants nodes describe three semantic disagreements: the connective change, the threshold comparison, and the named region predicate.

One connective error through two units

The confidential-object difference appears as

(And
  (Or (Eq (accountOf dst) (accountOf src))
      (Variants (Lit false) sseCmk))
  (Variants sseCmk (Lit true)))

Selecting both left alternatives gives (And (Or eq false) sseCmk). The Or identity reduces this to (And eq sseCmk), which is formulaA’s condition. Selecting both right alternatives gives (And (Or eq sseCmk) true). The And identity reduces that to (Or eq sseCmk), which is formulaB’s condition.

One semantic connective change therefore uses two syntactic markers. The term is optimal under Chapter 12’s objective, but “and versus or” is the clearer human description. Chapter 16 separates objective optimality from readable presentation.

Adding the domain fact

The approved-region expansion is a fact about this deployment, not an algebraic property of Or. The fixture asserts it as a rewrite and saturates:

(rewrite
  (approvedRegion r)
  (Or (usEast1 r) (euWest1 r)))
(run 3)

(antiunify formulaA formulaB :algorithm exact)
(checkau formulaA formulaB :max_size 35 :algorithm exact)

The new result is:

(anti-unify :size 35 :cr 0.4000 :completion exact
  (Implies
    permit
    (And
      (Implies
        (taggedConfidential obj)
        (And
          (Or (Eq (accountOf dst) (accountOf src)) (Variants (Lit false) sseCmk))
          (Variants sseCmk (Lit true))))
      (Ite
        (Variants
          (Lte (sizeOf obj) multipartThreshold)
          (Lt (sizeOf obj) multipartThreshold))
        directCopy
        multipartCopy)
      (versioningOn src)
      (approvedRegion (regionOf dst)))))

The domain marker is gone. Size falls from 42 to 35 and :cr from 0.5862 to 0.4000. The two samples still contain different syntax at that position, but saturation proved the terms equal. The connective and boundary questions remain.

Cross-checking under graph search

The same query under UCT uses a fixed 3,000-playout budget:

(antiunify formulaA formulaB :algorithm uct :playouts 3000)
(checkau formulaA formulaB :max_size 35 :algorithm uct :playouts 3000)

UCT returns the identical size-35 term with :cr 0.4000 and :completion exact. Agreement between the two implementations is differential evidence on this problem shape. It is not an independent proof because Exact and UCT share the action semantics defined in Chapter 14.

Limits

This chapter collects the boundaries established by the preceding chapters. Each result is relative to declared laws, asserted equations, implemented search procedures, and the evidence named below.

Saturation is a fixpoint of the selected rules

Chapter 8’s fixpoint contains what the declarations and selected rules derive. An omitted domain law remains unavailable. A passing disequality check says that the selected procedure did not derive equality; it is not a theorem of semantic inequality.

An algebraic declaration is an assertion

Chapter 4’s tags cause Semper to enforce the listed laws, but Semper does not prove that the modeled operator satisfies them. Structural declaration invariants, including equal argument and result sorts for associative operators, are checked separately.

Inverse and cancellative reasoning are narrow

Chapter 4 defines the current behavior. :inverse cancels represented inverse pairs and :cancellative contributes inference during AC completion. Pairs exposed only after later merges can require completion, and the tags do not derive double inverse, inverse distribution, or normalized signed coefficients.

Completion is opt-in and operational

Chapter 11’s eager and lazy completion can stop at a growth or alternation budget. An unchanged implemented round is an operational fixpoint, not an unconditional completeness theorem. Lazy completion serves equality checks and restores its transaction before anti-unification; Chapter 16 measures the resulting difference.

AC matching is maximum-partition matching

Chapter 5’s scalar variables bind complete stored children and their multiplicities. They do not range over implicit sub-sums or split one stored multiplicity among several scalar variables. The implemented relation is a specialization of classical AC matching, not a complete implementation of it. Chapter 5 lists what matching does and does not reach over A, C, AC, and ACI nodes, including :flatten views and the subsets a sequence filter gives up.

AU optimality has three qualifications

As Chapters 14 and 16 show, :completion exact certifies the minimum under the (size, variant_mass) objective, over the equalities in the current e-graph snapshot, and within the derivations admitted by the selected cycle policy. Changing any of those three inputs can change the result.

The production solver is not machine-verified

The au-verus crate proves objective and recurrence lemmas, not end-to-end refinement of the Rust solver. Its lemmas do not prove that the recurrence value equals the optimum. Pair-cycle erasure, AC and ACI transport, and global optimality retain prose arguments plus finite oracle and regression evidence. Chapter 16 and the AU correctness plan state the boundary.

checkau and :cr are measurements

Chapter 12 defines both fields. checkau asserts only that the result is no larger than :max_size; it does not assert an exact size. For e-classes, :cr compares against independently smallest representatives while search may select larger terms, so it can exceed one.

Agreement is not evidence of correctness

Chapter 17 explains the correlated-error case. Samples can share the same mistake, especially when one model and prompt produced all of them. Clustering then reports agreement at that position because there is no disagreement to localize.

The smallest result need not be the clearest explanation

Chapter 16 demonstrates the objective’s preference for a smaller common representation, and Chapter 22 shows one connective change through two identity elements. A presentation layer may need to regroup markers into domain-facing decisions.

Surface clustering is quadratic

Chapter 18 uses n(n - 1) / 2 equality checks because Semper has no clustering command. That grid is practical for the three-to-five-sample workflow in this book. Larger collections require host code to group e-class identifiers.

A solver’s arithmetic is its own

Semper checks every number it hands a solver against that solver’s range, but ASP and MiniZinc criteria compute inside the solver, and clasp, clingo, Chuffed, and COIN-BC were measured giving wrong optima, with no error, on values past their ranges. A cost function that overflows the solver’s number representation is the author’s responsibility; Number ranges lists each solver’s range and the solvers to use for large costs.

The application evidence is limited

The examples in Part IV are constructed cases. The repository’s formalizer pilot uses one system to produce both readings and explicitly reports an optimistic bound. It does not measure independent formalizers or population error rates.

Anti-unification does not adjudicate

Chapter 12 defines an anti-unifier as a shared skeleton with alternatives. Schema validation, tests, domain facts, or a person must decide which alternative should be enforced.

Extraction under cost models

Chapter 8 defines extraction under an additive cost: each node has a fixed price, and a term costs the sum of its nodes. This part defines extraction under a cost model, a cost written by the user that need not be additive. The commands are part of the default build; the library that implements them is the module semi_persistent_egraph::extraction.

This chapter explains what extraction under a cost model chooses and how, then covers what every cost model shares: the two commands, the line Semper prints for each extraction, the ladder of rungs, and the number ranges. Chapter 25 teaches cost scripts in Roto, Chapter 26 criteria in answer-set programming, and Chapter 27 criteria in MiniZinc. Chapter 28 covers the solvers, the number range of each, certificates, cost bands, and the files Semper writes.

Extraction as a choice

An e-graph holds many terms at once. Each class says “any one of my members”, and each node says “my operator applied to one term of each of my child classes”. Extracting a term is choosing: for the root class one member, then for each child class of that member one member, and so on down to the leaves. In this e-graph

class 0 (root): { And(c1, c2) }
class 1:        { G[0,9](c3),  F[0,9](c3) }
class 2:        { F[2,3](c4) }
class 3:        { Var "a" }
class 4:        { Var "b" }

the only decision is which member of class 1 to take, so there are two terms.

Chapter 8 makes that choice for an additive cost, a fixed price per node summed over the term, without a solver. Every other cost is solved by stating the choice as a constraint problem. Semper gives every class a Boolean “class is chosen” and every node a Boolean “node is chosen”, and adds the rules that make a set of chosen nodes a term:

• the root class is chosen;
• a chosen class chooses exactly one of its members;
• a chosen node chooses each of its child classes.

A solution of these rules is a term, and a term is one solution. A cost is then an objective over the same Booleans: “this node costs 3 when it is chosen” adds 3 times that node’s Boolean to the sum the solver minimizes. Costs that are not sums of such prices, a maximum over children or a delay along a path, are built from integers whose value follows the choice; Chapter 25 shows how a script writes them.

When the cost depends on a grouping the e-graph does not store

An :assoc-comm or :assoc-comm-idem operator (Chapter 4) stores every grouping and ordering of its operands as one flat node, and an :assoc operator stores every bracketing of its sequence as one node. That keeps saturation from enumerating them. A cost that depends on the grouping cannot be read off the flat node, so the extraction has to choose a grouping too, and return the tree it chose.

The example of this part is the memory of an R2U2 runtime monitor. R2U2 checks a specification in mission-time LTL (MLTL), a temporal logic whose operators carry an integer interval: G[l,u] p says p holds at every step from l to u steps ahead, and F[l,u] p at some step in that range. The monitor evaluates each subformula as a stream of verdicts. A subformula’s verdict for a step arrives between a best-case and a worst-case delay: an atom has 0 and 0, and F[l,u] p adds l and u to the delays of p. A conjunction needs all its operands’ verdicts for the same step, so an operand that is ready early has to keep its verdicts in a queue until its slowest sibling catches up. Its queue holds (worst delay of its slowest sibling) − (its own best delay) verdicts, plus one. Johannsen and Rozier shrink these monitors with equality saturation; see their FMCAD 2026 paper, “Shrinking Mission-time LTL Runtime Monitors with Equality Saturation”, whose specifications this book does not reproduce. The terms are MLTL formulas: atoms (Var "p"), the Boolean connectives, with And and Or declared :assoc-comm-idem, and Global, Future, Until, and Release over an (Interval l u). The rules, ported from their artifact (egraph/tests/mltl/rules/mltl.egg), produce equivalent formulas that need less memory. The one that saves the most factors a common window out of a conjunction: G[2,5] p ∧ G[3,9] q equals G[2,5] (p ∧ G[1,4] q), and its memory falls from 15 to 10, because the conjunction inside waits for less. The memory to minimize counts one slot per subformula and per group, one for the specification, and every queue; the design chapter gives the full definition.

Take p ∧ q ∧ r, where p and q are atoms and r = F[0,10] s, so r may be 10 steps late and everything else is on time. A group of operands acts as one operand whose worst delay is its slowest member’s and whose best delay is its fastest member’s:

The memory counts one slot per subformula and group as well as the queues. All three terms are the same flat node in the e-graph. The cheapest one groups the fast operands and leaves the slow one outside, which no price on the flat node can say. With the cost script of Chapter 25:

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

;; p ∧ q ∧ r with r = F[0,10] s. (let flat (And (Var “p”) (Var “q”) (Future (Interval 0 10) (Var “s”))))

(cost-model memory :script “memory.roto”) (extract flat :cost memory :rung selection) (extract flat :cost memory :rung splits)

; cost 26 proved at rung selection (2 solves, 0 cycle exclusions)
(And (Future 0 10 (Var "s")) (Var "p") (Var "q"))
; cost 17 proved at rung splits (3 solves, 0 cycle exclusions)
(And (And (Var "p") (Var "q")) (Future 0 10 (Var "s")))

How the grouping becomes part of the choice

Listing every grouping of every flat node would bring back the blow-up the flat nodes avoid: ten operands have 282,137,824 groupings. Semper instead adds a few Booleans per operand of each flat node, and rules under which each grouping is exactly one solution. In outline, every operand of a flat node gets a depth (“how many groups deep it sits”) and, at each depth, a label saying which sub-group it continues into. Operands with the same labels down to some depth are in one group there. The rules number the groups by their smallest operand, so a grouping cannot be written twice, and they forbid a group of one. For each group that may exist, the cost sees an inner node: whether it exists, its members, and its siblings. An operand repeated k times in an AC node is one operand at every rung, so the number of groupings depends only on the distinct operands.

Different costs need different amounts of this structure, and more structure is a bigger problem. :rung chooses how much to add; the next section lists the rungs.

A first extraction under a cost model

The program below has two equal terms. (Twice x) costs 3, and the rewrite gives the class a second member, (Add x x), whose two children are one shared class:

(sort E) (function V (String) E) (function F (E) E) (function Add (E E) E) (function Twice (E) E :cost 3) (rewrite (Twice x) (Add x x))

(let e (Twice (F (F (V “a”))))) (run 1)

; Additive extraction (Chapter 8): a shared child is paid at every use. (extract e) ; The same prices, with every node of the term paid once. (cost-model dag :script “24-first.roto”) (extract e :cost dag) ; The term additive extraction chooses, scored by the model. (extract e :cost dag :solver greedy)

The model dag is a Roto script. It charges every chosen node once, whatever the number of its parents:

#![allow(unused)]
fn main() {
// The term's size as a DAG: every node of the term is paid once, however many
// parents share it. `Twice` costs 3, every other operator 1.
fn cost(g: Graph) {
    for n in g.nodes() {
        if n.is("Twice") {
            n.chosen().charge_if(3);
        } else {
            n.chosen().charge_if(1);
        }
    }
}
}

Run from doc/book/examples/cost-models/, the program prints:

(Twice (F (F (V a))))
; cost 4 proved at rung selection (3 solves, 0 cycle exclusions)
(Add (F (F (V "a"))) (F (F (V "a"))))
; cost 6 greedy at rung selection
(Twice (F (F (V "a"))))

The first line is Chapter 8’s extraction. It counts the shared subterm (F (F (V "a"))) once per use, so Add costs 7 against 6 for Twice. The model pays each node of the term once. (Add x x) then costs 1 plus 3 for the shared subterm, which is 4, and the extraction proves that no term costs less. The last extraction scores the additive choice under the model: 3 for Twice plus 3, so 6.

Declaring a cost model

A cost model is named once and used by any number of extract commands:

(cost-model NAME :script "f.roto")
(cost-model NAME :asp "f.lp")
(cost-model NAME :minizinc "f.mzn")
(cost-model NAME :rust "id")

Each language works on its own view of the e-graph:

A path is relative to the working directory, not to the program file. The model is loaded when the program is checked, before any command runs. A script is compiled then, so a type error in it is a sort error of the program. An ASP or MiniZinc file is read then, and a missing file is a sort error too.

The extract command

(extract TERM :cost NAME [:rung R] [:solver S] [:budget N]
              [:file "f.json"] [:proof "dir"] [:band LO HI] [:count K])

The keywords after TERM may come in any order. :cost is required, and the others have defaults:

LO, HI, K, and N are non-negative integers. A model, a rung, and a solver must agree, and the checker rejects a disagreement before the program runs:

The five programs manual/24-check-*.egg differ only in their last line. Their messages are:

sort error at line 11 column 1: :band runs on the internal solver
sort error at line 11 column 1: :proof needs a proof-logging pseudo-Boolean solver, :solver (opb ...)
sort error at line 11 column 1: cost-model dag-asp is written in ASP: it is solved by clingo, :solver (asp "clingo")
sort error at line 11 column 1: cost-model dag-mzn is written in MiniZinc: it is solved through minizinc, :solver (minizinc "cp-sat")
sort error at line 11 column 1: cost-model dag is not written in MiniZinc: a MiniZinc solver takes (cost-model NAME :minizinc "f.mzn")

The reported cost

The first line of each extraction has the form:

; cost C STATUS at rung R (n solves, m cycle exclusions)

C is the reported cost, R the rung the problem was built at, and STATUS proved or bounded:

When no term exists, or a limit runs out before the first term, the extraction stops with an error instead: no term: Infeasible or no term: Bounded.

m counts the clauses added to exclude a cyclic solution (Chapter 28). n counts the SAT calls of the internal solver’s descent, the last one included. It is 1 for a script solved by clingo, and 0 where Semper makes no SAT call: an OPB solver, and an ASP or MiniZinc model.

The reported cost is not the solver’s objective. For a script or a Rust cost, the library evaluates the cost the script stated on the term it returns, recursive attributes included. A one-directional encoding lets a solution’s objective exceed its term’s true cost, and evaluating on the term removes the difference. For ASP and MiniZinc, Semper solves a second time with the term fixed: every choice atom or variable takes the value the term gives it. The reported cost is then the file’s definition evaluated on the term. The design chapter gives the argument.

Some lines can follow the first one, before the term:

:solver greedy prints ; cost C greedy at rung selection, whatever :rung says. It solves nothing: it takes the term Chapter 8’s additive extraction chooses and reports its cost under the model.

The ladder of rungs

:rung chooses how much of a bracketed node’s structure the cost can see. A bracketed node is an AC node (:assoc-comm, :assoc-comm-idem) or an :assoc sequence. A fold (:assoc-left, :assoc-right) has one bracketing, its prefixes or its suffixes, at every rung. Each rung represents every candidate tree exactly once:

A sequence of k operands has the little Schröder number of trees at splits (3, 11, 45 for k = 3, 4, 5) and the Catalan number at binary (2, 5, 14). An operand of multiplicity k in an AC node is one leaf with all its copies at every rung. The reconstructed term writes it once with its count, x:k, the syntax Semper reads back. A class at two positions of a sequence is two leaves.

What each rung adds:

• selection adds nothing: a flat node is costed as written, each operand’s siblings being all the other operands.
• levels gives each operand a depth. Operands at one depth form one group, and each group holds the next, so the trees are chains: And(And(p, q), r), but not And(And(a, b), And(c, d)).
• splits adds the labels that let a group split into several sub-groups: every tree.
• binary keeps the labels of splits and requires exactly two children per group.
• orders adds a position for each operand inside its group, for at most 8 operands.

A cost reads the rung through four views, and each is empty where the rung decides nothing. Every language has them:

A cost written over siblings and groups, as the monitor memory is, runs unchanged at every rung; only :rung changes. The monitor memory of the introduction, as a script (Chapter 25), at each rung:

(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) (function Future (IntervalSort MLTL) MLTL)

(let e (And (Global (Interval 0 9) (Var “a0”)) (Future (Interval 2 3) (Var “a1”)) (Global (Interval 1 4) (Var “a1”)) (Future (Interval 0 7) (Var “a0”))))

(cost-model memory :script “memory.roto”) (extract e :cost memory :rung selection) (extract e :cost memory :rung levels) (extract e :cost memory :rung splits) (extract e :cost memory :rung binary) (extract e :cost memory :rung orders) (extract e :cost memory :solver greedy)

; cost 39 proved at rung selection (2 solves, 0 cycle exclusions)
(And (Future 0 7 (Var "a0")) (Future 2 3 (Var "a1")) (Global 0 9 (Var "a0")) (Global 1 4 (Var "a1")))
; cost 37 proved at rung levels (3 solves, 0 cycle exclusions)
(And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0")) (Global 0 9 (Var "a0")))
; cost 37 proved at rung splits (3 solves, 0 cycle exclusions)
(And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0")) (Global 0 9 (Var "a0")))
; cost 40 proved at rung binary (4 solves, 0 cycle exclusions)
(And (And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0"))) (Global 0 9 (Var "a0")))
; cost 37 proved at rung orders (3 solves, 0 cycle exclusions)
(And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0")) (Global 0 9 (Var "a0")))
; cost 39 greedy at rung selection
(And (Future 0 7 (Var "a0")) (Future 2 3 (Var "a1")) (Global 0 9 (Var "a0")) (Global 1 4 (Var "a1")))

At selection the conjunction stays flat and costs 39. At levels, splits, and orders the two operands over a1 are grouped, which removes two slots of queue memory and costs 37. binary allows only two operands per group, and its best tree costs 40. The last line scores the term additive extraction chooses (:solver greedy) under the same model.

Choosing a rung

Choose the lowest rung that decides what the cost depends on:

• selection when the cost depends only on which nodes the term uses. It builds no tree variables, so it is the smallest problem.
• levels when the cost depends on how deep each operand sits, as a delay through a chain of operators does.
• splits when the cost depends on which operands are grouped, as the monitor memory does.
• binary when the target only has two-operand operators, so every group must have two members.
• orders when the order of the operands within a group also matters.

levels and splits each offer every term of the rung before them, and more, and so does orders for nodes of at most 8 operands. binary offers only binary trees: it excludes the flat node and every group of three or more operands, which is why it costs 40 above. A higher rung builds a larger problem. A rung whose estimated encoding exceeds :budget clauses (default 3,000,000) steps down the ladder and says so on standard error:

warning: rung splits estimated above the budget; extracting at selection

orders steps to splits, splits to levels, levels to selection, and binary straight to selection. The rung printed in the first line is the one used. A bracketed node with fewer than 3 operands has one tree. One with more than 16 operands (more than 8 at orders for an AC node) is kept flat at every rung. Raise :budget for an instance that needs a higher rung and fits in memory.

Number ranges

Semper’s own arithmetic on costs is exact: a value past 64 bits is held exactly, never wrapped. Two ranges decide whether a cost is computed correctly.

• The cost width, --cost-bits 32, 64, or big (the default, no cap). Under a cap, every integer of a script or Rust cost and the reported cost must lie in that signed width, and one outside it is an error naming the operation.
• The solver’s range. Semper checks every number it writes for a solver against that solver’s range and refuses one outside it with an error naming the solver.

ASP and MiniZinc criteria compute inside the solver, and Semper does not check that arithmetic. If you write cost functions that can overflow the solver’s internal number representation, you are on your own. Number ranges in Chapter 28 lists each solver’s range, as measured, and the recommended choices.

Cost functions in Roto

A :script cost model is a file in Roto, a statically typed scripting language that compiles to native code. Semper compiles the script against its own binding when the program is checked. This chapter builds scripts from a first one to the full API; every example runs from doc/book/examples/cost-models/.

Data and decisions

A script defines fn cost(g: Graph). It does not compute a number. It runs once, while the problem is built, and never sees a solution. What it reads falls in two groups, with distinct types.

• The e-graph is data. Classes, nodes, operators, children, multiplicities, and payloads are fixed before the script runs. The script reads them as String, u64, i64, bool, and lists, and may branch on them with if.
• The solver’s decisions are solver values. Which node each class takes, whether an internal node exists, and an operand’s depth are unknown to the script. It holds them as Bool and integer values, combines them, and charges under them. It cannot test them with if.

What the script builds is a formula: definitions, constraints, and one objective, the sum of its charges. The library adds the rung’s constraints, encodes the whole for the chosen solver, and evaluates the objective on the term the solver returns (The reported cost).

A first script

The script of Chapter 24 charges each chosen node once:

#![allow(unused)]
fn main() {
// The term's size as a DAG: every node of the term is paid once, however many
// parents share it. `Twice` costs 3, every other operator 1.
fn cost(g: Graph) {
    for n in g.nodes() {
        if n.is("Twice") {
            n.chosen().charge_if(3);
        } else {
            n.chosen().charge_if(1);
        }
    }
}
}

g.nodes() lists every candidate node of every class reachable from the root. n.is("Twice") reads the operator, a fact the script branches on. n.chosen() is a solver value: the condition that the node’s class is in the term and takes this node. charge_if(3) adds 3 to the objective where that condition holds. A node shared by two parents is chosen once, so it is charged once.

Reading the e-graph

A cost that depends on context reads more of the e-graph. In this model a Delay node needs a buffer of its operand, as wide as its integer payload. A class shared by several Delay parents is buffered once, over the widest window a chosen parent needs. A Hold keeps its operand without a buffer, at a price of 4:

#![allow(unused)]
fn main() {
// The window a `Delay` node needs of its operand: its integer payload.
fn window(n: Node) -> i64 {
    if n.is("Delay") {
        match n.int(0) {
            Some(w) => w,
            None => 0,
        }
    } else {
        0
    }
}

// Each class is buffered once, over the widest window a chosen parent needs of it.
// A `Hold` keeps its operand without a buffer, at a fixed price of 4.
fn cost(g: Graph) {
    for c in g.classes() {
        let uses = [];
        for u in c.parents() {
            let w = window(u.parent());
            if w > 0 {
                uses.push(g.constant(w).over().when(u.parent().chosen()));
            }
        }
        g.max_over(uses).charge();
    }
    for n in g.nodes() {
        if n.is("Hold") {
            n.chosen().charge_if(4);
        }
    }
}
}

c.parents() lists the nodes that have c as a child, each as a Use whose parent() is the node. n.int(0) is the first integer of the node’s payload, or None past the end. g.constant(w) is the integer w as a solver value, and .over() marks it as a value the cost may overstate (Polarity). .when(b) makes it a part that counts where b holds, and g.max_over(parts) is the largest part that holds, 0 when none does. charge() adds that maximum to the objective.

The program offers (Delay 5 x) and (Hold x) as equal terms, in two contexts:

(sort E) (function S (String) E) (function Delay (i64 E) E) (function Hold (E) E) (function Pair (E E) E)

; x delayed by 5 has two forms; in shared, a sibling already buffers x for 3. (union (Delay 5 (S “x”)) (Hold (S “x”))) (let shared (Pair (Delay 5 (S “x”)) (Delay 3 (S “x”)))) (let alone (Pair (Delay 5 (S “x”)) (Delay 3 (S “y”))))

(cost-model buffers :script “25-window.roto”) (extract shared :cost buffers) (extract alone :cost buffers) (cost-model no-hold :script “25-no-hold.roto”) (extract alone :cost no-hold)

; cost 5 proved at rung selection (3 solves, 0 cycle exclusions)
(Pair (Delay 5 (S "x")) (Delay 3 (S "x")))
; cost 7 proved at rung selection (2 solves, 0 cycle exclusions)
(Pair (Hold (S "x")) (Delay 3 (S "y")))
; cost 8 proved at rung selection (2 solves, 0 cycle exclusions)
(Pair (Delay 5 (S "x")) (Delay 3 (S "y")))

In shared, a sibling already buffers x for 3, so (Delay 5 x) widens the buffer by 2. The term keeps it, at a cost of 5. In alone, x has no other buffer, so (Delay 5 x) would add 5 and (Hold x) adds 4: the term costs 4 plus 3 for y. The same node is chosen in one context and not in the other, which no price per node can state.

The third model, no-hold, replaces the price of Hold by a requirement:

#![allow(unused)]
fn main() {
// The window a `Delay` node needs of its operand: its integer payload.
fn window(n: Node) -> i64 {
    if n.is("Delay") {
        match n.int(0) {
            Some(w) => w,
            None => 0,
        }
    } else {
        0
    }
}

// The buffers of 25-window.roto, with `Hold` forbidden: a requirement, not a price.
fn cost(g: Graph) {
    for c in g.classes() {
        let uses = [];
        for u in c.parents() {
            let w = window(u.parent());
            if w > 0 {
                uses.push(g.constant(w).over().when(u.parent().chosen()));
            }
        }
        g.max_over(uses).charge();
    }
    for n in g.nodes() {
        if n.is("Hold") {
            n.chosen().not().require();
        }
    }
}
}

n.chosen().not() is the condition that the node is not chosen, and require() makes it hold in every solution. The term of alone must then delay x, at 5 + 3 = 8.

Recursive attributes

A cost over the whole chosen term, such as the latency of its critical path, is a recursive attribute. g.node_values() is a table of one u64 per node, 0 where unset. g.attribute_max(offsets) defines, for each class, the chosen node’s offset plus the largest attribute among its operands, or the offset alone for a leaf:

#![allow(unused)]
fn main() {
// The latency of the term's critical path: a `Mul` takes 3 cycles, an `Add` 1,
// and an input none. A node's result is ready its latency after its latest operand.
fn latency(n: Node) -> u64 {
    if n.is("Mul") {
        3
    } else if n.is("Add") {
        1
    } else {
        0
    }
}

fn cost(g: Graph) {
    let lat = g.node_values();
    for n in g.nodes() {
        lat.set(n, latency(n));
    }
    let ready = g.attribute_max(lat);
    ready.of(g.root()).charge();
}
}

ready.of(c) is class c’s attribute, an over-estimate, and the script charges the root’s. The rewrite turns each doubling into an addition:

(sort E) (function V (String) E) (function Two () E) (function Mul (E E) E) (function Add (E E) E) (rewrite (Mul x Two) (Add x x))

(let e (Add (Mul (Mul (V “a”) Two) Two) (V “b”))) (run 2)

(cost-model latency :script “25-latency.roto”) (extract e :cost latency)

; cost 3 proved at rung selection (4 solves, 0 cycle exclusions)
(Add (Add (Add (V "a") (V "a")) (Add (V "a") (V "a"))) (V "b"))

The written term takes 3 + 3 + 1 = 7 cycles; the extracted one takes 3, one per Add. g.attribute_min(offsets) uses the smallest operand instead, and gives an under-estimate. g.attribute_max_under and g.attribute_min_over give the same attributes with the opposite polarity.

Polarity

Costs are built from order-encoded integers: a value set v0 < v1 < ... with one literal per value meaning “at least vj”. Values are signed. A solver can set some of these literals more freely than the term requires, so each integer has one of three types, which record how the encoded value relates to the value on the term.

The operations are typed so that every combination is sound:

• x.when(b) makes a part that counts where b holds. g.max_over(parts) over over-estimates is an over-estimate, and g.min_under(parts) over under-estimates is an under-estimate. g.max_under and g.min_over are their duals.
• a.minus(b) is a - b, unclamped. On an Over it accepts only an Under and gives an Over; on an Under it accepts only an Over and gives an Under. max(a - b, 0) is a.minus(b).clamp(0).
• x.neg() exchanges Over and Under.
• x.charge() accepts an Exact or an Over, never an Under.
• A threshold of an Over or Under is one-sided and has its own type. x.at_least(v) of an Over is a BoolOver, which may hold where the true value is below v. charge_if accepts a Bool or a BoolOver, and require a Bool or a BoolUnder.

Subtracting an over-estimate would let the solver report a cost below the true one. The types make that a compile error, reported when the program is checked, with the script’s line:

#![allow(unused)]
fn main() {
// Subtracts an over-estimate: the delay of a sibling taken as the wait's base.
fn cost(g: Graph) {
    let wpd = g.attribute_max(g.node_values());
    wpd.of(g.root()).minus(wpd.of(g.root())).charge();
}
}

(sort T) (function Leaf () T) (cost-model broken :script “25-polarity.roto”)

sort error at line 7 column 1: cost-model broken: Error: Type error: mismatched types
   ╭─[ 25-polarity.roto:7:28 ]
   │
 7 │     wpd.of(g.root()).minus(wpd.of(g.root())).charge();
   │                            ────────┬───────  
   │                                    ╰───────── expected `Under`, found `Over`
───╯

(The listing is the message with its colour codes removed.) The error does not depend on the branch being taken: a mistake in a rarely reached case is rejected like any other.

The MLTL monitor memory of Chapter 24 needs both polarities. A producer that finishes early waits for its latest sibling, so its queue is the latest sibling’s worst-case delay (wpd, an over-estimate) less its own best-case delay (bpd, an under-estimate):

#![allow(unused)]
fn main() {
fn cost(g: Graph) {
    let ub = g.node_values();
    let lb = g.node_values();
    for n in g.nodes() {
        ub.set(n, bound(n, 1));
        lb.set(n, bound(n, 0));
    }
    let wpd = g.attribute_max(ub);
    let bpd = g.attribute_min(lb);
    g.charge_const(1);
    for c in g.classes() {
        // Every sibling c may wait for, under every parent, where it is one.
        let peers = [];
        for u in c.parents() {
            for s in u.siblings() {
                peers.push(wpd.of(s.class()).when(s.present()));
            }
        }
        let queue = g.max_over(peers).minus(bpd.of(c)).clamp(0);
        if !first_is(c, "Bool") {
            c.chosen().charge_if(1);
            queue.charge();
        }
        // The same for every internal node a rendering of a flat node may contain.
        for n in c.nodes() {
            for t in n.inner_nodes() {
                let sibs = [];
                for s in t.siblings() {
                    sibs.push(wpd.of(s.class()).when(t.exists().and(s.present())));
                }
                let mems = [];
                for m in t.members() {
                    mems.push(bpd.of(m.class()).when(t.exists().and(m.present())));
                }
                t.exists().charge_if(1);
                g.max_over(sibs).minus(g.min_under(mems)).clamp(0).charge();
            }
        }
    }
}
}

u.siblings() lists the parent’s other operands, each with present(), the condition that the parent is chosen and, where the rung renders a tree, that the operand is in the same block. The inner loop charges the same queue for every internal node of a rendered tree (Bracketed nodes).

Bracketed nodes

At the tree rungs, a bracketed node’s tree is a decision. Two parts of the API read it:

• n.inner_nodes() lists the internal nodes a rendering of n may contain, each with exists(), members() (the operands that may lie under it), and siblings(). A fold’s internal nodes, its prefixes or suffixes, are listed at every rung, with exists() true whenever the fold is chosen. For an AC node or an :assoc sequence the list is empty at selection, so the same script runs at every rung.
• k.depth() is a child’s depth in its node’s tree, 1 directly under the node, where the rung decides the tree, and None elsewhere. k.position(d) is its position within its block at depth d, at the orders rung only, for d from 1 (the node itself) to the tree’s depth, and None for any other d.

This script charges the depth of the deepest operand of any chosen node:

#![allow(unused)]
fn main() {
// The depth of the deepest operand of any chosen node, an operand directly under
// its node at depth 1. Where the rung does not decide a node's tree, `depth()` is
// `None` and the operand is at depth 1.
fn cost(g: Graph) {
    let depths = [];
    for n in g.nodes() {
        for k in n.children() {
            match k.depth() {
                Some(d) => depths.push(d.over().when(n.chosen())),
                None => depths.push(g.constant(1).over().when(n.chosen())),
            }
        }
    }
    g.max_over(depths).charge();
}
}

(sort E) (function V (String) E) (function And (E) E :assoc-comm) (let e (And (V “a”) (V “b”) (V “c”) (V “d”)))

(cost-model depth :script “25-depth.roto”) (extract e :cost depth :rung selection) (extract e :cost depth :rung levels) (extract e :cost depth :rung binary)

; cost 1 proved at rung selection (2 solves, 0 cycle exclusions)
(And (V "a") (V "b") (V "c") (V "d"))
; cost 1 proved at rung levels (2 solves, 0 cycle exclusions)
(And (V "a") (V "b") (V "c") (V "d"))
; cost 2 proved at rung binary (3 solves, 0 cycle exclusions)
(And (And (V "a") (V "d")) (And (V "b") (V "c")))

At selection and levels the flat node keeps every operand at depth 1: a chain of blocks only deepens some of them. binary requires two operands per group, and the shallowest binary tree over four operands has depth 2. Chapter 26 and Chapter 27 state the same cost in ASP and in MiniZinc.

Pseudo-Boolean terms

A pseudo-Boolean term is a weighted sum of literals and a constant. It is linear and needs no encoding until it is compared or sorted. b.times(k) is k where b holds, g.count(bs) the number of bs that hold, g.pb_const(c) a constant, and x.linear() an integer’s linear form. t.plus(u), t.minus(u), t.times(c), and t.plus_const(k) combine terms. t.charge() adds a term to the objective with no integer built. t.at_least(k) and t.at_most(k) give its threshold literals, and t.sorted() turns it into an order-encoded integer.

Terms carry a polarity as integers do: Pb, PbOver, and PbUnder. BoolOver.times and Over.linear give a PbOver; minus takes a term of the opposite polarity; charge accepts a Pb or a PbOver.

Exact integers

Roto’s own i64 and u64 arithmetic is not checked: +, -, and * wrap silently, and / and % by zero abort the process. A cost computed with them could be wrong without an error, so Semper refuses a cost script that uses any of these operators, or their compound forms +=, -=, *=, /=, %=. The script is refused when the program is checked, before anything runs, with the operator’s line and column. A - that starts a negative literal, as in g.int([-3, 3]), is allowed, and so are comparisons, which cannot wrap:

#![allow(unused)]
fn main() {
// Roto's own `i64` arithmetic would wrap without an error, so the script is refused.
fn cost(g: Graph) {
    let k: i64 = 9223372036854775807;
    g.charge_const(k + 2);
}
}

(sort E) (function V (String) E) (let e (V “a”))

(cost-model wrapped :script “25-wrap.roto”) (extract e :cost wrapped)

sort error at line 9 column 1: cost-model wrapped: 25-wrap.roto:7:22: `+` is Roto's own arithmetic, which wraps on overflow or aborts on division by zero; cost scripts must compute with the exact methods (`plus`, `minus`, `times`, `div`, `rem`, `neg`) of IBig, UBig, and the encoded integers

All arithmetic in a cost script therefore goes through exact methods. For any value that can grow, such as a multiplicity times a weight, a sum over a large e-graph, or an interval bound, compute with IBig (signed) or UBig (unsigned) instead. Both are exact at any size, and a script may branch on their comparisons. This script charges each node 1 plus 4 per operand copy, and a fixed 10^20:

#![allow(unused)]
fn main() {
// Each chosen node costs 1 plus 4 per operand copy, computed exactly, and the
// term carries a fixed charge of 10^20, a constant past `i64`.
fn cost(g: Graph) {
    let four = g.ubig(4);
    for n in g.nodes() {
        let total = g.ubig(1);
        for k in n.children() {
            total = total.plus(k.count().times(four));
        }
        n.chosen().charge_if_big(total);
    }
    g.charge_const_big(g.ibig_str("100000000000000000000"));
}
}

(sort E) (function V (String) E) (function Plus (E) E :assoc-comm) (let e (Plus (V “a”):3000000000 (V “b”)))

(cost-model exact :script “25-exact.roto”) (extract e :cost exact)

; cost 100000000012000000007 proved at rung selection (2 solves, 0 cycle exclusions)
(Plus (V "a"):3000000000 (V "b"))

(V "a"):3000000000 is one operand with a multiplicity of 3,000,000,000. k.count() reads it as a UBig, and the cost, 10^20 + 12,000,000,007, is reported exactly. The operations:

Division by zero, a UBig result below zero, and a malformed decimal string are build errors that name the operation. A big variant takes the place of each 64-bit constant:

A 64-bit read of a value it cannot hold, such as x.values(), n.int(j), or v.get(n) on a value past i64 or u64, is an error that names the exact call to use.

Every value a script hands to the library, and every value the library computes (integers, terms, the objective, and the reported cost), is exact. A value outside the cap --cost-bits sets, if one is set, is an error. So is a value outside the range of the solver the problem goes to (Number ranges).

Costs written in Rust

(cost-model NAME :rust "id") names a cost compiled into Semper. Three are registered: mltl-memory, pipeline-registers, and monitor-history, the same costs as the scripts in egraph/tests/mltl/costs/. A Rust cost runs on the same solvers as a script and reports its cost the same way:

(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) (function Future (IntervalSort MLTL) MLTL)

(let e (And (Global (Interval 0 9) (Var “a0”)) (Future (Interval 2 3) (Var “a1”)) (Global (Interval 1 4) (Var “a1”)) (Future (Interval 0 7) (Var “a0”))))

(cost-model memory :script “memory.roto”) (cost-model memory-rs :rust “mltl-memory”) (extract e :cost memory :rung splits) (extract e :cost memory-rs :rung splits)

; cost 37 proved at rung splits (3 solves, 0 cycle exclusions)
(And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0")) (Global 0 9 (Var "a0")))
; cost 37 proved at rung splits (3 solves, 0 cycle exclusions)
(And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0")) (Global 0 9 (Var "a0")))

Another name is a sort error that lists the three.

Script API reference

Every value the API hands out belongs to the part of the e-graph reachable from the root through candidates, the members that are not subsumed.

The e-graph

n.children() is one Child per position, except for a multiset or set node, where it is one per distinct operand with its multiplicity:

is_flat() holds for a multiset or set node. is_bracketed() holds for a node whose tree the rung decides: a flat node, or an :assoc sequence.

A child whose sort is a value sort is not a child the script sees: it becomes payload of its parent. A value sort is one every node of which has only value-sort children, less the root’s sort; literal sorts are value sorts, and so is IntervalSort in the MLTL examples. Its scalars are collected depth first and left to right: an integer literal goes to ints, any other literal to strings. So (Global (Interval 0 9) p) is a node with ints [0, 9] and one child, p. A Boolean literal arrives as the string "true" or "false".

Solver values

b.require() makes b hold in every solution; g.at_most(bs, k) and g.at_least(bs, k) bound the number of bs that hold. The objective is the sum of every charge. An operation whose values leave a cap set by --cost-bits records an error, and the extraction then fails with the errors in order instead of solving. The design chapter describes how the library encodes these values.

Criteria in ASP

An :asp cost model is a file of clingo rules: a criterion, stated in answer-set programming over facts that describe the e-graph. This chapter shows how to write one, lists every predicate Semper defines, and names the pitfalls of grounding. Every example runs from doc/book/examples/cost-models/ and needs clingo on the PATH.

How Semper runs a criterion

(extract t :cost m :solver (asp "clingo")) runs four steps:

1. Semper writes the part of the e-graph reachable from t as facts, and the chosen rung as rules whose answer sets are the candidate terms.
2. It appends the criterion file and runs clingo on the whole program. Each answer set is one term, and clingo minimizes the criterion’s #minimize statements.
3. It decodes the best answer set into a term.
4. It runs clingo a second time with that term fixed, and reports the criterion’s value on it (The reported cost).

The program itself excludes cyclic terms, so no exclusion loop runs, and the first line of the output reports 0 solves and 0 cycle exclusions. An ASP model runs only with an (asp ...) solver; any other solver is a sort error.

A first criterion

The criterion of the first example of Chapter 24, in ASP:

% Every picked node is paid once: `Twice` 3, every other operator 1.
price(N,3) :- node(N,_,"Twice").
price(N,1) :- node(N,_,Op), Op != "Twice".
#minimize { P,N : pick(N), price(N,P) }.

node(N,C,Op) is a fact: node N belongs to class C and has operator Op, a string. pick(N) holds in an answer set when the term takes node N for its class. The #minimize statement pays P once for each picked node, so a node shared by two parents is paid once.

(sort E) (function V (String) E) (function F (E) E) (function Add (E E) E) (function Twice (E) E) (rewrite (Twice x) (Add x x))

(let e (Twice (F (F (V “a”))))) (run 1)

(cost-model dag :asp “26-first.lp”) (extract e :cost dag :solver (asp “clingo”))

; cost 4 proved at rung selection (0 solves, 0 cycle exclusions)
; solver objective [4] (most important first)
(Add (F (F (V "a"))) (F (F (V "a"))))

The cost is 4, as the Roto script gives. The second line lists clingo’s optimization values, one per priority, most important first; this criterion has one.

The facts Semper writes

For the program above, at the selection rung, Semper writes these facts before its rules and the criterion:

% The e-graph.
root(3).
class(0).
first(0,3).
node(3,0,"V").
kind(3,plain).
str(3,0,"a").
class(1).
first(1,0).
node(0,1,"F").
kind(0,plain).
kid(0,0,0).
operand(0,0). mult(0,0,1).
leaf(0,0,0).
class(2).
first(2,4).
node(4,2,"F").
kind(4,plain).
kid(4,0,1).
operand(4,1). mult(4,1,1).
leaf(4,0,1).
class(3).
first(3,1).
node(1,3,"Add").
kind(1,plain).
kid(1,0,2).
kid(1,1,2).
operand(1,2). mult(1,2,2).
leaf(1,0,2).
node(2,3,"Twice").
kind(2,plain).
kid(2,0,2).
operand(2,2). mult(2,2,1).
leaf(2,0,2).

Classes and nodes keep the numbers of Semper’s extraction graph, which are stable from run to run but not consecutive within a class. Class 3 has two candidates: node 1, Add, and node 2, Twice. Add has two positional children, both class 2, so kid lists both positions, while operand and leaf list the class once, with mult(1,2,2). The predicates, for the reachable classes and their candidates:

The payload follows the rule of the Roto binding: a child of a value sort, such as an interval, becomes integers and strings of its parent (Script API reference). So (Global (Interval 0 9) p) has int(N,0,0) and int(N,1,9).

The choice atoms

The rules make each candidate term one answer set. A criterion reads its atoms:

Tree atoms exist only for picked nodes. bmem(N,root,P) and depth(N,P,D) hold for every leaf of every picked node, at every rung. inner holds only for a bracketed node with 3 to 16 leaves (8 at orders for an AC node) at a tree rung, and for a fold at every rung, whose blocks are its prefixes or suffixes.

A block is blk(I,J) for a sequence or fold, the leaves at positions I to J. For an AC node it is blk(R,S), a block of size S whose least leaf is R; bmem says which other leaves it holds. For an AC node of four operands at binary, the facts include:

cand(1,blk(0,2)). least(1,blk(0,2),0). size(1,blk(0,2),2).

Names a criterion must not define

The facts and rules above also define ac, arity, binary, cand, chains, child, closer, closerb, fixed, least, meet, ok, ordered, out, size, span, sub, and taken. The second solve, with the term fixed, adds free, held_inner, held_bmem, and held_pos. A criterion must not define any of these, nor any predicate of the two tables above. Clingo accepts a rule that adds atoms to one of them without a warning, and the answer sets may then no longer be the candidate terms. Use names of your own for every derived predicate.

Trees

The depth cost of Chapter 25, the depth of the deepest leaf of any picked node, reads depth/3:

% The depth of the deepest leaf of any picked node, a leaf directly under its node
% at depth 1.
deepest(D) :- D = #max { X,N,P : pick(N), depth(N,P,X) ; 0 }.
#minimize { D : deepest(D) }.

The ; 0 element makes the maximum 0 when no leaf exists.

(sort E) (function V (String) E) (function And (E) E :assoc-comm) (let e (And (V “a”) (V “b”) (V “c”) (V “d”)))

(cost-model depth :asp “26-depth.lp”) (extract e :cost depth :rung selection :solver (asp “clingo”)) (extract e :cost depth :rung levels :solver (asp “clingo”)) (extract e :cost depth :rung binary :solver (asp “clingo”))

; cost 1 proved at rung selection (0 solves, 0 cycle exclusions)
; solver objective [1] (most important first)
(And (V "a") (V "b") (V "c") (V "d"))
; cost 1 proved at rung levels (0 solves, 0 cycle exclusions)
; solver objective [1] (most important first)
(And (V "a") (V "b") (V "c") (V "d"))
; cost 2 proved at rung binary (0 solves, 0 cycle exclusions)
; solver objective [2] (most important first)
(And (And (V "a") (V "b")) (And (V "c") (V "d")))

The costs are those of the Roto script: 1, 1, and 2.

Several objectives

A file may state several #minimize statements at different priorities; a higher priority is more important. This criterion counts the classes of the term first, and among the terms with the fewest, the Add nodes:

% First the number of classes in the term; among terms with the fewest, the number
% of `Add` nodes. A higher priority is more important.
#minimize { 1@2,C : used(C) }.
#minimize { 1@1,N : pick(N), node(N,_,"Add") }.

(sort E) (function V (String) E) (function F (E) E) (function Add (E E) E) (function Twice (E) E) (rewrite (Twice x) (Add x x))

(let e (Twice (F (F (V “a”))))) (run 1)

(cost-model classes-then-adds :asp “26-priorities.lp”) (extract e :cost classes-then-adds :solver (asp “clingo”))

; cost 4 proved at rung selection (0 solves, 0 cycle exclusions)
; solver objective [4, 0] (most important first)
(Twice (F (F (V "a"))))

Both terms use 4 classes, and the second priority prefers Twice, with no Add. The extraction prints ; solver objective [v1, v2, ...] (most important first), clingo’s values in priority order. The reported cost is the first value, here 4. A file with no #minimize statement reports 0.

Grounding

Clingo grounds the program, instantiating every rule over every value, before it chooses anything. Three habits keep grounding finite and small.

• Bound every recursive attribute. A rule such as wpd(C,O+M) :- pick(N), ..., M = #max { A,K : operand(N,K), wpd(K,A) } grounds without end around a cycle of the e-graph, which no term can take. On an acyclic term the value is at most the sum of the offsets. State that bound, utop(S) :- S = #sum { V,N : ub(N,V) }., and add utop(S), O+M <= S to the rule.
• Aggregate first, subtract after. An aggregate over siblings in a rule that also binds the class’s own value is grounded once per value of the class’s own value. Take the maximum in its own rule, latest(C,X) :- ..., X = #max { A : sibw(C,A) }., and subtract in the next: queue(C,X-B) :- bpd(C,B), latest(C,X), X > B.
• Derive a default from facts only. lat(N,0) :- node(N,_,_), not haslat(N). with haslat(N) :- lat(N,_). has no stable model. Test the explicit facts instead, as has_operand(N) :- operand(N,_). does below.

The MLTL monitor memory follows all three:

temporal("Global"). temporal("Future"). temporal("Until"). temporal("Release").
bounded(N) :- node(N,_,Op), temporal(Op), int(N,0,_), int(N,1,_).
lb(N,(V+|V|)/2) :- bounded(N), int(N,0,V).
ub(N,(V+|V|)/2) :- bounded(N), int(N,1,V).
lb(N,0) :- node(N,_,_), not bounded(N).
ub(N,0) :- node(N,_,_), not bounded(N).
has_operand(N) :- operand(N,_).

% Worst- and best-case propagation delays over the chosen term. On an acyclic term
% each is at most the sum of its offsets; the bounds keep grounding finite where the
% e-graph has a cycle, which no term can take.
utop(S) :- S = #sum { V,N : ub(N,V) }.
ltop(S) :- S = #sum { V,N : lb(N,V) }.
wpd(C,O+M) :- pick(N), node(N,C,_), ub(N,O), has_operand(N), M = #max { A,K : operand(N,K), wpd(K,A) }, utop(S), O+M <= S.
wpd(C,O)   :- pick(N), node(N,C,_), ub(N,O), not has_operand(N).
bpd(C,O+M) :- pick(N), node(N,C,_), lb(N,O), has_operand(N), M = #min { A,K : operand(N,K), bpd(K,A) }, ltop(S), O+M <= S.
bpd(C,O)   :- pick(N), node(N,C,_), lb(N,O), not has_operand(N).

counted(C) :- used(C), first(C,N), node(N,_,Op), Op != "Bool".
sibw(C,A) :- pick(N), leaf(N,P,C), parent(N,leaf(P),G), bmem(N,G,Q), Q != P, leaf(N,Q,S), wpd(S,A).
% (The latest sibling is taken first and subtracted after, so the aggregate is not
% grounded once per value of the class's own delay.)
latest(C,X) :- counted(C), X = #max { A : sibw(C,A) }.
queue(C,X-B) :- counted(C), bpd(C,B), latest(C,X), X > B.

own(N,B,M) :- inner(N,B), M = #min { A,Q : bmem(N,B,Q), leaf(N,Q,S), bpd(S,A) }.
blatest(N,B,X) :- inner(N,B), parent(N,B,G), X = #max { A,Q : bmem(N,G,Q), not bmem(N,B,Q), leaf(N,Q,S), wpd(S,A) }.
iqueue(N,B,X-M) :- own(N,B,M), blatest(N,B,X), X > M.

#minimize { 1,spec : #true ; 1,cls,C : counted(C) ; W,queue,C : queue(C,W) ; 1,inner,N,B : inner(N,B) ; W,iqueue,N,B : iqueue(N,B,W) }.

(V+|V|)/2 is max(V, 0). The criterion charges 1 for the specification, 1 per counted class, each class’s queue, and the same for each internal node of a rendered tree.

(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) (function Future (IntervalSort MLTL) MLTL)

(let e (And (Global (Interval 0 9) (Var “a0”)) (Future (Interval 2 3) (Var “a1”)) (Global (Interval 1 4) (Var “a1”)) (Future (Interval 0 7) (Var “a0”))))

(cost-model memory :asp “memory.lp”) (extract e :cost memory :rung selection :solver (asp “clingo”)) (extract e :cost memory :rung splits :solver (asp “clingo”))

; cost 39 proved at rung selection (0 solves, 0 cycle exclusions)
; solver objective [39] (most important first)
(And (Future 0 7 (Var "a0")) (Future 2 3 (Var "a1")) (Global 0 9 (Var "a0")) (Global 1 4 (Var "a1")))
; cost 37 proved at rung splits (0 solves, 0 cycle exclusions)
; solver objective [37] (most important first)
(And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0")) (Global 0 9 (Var "a0")))

The costs, 39 at selection and 37 at splits, are those of the Roto script in Chapter 24.

Solver options and inspection

(asp "PROG" "ARG" ...) runs PROG with --outf=2 --quiet=1, then the given arguments, then the path of the program. PROG is clingo, or any solver that prints clingo’s JSON output. Semper sets no time limit; pass clingo’s own, as (asp "clingo" "--time-limit=60"). When clingo stops before it proves its optimum, the status is bounded.

EXTRACT_API_KEEP_LP=dir keeps every program clingo is given in dir, as call000.lp, call001.lp, and so on: two per extraction, the search and the solve with the term fixed. The directory must exist, and the numbering continues from the number of files already in it. The kept program is the way to see the facts of a larger e-graph.

Every integer Semper writes into the facts, a payload integer or a multiplicity, must be one of clingo’s 32-bit integers, and one outside is refused before clingo runs (Number ranges). The values the criterion computes, such as a #sum, are clingo’s arithmetic. Semper does not check them. If you write cost functions that can overflow the solver’s internal number representation, you are on your own.

egraph/tests/mltl/costs/ holds the three MLTL costs in ASP. The lp.rs source holds the rules Semper writes.

Criteria in MiniZinc

A :minizinc cost model is a MiniZinc file: a criterion over arrays and variables that describe the e-graph. This chapter shows how to write one, lists every name Semper defines, and compares the solvers. Every example runs from doc/book/examples/cost-models/ and needs minizinc on the PATH.

How Semper runs a criterion

(extract t :cost m :solver (minizinc "cp-sat")) runs four steps:

1. Semper numbers the classes reachable from t 1..C and their candidates 1..N. It writes the e-graph as data, and the chosen rung as variables and constraints whose solutions are the candidate terms.
2. It appends the criterion file and runs MiniZinc with the named solver. Integers stay integer variables: nothing is order-encoded before the solver sees them.
3. It decodes the last solution into a term.
4. It solves a second time with that term fixed, and reports the objective on it (The reported cost).

Every auxiliary variable is determined by the term, so each term is one solution. The model itself excludes cyclic terms through rank, so the first line of the output reports 0 solves and 0 cycle exclusions. A MiniZinc model runs only with a (minizinc ...) solver, and a (minizinc ...) solver only with a MiniZinc model; any other pairing is a sort error.

A first criterion

The criterion of the first example of Chapter 24, in MiniZinc:

% Every picked node is paid once: `Twice` 3, every other operator 1.
array[1..N] of int: price = [if op[n] = "Twice" then 3 else 1 endif | n in 1..N];
var int: cost = sum(n in 1..N)(price[n] * bool2int(pick[n]));
solve minimize cost;

op[n] is node n’s operator, a string, and pick[n] is the variable that is true when the term takes node n for its class. The file declares its own names, here price and cost, and ends with one solve minimize item.

(sort E) (function V (String) E) (function F (E) E) (function Add (E E) E) (function Twice (E) E) (rewrite (Twice x) (Add x x))

(let e (Twice (F (F (V “a”))))) (run 1)

(cost-model dag :minizinc “27-first.mzn”) (extract e :cost dag :solver (minizinc “cp-sat”))

; cost 4 proved at rung selection (0 solves, 0 cycle exclusions)
; solver lower bound 4
(Add (F (F (V "a"))) (F (F (V "a"))))

The cost is 4, as in Roto and in ASP. The second line is the solver’s lower bound on the objective. On a run stopped by a time limit, the bound tells how far the reported term can be from the optimum.

The data Semper writes

For the program above, at the selection rung, Semper writes this data before its variables, its constraints, and the criterion:

% The e-graph.
int: C = 4;
int: N = 5;
int: B = 0;
int: MAXK = 2;
int: MAXL = 1;
int: MAXJ = 1;
int: ROOT = 4;
int: PLAIN = 0; int: COMM = 1; int: SEQ = 2; int: SEQ_LEFT = 3; int: SEQ_RIGHT = 4; int: MSET = 5; int: SET = 6;
array[1..C] of int: class_id = [0, 1, 2, 3];
array[1..N] of int: node_id = [3, 0, 4, 1, 2];
array[1..N] of 1..C: cls = [1, 2, 3, 4, 4];
array[1..N] of string: op = ["V", "F", "F", "Add", "Twice"];
array[1..N] of int: kind = [0, 0, 0, 0, 0];
array[1..N] of set of 1..C: kids = [{}, {1}, {2}, {3}, {3}];
array[1..N] of int: nkid = [0, 1, 1, 2, 1];
array[1..N, 1..MAXK] of 0..C: kid = [| 0, 0 | 1, 0 | 2, 0 | 3, 3 | 3, 0 |];
array[1..N, 1..MAXK] of int: kmult = [| 0, 0 | 1, 0 | 1, 0 | 1, 1 | 1, 0 |];
function int: mult(int: n, int: k) = sum(i in 1..nkid[n])(if kid[n, i] = k then kmult[n, i] else 0 endif);
array[1..N] of int: nint = [0, 0, 0, 0, 0];
array[1..N, 1..MAXJ] of int: ints = [| 0 | 0 | 0 | 0 | 0 |];
array[1..C] of 1..N: first = [1, 2, 3, 4];
array[1..N] of int: nleaf = [0, 1, 1, 1, 1];
array[1..N, 1..MAXL] of 0..C: leaf = [| 0 | 1 | 2 | 3 | 3 |];
% 0 no tree, 1 chains, 2 trees, 3 binary trees, 4 ordered trees, 5 a fold.
array[1..N] of int: family = [0, 0, 0, 0, 0];
array[1..B] of 1..N: bnode = [];
array[1..B] of bool: interval = [];
array[1..B] of int: blo = [];
array[1..B] of int: bhi = [];

Node 4, Add, has two children, both class 3: kid and kmult list both positions, and kids holds the class once. The names, with n a node, c a class, and b a block:

The payload is integers only: unlike the ASP facts’ str, no string payload is written.

The variables

Blocks exist only for a bracketed node with 3 to 16 leaves (8 at orders for an AC node) at a tree rung, and for a fold at every rung. depth[n, p] is defined for every node n and every p in 1..MAXL; it is 1 for every leaf of a node with no blocks.

Names a criterion must not redefine

The dump also defines the function children and the predicates meet and within. A criterion must not redefine them, nor declare any name of the two tables above; MiniZinc then stops with an error, such as an ambiguous call for a second meet. A parameter-only predicate that an int function uses is declared with test, not predicate, as bounded is in A larger criterion.

Trees

The depth cost of Chapter 25 in MiniZinc:

% The depth of the deepest leaf of any picked node, a leaf directly under its node
% at depth 1.
var 0..MAXL: deepest;
constraint forall(n in 1..N, p in 1..nleaf[n])(pick[n] -> deepest >= depth[n, p]);
solve minimize deepest;

(sort E) (function V (String) E) (function And (E) E :assoc-comm) (let e (And (V “a”) (V “b”) (V “c”) (V “d”)))

(cost-model depth :minizinc “27-depth.mzn”) (extract e :cost depth :rung selection :solver (minizinc “cp-sat”)) (extract e :cost depth :rung levels :solver (minizinc “cp-sat”)) (extract e :cost depth :rung binary :solver (minizinc “cp-sat”))

; cost 1 proved at rung selection (0 solves, 0 cycle exclusions)
; solver lower bound 1
(And (V "a") (V "b") (V "c") (V "d"))
; cost 1 proved at rung levels (0 solves, 0 cycle exclusions)
; solver lower bound 1
(And (V "a") (V "b") (V "c") (V "d"))
; cost 2 proved at rung binary (0 solves, 0 cycle exclusions)
; solver lower bound 2
(And (And (V "a") (V "c")) (And (V "b") (V "d")))

The costs are 1, 1, and 2, as in Roto and in ASP. At binary the term differs: CP-SAT returns (And (And a c) (And b d)), where the internal solver and clingo return (And (And a b) (And c d)). Both cost 2. Among terms of equal cost, each solver returns the one it finds, and the reported cost is the same.

A larger criterion

The MLTL monitor memory in MiniZinc:

test bounded(int: n) = (op[n] = "Global" \/ op[n] = "Future" \/ op[n] = "Until" \/ op[n] = "Release") /\ nint[n] >= 2;
function int: lb(int: n) = if bounded(n) then max(ints[n, 1], 0) else 0 endif;
function int: ub(int: n) = if bounded(n) then max(ints[n, 2], 0) else 0 endif;
int: TOP = sum(n in 1..N)(ub(n) + lb(n));

% Worst- and best-case propagation delays over the chosen term.
array[1..C] of var 0..TOP: wpd;
array[1..C] of var 0..TOP: bpd;
constraint forall(n in 1..N)(pick[n] -> wpd[cls[n]] = ub(n) + max([0] ++ [wpd[k] | k in kids[n]]));
constraint forall(n in 1..N)(pick[n] -> bpd[cls[n]] = lb(n) + if card(kids[n]) = 0 then 0 else min([bpd[k] | k in kids[n]]) endif);

predicate counted(int: c) = used[c] /\ op[first[c]] != "Bool";
predicate sibling(int: n, int: p, int: q) =
    parent_leaf[n, p] = 0 \/ exists(b in 1..B where bnode[b] = n)(parent_leaf[n, p] = b /\ bmem[b, q]);

array[1..C] of var 0..TOP: queue;
constraint forall(n in 1..N, p, q in 1..nleaf[n] where p != q)(
    (pick[n] /\ sibling(n, p, q) /\ op[first[leaf[n, p]]] != "Bool") -> queue[leaf[n, p]] >= wpd[leaf[n, q]] - bpd[leaf[n, p]]);

% An internal node's queue: its latest outside sibling less its earliest member.
array[1..B] of var 0..TOP: own;
constraint forall(b in 1..B)(own[b] = min([TOP] ++ [if bmem[b, p] then bpd[leaf[bnode[b], p]] else TOP endif | p in 1..nleaf[bnode[b]]]));
array[1..B] of var 0..TOP: iqueue;
constraint forall(b in 1..B, q in 1..nleaf[bnode[b]])(
    (inner[b] /\ not bmem[b, q] /\ (parent_blk[b] = 0 \/ exists(b2 in 1..B where bnode[b2] = bnode[b])(parent_blk[b] = b2 /\ bmem[b2, q])))
    -> iqueue[b] >= wpd[leaf[bnode[b], q]] - own[b]);

var int: cost = 1 + sum(c in 1..C)(bool2int(counted(c))) + sum(c in 1..C)(queue[c])
    + sum(b in 1..B)(bool2int(inner[b])) + sum(b in 1..B)(iqueue[b]);
solve minimize cost;

Each attribute is an array of variables with an explicit domain, 0..TOP, where TOP bounds every delay of an acyclic term. A constraint under pick[n] -> ... defines a node’s value only where the term takes it.

(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) (function Future (IntervalSort MLTL) MLTL)

(let e (And (Global (Interval 0 9) (Var “a0”)) (Future (Interval 2 3) (Var “a1”)) (Global (Interval 1 4) (Var “a1”)) (Future (Interval 0 7) (Var “a0”))))

(cost-model memory :minizinc “memory.mzn”) (extract e :cost memory :rung selection :solver (minizinc “cp-sat”)) (extract e :cost memory :rung splits :solver (minizinc “cp-sat”))

; cost 39 proved at rung selection (0 solves, 0 cycle exclusions)
; solver lower bound 39
(And (Future 0 7 (Var "a0")) (Future 2 3 (Var "a1")) (Global 0 9 (Var "a0")) (Global 1 4 (Var "a1")))
; cost 37 proved at rung splits (0 solves, 0 cycle exclusions)
; solver lower bound 37
(And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0")) (Global 0 9 (Var "a0")))

Choosing a solver

(minizinc "SOLVER" "ARG" ...) runs minizinc --solver SOLVER ARG ... --output-mode json --output-objective -s -i FILE. SOLVER is any name minizinc --solvers lists, such as cp-sat, chuffed, gecode, highs, or coin-bc. Semper sets no time limit; pass MiniZinc’s own, in milliseconds, as an argument:

(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) (function Future (IntervalSort MLTL) MLTL)

(let e (And (Global (Interval 0 9) (Var “a0”)) (Future (Interval 2 3) (Var “a1”)) (Global (Interval 1 4) (Var “a1”)) (Future (Interval 0 7) (Var “a0”))))

(cost-model memory :minizinc “memory.mzn”) (extract e :cost memory :rung splits :solver (minizinc “chuffed”)) (extract e :cost memory :rung splits :solver (minizinc “gecode”)) (extract e :cost memory :rung splits :solver (minizinc “highs”)) (extract e :cost memory :rung splits :solver (minizinc “coin-bc”)) ; A time limit in milliseconds, passed to minizinc after the solver’s name. (extract e :cost memory :rung splits :solver (minizinc “cp-sat” “–time-limit” “60000”))

; cost 37 proved at rung splits (0 solves, 0 cycle exclusions)
(And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0")) (Global 0 9 (Var "a0")))
; cost 37 proved at rung splits (0 solves, 0 cycle exclusions)
(And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0")) (Global 0 9 (Var "a0")))
; cost 37 proved at rung splits (0 solves, 0 cycle exclusions)
; solver lower bound 37
(And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0")) (Global 0 9 (Var "a0")))
; cost 37 proved at rung splits (0 solves, 0 cycle exclusions)
; solver lower bound 37
(And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0")) (Global 0 9 (Var "a0")))
; cost 37 proved at rung splits (0 solves, 0 cycle exclusions)
; solver lower bound 37
(And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0")) (Global 0 9 (Var "a0")))

Every solver proves 37 at splits. HiGHS, COIN-BC, and CP-SAT report a lower bound; Chuffed and Gecode do not, and print no bound line. When a solve stops before it proves its optimum, the status is bounded, and the bound, when printed, limits the distance to the optimum.

Each solver reads integers in its own range, and Semper checks the integers it writes, the payload and the multiplicities, against the range of the named solver: 32 bits for Chuffed and Gecode, exact to 2^53 for the MIP solvers, 64 bits for CP-SAT and any other. The values the criterion computes are the solver’s arithmetic, which Semper does not check. If you write cost functions that can overflow the solver’s internal number representation, you are on your own. CP-SAT, whose 64-bit range the MiniZinc compiler also checks, is the recommended solver for criteria whose values can grow (Number ranges).

EXTRACT_API_KEEP_MZN=dir keeps every model MiniZinc is given in dir, as call000.mzn, call001.mzn, and so on: two per extraction. The directory must exist. egraph/tests/mltl/costs/ holds the three MLTL costs in MiniZinc. The mzn.rs source holds the constraints Semper writes.

Solvers, certificates, and export

This chapter covers what surrounds an extraction: the solvers and their limits, the number range of each solver, certificates, listing the terms of a cost band, and the two JSON files Semper writes. It ends with the alternatives considered and the limits. Examples run from doc/book/examples/cost-models/; those in its manual/ directory need RoundingSat or end in an error, so the book test does not run them.

Solvers

:solver chooses how the problem is solved. The default is internal.

Cycles in the e-graph are excluded by Semper for every solver. An ASP model with a solver other than asp, a MiniZinc model with a solver other than minizinc, and a minizinc solver with any other model are sort errors naming the model (The extract command).

The internal solvers on the ladder program’s problem:

(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) (function Future (IntervalSort MLTL) MLTL)

(let e (And (Global (Interval 0 9) (Var “a0”)) (Future (Interval 2 3) (Var “a1”)) (Global (Interval 1 4) (Var “a1”)) (Future (Interval 0 7) (Var “a0”))))

(cost-model memory :script “memory.roto”) (extract e :cost memory :rung splits :solver internal) (extract e :cost memory :rung splits :solver dpw) (extract e :cost memory :solver greedy)

; cost 37 proved at rung splits (3 solves, 0 cycle exclusions)
(And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0")) (Global 0 9 (Var "a0")))
; cost 37 proved at rung splits (3 solves, 0 cycle exclusions)
(And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0")) (Global 0 9 (Var "a0")))
; cost 39 greedy at rung selection
(And (Future 0 7 (Var "a0")) (Future 2 3 (Var "a1")) (Global 0 9 (Var "a0")) (Global 1 4 (Var "a1")))

dpw sums its weights in 64 bits. An objective whose weights total more is refused with an error that names internal and roundingsat, which are exact.

roundingsat is looked up as $ROUNDINGSAT, then ~/.local/bin/roundingsat, then on the PATH, and run with --print-sol=1 --verbosity=0. (opb "prog" ...) runs prog with the given arguments and the OPB file’s path appended. The program must print competition output: s OPTIMUM FOUND or s UNSATISFIABLE, and v lines.

A script also runs on clingo, as its formula written as ASP:

(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) (function Future (IntervalSort MLTL) MLTL)

(let e (And (Global (Interval 0 9) (Var “a0”)) (Future (Interval 2 3) (Var “a1”)) (Global (Interval 1 4) (Var “a1”)) (Future (Interval 0 7) (Var “a0”))))

(cost-model memory :script “memory.roto”) (extract e :cost memory :rung splits :solver (asp “clingo”))

; cost 37 proved at rung splits (1 solves, 0 cycle exclusions)
(And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0")) (Global 0 9 (Var "a0")))

This backend is slower. On 64 of the MLTL specifications of Johannsen and Rozier (FMCAD 2026), clingo took 15 times longer than the internal solver on the median instance. That measurement was recorded by a tool since removed from the repository, and the current tree does not reproduce it.

Limits on a solve

A limit that runs out after a term was found gives the status bounded. One that runs out before gives the error no term: Bounded.

Keeping the solver’s input

Each variable names an existing directory, in which Semper keeps a copy of every file it gives a solver, numbered call000, call001, and so on:

Number ranges

Semper’s own arithmetic on costs is exact: a script’s IBig and UBig, a Rust cost’s integers, the terms, the objective, the totalizer that bounds it, and the reported cost. Two ranges then decide whether a cost is computed correctly. The first is an optional cap, which Semper enforces. The second is the range of the solver, which Semper enforces on every number it writes for that solver.

The cost width. --cost-bits big (the default) sets no cap. --cost-bits 32 or 64 caps every integer of a script or Rust cost, and the reported cost of any model, at that signed width. A value outside the cap is an error naming the operation, never a wrapped value. This script charges 2^63:

#![allow(unused)]
fn main() {
// 2^62 doubled is 2^63, one past the largest signed 64-bit integer.
fn cost(g: Graph) {
    g.constant(4611686018427387904).scale(2).charge();
}
}

(sort E) (function V (String) E) (let e (V “a”))

(cost-model big :script “28-cost-bits.roto”) (extract e :cost big)

Run from manual/ with no flag, it prints:

; cost 9223372036854775808 proved at rung selection (1 solves, 0 cycle exclusions)
(V "a")

With --cost-bits 64, it stops with:

error: check failed: extract :cost: the cost script's build failed: scale: the value 9223372036854775808 is outside the 64-bit cost range (--cost-bits)

A Roto literal is still 64-bit, because Roto has no larger integer type. A larger constant is written as g.ibig_str("…") (Exact integers).

The solver’s range. Each solver reads integers in its own representation, and several read a value past it wrongly without reporting anything. Before a solver runs, Semper checks every number it writes for that solver against the solver’s range, and refuses one outside it with an error naming the solver. The numbers checked are the coefficients, bounds, and weights of an OPB file or an ASP program, and the integers and multiplicities of the ASP and MiniZinc dumps. A weight of 3,000,000,000 is exact on the internal solver and refused for clingo:

#![allow(unused)]
fn main() {
// A weight of 3,000,000,000: exact for Semper, past clingo's 32-bit integers.
fn cost(g: Graph) {
    g.root().chosen().charge_if(3000000000);
}
}

(sort E) (function V (String) E) (let e (V “a”))

(cost-model heavy :script “28-solver-range.roto”) (extract e :cost heavy) (extract e :cost heavy :solver (asp “clingo”))

; cost 3000000000 proved at rung selection (2 solves, 0 cycle exclusions)
(V "a")
error: check failed: extract :cost: the cost script's build failed: an objective weight 3000000000 is outside clingo's 32-bit integers

A payload integer past clingo’s range, under an ASP model, is refused the same way, and the message says what Semper does not check:

(sort E) (function Num (i64) E) (let e (Num 3000000000))

(cost-model size :asp “../26-first.lp”) (extract e :cost size :solver (asp “clingo”))

error: check failed: extract :cost: the integer of node 0 (Num) 3000000000 is outside clingo's 32-bit integers. Semper checks the numbers it writes for the solver; an overflow inside your ASP or MiniZinc criteria is not checked, and is yours to rule out

What Semper does not check. ASP and MiniZinc criteria compute inside the solver. A criteria file that computes a value its solver cannot represent, such as a #sum past 2^31 in clingo, a product past 2^31 in Chuffed, or a sum past 2^53 in a MIP solver, can give a wrong optimum, and nothing reports it. If you write cost functions that can overflow the solver’s internal number representation, you are on your own. Keep the values your criteria compute inside the range of the solver you run them on, or choose a solver whose range holds them.

What each solver does with a number past its range, measured on 2026-10-06 with the inputs in egraph/tests/data/solver_width/ (the README names the solver versions):

Semper recognizes an OPB solver by its program name: one containing roundingsat is unbounded, one containing clasp or clingo is 32-bit. A MiniZinc solver named chuffed or gecode is 32-bit; coin, cbc, highs, scip, gurobi, cplex, xpress, or mip is exact to 2^53; any other is 64-bit.

Recommended. For costs that can grow large, state the cost in Rust or as a script using IBig and UBig, and solve on internal or roundingsat, the two solvers that take numbers of any size. For MiniZinc criteria use cp-sat, whose 64-bit range the MiniZinc compiler also checks. Use clasp, clingo, Chuffed, Gecode, and the MIP solvers only when every value the criteria compute stays inside their range.

Certificates

:proof "dir" runs a proof-logging pseudo-Boolean solver with --proof-log, RoundingSat’s flag, and keeps each call’s instance and proof in dir, as call000.opb and call000.pbp, and so on. It prints the claim of the final call and the command that checks it. :proof needs :solver roundingsat or (opb ...):

(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) (function Future (IntervalSort MLTL) MLTL)

(let e (And (Global (Interval 0 9) (Var “a0”)) (Future (Interval 2 3) (Var “a1”)) (Global (Interval 1 4) (Var “a1”)) (Future (Interval 0 7) (Var “a0”))))

(cost-model memory :script “../memory.roto”) (extract e :cost memory :solver roundingsat :proof “proofs”) (extract e :cost memory :rung splits :solver (opb “roundingsat” “–print-sol=1”) :proof “proofs-splits”)

; cost 39 proved at rung selection (0 solves, 0 cycle exclusions)
; certificate Bounds { lower: 38 }: veripb proofs/call000.opb proofs/call000.pbp
(And (Future 0 7 (Var "a0")) (Future 2 3 (Var "a1")) (Global 0 9 (Var "a0")) (Global 1 4 (Var "a1")))
; cost 37 proved at rung splits (0 solves, 0 cycle exclusions)
; certificate Bounds { lower: 36 }: veripb proofs-splits/call000.opb proofs-splits/call000.pbp
(And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0")) (Global 0 9 (Var "a0")))

VeriPB checks the first certificate:

Running VeriPB version 3.0.2
Info: Switched to proof version 2.0 (it is recommended to migrate to proof version 3.0).
s VERIFIED BOUNDS 38 <= obj <= 38

The bound is on the objective in the OPB file, which leaves out the cost’s constant part (here the specification wrapper’s 1): the certified cost is 39, the selection optimum, and 37 at splits. The claim is Bounds { lower: L } when the final call found an optimum, and Unsat { below: ... } when it refuted a cheaper term. The certificate covers the solver’s reasoning on the final instance: no model has a lower objective. That every acyclic term has a model whose objective is its cost is a property of the encodings, established by Semper’s tests rather than by the certificate.

Listing terms in a cost band

:band lo hi lists the terms whose cost lies in [lo, hi], at most :count n of them (default 10), instead of the cheapest one. Both bounds are added to the objective before solving, and each term found is excluded by its rung literals, so no term in the band is lost and none is listed twice. A band runs on the internal solver, with a script or Rust model; any other :solver is a sort error. The second command below asks for splits under a budget of 10 clauses, which steps down:

(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) (function Future (IntervalSort MLTL) MLTL)

(let e (And (Global (Interval 0 9) (Var “a0”)) (Future (Interval 2 3) (Var “a1”)) (Global (Interval 1 4) (Var “a1”)) (Future (Interval 0 7) (Var “a0”))))

(cost-model memory :script “memory.roto”) ; Every term whose cost lies in [37, 40], at most 4 of them. (extract e :cost memory :rung splits :band 37 40 :count 4) ; A budget of 10 clauses is below the splits encoding: the rung steps down. (extract e :cost memory :rung splits :budget 10)

; 4 terms with cost in [37, 40] at rung splits
; cost 37 in band at rung splits
(And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0")) (Global 0 9 (Var "a0")))
; cost 39 in band at rung splits
(And (Future 0 7 (Var "a0")) (Future 2 3 (Var "a1")) (Global 0 9 (Var "a0")) (Global 1 4 (Var "a1")))
; cost 40 in band at rung splits
(And (And (And (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Future 0 7 (Var "a0"))) (Global 0 9 (Var "a0")))
; cost 40 in band at rung splits
(And (And (Future 0 7 (Var "a0")) (Future 2 3 (Var "a1")) (Global 1 4 (Var "a1"))) (Global 0 9 (Var "a0")))
; cost 39 proved at rung selection (2 solves, 0 cycle exclusions)
(And (Future 0 7 (Var "a0")) (Future 2 3 (Var "a1")) (Global 0 9 (Var "a0")) (Global 1 4 (Var "a1")))

The terms come by increasing cost, then by their text, each with its cost; the order the solver finds them in depends on its version and platform. Standard error carries warning: rung splits estimated above the budget; extracting at selection. With the optimum proved, a band gives equivalent terms at a known gap above it: benchmarks with known answers, variants for differential testing, and pairs of suboptimal and optimal terms.

Writing the term

:file "f.json" writes the extracted term as JSON. It has one entry per class of the term, named c and the class’s number in the extraction graph, with its operator, its children’s entries, and its payload. A multiset node also carries "mults", each child’s count, parallel to "children": a child of multiplicity k is listed once. Under :band, each term goes to f.json.0.json, f.json.1.json, and so on.

(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 e (And (Global (Interval 0 9) (Var “a0”)) (Global (Interval 1 4) (Var “a1”)))) (cost-model memory :script “memory.roto”) (extract e :cost memory :file “28-file.json”)

(sort E) (function V (String) E) (function Plus (E) E :assoc-comm) (let p (Plus (V “a”):2 (V “b”))) (cost-model dag :script “24-first.roto”) (extract p :cost dag :file “28-file-mults.json”)

; cost 18 proved at rung selection (2 solves, 0 cycle exclusions)
(And (Global 0 9 (Var "a0")) (Global 1 4 (Var "a1")))
; cost 3 proved at rung selection (2 solves, 0 cycle exclusions)
(Plus (V "a"):2 (V "b"))

The first file, 28-file.json:

{
  "nodes": {
    "c0": {
      "children": [
        "c3"
      ],
      "ints": [
        1,
        4
      ],
      "op": "Global",
      "strings": []
    },
    "c1": {
      "children": [
        "c4"
      ],
      "ints": [
        0,
        9
      ],
      "op": "Global",
      "strings": []
    },
    "c2": {
      "children": [
        "c0",
        "c1"
      ],
      "ints": [],
      "op": "And",
      "strings": []
    },
    "c3": {
      "children": [],
      "ints": [],
      "op": "Var",
      "strings": [
        "a1"
      ]
    },
    "c4": {
      "children": [],
      "ints": [],
      "op": "Var",
      "strings": [
        "a0"
      ]
    }
  },
  "root": "c2"
}

The second, 28-file-mults.json, with the count of (V "a"):

{
  "nodes": {
    "c4": {
      "children": [],
      "ints": [],
      "op": "V",
      "strings": [
        "b"
      ]
    },
    "c6": {
      "children": [],
      "ints": [],
      "op": "V",
      "strings": [
        "a"
      ]
    },
    "c7": {
      "children": [
        "c4",
        "c6"
      ],
      "ints": [],
      "mults": [
        1,
        2
      ],
      "op": "Plus",
      "strings": []
    }
  },
  "root": "c7"
}

The exported e-graph

(dump-egraph t :file "f.json") writes the whole e-graph, marking t’s class as the root, for a tool that extracts outside Semper. The format is egglog’s --to-json, plus a colour per class and the kind of each operator:

(sort E) (function a () E) (function b () E) (function F (E) E) (function Plus (E) E :assoc-comm) (let p (Plus (F a) (F a) b)) (dump-egraph p :file “28-dump-egraph.json”)

{
 "nodes": {
  "n0e3163c6ae86c6765650b5b783c0b759-E": {"op": "Plus", "children": ["n0f1448134acd95981b3931e16014521c-E", "nd5ec398aba3e06fa32d7228d5a59cd00-E"], "mults": [2, 1], "eclass": "E-823989c50677dc443bbb3b68e0b57913", "cost": 1, "subsumed": false},
  "n0f1448134acd95981b3931e16014521c-E": {"op": "F", "children": ["n986a608e2ec286cfc5a691e55b30a36f-E"], "eclass": "E-4d6895f531715b14080654f7417251f5", "cost": 1, "subsumed": false},
  "n986a608e2ec286cfc5a691e55b30a36f-E": {"op": "a", "children": [], "eclass": "E-4c4de7d182b2ab841f1155f98333ff02", "cost": 1, "subsumed": false},
  "nd5ec398aba3e06fa32d7228d5a59cd00-E": {"op": "b", "children": [], "eclass": "E-4e661d73fc43b09769cade26489d3916", "cost": 1, "subsumed": false}
 },
 "class_data": {
  "E-4c4de7d182b2ab841f1155f98333ff02": {"type": "E", "colour": "4c4de7d182b2ab841f1155f98333ff02"},
  "E-4d6895f531715b14080654f7417251f5": {"type": "E", "colour": "4d6895f531715b14080654f7417251f5"},
  "E-4e661d73fc43b09769cade26489d3916": {"type": "E", "colour": "4e661d73fc43b09769cade26489d3916"},
  "E-823989c50677dc443bbb3b68e0b57913": {"type": "E", "colour": "823989c50677dc443bbb3b68e0b57913"}
 },
 "op_kinds": {
  "F": "plain",
  "Plus": "ac",
  "a": "plain",
  "b": "plain"
 },
 "root_eclasses": ["E-823989c50677dc443bbb3b68e0b57913"]
}

Every name is a content colour: a hash of the class’s structure, computed by refining over the classes until the partition stops changing. A class is {sort}-{colour} and a node n{colour}-{sort}. Nodes and classes are written in name order, and an AC, ACI, or commutative node’s children in name order too. Two runs that build the same e-graph therefore write the same bytes, whatever node ids they allocated: on the 1,172 MLTL specifications Johannsen and Rozier publish with their FMCAD 2026 paper (Chapter 24), naive and semi-naive saturation write identical dumps. A child entry names one member of the child class, the one whose name sorts first; a consumer reads that member’s eclass. A multiset child of multiplicity k is written once, with k in "mults", parallel to "children", as F under Plus above (count 2). A congruent duplicate node is omitted. op_kinds (plain, comm, a, ac, aci, or lit) tells a consumer which operators’ child order carries no meaning. The design chapter on extraction defines the colouring.

Alternatives considered

• Choosing the nodes, then the grouping. An earlier extractor proved the optimum of the flat cost, with every AC node flat, and then chose each node’s grouping. Sequencing the two is not optimal: on 600 instances of the monitor memory problem it is above the joint optimum on 130 (21.7%), by up to 31% (egraph/tests/ex_paper_claims.rs). The loss comes from the choice among flat optima: the best grouping over every flat optimum reaches the joint optimum on all 600. The splits rung chooses both in one encoding.
• A separate extractor over the dump. That extractor read the exported JSON and took its candidates in the order of the dump’s node names, which were node ids. Its result then depended on the order rules were applied in: naive and semi-naive saturation built the same e-graph on all of those 1,172 specifications, and their extracted terms differed on 50. Extraction now runs inside Semper, and the dump’s names are content colours.
• Breaking ties by a second objective. Making equal-cost terms distinct by a lexicographic second cost changes every benchmark’s encoding and optimality proof, and a rank sum is not a total order on terms. Ties are instead resolved by content: the export orders by colour, and the greedy extractor breaks a cost tie by term height and then by node colour.

The design chapter records the others.

Limits

• A script has no resource bound: it can loop, exhaust memory, or overflow the stack, since Roto compiles to native code without an instruction count.
• Costs are exact, within the cap --cost-bits sets if any, and within the range of the solver they are exported to; what ASP and MiniZinc criteria compute inside the solver is the solver’s arithmetic (Number ranges).
• Roto’s own i64/u64 operators wrap and its division by zero aborts, so a cost script that uses +, -, *, /, or % is refused when the program is checked; scripts compute with the exact methods of IBig, UBig, and the encoded integers (Exact integers).
• Deciding the binary grouping of a flat node with ten or more operands can take CaDiCaL an hour or more.
• A recursive attribute keeps every value it can take per class. A cap can be set through the Rust API (Build::set_attribute_cap); reaching it is an error, never a smaller domain.
• Script, criteria, :file, and :proof paths are relative to the working directory, not to the program file.
• Clingo and MiniZinc run with no time limit from Semper unless the solver’s own arguments set one.

Annex A. Complete surface-language grammar

This annex collects the complete surface grammar in one place. The grammar describes source forms; the chapters that introduce each form define its behavior.

Braces mean zero or more repetitions, brackets mark an optional item, and | separates alternatives. Quoted words and punctuation are literal tokens. Whitespace and comments may appear between tokens unless a production states otherwise.

alphabetic       = any alphabetic character
alphanumeric     = any alphabetic character or decimal digit
digit            = "0" | "1" | "2" | "3" | "4"
                 | "5" | "6" | "7" | "8" | "9"

identifier       = identifier-start { identifier-rest }
identifier-start = alphabetic | "_"
identifier-rest  = alphanumeric | "_"

symbol           = "<<" | ">>" | "<=" | ">=" | "!=" | "==" | "=>"
                 | "+" | "-" | "*" | "/" | "%" | "<" | ">"
                 | "&" | "|" | "^" | "~"

operator         = identifier
                 | identifier "::" ( identifier | symbol )
                 | symbol

comment          = ";" { any character except newline } [ newline ]

unsigned-integer = digit { digit }
integer          = [ "-" ] unsigned-integer
rational         = integer "/" integer
exponent         = ( "e" | "E" ) [ "+" | "-" ] unsigned-integer
floating-point   = [ "-" ] unsigned-integer
                   ( "." { digit } [ exponent ] | exponent )
boolean          = "true" | "false"
quote            = character U+0022
backslash        = character U+005C
string           = quote { string-character | escape } quote
string-character = any character except quote and backslash
escape           = backslash any character
literal          = rational | floating-point | integer | boolean | string


program          = { command }

command          = declaration
                 | rule-command
                 | term-command
                 | control-command
                 | query-command


declaration      = sort-declaration
                 | operator-declaration
                 | datatype-declaration

sort-declaration = "(" "sort" identifier ")"

operator-declaration
                 = "(" ( "function" | "constructor" ) identifier
                   "(" { identifier } ")" identifier
                   { declaration-tag } ")"

datatype-declaration
                 = "(" "datatype" identifier { variant } ")"

variant          = "(" identifier { identifier }
                   { declaration-tag } ")"

declaration-tag  = algebraic-tag | extraction-tag

algebraic-tag    = ":assoc"
                 | ":comm"
                 | ":assoc-comm"
                 | ":assoc-comm-idem"
                 | ":assoc-left"
                 | ":assoc-right"
                 | ":idempotent"
                 | ":nilpotent" [ unsigned-integer ]
                 | ":identity" term
                 | ":cancellative"
                 | ":inverse" identifier

extraction-tag   = ":cost" unsigned-integer
                 | ":unextractable"


term             = literal
                 | identifier
                 | "(" operator { term-child } ")"

term-child       = term [ ":" unsigned-integer ]


pattern          = literal
                 | identifier
                 | "(" "=" pattern pattern ")"
                 | "(" operator [ rest ] { pattern-item } [ rest ] ")"

pattern-item     = pattern-child
                 | rest
                 | sequence-filter

pattern-child    = pattern [ ":" multiplicity-spec ]
rest             = ".." identifier

sequence-filter  = "(" ".." identifier [ ":" multiplicity-spec ]
                   pattern [ ":except" identifier ] ")"

multiplicity-spec
                 = unsigned-integer
                 | identifier [ comparison unsigned-integer ]

comparison       = ">=" | "<=" | "==" | "!=" | ">" | "<"


rhs              = literal
                 | identifier
                 | "(" operator { rhs-child } ")"

rhs-child        = rhs [ ":" multiplicity-expression ]
                 | splice

splice           = ".." identifier
                 | set-comprehension
                 | multiset-comprehension
                 | sequence-comprehension
                 | row-comprehension

set-comprehension
                 = ".." "{" rhs "for" identifier "in" identifier
                   [ filter ] "}"

multiset-comprehension
                 = ".." "{" rhs ":" multiplicity-expression
                   "for" identifier ":" identifier "in" identifier
                   [ filter ] "}"

sequence-comprehension
                 = ".." "[" rhs "for" identifier "in" identifier
                   [ filter ] "]"

row-comprehension
                 = ".." ( "{" | "[" ) rhs [ ":" multiplicity-expression ]
                   "for" binders "in" source [ filter ] ( "}" | "]" )

binders          = binder
                 | "(" binder { binder } ")"

binder           = identifier [ ":" ( identifier | "_" ) ]

source           = identifier
                 | rhs

filter           = "if" rhs

multiplicity-expression
                 = unsigned-integer
                 | identifier
                 | "(" multiplicity-operator
                   multiplicity-expression multiplicity-expression ")"

multiplicity-operator
                 = "u64::+" | "u64::-" | "u64::*" | "u64::/"
                 | "u64::%" | "u64::min" | "u64::max"


rule-command     = ruleset-declaration
                 | rewrite
                 | birewrite
                 | rule

ruleset-declaration
                 = "(" "ruleset" identifier ")"

rewrite          = "(" "rewrite" pattern rhs { rewrite-tag } ")"
                 | "(" "rewrite" pattern rhs { sequence-rewrite-tag } ")"

birewrite        = "(" "birewrite" pattern pattern
                   { birewrite-tag } ")"

rule             = "(" "rule"
                   "(" { pattern } ")"
                   "(" { action } ")"
                   { ruleset-tag | ":flatten" } ")"

rewrite-tag      = when-clause | ":subsume" | ":flatten" | ruleset-tag
sequence-rewrite-tag
                 = sequence-when-clause | let-clause | ":flatten"
                 | ruleset-tag
birewrite-tag    = when-clause | ":flatten" | ruleset-tag
when-clause      = ":when" "(" { pattern } ")"
sequence-when-clause
                 = ":when" "(" { rhs } ")"
let-clause       = ":let" "(" { "(" identifier rhs ")" } ")"
ruleset-tag      = ":ruleset" identifier

action           = "(" "union" rhs rhs ")"
                 | "(" "set" "(" identifier { rhs } ")" rhs ")"
                 | "(" operator { insert-child } ")"

insert-child     = rhs | splice


term-command     = "(" "let" identifier term ")"
                 | "(" "union" term term ")"
                 | "(" identifier { term } ")"


control-command  = run
                 | push
                 | pop

run              = "(" "run" [ identifier ] unsigned-integer
                   [ until-clause ] ")"

until-clause     = ":until"
                   "(" ( "=" | "!=" ) term term ")"

push             = "(" "push" [ ":shrink" ] ")"
pop              = "(" "pop" ")"


query-command    = check
                 | extract
                 | cost-model
                 | dump-egraph
                 | print-size
                 | print-stats
                 | antiunify
                 | checkau

check            = "(" "check" check-body ")"

check-body       = term
                 | "(" "=" term term ")"
                 | "(" "!=" term term ")"

extract          = "(" "extract" term { extract-option } ")"

extract-option   = ":cost" cost-name
                 | ":rung" ( "selection" | "levels" | "splits"
                           | "binary" | "orders" )
                 | ":budget" unsigned-integer
                 | ":solver" ( "internal" | "dpw" | "roundingsat" | "greedy"
                             | "(" ( "opb" | "asp" | "minizinc" )
                               string { string } ")" )
                 | ":file" string
                 | ":proof" string
                 | ":band" unsigned-integer unsigned-integer
                 | ":count" unsigned-integer

cost-model       = "(" "cost-model" cost-name
                   ( ":script" | ":rust" | ":asp" | ":minizinc" ) string ")"

cost-name        = identifier-start { identifier-rest | "-" }

dump-egraph      = "(" "dump-egraph" term ":file" string ")"

print-size       = "(" "print-size" [ operator ] ")"

print-stats      = "(" "print-stats"
                   [ ":file" string ] ")"

antiunify        = "(" "antiunify" term term
                   { antiunify-option } ")"

checkau          = "(" "checkau" term term
                   { checkau-option } ")"

antiunify-option = ":playouts" unsigned-integer
                 | ":algorithm" ( "exact" | "uct" )
                 | ":cycles" cycle-mode

checkau-option   = antiunify-option
                 | ":max_size" unsigned-integer

cycle-mode       = "sides" | "sides-current" | "pair"

The symbol tokens are lexical. No predeclared primitive is named << or >>, so Semper has no shift operators.

Restrictions checked after parsing

The grammar gives the shape of each form. Name resolution and sortchecking add constraints that depend on earlier declarations and therefore cannot be expressed in the productions above.

• Declarations are processed in source order. Sorts, operators, rulesets, and names introduced by let must exist before a command refers to them.
• A bare top-level application is an insertion. Its head must be a declared operator name that is not one of the command keywords. Its direct children carry no counts.
• A term-child count is written with no space before the colon. It is at least 1 and is accepted only on the children of an :assoc, :assoc-comm, or :assoc-comm-idem application.
• Pattern rest variables are legal only on variadic operators. An ordinary pattern permits a prefix rest, a suffix rest, or both, on any variadic operator. A sequence rewrite (below) permits any number of bare sequences between children under :assoc, and at most one under AC or ACI.
• Multiplicity specifications in patterns apply only to AC multiset elements; sequence and set pattern elements do not carry them. An RHS multiplicity expression may annotate a child of an AC or associative application: under :assoc the child is repeated. An ACI operator stores a set, so a count on its child is rejected in a ground term, a pattern, and a right-hand side.
• (= p q) is the reserved root-binding pattern. In a pattern, a primitive expression is accepted only as a predicate guard rooted at a top-level conjunct in a rule body or :when clause, and the guard must return bool.
• A splice or comprehension must consume a rest variable of the corresponding sequence, set, or multiset kind. A right-hand-side name must be bound on the left-hand side, introduced by its comprehension, or refer to an earlier let binding.
• birewrite rejects :subsume, multiplicity annotations, and sequence patterns on either side. A rule accepts :ruleset, but not :when or :subsume; guard patterns go directly in its body.
• Declaration tag combinations, operator arities, term sorts, and literal spellings are validated during sortchecking. Available literals depend on the selected literal model.
• A sequence rewrite is a rewrite whose root pattern has a sequence filter or a bare sequence between children. It takes sequence-rewrite-tags; an ordinary rewrite takes rewrite-tags. Its root operator is :assoc, :assoc-comm, or :assoc-comm-idem; under :comm it is rejected, since two simple patterns already match both orders. Filters appear at the root only: a filter inside a filter, and a filter or bare sequence outside the left-hand side of a rewrite, are rejected. A multiplicity on a filter is accepted under AC, and under ACI only if 1 satisfies it. :except is accepted under AC and ACI only. It names another filter of the same pattern, and a cycle of :except is rejected. Every variable of a filter’s pattern names a sequence; where a scalar is expected, a sequence is rejected unless it is under a reduction (min, max, sum, count), a sequence primitive (zip, concat, union-by, narrow, narrowed), a splice, or a comprehension. A comprehension binding k names needs a source of k columns, and a column of a multiset sequence is bound as x:k or x:_. :let is accepted on sequence rewrites. :subsume is not. A multiplicity expression in a sequence rewrite uses +, -, *, min, or max, with or without the u64:: prefix.
• extract with options needs :cost, naming an earlier cost-model. The rung defaults to selection and the solver to internal. A cost-model with :script compiles the Roto script when the program is checked, so an error in the script, a polarity error included, rejects the program. An :asp model needs an asp solver. A :minizinc model needs a minizinc solver, and a minizinc solver needs a :minizinc model. :band needs the internal solver, and :count defaults to 10. :proof needs an opb or roundingsat solver. Part V defines these options.
• A :nilpotent order is between 2 and 255. Values for :cost and checkau :max_size must fit in an unsigned 32-bit integer. Run limits, playout counts, and parsed multiplicities use unsigned 64-bit integers.

Annex B. Command reference

This annex is a compact index of Semper’s commands. Follow the chapter links for semantics and Annex A for the complete grammar.

Symbol declarations and algebraic properties

Algebraic properties are attached to operator declarations and individual datatype variants as tags. They determine an operator’s representation and required arity. Chapter 4 gives their laws, legal combinations, and exact arity rules. Chapter 3 defines the extraction tags. Annex A contains the complete declaration grammar.

Building terms

A bare operator application at top level is an insertion command. A name introduced by let denotes the resulting e-class and may be used wherever a ground term is accepted. Chapter 3 explains term construction in detail.

Rules

Modifiers may appear in any order. birewrite rejects :subsume, and so does a sequence rewrite. A general rule puts guards in its query list and accepts only :flatten and :ruleset as trailing modifiers.

General-rule actions

Chapter 5 defines pattern matching, multiplicities, rest variables, comprehensions, modifiers, and action ordering.

Running rules and scopes

A run selects exactly one ruleset. Chapter 8 defines round ordering, stopping, and statistics. Chapter 7 defines scope lifetime and :shrink.

Checks, extraction, and statistics

Chapter 8 defines extraction and statistics. Chapter 11 explains how the completion mode affects equality and disequality checks.

Anti-unification

Chapter 12 defines the result and size bound. Chapters 14 and 15 define the algorithms, cycle modes, and playout budget.

Annex C. Flag reference

The command-line form is:

semi-persistent [OPTIONS] <FILE>

FILE is the required path to one Semper program.

Representation and literal model

The machine group provides i64, u64, f64, usize, String, and bool; the bignum group provides IBig, UBig, RBig, and bool.

Saturation and completion

Chapters 9 and 11 define the evaluation and completion modes.

Matching and union policies

The parser does not enforce the three “relevant with” conditions: the value is accepted and has no effect. | --union-by | rank, size, uses, sum | rank | Choose the surviving representative by union-find rank, class size, use-list length, or size plus uses. |

These policies change operational work and representative choice, not the equalities asserted by the input program.

Help

An unknown flag or an invalid value exits with status 2 and a usage line.

Test directives

The test harness in egraph/tests/egg_tests.rs reads directives from the first eight lines of a program. Each directive mirrors a flag; pass the flag when running the file by hand.

The harness runs every file under both the static and the runtime atom-scheduling modes, with the 32-bit preset and without proof recording.

Feature-gated diagnostics

Two environment variables affect binaries built with optional instrumentation features; they are not command-line flags:

Without the corresponding Cargo feature, setting the environment variable has no effect.