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.