• 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-alist-extract
        • 4v-sexpr-compose
        • 4v-nsexpr-p
        • 4v-sexpr-purebool-p
        • 4v-sexpr-<=
        • Sfaig
        • Sexpr-equivs
        • 3v-syntax-sexprp
        • Sexpr-rewriting
          • 4v-shannon-expansion
          • Onehot-rewriting
          • 4v-sexpr-restrict-with-rw
          • 4v-sexpr-compose-with-rw
          • Sexpr-rewrite
          • Sexpr-rewrite-default
          • Sexpr-rewriting-internals
          • *sexpr-rewrites*
        • 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

• Sexpr-rewriting
• Sexpr-rewriting-internals

Sexpr-rewrite

Applies inside-out rewriting to an s-expression using a user-provided set of rewrite rules.

A good (?) default set of rules is provided in *sexpr-rewrites*. It is a theorem that, if the rewrite rules are recognized by 4v-sexpr-rewrite-alistp, then the result is 4v-sexpr-equiv to the input. It is also a theorem that the variables of the result are a subset of those of the input.

Definitions and Theorems

Function: sexpr-rewrite

(defun sexpr-rewrite (x rewrites)
       (declare (xargs :guard t))
       (if (atom x)
           x
           (b* ((args (sexpr-rewrite-list (cdr x) rewrites)))
               (sexpr-rewrite-fncall 100 (car x)
                                     args rewrites))))

Function: sexpr-rewrite-list

(defun sexpr-rewrite-list (x rewrites)
       (declare (xargs :guard t))
       (if (atom x)
           nil
           (hons (sexpr-rewrite (car x) rewrites)
                 (sexpr-rewrite-list (cdr x) rewrites))))

Function: sexpr-rewrite-memoize-condition

(defun sexpr-rewrite-memoize-condition
       (x rewrites)
       (declare (ignorable x rewrites)
                (xargs :guard 't))
       (consp x))

Function: sexpr-rewrite-flag

(defun
   sexpr-rewrite-flag (flag x rewrites)
   (declare (xargs :non-executable t))
   (declare (ignorable x rewrites))
   (prog2$ (throw-nonexec-error 'sexpr-rewrite-flag
                                (list flag x rewrites))
           (cond ((equal flag 'rw)
                  (if (consp x)
                      ((lambda (args rewrites x)
                               (sexpr-rewrite-fncall '100
                                                     (car x)
                                                     args rewrites))
                       (sexpr-rewrite-flag 'rw-list
                                           (cdr x)
                                           rewrites)
                       rewrites x)
                      x))
                 (t (if (consp x)
                        (hons (sexpr-rewrite-flag 'rw
                                                  (car x)
                                                  rewrites)
                              (sexpr-rewrite-flag 'rw-list
                                                  (cdr x)
                                                  rewrites))
                        'nil)))))

Theorem: sexpr-rewrite-flag-equivalences

(defthm sexpr-rewrite-flag-equivalences
        (and (equal (sexpr-rewrite-flag 'rw x rewrites)
                    (sexpr-rewrite x rewrites))
             (equal (sexpr-rewrite-flag 'rw-list x rewrites)
                    (sexpr-rewrite-list x rewrites))))

Theorem: sexpr-rewrite-correct

(defthm sexpr-rewrite-correct
        (implies (4v-sexpr-rewrite-alistp rewrites)
                 (4v-sexpr-equiv (sexpr-rewrite x rewrites)
                                 x)))

Theorem: sexpr-rewrite-list-correct

(defthm
     sexpr-rewrite-list-correct
     (implies (4v-sexpr-rewrite-alistp rewrites)
              (4v-sexpr-list-equiv (sexpr-rewrite-list x rewrites)
                                   x)))

Theorem: sexpr-rewrite-vars

(defthm
    sexpr-rewrite-vars
    (implies
         (not (member v (4v-sexpr-vars x)))
         (not (member v
                      (4v-sexpr-vars (sexpr-rewrite x rewrites))))))

Theorem: sexpr-rewrite-list-vars

(defthm
 sexpr-rewrite-list-vars
 (implies
  (not (member v (4v-sexpr-vars-list x)))
  (not
    (member v
            (4v-sexpr-vars-list (sexpr-rewrite-list x rewrites))))))

Function: sexpr-rewrite-alist

(defun sexpr-rewrite-alist (x rewrites)
       (declare (xargs :guard t))
       (if (atom x)
           nil
           (if (atom (car x))
               (sexpr-rewrite-alist (cdr x) rewrites)
               (cons (cons (caar x)
                           (sexpr-rewrite (cdar x) rewrites))
                     (sexpr-rewrite-alist (cdr x)
                                          rewrites)))))