• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
      • 4v-sexprs
        • 4v-sexpr-vars
        • 4v-sexpr-eval
          • 4v-sexpr-simp-and-eval
          • 4v-sexpr-eval-alist
          • 4v-sexpr-eval-list-list
          • 4v-sexpr-eval-alists
          • 4v-sexpr-eval-list
        • 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
  • Testing-utilities
  • Math

• 4v-sexpr-eval

4v-sexpr-eval-alist

Extension of 4v-sexpr-eval to alists.

(4v-sexpr-eval-alist x env) is given an alist x that should bind names to sexprs. It evaluates the sexprs under env and returns a new alist that binds the same names to the resulting four-valued constants. The new alist is an ordinary, non-fast alist.

It is beneficial for env to be a fast alist; if it is not fast, we temporarily make it fast.

Definitions and Theorems

Function: 4v-sexpr-eval-alist1

(defun 4v-sexpr-eval-alist1 (x env)
       "Assumes ENV is fast"
       (declare (xargs :guard t))
       (cond ((atom x) nil)
             ((atom (car x))
              (4v-sexpr-eval-alist1 (cdr x) env))
             (t (cons (cons (caar x)
                            (4v-sexpr-eval (cdar x) env))
                      (4v-sexpr-eval-alist1 (cdr x) env)))))

Function: 4v-sexpr-eval-alist

(defun
     4v-sexpr-eval-alist (x env)
     "Makes ENV fast if necessary"
     (declare (xargs :guard t))
     (mbe :logic (cond ((atom x) nil)
                       ((atom (car x))
                        (4v-sexpr-eval-alist (cdr x) env))
                       (t (cons (cons (caar x)
                                      (4v-sexpr-eval (cdar x) env))
                                (4v-sexpr-eval-alist (cdr x) env))))
          :exec (with-fast-alist env (4v-sexpr-eval-alist1 x env))))

Theorem: 4v-sexpr-eval-alist1-removal

(defthm 4v-sexpr-eval-alist1-removal
        (equal (4v-sexpr-eval-alist1 x env)
               (4v-sexpr-eval-alist x env)))

Theorem: lookup-sexpr-eval-alist

(defthm
     lookup-sexpr-eval-alist
     (equal (hons-assoc-equal x (4v-sexpr-eval-alist al env))
            (and (hons-assoc-equal x al)
                 (cons x
                       (4v-sexpr-eval (cdr (hons-assoc-equal x al))
                                      env)))))

Theorem: 4v-sexpr-eval-alist-append

(defthm 4v-sexpr-eval-alist-append
        (equal (4v-sexpr-eval-alist (append a b) env)
               (append (4v-sexpr-eval-alist a env)
                       (4v-sexpr-eval-alist b env))))

Theorem: alist-keys-4v-sexpr-eval-alist

(defthm alist-keys-4v-sexpr-eval-alist
        (equal (alist-keys (4v-sexpr-eval-alist a env))
               (alist-keys a)))

Theorem: 4v-alist-<=-sexpr-eval-alist-monotonic-env

(defthm 4v-alist-<=-sexpr-eval-alist-monotonic-env
        (implies (4v-alist-<= a b)
                 (4v-alist-<= (4v-sexpr-eval-alist x a)
                              (4v-sexpr-eval-alist x b))))