• 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
            • 4vs-not-list
            • 4vs-onehot
              • 4v-onehot-list-p
            • 4vs-ite*-list-dumb
            • 4vs-and-list-dumb
            • 4vs-not
            • 4vs-and-list
            • 4vs-and-dumb
            • 4vs-and
            • 4vs-zif-dumb
            • 4vs-z
            • 4vs-ite*-dumb
            • 4vs-x
            • 4vs-t
            • 4vs-f
            • 4vs-xor
            • 4vs-or
            • 4vs-iff
            • 4vs-buf
            • 4vs-implies-lists
            • 4vs-xor-lists
            • 4vs-or-lists
            • 4vs-or-list
            • 4vs-implies
            • 4vs-iff-lists
            • 4vs-and-lists
          • 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-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
  • 4vs-constructors
  • Onehot-rewriting

4vs-onehot

(4vs-onehot sexprs) constructs an s-expression that is T when the members of X are one-hot.

X should be a list of s-expressions, say (A1 ... AN). The s-expression we construct to check whether these are one-hot is somewhat ugly, and looks something like this:

(ITE* A1
      (AND (NOT A2) (NOT A3) ... (NOT AN))
  (ITE* A2
        (AND (NOT A3) ... (NOT AN))
    (ITE* AN
          (T)
        (F)) ...))

Note that although the printed representation is particularly large looking, the AND terms here can be mostly structure shared. For instance, the [~A2...~AN] term is really just (AND (NOT A2) [~A3...~AN]), so by honsing sexprs we get a lot of reuse here.

See also 4v-onehot-list-p.

Definitions and Theorems

Function: 4vs-onehot

(defun 4vs-onehot (sexprs)
  (declare (xargs :guard t))
  (if (atom sexprs)
      (4vs-f)
    (4vs-ite*-dumb (car sexprs)
                   (4vs-and-list-dumb (4vs-not-list (cdr sexprs)))
                   (4vs-onehot (cdr sexprs)))))

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

(defthm 4v-sexpr-eval-of-4vs-onehot
  (equal (equal (4v-sexpr-eval (4vs-onehot sexprs) env)
                *4vt*)
         (4v-onehot-list-p (4v-sexpr-eval-list sexprs env))))

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

(defthm 4v-sexpr-vars-of-4vs-onehot
  (set-equiv (4v-sexpr-vars (4vs-onehot sexprs))
             (4v-sexpr-vars-list sexprs)))

Subtopics

4v-onehot-list-p
(4v-onehot-list-p x) determines if a list of 4vps has exactly one member that is T while the rest are F.