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.