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.