Major Section: ACL2 Documentation
Debugging forward-chaining rules can be hard because their effects are not directly visible on the goal. In this documentation we tell you how to get reports on the forward chaining activity occurring in your proof attempts. This documentation is written in several parts. The first part is an introduction for the first-time user of forward chaining reports. The next two parts describe how to read reports. The last part describes how to monitor forward chaining activity only for selected runes, etc. We recommend the new user of these reports read everything!
A Quick Introduction to Forward Chaining Reports
Caution: The reporting mechanism maintains some state and if you have already used forward chaining reporting in a session the directions below may not work as advertised! To return to the default forward chaining reporting state, execute this form at the top level:
You can get a report about all forward chaining activity in subsequent proofs by doing:
(set-fc-criteria t)Options will be discussed later that allow you to monitor the activity caused by particular
:forward-chainingrules or terms.
Then do a proof that is expected to cause some forward chaining. In the proof output you will see lines like this:
(Forward Chaining on behalf of PREPROCESS-CLAUSE: (FC-Report 1))This is the only difference you should see in the proof output.
After the proof attempt has terminated, you can execute:
(fc-report k)for any
kprinted during the immediately preceding proof attempt. That will print a much longer report describing the activity that occurred during the
kth use of forward chaining in that proof attempt.
If you want to see these reports in real time (embedded in the proof output), do this before invoking the prover:
Collecting the data used to generate these reports slows down the prover. If you no longer wish to see such reports, do
How To Read FC Reports
The report printed by
(fc-report k) is of the form:
Forward Chaining Report k: Caller: token Clause: (lit1 lit2 ... litn) Number of Rounds: m Contradictionp: bool Activations: (act1 act2 ...)
This report means that the kth use of forward chaining in the most
recent proof attempt was done on behalf of token (see below). The
initial context (set of assumptions) consisted of the negations of the
literals listed in the clause shown and the initial candidate trigger terms
are all those appearing in that clause. This invocation of forward chaining
proceeded to do m rounds of successive extensions of the initial context
and ultimately either reached a contradiction (bool =
T) or returned
an extended context (bool =
NIL). Note that reaching a
contradiction from the negations of all the literals in a clause is ``good''
because it means the clause is true. The report concludes with the final
status of all the forward chaining rules fired during the process. We
explain how to read one of these activation reports in the next section.
Forward chaining is done on behalf of many proof techniques in the system.
Each is associated with a token. The main proof technique that uses
forward chaining is
SIMPLIFY-CLAUSE. This is the call of forward
chaining that sets up the context used by the rewriter to relieve hypotheses
during backchaining. Another common caller of forward chaining is
PREPROCESS-CLAUSE, the first process in the ACL2
waterfall (see hints-and-the-waterfall). Forward chaining often proves
``near propositional'' goals (those depending just on boolean implications
between basic predicates). Other tokens you may see include
which uses forward chaining to set up a context for applying
induction rules, and the definitional principle (and related
utilities such as
uses forward chaining during the construction of both measure conjectures and
guard conjectures. When used this way, the token is
How to Read Activation Reports
The forward chaining report concludes with a list of activation reports.
Activations: (act1 act2 ...)Each acti is of the form:
(rune (:TRIGGER inst-trig) ((:UNIFY-SUBST subst) (:DISPOSITION outcome-part1 outcome-part2 inst-term)) ...)where the
...indicates that the rest of the report consists of more of those tuples listing a
:DISPOSITION. We call each tuple a disposition of the activation and each disposition describes a substitution subst identifying the final instantiation of the rule and how the activation fared. Suppose there are n dispositions. (If the rule in question contains no free variables, n will be 1.)
This activation report means that during the forward chaining process in
forward-chaining rune rune was fired due
to the presence in the evolving context of the trigger term inst-trig.
(Note that inst-trig is an instantiation of the trigger term of the
named rule. That is, the variable symbols you see in inst-trig are
those of the clause printed in the forward chaining report.) The activation
of rune by inst-trig proceeded to split n ways as different
choices were made for the free-variables occuring among the hypotheses.
Each of those n choices gave rise to a different substitution subst,
and each succeeded or failed as described by the corresponding
:DISPOSITION of an activation is described in three parts,
outcome-part1, outcome-part2, and inst-term.
Outcome-part1 is either
BLOCKED, meaning that the
instance given by subst either succeeded in the sense that all of its
instantiated hypotheses were found in the context, or failed because some
instantiated hypothesis was not found.
SUCCESS then inst-term is the instantiated
conclusion produced by the rule. Outcome-part2 is
the instantiated conclusion was acceptable to our heuristics designed to
prevent looping and not already known in the evolving context.
REJECTED if the instantiated conclusion was
not approved by our heuristics. Outcome-part2 is
the instantiated conclusion was approved by the heuristics but already
known true in the current evolving context. If
truth of the instantiated conclusion is added to the evolving context.
Otherwise, it is not.
outcome-part2 is one of three
FALSE, in which case inst-term is an instantiated
hypothesis of the rule that is assumed false in the current context,
UNRELIEVED-HYP, in which case inst-term is an instantiated
hypothesis whose truthvalue is not determined by the context, or
UNRELIEVED-HYP-FREE, in which case inst-term is an oddly
instantiated hypothesis whose truthvalue is not determined by the context and
which also contains free variables. In the last case, the ``odd''
instantiation was by the substitution subst but extended so that free
variables in the hypothesis are renamed to start with the prefix
UNBOUND-FREE- to draw your attention to them.
Note: All of the terms printed in the report are instantiated with the relevant unifying substitution (possibly extended to bind free variables).
Specifying the Tracking Criteria
During a proof attempt, the forward chaining module stores information about
the activations satisfying certain criteria. The criteria is a list of
triples. Each triple consists of a forward chaining rune, an
instantiated trigger term, and an instantiated conclusion to watch for.
However, any or all of the components of such a triple may be
t and that
is given special significance.
satisfies a criteria if it satisfies at least one of the
triples. An activation satisfies a triple if it satisfies all three of the
components. Every activation satisfies the component
t. An activation
satisfies a rune if the activation describes a firing of the named rule.
An activation satisfies an instantiated trigger term if the activation was
created by that trigger being present in the context. An activation
satisfies an instantiated conclusion if the activation could produce the
instantiated conclusion (with the right choice of any free variables).
Thus, the criteria is interpreted as a disjunction of conjunctions, making it possible to track a specific set of runes, triggers, and conclusions. For example, here is a triple that might appear in the criteria:
((:FORWARD-CHAINING ALISTP-FORWARD-TO-TRUE-LISTP) t t).This triple would cause every activation of the given rule to be tracked. However, the triple
((:FORWARD-CHAINING ALISTP-FORWARD-TO-TRUE-LISTP) (ALISTP (MAKE-BINDINGS VARS (TOP-N (OP1 INST) (STACK S)))) t)would only track activations of that rule fired by the specific term shown as the second element of the triple. Futhermore
(t (ALISTP (MAKE-BINDINGS VARS (TOP-N (OP1 INST) (STACK S)))) t)would track any forward chaining rule triggered by that term, and
(t t (TRUE-LISTP (MAKE-BINDINGS VARS (TOP-N (OP1 INST) (STACK S)))))would track any rule fired by any trigger that might lead to the specific term given as the third component above.
Note: The condition on how an activation satisfies an instantiated conclusion is a little subtle. Consider the activation of the forward chaining rule
(implies (and (symbol-listp x) (equal (len x) (len y))) (true-listp (make-bindings x y)))triggered by
(SYMBOL-LISTP VARS)arising in the current context. This activation could produce the specific conclusion shown in the last triple above, if it just happened that
(TOP-N (OP1 INST) (STACK S))were chosen as the binding of the free variable
y. Thus, the activation of this rule triggered by
(SYMBOL-LISTP VARS)satisfies the last triple above.
Observe that the triple
(t t t)is satisfied by every activation of any rule by any trigger term producing any conclusion.
set-fc-criteria sets the criteria describing
which activations are to be tracked.
For example, if you execute:
(set-fc-criteria ((:FORWARD-CHAINING LEMMA1) t t) ((:FORWARD-CHAINING LEMMA2) (ALISTP (BASIC-MAPPER A B)) t) (t t (TRUE-LISTP (DLT D)))),the system would track all activations of the forward-chaining rule
LEMMA1, plus those activations of forward-chaining rule
LEMMA2triggered by the term given in the second triple, plus any activation of any rule that might derive
(TRUE-LISTP (DLT D)).
Because criteria generally mention variable symbols used in a specific conjecture, it is probably best to reconsider your criteria every time you want to track forward chaining.
If the criteria is
nil, then nothing is tracked. Setting the criteria to
nil is the way you turn off tracking and reporting of forward chaining
activity. You may do this either by
(set-fc-criteria) or by
(set-fc-criteria nil). (Technically the second form is an odd
set-fc-criteria, which expects any supplied arguments to be
triples; if the ``triple''
nil is the only one supplied, we take it
to mean that the entire criteria should be
To track every forward chaining activation you may set the criteria with
(set-fc-criteria (t t t)) or use the abbreviation
If, when you read a forward chaining report, you see no mention of
an activation you have in mind, e.g., of a certain rune or deriving a
certain conclusion, and you have set the criteria correctly, then the
activation never happened. (This is akin to using
monitor to monitor the application of a rewrite rule and
then seeing no interactive break.)
For some relevant functions to help you manage criteria and when the full
reports are printed see