Forward-chaining-reports
To see reports about the forward chaining process
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:
(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
occurring 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 truth value is not determined by the context, or
UNRELIEVED-HYP-FREE, in which case inst-term is an oddly
instantiated hypothesis whose truth value 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. Furthermore
(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.
Subtopics
- Set-fc-criteria
- To set the tracking criteria for forward chaining reports
- Set-fc-report-on-the-fly
- To determine when forward-chaining reports are printed
- Reset-fc-reporting
- Reset the forward-chaining tracking state to its initial configuration
- Fc-report
- To report on the forward chaining activity in the most recent proof
- Show-fc-criteria
- Print the forward-chaining tracking criteria
