• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
      • Gl
        • Term-level-reasoning
        • Glmc
        • Other-resources
        • Optimization
        • Reference
          • Def-gl-thm
          • Shape-specs
            • G-call
            • Flex-bindings
              • Auto-bindings
              • G-int
            • 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$
          • 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
          • 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
      • 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.