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

• Sexpr-rewriting

Sexpr-rewrite-default

Rewrite an s-expression with the default rewrite rules, *sexpr-rewrites*.

May be a bit faster than using sexpr-rewrite, because there is only one argument to be memoized. On the other hand, it has to resolve the special variable *sexpr-rewrites*, but probably that's cheaper than an extra hash. Test this sometime?

Definitions and Theorems

Function: sexpr-rewrite-default

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

Function: sexpr-rewrite-default-list

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

Function: sexpr-rewrite-default-memoize-condition

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

Theorem: sexpr-rewrite-default-is-sexpr-rewrite

(defthm sexpr-rewrite-default-is-sexpr-rewrite
  (equal (sexpr-rewrite-default x)
         (sexpr-rewrite x *sexpr-rewrites*)))

Theorem: sexpr-rewrite-default-list-is-sexpr-rewrite-list

(defthm sexpr-rewrite-default-list-is-sexpr-rewrite-list
  (equal (sexpr-rewrite-default-list x)
         (sexpr-rewrite-list x *sexpr-rewrites*)))

Function: sexpr-rewrite-default-alist

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

Theorem: sexpr-rewrite-default-alist-is-sexpr-rewrite-alist

(defthm sexpr-rewrite-default-alist-is-sexpr-rewrite-alist
  (equal (sexpr-rewrite-default-alist x)
         (sexpr-rewrite-alist x *sexpr-rewrites*)))

Function: sexpr-rewrite-default-alists

(defun sexpr-rewrite-default-alists (x)
  (declare (xargs :guard t))
  (if (atom x)
      nil
    (cons (sexpr-rewrite-default-alist (car x))
          (sexpr-rewrite-default-alists (cdr x)))))