		Search-engine friendly clone of the ACL2 documentation.

4v-sexpr-eval

4v-sexpr-simp-and-eval

Version of 4v-sexpr-eval that simplifies before evaluating

4v-sexpr-simp-and-eval computes the same result as 4v-sexpr-eval, but does so in a roundabout way where it first simplifies the given S-expression under the assignments given in the alist. However, missing assignments, which in 4v-sexpr-eval are treated as X, are ignored during this simplification pass, which uses 4v-sexpr-restrict-with-rw. After simplification, 4v-sexpr-eval is called with an empty environment, so that all remaining variables are assigned X. What is the advantage of 4v-sexpr-simp-and-eval? Sometimes during verification we have a complicated S-expression that contains variables that probably don't matter, and since we don't want to assume anything about their values, we leave them as Xes. But sometimes we then find that the result we get is itself X, and we want to know why. We can set 4v-lookup to complain when it doesn't find a variable in the environment, but if we're running the standard 4v-sexpr-eval we'll just get complaints about all the missing variables. However, if we run 4v-sexpr-simp-and-eval instead, we only get complaints about the ones that seem to actually matter in the final result, i.e. they weren't pruned away when simplifying using the known signals.

Definitions and Theorems

Function: 4v-sexpr-simp-and-eval

(defun 4v-sexpr-simp-and-eval (x al)
  (declare (xargs :guard t))
  (mbe :logic (4v-sexpr-eval x al)
       :exec
       (b* ((restrict-al (make-fast-alist (4v-al-to-sexpr-al al)))
            (simpl-x (4v-sexpr-restrict-with-rw x restrict-al)))
         (4v-sexpr-simp-and-eval-output simpl-x 'sexpr)
         (fast-alist-free restrict-al)
         (clear-memoize-table '4v-sexpr-restrict-with-rw)
         (4v-sexpr-eval simpl-x nil))))

Function: 4v-sexpr-simp-and-eval-list

(defun 4v-sexpr-simp-and-eval-list (x al)
 (declare (xargs :guard t))
 (mbe :logic (4v-sexpr-eval-list x al)
      :exec
      (b* ((restrict-al (make-fast-alist (4v-al-to-sexpr-al al)))
           (simpl-x (4v-sexpr-restrict-with-rw-list x restrict-al)))
        (fast-alist-free restrict-al)
        (4v-sexpr-simp-and-eval-output simpl-x 'list)
        (clear-memoize-table '4v-sexpr-restrict-with-rw)
        (4v-sexpr-eval-list simpl-x nil))))

Function: 4v-sexpr-simp-and-eval-alist

(defun 4v-sexpr-simp-and-eval-alist (x al)
 (declare (xargs :guard t))
 (mbe
     :logic (4v-sexpr-eval-alist x al)
     :exec
     (b* ((restrict-al (make-fast-alist (4v-al-to-sexpr-al al)))
          (simpl-x (4v-sexpr-restrict-with-rw-alist x restrict-al)))
       (4v-sexpr-simp-and-eval-output simpl-x 'alist)
       (fast-alist-free restrict-al)
       (clear-memoize-table '4v-sexpr-restrict-with-rw)
       (4v-sexpr-eval-alist simpl-x nil))))

Function: 4v-sexpr-simp-and-eval-alists

(defun 4v-sexpr-simp-and-eval-alists (x al)
 (declare (xargs :guard t))
 (mbe
    :logic (4v-sexpr-eval-alists x al)
    :exec
    (b* ((restrict-al (make-fast-alist (4v-al-to-sexpr-al al)))
         (simpl-x (4v-sexpr-restrict-with-rw-alists x restrict-al)))
      (4v-sexpr-simp-and-eval-output simpl-x 'alists)
      (fast-alist-free restrict-al)
      (clear-memoize-table '4v-sexpr-restrict-with-rw)
      (4v-sexpr-eval-alists simpl-x nil))))

Function: 4v-sexpr-simp-and-eval-list-list

(defun 4v-sexpr-simp-and-eval-list-list (x al)
 (declare (xargs :guard t))
 (mbe
   :logic (4v-sexpr-eval-list-list x al)
   :exec
   (b*
     ((restrict-al (make-fast-alist (4v-al-to-sexpr-al al)))
      (simpl-x (4v-sexpr-restrict-with-rw-list-list x restrict-al)))
     (4v-sexpr-simp-and-eval-output simpl-x 'list-list)
     (fast-alist-free restrict-al)
     (clear-memoize-table '4v-sexpr-restrict-with-rw)
     (4v-sexpr-eval-list-list simpl-x nil))))