• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
      • Gl
        • Term-level-reasoning
        • Glmc
        • Other-resources
        • Optimization
        • Reference
          • Def-gl-thm
          • Shape-specs
          • Symbolic-objects
          • Gl-aside
          • Def-gl-param-thm
          • Symbolic-arithmetic
          • Bfr
          • Def-gl-boolean-constraint
          • Gl-mbe
          • Bvec
          • Flex-bindings
            • Auto-bindings
            • Gl-interp
            • Gl-set-uninterpreted
            • Def-gl-clause-processor
            • Def-glcp-ctrex-rewrite
            • ACL2::always-equal
            • Gl-hint
            • Def-gl-rewrite
            • Def-gl-branch-merge
            • Gl-force-check
            • Gl-concretize
            • Gl-assert
            • Gl-param-thm
            • Gl-simplify-satlink-mode
            • Gl-satlink-mode
            • Gl-bdd-mode
            • Gl-aig-bddify-mode
            • Gl-fraig-satlink-mode
          • Debugging
          • Basic-tutorial
        • Witness-cp
        • Ccg
        • Install-not-normalized
        • Rewrite$
        • Removable-runes
        • Efficiency
        • Rewrite-bounds
        • Bash
        • Def-dag-measure
        • Fgl
        • 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
    • Reference
    • Shape-specs

    Flex-bindings

    Shape specifiers for :g-bindings, more flexible than auto-bindings.

    The flex-bindings function lets you create somewhat more complicated shape-specs than is possible with auto-bindings. We assume familiarity with auto-bindings in this documentation. The specific feature flex-bindings offers that auto-bindings does not is the ability to split an integer variable into segments and generate indices for each segment independently.

    (def-gl-thm foo
      ...
      :g-bindings (flex-bindings                          ; expands to:
                    ;; auto-bindings list -- generates indices
                    ((:int a1 10)
                     (:rev (:mix (:int a2 13)
                                 (:int b1 13)))
                     (:int b2 10))
                    :arrange         ;; generate shape spec bindings from the indices
                    ((:int a a1 a2)  ;; a is a g-integer, indices are a1's appended to a2's
                     (:int b b1 b2))))

    The first argument is just a list of auto-bindings (though the syntax differs trivially in that flex-bindings takes them in a single argument whereas auto-bindings uses &rest args). They are used to generate indices, but not the actual g-bindings. We generate from these a mapping from each variable name to its list of indices.

    The :arrange argument, if provided, must be a list consisting of the following sorts of forms:

    • (:int a b c ...) means generate an integer shape-spec binding for variable a, consisting of the appended indices of b, c, etc., from the auto-bindings form.
    • (:int a) means generate an integer shape-spec binding for variable a using the indices of a from the auto-bindings form.
    • (:bool a) means generate a Boolean binding for variable a, using the index of a from the auto-bindings form.
    • (:bool a b) means generate a Boolean binding for variable a, using the index of b from the auto-bindings form.

    If the :arrange argument is not provided, flex-bindings acts just like auto-bindings -- it generates an entry for each variable mentioned in the auto-bindings.