• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
      • 4v-sexprs
        • 4v-sexpr-vars
        • 4v-sexpr-eval
        • 4v-sexpr-to-faig
        • 4v-sexpr-restrict-with-rw
        • 4vs-constructors
        • 4v-sexpr-compose-with-rw
        • 4v-sexpr-restrict
        • 4v-sexpr-alist-extract
        • 4v-sexpr-compose
        • 4v-nsexpr-p
        • 4v-sexpr-purebool-p
        • 4v-sexpr-<=
        • Sfaig
        • Sexpr-equivs
        • 3v-syntax-sexprp
        • Sexpr-rewriting
        • 4v-sexpr-ind
        • 4v-alist-extract
      • 4v-monotonicity
      • 4v-operations
      • Why-4v-logic
      • 4v-<=
      • 4vp
      • 4vcases
      • 4v-fix
      • 4v-lookup
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 4v-sexprs

4v-sexpr-alist-extract

Extract a portion of a 4v-sexpr alist.

(4v-sexpr-alist-extract keys al) is given:

• keys, a list of names, and
• al, a fast alist binding names to sexprs.

It produces a new alist that binds all of the names in keys to their corresponding sexprs in al. The result is an ordinary, non-fast alist.

More precisely, the new alist binds each k in keys to:

• al[k] when k is bound in al, or
• NIL (which just evaluates to X) otherwise.

This is just slightly different than fal-extract: whereas fal-extract omits missing keys, this binds them to nil.

This function can be a useful for removing any "extraneous" bindings from an the sexpr-alist al. Some equivalence relations like 4v-sexpr-alist-equiv check whether alists have the same bindings because this allows for powerful composition theorems. For instance, the following rule would not hold if a-equiv were allowed to contain bind variables not bound by a:

Theorem: 4v-sexpr-alist-equiv-implies-4v-sexpr-alist-equiv-append-1

(defthm 4v-sexpr-alist-equiv-implies-4v-sexpr-alist-equiv-append-1
  (implies (4v-sexpr-alist-equiv a a-equiv)
           (4v-sexpr-alist-equiv (append a b)
                                 (append a-equiv b)))
  :rule-classes (:congruence))

Definitions and Theorems

Function: 4v-sexpr-alist-extract1

(defun 4v-sexpr-alist-extract1 (keys al)
  "Assumes AL is fast"
  (declare (xargs :guard t))
  (if (atom keys)
      nil
    (cons (cons (car keys)
                (cdr (hons-get (car keys) al)))
          (4v-sexpr-alist-extract1 (cdr keys)
                                   al))))

Function: 4v-sexpr-alist-extract

(defun 4v-sexpr-alist-extract (keys al)
 "Makes AL fast if necessary"
 (declare (xargs :guard t))
 (mbe :logic
      (if (atom keys)
          nil
        (cons (cons (car keys)
                    (cdr (hons-get (car keys) al)))
              (4v-sexpr-alist-extract (cdr keys) al)))
      :exec (with-fast-alist al (4v-sexpr-alist-extract1 keys al))))

Theorem: 4v-sexpr-alist-extract1-removal

(defthm 4v-sexpr-alist-extract1-removal
  (equal (4v-sexpr-alist-extract1 keys al)
         (4v-sexpr-alist-extract keys al)))

Theorem: alist-equiv-implies-equal-4v-sexpr-alist-extract-2

(defthm alist-equiv-implies-equal-4v-sexpr-alist-extract-2
  (implies (alist-equiv al al-equiv)
           (equal (4v-sexpr-alist-extract keys al)
                  (4v-sexpr-alist-extract keys al-equiv)))
  :rule-classes (:congruence))