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.