• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • 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-getting-bits-from-objects
        • Fgl-primitive-and-meta-rules
        • Fgl-counterexamples
        • Fgl-interpreter-overview
        • Fgl-correctness-of-binding-free-variables
        • Fgl-debugging
        • Fgl-testbenches
        • Def-fgl-boolean-constraint
        • Fgl-stack
        • Fgl-rewrite-tracing
        • Def-fgl-param-thm
        • Def-fgl-thm
        • Fgl-fast-alist-support
        • Fgl-array-support
          • Fgarray
          • 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-array-support

    Fgarray

    The abstract stobj interface on which FGL's array support is based

    An fgarray is an abstract stobj whose logical form is an alist with natural number keys and whose implementation uses an array for fast lookups. The fgarray interface is used in FGL for fast array access during rewriting.

    The supported interface functions are the following:

    • (fgarray-get i fgarray) gets the key/value pair associated with index i, or nil if it doesn't exist. Logically equal to (hons-assoc-equal (nfix i) fgarray).
    • (fgarray-set i val fgarray) sets the key i to value val; logically equal to (cons (cons (nfix i) val) fgarray).
    • (fgarray-compress fgarray) rearranges the alist representation so that the keys are in order with no duplicates.
    • (fgarray-init size fgarray) empties the fgarray and sets its backing array to the given size; logically equal to nil.
    • (fgarray->alist fgarray) returns the alist object of the fgarray.

    The stobj creator function is (create-fgarray), but as with all stobjs, this can only be invoked indirectly using with-local-stobj.

    Implementation note: The implementation of the fgarray builds a real alist equal to the logical representation. This is unnecessary for standalone use and is done so that FGL can ensure that the stobj storing the fgarray data is correctly in sync with the symbolic object representation. Thus if all you want is a stobj array that is logically represented as an alist, it would be better to define a different abstract stobj without this feature.