• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
      • Term
      • Ld
      • Hints
      • Type-set
      • Ordinals
      • Clause
      • ACL2-customization
      • With-prover-step-limit
      • Set-prover-step-limit
      • With-prover-time-limit
      • Local-incompatibility
      • Set-case-split-limitations
      • Subversive-recursions
      • Specious-simplification
      • Defsum
      • Gcl
      • Oracle-timelimit
      • Thm
      • Defopener
      • Case-split-limitations
      • Set-gc-strategy
      • Default-defun-mode
      • Top-level
      • Reader
      • Ttags-seen
      • Adviser
        • Pick-a-point
        • Defadvice
      • Ttree
      • Abort-soft
      • Defsums
      • Gc$
      • With-timeout
      • Coi-debug::fail
      • Expander
      • Gc-strategy
      • Coi-debug::assert
      • Sin-cos
      • Def::doc
      • Syntax
      • Subversive-inductions
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Adviser

Defadvice

Adds a rule to the Adviser database

General Form:
(defadvice rule-name term
  :rule-classes rule-classes)

where name is a new symbolic name See ACL2::name, term is a term alleged to be a useful piece of advice, and rule-classes describe the type of advice being added and when to suggest hints of this nature.

When Adviser is first loaded, no rules are installed in its database, so it will never suggest any hints. To make Adviser useful, rules must be added to it using defadvice. In principle, many types of advice could be added to the Adviser service, and in the future other classes of advice might be added. But, for now, the only understood rule class is :pick-a-point.

See pick-a-point for documentation and examples about :pick-a-point rules.