		Search-engine friendly clone of the ACL2 documentation.

4v-sexprs

4v-sexpr-eval

Evaluate a sexpr under an environment.

(4v-sexpr-eval x env) evaluates the 4v-sexpr x under the environment env, producing a 4vp.

This environment is an alist binding the variables of x to four-valued logic constants. It must be a fast alist.

Unbound variables evaluate to X.
Variables bound to non-4vp values evaluate to X.
Ill-formed sexprs evaluate to X.

This is an especially simple evaluator, and together with the 4v-operations it invokes it defines the semantics of our s-expressions. Moreover, the main theorems about other 4v-sexpr operations are usually stated in terms of the evaluations of their results.

We memoize evaluation to avoid having to recompute shared subexpressions. Note that we do not memoize with :forget t because you frequently want to evaluate several related expressions under the same environment, as in 4v-sexpr-eval-alist. As a consequence, you'll generally need to manage its memo table yourself.

This evaluator performs well enough to be practically useful for single-bit evaluations under a fixed environment. However, it is almost certainly too slow to use this function when doing any significant amount of evaluation, e.g., vector simulations of the same sexpr under random environments. For that sort of thing, it should be possible to develop a much faster simulator, e.g., by compiling the sexpr into a bytecode program and using a stobj array of fixnums to hold the values, or similar.

Definitions and Theorems

Function: 4v-sexpr-apply

(defun 4v-sexpr-apply (fn args)
  (declare (xargs :guard (true-listp args)))
  (b* (((when (or (eq fn (4vt))
                  (eq fn (4vf))
                  (eq fn (4vx))
                  (eq fn (4vz))))
        fn)
       (arg1 (4v-first args))
       (arg2 (4v-second args))
       (arg3 (4v-third args)))
    (case fn
      (not (4v-not arg1))
      (and (4v-and arg1 arg2))
      (xor (4v-xor arg1 arg2))
      (iff (4v-iff arg1 arg2))
      (or (4v-or arg1 arg2))
      (ite* (4v-ite* arg1 arg2 arg3))
      (zif (4v-zif arg1 arg2 arg3))
      (buf (4v-unfloat arg1))
      (xdet (4v-xdet arg1))
      (res (4v-res arg1 arg2))
      (tristate (4v-tristate arg1 arg2))
      (ite (4v-ite arg1 arg2 arg3))
      (pullup (4v-pullup arg1))
      (id (4v-fix arg1))
      (otherwise (4vx)))))

Function: 4v-sexpr-eval

(defun 4v-sexpr-eval (x env)
  (declare (xargs :guard t))
  (b* (((when (atom x))
        (if x (4v-lookup x env) (4vx)))
       (fn (car x))
       ((when (or (eq fn (4vt))
                  (eq fn (4vf))
                  (eq fn (4vx))
                  (eq fn (4vz))))
        fn)
       (args (4v-sexpr-eval-list (cdr x) env))
       (arg1 (4v-first args))
       (arg2 (4v-second args))
       (arg3 (4v-third args)))
    (case fn
      (not (4v-not arg1))
      (and (4v-and arg1 arg2))
      (xor (4v-xor arg1 arg2))
      (iff (4v-iff arg1 arg2))
      (or (4v-or arg1 arg2))
      (ite* (4v-ite* arg1 arg2 arg3))
      (zif (4v-zif arg1 arg2 arg3))
      (buf (4v-unfloat arg1))
      (xdet (4v-xdet arg1))
      (res (4v-res arg1 arg2))
      (tristate (4v-tristate arg1 arg2))
      (ite (4v-ite arg1 arg2 arg3))
      (pullup (4v-pullup arg1))
      (id (4v-fix arg1))
      (otherwise (4vx)))))

Function: 4v-sexpr-eval-list

(defun 4v-sexpr-eval-list (x env)
  (declare (xargs :guard t))
  (if (atom x)
      nil
    (cons (4v-sexpr-eval (car x) env)
          (4v-sexpr-eval-list (cdr x) env))))

Theorem: 4v-sexpr-eval-redef

(defthm 4v-sexpr-eval-redef
  (equal (4v-sexpr-eval x env)
         (b* (((when (atom x))
               (if x (4v-lookup x env) (4vx)))
              (args (4v-sexpr-eval-list (cdr x) env)))
           (4v-sexpr-apply (car x) args)))
  :rule-classes
  ((:definition :clique (4v-sexpr-eval 4v-sexpr-eval-list)
                :controller-alist ((4v-sexpr-eval t nil)
                                   (4v-sexpr-eval-list t nil)))))

Function: 4v-sexpr-eval-memoize-condition

(defun 4v-sexpr-eval-memoize-condition (x env)
  (declare (ignorable x env)
           (xargs :guard 't))
  (and (consp x) (consp (cdr x))))

Theorem: 4v-sexpr-eval-possibilities

(defthm 4v-sexpr-eval-possibilities
  (implies (and (not (equal (4v-sexpr-eval x env) (4vt)))
                (not (equal (4v-sexpr-eval x env) (4vf)))
                (not (equal (4v-sexpr-eval x env) (4vz))))
           (equal (equal (4v-sexpr-eval x env) (4vx))
                  t)))

Theorem: 4v-sexpr-eval-nil

(defthm 4v-sexpr-eval-nil
  (equal (4v-sexpr-eval nil env) (4vx)))

Theorem: 4v-sexpr-eval-4vx-sexpr

(defthm 4v-sexpr-eval-4vx-sexpr
  (equal (4v-sexpr-eval *4vx-sexpr* env)
         (4vx)))

Theorem: 4v-fix-4v-sexpr-eval

(defthm 4v-fix-4v-sexpr-eval
  (equal (4v-fix (4v-sexpr-eval x env))
         (4v-sexpr-eval x env)))

Theorem: 4v-sexpr-eval-monotonicp

(defthm 4v-sexpr-eval-monotonicp
  (implies (4v-alist-<= env env1)
           (4v-<= (4v-sexpr-eval x env)
                  (4v-sexpr-eval x env1))))

Theorem: 4v-sexpr-eval-list-monotonicp

(defthm 4v-sexpr-eval-list-monotonicp
  (implies (4v-alist-<= env env1)
           (4v-list-<= (4v-sexpr-eval-list x env)
                       (4v-sexpr-eval-list x env1))))

Theorem: nth-of-4v-sexpr-eval-list

(defthm nth-of-4v-sexpr-eval-list
  (4v-equiv (nth n (4v-sexpr-eval-list x env))
            (4v-sexpr-eval (nth n x) env)))

Subtopics

4v-sexpr-simp-and-eval: Version of 4v-sexpr-eval that simplifies before evaluating
4v-sexpr-eval-alist: Extension of 4v-sexpr-eval to alists.
4v-sexpr-eval-list-list
4v-sexpr-eval-alists
4v-sexpr-eval-list: Evaluate a list of sexprs under an environment.