Cgraph
FGL counterexample generator graph
A counterexample generation graph (cgraph) is akin to a bipartite directed
graph. That is, there are two types of nodes, and edges only go between
opposite node types. The first type of node is an object node, which
is some FGL symbolic object for which we want to derive a concrete value. The
other type of node is divided into two subtypes: formula nodes and equivalence
nodes. Both subtypes signify relations betwee object nodes.
- Object nodes are each associated with some FGL symbolic object. At
the start of counterexample generation, we have an assignment of values to
certain objects (those associated with Boolean variables in the Boolean
variable database), and we want to get an assignment of values to other
objects (namely, the top level variables of the theorem).
- Formula nodes each offer a formula for deciding on a value of (or,
sometimes, updating the value of) some particular object (its target). Each
formula node has exactly one in-edge, coming from its target object node. It
may have several out-edges, pointing to objects (dependencies) whose derived
values could be used in the formula to help compute the target object's
value.
- Equivalence nodes each describe a potential equivalence between
object nodes. An equivalence node has one in-edge (from one of the two
potentially equivalent objects), an out-edge to the equivalence term (an object
signifying the equivalence itself, which if assigned the value T means the two
equivalent objects are the same), and another out-edge to the other potentially
equivalent object; there will be another corresponding equivalence node with
the edges between the two potentially equivalent objects reversed.
The representation of the graph is a map from FGL objects (target object
nodes) to lists of formula nodes and equivalence nodes to which it has
out-edges. Each formula node and equivalence node contains the objects to
which it has out-edges, as well as other info about the formula.
Deriving Object Values from a Cgraph
To derive a value for an object given a counterexample generation graph, we
traverse the graph depth-first starting at that object. We check the following
two "short-circuit" cases:
- If the object corresponds to a Boolean variable from the database, the
counterexample assignment from SAT determines its value.
- If the object is variable-free (has no :g-var sub-objects) and its
value can be computed, that determines its value.
If neither of these two cases holds, we proceed to look at the object's
equivalence nodes. For each equivalence node, we recursively try to determine a
value for the equivalence object. If this is successful and the value is true,
then we collect the equivalent object into a set with the original object, add
its formula nodes to the original object's formula nodes, and continue to
explore both the original object's equivalences and the equivalent
object's. When done, this results in an equivalence class of objects and a set
of formula edges. However, it is also possible that some equivalent object
satisfies one of the short-circuit cases: if this is found to be true, then all
the equivalent objects are assigned that value.
If no short-circuit case was found, then we try each formula node collected
from the equivalence classes. For each formula, we recursively try to derive
the values for each of its dependencies (objects connected by object edges from
the formula node). After visiting all these edges (successfully determining
values for the objects or not), the formula node computes some results:
- a decision of whether the formula was computed successfully or not, based
on the success/failure and values of the dependencies
- if successful, the computed value for the object
- if successful, a priority value to compare to other potential formula nodes
for the object.
If the formula was successful, then the equivalence class of objects has a
candidate value, but other formulas may also offer their own values. These may
even use the value computed from other formulas. The priority values produced
by successful formulas decide which one wins.
Building a Cgraph
A cgraph is generated via rules that trigger on object nodes that are added
to the graph. If a new object node matches such a rule, the rule adds a new
formula node for some object (which may also be new, potentially triggering
more rules). The object edges of the new formula again potentially add new
objects and trigger more rules.
Kinds of Cgraph Rules/Formulas
- Elim rules say how to compute the value of some aggregate/product once we
have computed values for their fields. Typically, an elim rule is triggered by
an object that is a field accessor call -- say (field1 (foo x)). It
provides a value for the argument to the accessor (here (foo x)) and it
has object edges to all of the accessors. Once we have derived the values for
all the accessor calls (or failed at some of them), the formula says how to
construct the object, perhaps giving default values for any accessors for which
we've failed to derive a value. The appearance of other accessor calls of the
same target object doesn't add new formula nodes; elim rules create one formula
node per target.
- Property rules contribute updates to some object such as an alist or
map. Like elim rules, they are typically triggered by a call of a lookup of
some sort, e.g. (assoc key (foo x)). This will add a formula node
targeting (foo x) and depending on (assoc key (foo x)) and
key. The formula describes how to update the target based on the value of
the lookup and the key; e.g., (cons (cons key lookup) target). It is
expected that several property rule formula nodes may update their mutual
target, and it shouldn't matter the order in which the updates happen.
- Fixup rules create formulas that are supposed to run after all non-fixup
formulas for the target object, and fix up the existing value of the object to
meet some desired condition.
- Implicitly, for any object that is a function call, that object's value can
be computed by computing values for the arguments of the call and then applying
the function to those arguments. This method should usually have lower priority
than other formulas, if there are any: typically, we are trying to compute
values for "small" terms (variables) starting with values for "large"
terms (Boolean variable database entries), and this sort of rule goes the other
way--trying to derive the value of a larger term from its smaller
components.
These behaviors can be generally expressed with a few rule parameters:
- Match conditions -- what objects induce the application of the rule to
update the graph. Typical rules trigger on one or more term patterns with
leading function symbols, and match if a new object node unifies with the
pattern.
- Target object -- typically formulated in terms of the matching object's
unifying substitution
- Dependencies -- often overlap with matching triggers but may include others
- Order -- e.g., fixup formulae should run last, equivalence formulas should
run first
- Value formula
- Success formula
- Priority formula
These last formulas can use various variables in them: the values and
success flags of the dependencies, and the the previous value, success flag,
and priority of the target. These are initialized and updated according to
these rules:
- If the formula's success flag is NIL, then there are no updates to the
target success, priority, and value. The rest of these rules assume that the
formula succeeded.
- The target success flag is initially NIL and is updated to T when a formula
succeeds.
- The target priority is updated to the formula priority if the target
success flag was NIL or if the formula priority was greater than the target
priority.
- The target value is updated to the formula value if the target success flag
was NIL or if the formula priority was greater than the target priority.
- If the target success flag was T, the target priority equals the formula
priority, and the formula value differs from the target value, then a
conflicting assignment warning is stored.
Subtopics
- Cgraph-p
- Recognizer for cgraph.
- Ctrex-rule
- Internal structure of a counterexample generation rule
- Cgraph-fix
- (cgraph-fix x) is an ACL2::fty alist fixing function that follows the drop-keys strategy.
- Cgraph-equiv
- Basic equivalence relation for cgraph structures.
