• 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
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Sexpr-rewriting
• 4v-sexprs

4v-sexpr-restrict-with-rw

4v-sexpr-restrict with inline rewriting.

This is different from sexpr-rewrite-of-restrict because it doesn't apply rewriting to the alist lookups; it basically assumes they've already been rewritten. So while we can't prove that this is equal to sexpr-rewrite of 4v-sexpr-restrict, we can prove that it's sexpr-equivalent to 4v-sexpr-restrict, and contains a subset of its variables.

Careful about memoization here; wouldn't want to use this when you're about to (or just have) done a 4v-sexpr-restrict of a similar sexpression with the same alist, or done a sexpr-rewrite of an sexpression similar to your result. Memoization won't carry over.

Definitions and Theorems

Function: 4v-sexpr-restrict-with-rw

(defun 4v-sexpr-restrict-with-rw (x al)
  (declare (xargs :guard t))
  (if (atom x)
      (and x
           (let ((look (hons-get x al)))
             (if look (cdr look) x)))
    (b* ((args (4v-sexpr-restrict-with-rw-list (cdr x)
                                               al)))
      (sexpr-rewrite-fncall 100 (car x)
                            args *sexpr-rewrites*))))

Function: 4v-sexpr-restrict-with-rw-list

(defun 4v-sexpr-restrict-with-rw-list (x al)
  (declare (xargs :guard t))
  (if (atom x)
      x
    (hons (4v-sexpr-restrict-with-rw (car x) al)
          (4v-sexpr-restrict-with-rw-list (cdr x)
                                          al))))

Function: 4v-sexpr-restrict-with-rw-memoize-condition

(defun 4v-sexpr-restrict-with-rw-memoize-condition (x al)
  (declare (ignorable x al)
           (xargs :guard 't))
  (consp x))

Theorem: 4v-sexpr-restrict-with-rw-equiv-to-4v-sexpr-restrict

(defthm 4v-sexpr-restrict-with-rw-equiv-to-4v-sexpr-restrict
  (4v-sexpr-equiv (4v-sexpr-restrict-with-rw x al)
                  (4v-sexpr-restrict x al)))

Theorem: 4v-sexpr-restrict-with-rw-list-equiv-to-4v-sexpr-restrict-list

(defthm
     4v-sexpr-restrict-with-rw-list-equiv-to-4v-sexpr-restrict-list
  (4v-sexpr-list-equiv (4v-sexpr-restrict-with-rw-list x al)
                       (4v-sexpr-restrict-list x al)))

Theorem: 4v-sexpr-vars-4v-sexpr-restrict-with-rw

(defthm 4v-sexpr-vars-4v-sexpr-restrict-with-rw
 (implies
    (and (not (member-equal k (4v-sexpr-vars-list (alist-vals al))))
         (not (and (member-equal k (4v-sexpr-vars x))
                   (not (member-equal k (alist-keys al))))))
    (not (member-equal
              k
              (4v-sexpr-vars (4v-sexpr-restrict-with-rw x al))))))

Theorem: 4v-sexpr-vars-list-4v-sexpr-restrict-with-rw-list

(defthm 4v-sexpr-vars-list-4v-sexpr-restrict-with-rw-list
 (implies
  (and (not (member-equal k (4v-sexpr-vars-list (alist-vals al))))
       (not (and (member-equal k (4v-sexpr-vars-list x))
                 (not (member-equal k (alist-keys al))))))
  (not
   (member-equal
      k
      (4v-sexpr-vars-list (4v-sexpr-restrict-with-rw-list x al))))))

Function: 4v-sexpr-restrict-with-rw-alist-exec

(defun 4v-sexpr-restrict-with-rw-alist-exec (x al acc)
  (declare (xargs :guard t))
  (if (atom x)
      acc
    (if (atom (car x))
        (4v-sexpr-restrict-with-rw-alist-exec (cdr x)
                                              al acc)
      (4v-sexpr-restrict-with-rw-alist-exec
           (cdr x)
           al
           (cons (cons (caar x)
                       (4v-sexpr-restrict-with-rw (cdar x) al))
                 acc)))))

Function: 4v-sexpr-restrict-with-rw-alist

(defun 4v-sexpr-restrict-with-rw-alist (x al)
 (declare (xargs :guard t))
 (mbe
   :logic
   (if (atom x)
       nil
     (if (atom (car x))
         (4v-sexpr-restrict-with-rw-alist (cdr x)
                                          al)
       (cons (cons (caar x)
                   (4v-sexpr-restrict-with-rw (cdar x) al))
             (4v-sexpr-restrict-with-rw-alist (cdr x)
                                              al))))
   :exec (reverse (4v-sexpr-restrict-with-rw-alist-exec x al nil))))

Theorem: 4v-sexpr-restrict-with-rw-alist-exec-removal

(defthm 4v-sexpr-restrict-with-rw-alist-exec-removal
  (equal (4v-sexpr-restrict-with-rw-alist-exec x al acc)
         (revappend (4v-sexpr-restrict-with-rw-alist x al)
                    acc)))

Theorem: hons-assoc-equal-4v-sexpr-restrict-with-rw-alist

(defthm hons-assoc-equal-4v-sexpr-restrict-with-rw-alist
 (equal
  (hons-assoc-equal k
                    (4v-sexpr-restrict-with-rw-alist x al))
  (and (hons-assoc-equal k x)
       (cons k
             (4v-sexpr-restrict-with-rw (cdr (hons-assoc-equal k x))
                                        al)))))

Theorem: 4v-sexpr-restrict-with-rw-alist-equiv-to-4v-sexpr-restrict-alist

(defthm
   4v-sexpr-restrict-with-rw-alist-equiv-to-4v-sexpr-restrict-alist
  (4v-sexpr-alist-equiv (4v-sexpr-restrict-with-rw-alist x al)
                        (4v-sexpr-restrict-alist x al)))

Theorem: sexpr-eval-alist-of-4v-sexpr-restrict-with-rw-alist

(defthm sexpr-eval-alist-of-4v-sexpr-restrict-with-rw-alist
  (equal (4v-sexpr-eval-alist (4v-sexpr-restrict-with-rw-alist x al)
                              env)
         (4v-sexpr-eval-alist (4v-sexpr-restrict-alist x al)
                              env)))

Theorem: alist-keys-4v-sexpr-restrict-with-rw-alist

(defthm alist-keys-4v-sexpr-restrict-with-rw-alist
  (equal (alist-keys (4v-sexpr-restrict-with-rw-alist al env))
         (alist-keys al)))

Theorem: 4v-sexpr-restrict-with-rw-alist-append

(defthm 4v-sexpr-restrict-with-rw-alist-append
  (equal (4v-sexpr-restrict-with-rw-alist (append al1 al2)
                                          env)
         (append (4v-sexpr-restrict-with-rw-alist al1 env)
                 (4v-sexpr-restrict-with-rw-alist al2 env))))

Function: 4v-sexpr-restrict-with-rw-alists

(defun 4v-sexpr-restrict-with-rw-alists (x al)
  (declare (xargs :guard t))
  (if (atom x)
      nil
    (cons (4v-sexpr-restrict-with-rw-alist (car x)
                                           al)
          (4v-sexpr-restrict-with-rw-alists (cdr x)
                                            al))))

Function: 4v-sexpr-restrict-with-rw-list-list

(defun 4v-sexpr-restrict-with-rw-list-list (x al)
  (declare (xargs :guard t))
  (if (atom x)
      nil
    (cons (4v-sexpr-restrict-with-rw-list (car x)
                                          al)
          (4v-sexpr-restrict-with-rw-list-list (cdr x)
                                               al))))