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

• Sexpr-rewriting

4v-shannon-expansion

A conservative transformation of an s-expression that pulls a particular variable out into a top-level if-then-else.

The shannon expansion of a term M by a Boolean variable V is

if V then M' else M'',

where M' is formed from M by substituting true for V and M'' is formed by subsituting false for V.

For 4-valued terms we need to make a slight adjustment, because in the case where V is X, this doesn't work. Instead, the term we get looks like:

(XOR (XOR V V) (ITE V M' M'')).

Here the term (XOR V V) detects the case where V is X or Z, and XORing that with the if-then-else term makes the whole result X in that case.

This is useful for certain cases where a term may have false dependencies. Consider

(ITE V (ITE (NOT V) A B) C).

Intuitively, we'd think that the A branch wouldn't have any relevance, since we can only get there by going through a V and a (NOT V) test, which are contradictory. But in fact there is a case where A affects the result: when B and C are the same Boolean value and V=X. Then, if A is the same Boolean value as B and C, then the result is that value, otherwise X. But we may be willing to give up this special case and allow the term to evaluate to X whenever V is X, in exchange for getting rid of the dependency on A. The Shannon expansion (if combined with rewriting) accomplishes this: the Shannon-rewritten version of the term above looks like:

(XOR (XOR V V)
     (ITE (T) (ITE (NOT (T)) A B) C)
     (ITE (F) (ITE (NOT (F)) A B) C))

which rewrites to

(XOR (XOR V V) B C).

Definitions and Theorems

Function: 4v-shannon-expansion-true-al

(defun 4v-shannon-expansion-true-al (var)
       (declare (xargs :guard t))
       (hons-acons var *4vt-sexpr* nil))

Function: 4v-shannon-expansion-false-al

(defun 4v-shannon-expansion-false-al (var)
       (declare (xargs :guard t))
       (hons-acons var *4vf-sexpr* nil))

Function: 4v-shannon-expansion-few

(defun
 4v-shannon-expansion-few (var x)
 (declare (xargs :guard t))
 (b*
  ((true-al (4v-shannon-expansion-true-al var))
   (true-br (4v-sexpr-restrict x true-al))
   ((when (hons-equal true-br x)) x)
   (false-al (4v-shannon-expansion-false-al var))
   (false-br (4v-sexpr-restrict x false-al)))
  (cons
       'xor
       (cons (cons 'xor (cons var (cons var 'nil)))
             (cons (cons 'ite
                         (cons var
                               (cons true-br (cons false-br 'nil))))
                   'nil)))))

Function: 4v-shannon-expansion-many

(defun
 4v-shannon-expansion-many (var x)
 (declare (xargs :guard t))
 (b*
  ((vars (4v-sexpr-vars x))
   ((unless (gentle-member var vars)) x)
   (true-al (4v-shannon-expansion-true-al var))
   (true-br (4v-sexpr-restrict x true-al))
   (false-al (4v-shannon-expansion-false-al var))
   (false-br (4v-sexpr-restrict x false-al)))
  (cons
       'xor
       (cons (cons 'xor (cons var (cons var 'nil)))
             (cons (cons 'ite
                         (cons var
                               (cons true-br (cons false-br 'nil))))
                   'nil)))))

Theorem: 4v-sexpr-eval-with-redundant-cons

(defthm 4v-sexpr-eval-with-redundant-cons
        (implies (equal (cdr (hons-assoc-equal v env))
                        val)
                 (equal (4v-sexpr-eval x (cons (cons v val) env))
                        (4v-sexpr-eval x env))))

Theorem: 4v-sexpr-eval-list-with-redundant-cons

(defthm
     4v-sexpr-eval-list-with-redundant-cons
     (implies (equal (cdr (hons-assoc-equal v env))
                     val)
              (equal (4v-sexpr-eval-list x (cons (cons v val) env))
                     (4v-sexpr-eval-list x env))))

Theorem: 4v-sexpr-eval-with-non-variable-cons

(defthm 4v-sexpr-eval-with-non-variable-cons
        (implies (consp v)
                 (equal (4v-sexpr-eval x (cons (cons v val) env))
                        (4v-sexpr-eval x env))))

Theorem: 4v-sexpr-eval-list-with-non-variable-cons

(defthm
     4v-sexpr-eval-list-with-non-variable-cons
     (implies (consp v)
              (equal (4v-sexpr-eval-list x (cons (cons v val) env))
                     (4v-sexpr-eval-list x env))))

Theorem: rewrite-ite-by-var-ok-simpl

(defthm
   rewrite-ite-by-var-ok-simpl
   (4v-<= (4v-xor (4v-xor (4v-sexpr-eval v env)
                          (4v-sexpr-eval v env))
                  (4v-ite (4v-sexpr-eval v env)
                          (4v-sexpr-eval a (cons (cons v t) env))
                          (4v-sexpr-eval b (cons (cons v 'f) env))))
          (4v-ite (4v-sexpr-eval v env)
                  (4v-sexpr-eval a env)
                  (4v-sexpr-eval b env))))

Theorem: rewrite-ite-by-var-ok

(defthm
 rewrite-ite-by-var-ok
 (4v-<=
  (4v-sexpr-eval
   (cons
    'xor
    (cons
     (cons 'xor (cons v (cons v 'nil)))
     (cons
      (cons
       'ite
       (cons
         v
         (cons (4v-sexpr-restrict a (cons (cons v '(t)) 'nil))
               (cons (4v-sexpr-restrict b (cons (cons v '(f)) 'nil))
                     'nil))))
      'nil)))
   env)
  (4v-sexpr-eval (cons 'ite
                       (cons v (cons a (cons b 'nil))))
                 env)))

Theorem: 4v-sexpr-vars-4v-shannon-expansion-few

(defthm
 4v-sexpr-vars-4v-shannon-expansion-few
 (implies
      (and (not (member-equal k (4v-sexpr-vars x)))
           (atom var))
      (not (member-equal
                k
                (4v-sexpr-vars (4v-shannon-expansion-few var x))))))

Theorem: 4v-shannon-expansion-few-correct

(defthm 4v-shannon-expansion-few-correct
        (4v-<= (4v-sexpr-eval (4v-shannon-expansion-few var x)
                              env)
               (4v-sexpr-eval x env)))

Theorem: 4v-shannon-expansion-many-correct

(defthm 4v-shannon-expansion-many-correct
        (4v-<= (4v-sexpr-eval (4v-shannon-expansion-many var x)
                              env)
               (4v-sexpr-eval x env)))

Function: 4v-shannon-expansion-mode-p

(defun 4v-shannon-expansion-mode-p (x)
       (declare (xargs :guard t))
       (or (eq x :few-vars) (eq x :many-vars)))

Function: 4v-shannon-expansion-list

(defun 4v-shannon-expansion-list (sigs x mode)
       (declare (xargs :guard (4v-shannon-expansion-mode-p mode)))
       (b* (((when (atom sigs)) x)
            (x (4v-shannon-expansion-list (cdr sigs)
                                          x mode)))
           (if (eq mode :few-vars)
               (4v-shannon-expansion-few (car sigs) x)
               (4v-shannon-expansion-many (car sigs)
                                          x))))

Theorem: 4v-sexpr-vars-4v-shannon-expansion-list

(defthm
 4v-sexpr-vars-4v-shannon-expansion-list
 (implies
  (and (atom-listp sigs)
       (not (member-equal k (4v-sexpr-vars x))))
  (not
    (member-equal
         k
         (4v-sexpr-vars (4v-shannon-expansion-list sigs x mode))))))

Theorem: 4v-shannon-expansion-list-correct

(defthm
     4v-shannon-expansion-list-correct
     (4v-<= (4v-sexpr-eval (4v-shannon-expansion-list vars x mode)
                           env)
            (4v-sexpr-eval x env)))

Theorem: 4v-shannon-expansion-list-conservative

(defthm 4v-shannon-expansion-list-conservative
        (4v-sexpr-<= (4v-shannon-expansion-list vars x mode)
                     x))

Function: rewrite-with-shannon-expansion

(defun rewrite-with-shannon-expansion
       (vars x mode)
       (declare (xargs :guard (4v-shannon-expansion-mode-p mode)))
       (b* ((x (4v-shannon-expansion-list vars x mode)))
           (sexpr-rewrite x *sexpr-rewrites*)))

Theorem: rewrite-with-shannon-expansion-conservative

(defthm rewrite-with-shannon-expansion-conservative
        (4v-sexpr-<= (rewrite-with-shannon-expansion vars x mode)
                     x))

Theorem: 4v-sexpr-vars-rewrite-with-shannon-expansion

(defthm
 4v-sexpr-vars-rewrite-with-shannon-expansion
 (implies
  (and (atom-listp vars)
       (not (member-equal k (4v-sexpr-vars x))))
  (not
   (member-equal
    k
    (4v-sexpr-vars (rewrite-with-shannon-expansion vars x mode))))))

Function: rewrite-with-shannon-expansion-alist-main

(defun
   rewrite-with-shannon-expansion-alist-main
   (vars x mode)
   (declare (xargs :guard (4v-shannon-expansion-mode-p mode)))
   (b* (((when (atom x)) nil)
        ((when (atom (car x)))
         (rewrite-with-shannon-expansion-alist-main vars (cdr x)
                                                    mode)))
       (cons (cons (caar x)
                   (rewrite-with-shannon-expansion vars (cdar x)
                                                   mode))
             (rewrite-with-shannon-expansion-alist-main vars (cdr x)
                                                        mode))))

Theorem: 4v-sexpr-vars-rewrite-with-shannon-expansion-alist-main

(defthm
 4v-sexpr-vars-rewrite-with-shannon-expansion-alist-main
 (implies
  (and (atom-listp vars)
       (not (member-equal k (4v-sexpr-vars-list (alist-vals x)))))
  (not
   (member-equal
    k
    (4v-sexpr-vars-list
     (alist-vals
       (rewrite-with-shannon-expansion-alist-main vars x mode)))))))

Theorem: rewrite-with-shannon-expansion-alist-main-conservative

(defthm rewrite-with-shannon-expansion-alist-main-conservative
        (4v-sexpr-alist-<=
             (rewrite-with-shannon-expansion-alist-main vars x mode)
             x))

Theorem: alist-keys-rewrite-with-shannon-expansion-alist-main

(defthm
  alist-keys-rewrite-with-shannon-expansion-alist-main
  (equal
       (alist-keys
            (rewrite-with-shannon-expansion-alist-main vars x mode))
       (alist-keys x)))

Function: rewrite-with-shannon-expansion-alist

(defun
 rewrite-with-shannon-expansion-alist
 (vars x mode)
 (declare (xargs :guard (4v-shannon-expansion-mode-p mode)))
 (mbe
  :logic (rewrite-with-shannon-expansion-alist-main vars x mode)
  :exec
  (b*
     ((ans (rewrite-with-shannon-expansion-alist-main vars x mode)))
     (clear-memoize-table '4v-shannon-expansion-true-al)
     (clear-memoize-table '4v-shannon-expansion-false-al)
     (clear-memoize-table '4v-sexpr-restrict)
     (clear-memoize-table 'sexpr-rewrite)
     ans)))