Typically, when executing traversals, we only need to know whether a traversal succeeded or failed. For this purpose, it’s sufficient to check whether the traversal evaluates to a non-nil result in order to infer success.
But there are cases when you may need to modulate the computation being performed as part of the traversal. For instance, the “leap” feature in Symex computes a delta of each position in relation to the initial position, as it traverses, and stops traversing when the delta reaches 0 in both x (horizontal position along branch) and y (height from root) directions.
The remainder of this section explains how computations work, so that you can write similar traversals that may need to perform custom computations.
Symex executes traversals while evaluating an associated “fold”-like computation. By default, that computation simply assembles a sequence of the moves made during traversal evaluation, producing this full list as the result.
The computation is specified in terms of a “perceiving” operation that represents the underlying move (every traversal is ultimately composed of elementary moves) in a way that is relevant for the computation, and a “synthesizing” operation that combines the accumulated result with the new perceived input.
Traversals may be evaluated with arbitrary computations that are specified in this way. The in-progress result is always available to traversals as an argument, so that they may condition on this in-progress result (as “leap” does, stopping when a condition on the result is met).
For example, the following computation simply counts the number of moves made during traversal evaluation:
(defvar my-symex-compute-moves
(symex-make-computation :perceive (lambda (_x) 1)
:synthesize #'+)
It may be used as follows:
(symex-eval (symex-traversal
(circuit (move forward)))
my-symex-compute-moves)
This counts the number of moves made in traversing forward to the end of the containing expression.
Note that traversals sometimes return “zero” moves, that is, (move 0 0), to indicate an intentional absence of movement, as opposed to nil which indicates a failed traversal, so this computed result may return more moves than the actual number of steps taken. It is just an example of a simple computation, though, perhaps, not a very useful one.