FORWARD-CHAINING-REPORTS

to see reports about the forward chaining process 
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!

Some Related Topics

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:

(reset-fc-reporting)

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-chaining rules 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 k printed 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: 

(set-fc-report-on-the-fly t)

Collecting the data used to generate these reports slows down the prover. If you no longer wish to see such reports, do 

(set-fc-criteria nil)

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 INDUCT, which uses forward chaining to set up a context for applying :induction rules, and the definitional principle (and related utilities such as verify-termination and verify-guards) which uses forward chaining during the construction of both measure conjectures and guard conjectures. When used this way, the token is defun-or-guard-verification.

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 :UNIFY-SUBST and :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 question, the :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.

The :DISPOSITION of an activation is described in three parts, outcome-part1, outcome-part2, and inst-term. Outcome-part1 is either SUCCESS or 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.

If outcome-part1 is SUCCESS then inst-term is the instantiated conclusion produced by the rule. Outcome-part2 is APPROVED if the instantiated conclusion was acceptable to our heuristics designed to prevent looping and not already known in the evolving context. Outcome-part2 is REJECTED if the instantiated conclusion was not approved by our heuristics. Outcome-part2 is REDUNDANT if the instantiated conclusion was approved by the heuristics but already known true in the current evolving context. If APPROVED, the truth of the instantiated conclusion is added to the evolving context. Otherwise, it is not.

If outcome-part1 is BLOCKED then outcome-part2 is one of three possible things: 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.

An activation 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.

The function 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 LEMMA2 triggered 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 use of 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 nil.)

To track every forward chaining activation you may set the criteria with either (set-fc-criteria (t t t)) or use the abbreviation (set-fc-criteria t).

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 :brr and :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 fc-report, show-fc-criteria, set-fc-criteria, reset-fc-reporting, and set-fc-report-on-the-fly.