• 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-to-faig
        • 4v-sexpr-restrict-with-rw
        • 4vs-constructors
        • 4v-sexpr-compose-with-rw
        • 4v-sexpr-restrict
          • 4v-sexpr-restrict-alist
          • 4v-nsexpr-p-4v-sexpr-restrict
          • 4v-sexpr-restrict-list
        • 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-sexprs

4v-sexpr-restrict

Basic substitution operation for 4v-sexprs.

(4v-sexpr-restrict x al) takes a sexpr, x, and a fast alist, al that should bind variables to sexprs. It constructs a new sexpr that is just a copy of x where any variables bound in al have been replaced with their bound values.

We memoize this function to avoid repeatedly restricting shared subexpressions, but this only helps when you are restricting with the same alist. We don't use :forget t because you frequently want to restrict several related expressions under the same alist, as in 4v-sexpr-restrict-alist. So, you'll generally need to manage clearing the memoization table yourself.

Note that this function is "dumb" and does not try in any way to simplify the resulting expressions. The function 4v-sexpr-restrict-with-rw is a "smarter" alternative that is generally slower but can produce simpler sexprs as output.

Definitions and Theorems

Function: 4v-sexpr-restrict

(defun 4v-sexpr-restrict (x al)
  (declare (xargs :guard t))
  (if (atom x)
      (and x
           (let ((look (hons-get x al)))
             (if look (cdr look) x)))
    (hons (car x)
          (4v-sexpr-restrict-list (cdr x) al))))

Function: 4v-sexpr-restrict-list

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

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

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

Theorem: 4v-sexpr-eval-4v-sexpr-restrict

(defthm 4v-sexpr-eval-4v-sexpr-restrict
  (equal (4v-sexpr-eval (4v-sexpr-restrict x al1)
                        al2)
         (4v-sexpr-eval x
                        (append (4v-sexpr-eval-alist al1 al2)
                                al2))))

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

(defthm 4v-sexpr-eval-list-sexpr-4v-sexpr-restrict-list
  (equal (4v-sexpr-eval-list (4v-sexpr-restrict-list x al1)
                             al2)
         (4v-sexpr-eval-list x
                             (append (4v-sexpr-eval-alist al1 al2)
                                     al2))))

Subtopics

4v-sexpr-restrict-alist

Extension of 4v-sexpr-restrict to alists.

4v-nsexpr-p-4v-sexpr-restrict

4v-sexpr-restrict-list

Substitute into a list of sexprs.