• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
      • Gl
      • Witness-cp
      • Ccg
      • Install-not-normalized
      • Rewrite$
      • Fgl
      • 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
        • Rp-rewriter
          • Rp-ruleset
          • Defthmrp
          • Rp-rewriter/meta-rules
            • Add-meta-rule
            • Dont-rw
              • Attach-meta-fncs
              • Is-rp-clause-processor-up-to-date
            • Rp-utilities
            • Rp-rewriter-demo
            • Rp-rewriter/debugging
            • Rp-rewriter/applications
        • 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
    • Rp-rewriter/meta-rules

    Dont-rw

    A special data structure that RP-Rewriter meta rules may return to control rewriting of returned terms.

    When a term us returned from a meta rule, it appears as completely new to the rewriter and by default, it will be parsed completely and be rewritten for a second time. This can cause performance issues with big terms. To solve this problem, we use a special structure called dont-rw that meta functions may generate and return to control which subterms should be rewritten and which should not.

    The dont-rw structure has the same cons skeleton as the term itself such that it is traversed (car'ed and cdr'ed) the same way as the term. Whenever dont-rw structure becomes an atom and non-nil, the rewriting of corresponding term stops. For example, assume that a meta rule returns the following term and we would like to avoid rewriting all the instances of g, then the following dont-rw structure would enable that.

    (f1 (f2 (g a b) c) 
        (f3 d (g x y))) 
    
    (nil (nil t t) 
         (nil t t))