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

• 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)))))