• 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

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