|
|
|---|
|
|
|
|---|
A extensible hint suggestion daemon
Adviser is a a hint computation service. When the adviser book is loaded, this service is installed into the ACL2 world as a default hint. This service is consulted when goals becomes stable under simplification during your proof attempts. In other words, before destructor elimination, generalization, and so forth are tried, the theorem prover will now first consult the Adviser service and see if any hints is available.
When the Adviser is consulted, it examines the goal that ACL2 is stuck on and checks to see if it can give any suggestions. To make these suggestions, Adviser consults its own database of rules. These rules are kept in a new ACL2 table that Adviser manages, and efficiently stored using the btree library that comes with ACL2 (see books/misc/symbol-btree.lisp).
This database oriented approach has two advantages. First, users can extend Adviser's knowledge by adding new rules, without having to understand the tricky details of how computed hints work. (These rules are added through a new event called defadvice, which intentionally looks a lot like defthm). Second, by using a database of triggers, a single pass over each goal is sufficient to determine if advice is necessary. In contrast, if everyone created their own computed hints, we would have multiple passes over the same goal.
See defadvice for information on adding rules to Adviser.