• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
      • Gl
      • Witness-cp
      • Ccg
      • Install-not-normalized
      • Rewrite$
      • Removable-runes
      • Efficiency
      • Rewrite-bounds
      • Bash
      • Def-dag-measure
      • Fgl
        • Fgl-rewrite-rules
        • Fgl-function-mode
        • Fgl-object
        • Fgl-solving
        • Fgl-handling-if-then-elses
        • Fgl-getting-bits-from-objects
        • Fgl-primitive-and-meta-rules
        • Fgl-interpreter-overview
        • Fgl-counterexamples
        • Fgl-correctness-of-binding-free-variables
        • Fgl-debugging
        • Fgl-testbenches
        • Def-fgl-boolean-constraint
        • Fgl-stack
        • Fgl-rewrite-tracing
          • Def-fgl-param-thm
          • Def-fgl-thm
          • Fgl-fast-alist-support
          • Advanced-equivalence-checking-with-fgl
          • Fgl-array-support
          • Fgl-internals
        • Bdd
        • Remove-hyps
        • Contextual-rewriting
        • Simp
        • Rewrite$-hyps
        • Bash-term-to-dnf
        • Use-trivial-ancestors-check
        • Minimal-runes
        • Clause-processor-tools
        • Fn-is-body
        • Without-subsumption
        • Rewrite-equiv-hint
        • Def-bounds
        • Rewrite$-context
        • Try-gl-concls
        • Hint-utils
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Fgl

    Fgl-rewrite-tracing

    How to trace the FGL rewriter

    FGL allows attempts at applying rewrite rules to be traced using a configurable tracing function. By default, a basic tracing function is provided such that the user only needs to set up some state global variables to enable and use it. The function that performs the trace printing is attachable, so more advanced users can replace it with a custom version.

    Basic Tracing

    The default tracing implementation may be activated by setting the following state globals:

    ;; Enable the tracing function
    (assign :fgl-trace-rewrites t)
    
    ;; Alist whose keys are the rules that will be traced
    (assign :fgl-trace-rule-alist '(((:rewrite fgl::fgl-lognot))))
    
    ;; Evisc tuple for trace output
    (assign :fgl-trace-evisc-tuple (evisc-tuple 8 12 nil nil))

    If the attachments for the tracing functions have changed, they may be reset to the default functions as follows:

    (fgl-rewrite-trace-defaults)

    Custom Tracing

    The default attachment for the tracing functions may be replaced with custom versions. It may be useful to base it upon the default implementations, which append "-default" to the name of each function; i.e., the default implementation for fgl-rewrite-trace-cond is fgl-rewrite-trace-cond-default.

    The tracing functions have the following signatures:

    (fgl-rewrite-traced-rule-p rule interp-st state)
    (fgl-rewrite-trace-cond rule fn args interp-st state)
    (fgl-rewrite-trace-start-output depth rule fn args interp-st state)
    (fgl-rewrite-trace-success-output depth val rule fn args interp-st state)
    (fgl-rewrite-trace-failure-output depth failed-hyp rule fn args interp-st state)

    where the inputs are as follows:

    • rule, the rule being attempted, satisfying (fgl-generic-rule-p rule)
    • fn and args of the object that the rule is being applied to, where args satisfies fgl-objectlist-p
    • depth, the current stack depth of traced rule applications
    • status, either :start, :hyps, :finish, or :abort
    • val, the return value from a successful rewrite
    • failed-hyp, the index of the hypothesis that failed or nil if the rule application failed for some other reason
    • interp-st, the FGL interpreter state
    • state, the ACL2 state.