• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
    • Gl
      • Term-level-reasoning
        • G-call
        • Def-gl-boolean-constraint
        • Gl-set-uninterpreted
        • Def-glcp-ctrex-rewrite
        • Def-gl-rewrite
        • Def-gl-branch-merge
      • Glmc
      • Other-resources
      • Optimization
      • Reference
      • Debugging
      • Basic-tutorial
    • Witness-cp
    • Ccg
    • Install-not-normalized
    • Rewrite$
    • Removable-runes
    • Fgl
    • 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

• Reference
• Term-level-reasoning

Def-gl-rewrite

Define a rewrite rule for GL to use on term-level objects

GL can use ACL2-style rewrite rules to simplify term-level symbolic objects. However, typically one wants a different theory for ACL2 theorem proving than one wants to use inside GL. GL::DEF-GL-REWRITE defines a rewrite rule that is only used inside GL:

(gl::def-gl-rewrite my-rewrite-rule
   (implies (and (syntaxp (and (integerp n) (< 0 (integer-length n))))
                 (< 0 m))
            (equal (logand n m)
                   (logcons (b-and (logcar n) (logcar m))
                            (logand (logcdr n) (logcdr m)))))
  :hints ...)

This defines a disabled ACL2 rewrite rule called my-rewrite-rule, and adds my-rewrite-rule to the table of rules GL is allowed to use. (GL will still use it even though it is disabled, as long as it is in that table.)

Def-gl-rewrite supports syntaxp hypotheses, but the term representation used is different from ACL2's. Instead of being bound to TERMPs, the variables are bound to symbolic objects. See symbolic-objects for reference.