• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
      • Gl
      • Witness-cp
      • Ccg
      • Install-not-normalized
      • Rewrite$
      • Fgl
        • Fgl-rewrite-rules
        • Fgl-function-mode
        • Fgl-object
        • Fgl-solving
        • Fgl-handling-if-then-elses
        • Fgl-counterexamples
        • Fgl-getting-bits-from-objects
        • Fgl-primitive-and-meta-rules
        • Fgl-interpreter-overview
        • Fgl-correctness-of-binding-free-variables
        • Fgl-debugging
        • Fgl-testbenches
        • Def-fgl-boolean-constraint
        • Fgl-stack
        • Def-fgl-param-thm
        • Fgl-rewrite-tracing
          • Fgl-trace
          • Fgl-advanced-tracing
          • Fgl-modify-current-tracespec
            • Fgl-trace*
            • Trace-repl
            • Fgl-untrace*
            • Fgl-untrace-all*
            • Fgl-untrace
            • Fgl-delete-current-tracespec
            • Fgl-untrace-all
          • Def-fgl-thm
          • Fgl-fast-alist-support
          • Fgl-array-support
          • Advanced-equivalence-checking-with-fgl
          • Fgl-fty-support
          • Fgl-internals
        • Removable-runes
        • Efficiency
        • Rewrite-bounds
        • Bash
        • Def-dag-measure
        • 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
      • Math
      • Testing-utilities
    • Fgl-rewrite-tracing

    Fgl-modify-current-tracespec

    When invoked from a trace expression, change the trace processing of the current rule invocation.

    If called from a trace expression for some particular rule invocation, this changes how the tracing for the rest of this rule invocation will work.

    E.g., suppose a rule was initially traced as follows:

    (fgl::fgl-trace (:formula my-rule)
                    :on-entry (if (equal fgl::depth 5)
                                  (let ((?ignore (fgl::fgl-modify-current-tracespec
                                                  (:formula my-rule)
                                                  :on-success nil
                                                  :on-failure "Failed at trace depth 5")))
                                    "Entering at trace depth 5")
                                "Entering at trace depth other than 5")
                    :on-success "Success at trace depth other than 5"
                    :on-failure "Failed at trace depth other than 5")

    This will generally print "Entering at trace depth other than 5" on entry to the specified rule and "(Success/Failed) at trace depth other than 5" on exit. However, if the rule is ever applied at a trace depth of 5, then it will print "Entering at trace depth 5" and, because it modifies the current tracespec, it will then only print "Failed at trace depth 5" if it failed but print nothing if it succeeded.

    Similarly, a trace formula may delete the current tracespec using fgl-delete-current-tracespec.