• 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
  • Debugging
  • Projects
  • 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))))