• 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-onehot-sexpr-list-prime
            • 4v-onehot-sexpr-prime
            • 4v-onehot-rw-sexpr-alist-aux
            • 4v-onehot-rw-sexpr-alist
            • 4v-onehot-rw-sexpr
            • 4vs-onehot
            • 4vs-ite*-list-dumb
            • 4v-onehot-filter
            • 4v-onehot-list-p
          • 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

• Onehot-rewriting

4v-onehot-sexpr-prime

(4v-onehot-sexpr-prime vars sexpr) rewrites sexpr under the assumption that vars are one-hot.

How is this reduction accomplished? Well, in the implementation of 4v-shannon-expansion, reduced expressions are formed by using 4v-sexpr-restrict to assume that the variable being is first true, and then false. Our approach is basically similar, and our new sexpr is essentially the following:

(ITE* A1 SEXPR|_{A1=T,A2=NIL,A3=NIL,...AN=NIL)
 (ITE* A2 SEXPR|_{A1=NIL,A2=T,A3=NIL,...AN=NIL}
  ...
   (ITE* AN SEXPR|_{A1=NIL,A2=NIL,A3=NIL,...,AN=T} (X)) ...))

We prove this produces a conservative approximation of SEXPR under the assumption that the Ai really are one-hot.

Definitions and Theorems

Function: 4v-onehot-false-bindings

(defun 4v-onehot-false-bindings (vars)
  (declare (xargs :guard t))
  (if (atom vars)
      nil
    (cons (cons (car vars) (4vs-f))
          (4v-onehot-false-bindings (cdr vars)))))

Function: 4v-onehot-sexpr-prime-aux

(defun 4v-onehot-sexpr-prime-aux (vars false-bindings sexpr)
 "Returns SEXPR'"
 (declare (xargs :guard t))
 (b* (((when (atom vars))
       (fast-alist-free false-bindings)
       (4vs-x))
      (var (car vars))
      (bindings (hons-acons var (4vs-t) false-bindings))
      (sexpr/bindings (4v-sexpr-restrict-with-rw sexpr bindings))
      (false-bindings (hons-acons var (4vs-f) bindings)))
  (4vs-ite*-dumb (car vars)
                 sexpr/bindings
                 (4v-onehot-sexpr-prime-aux (cdr vars)
                                            false-bindings sexpr))))

Function: 4v-onehot-sexpr-prime

(defun 4v-onehot-sexpr-prime (vars sexpr)
  (declare (xargs :guard (and (atom-listp vars)
                              (not (member-equal nil vars)))))
  (4v-onehot-sexpr-prime-aux
       vars
       (make-fast-alist (4v-onehot-false-bindings vars))
       sexpr))

Theorem: alist-equiv-implies-equal-4v-onehot-sexpr-prime-aux-2

(defthm alist-equiv-implies-equal-4v-onehot-sexpr-prime-aux-2
 (implies
  (alist-equiv false-bindings false-bindings-equiv)
  (equal
       (4v-onehot-sexpr-prime-aux vars false-bindings sexpr)
       (4v-onehot-sexpr-prime-aux vars false-bindings-equiv sexpr)))
 :rule-classes (:congruence))

Theorem: 4v-sexpr-eval-of-4v-onehot-sexpr-prime

(defthm 4v-sexpr-eval-of-4v-onehot-sexpr-prime
  (implies (and (4v-onehot-list-p (4v-sexpr-eval-list vars env))
                (atom-listp vars)
                (not (member-equal nil vars)))
           (4v-<= (4v-sexpr-eval (4v-onehot-sexpr-prime vars sexpr)
                                 env)
                  (4v-sexpr-eval sexpr env))))

Theorem: 4v-sexpr-vars-of-4v-onehot-sexpr-prime

(defthm 4v-sexpr-vars-of-4v-onehot-sexpr-prime
 (implies
   (atom-listp vars)
   (subsetp-equal (4v-sexpr-vars (4v-onehot-sexpr-prime vars sexpr))
                  (append vars (4v-sexpr-vars sexpr)))))