• 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
            • 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
  • 4v-sexprs

4vs-constructors

Primitive functions for constructing 4v-sexprs.

Note that all of these operations use hons so that the S-Expressions they produce are structure shared.

These functions carry out a few trivial rewrites (constant folding, double negation elimination). An open question: how much rewriting should they do? Right now I don't try to optimize very aggressively, e.g., 4vs-and doesn't eat bufs. It's not clear how much of the code from sexpr-rewrite should be duplicated here.

Subtopics

4vs-not-list
(4vs-not-list x) maps 4vs-not across a list.
4vs-onehot
(4vs-onehot sexprs) constructs an s-expression that is T when the members of X are one-hot.
4vs-ite*-list-dumb
(4vs-ite*-list-dumb c as bs) produces a list of sexprs, basically (4V-ITE* C Ai Bi) for the corresponding elements of AS and BS.
4vs-and-list-dumb
(4vs-and-list-dumb sexprs) reduction ands together all the sexprs in the list x, producing a single sexpr representing their conjunction.
4vs-not
(4vs-not a) constructs a 4v-sexpr equivalent to (not a).
4vs-and-list
(4vs-and-list sexprs) reduction ands together all the sexprs in the list x, producing a single sexpr representing their conjunction.
4vs-and-dumb
(4vs-and-dumb a b) constructs exactly the 4v-sexpr (and a b).
4vs-and
(4vs-and a b) constructs a 4v-sexpr equivalent to (and a b).
4vs-zif-dumb
(4vs-zif-dumb c a b) constructs (ZIF C A B), i.e., the s-expression for an pass-gate style multiplexor.
4vs-z
(4vs-z) returns (Z), the s-expression for a constant undriven/floating value.
4vs-ite*-dumb
(4vs-ite*-dumb c a b) constructs (ITE* C A B), i.e., the s-expression for a conservative multiplexor.
4vs-x
(4vs-x) returns (X), the s-expression for a constant unknown value.
4vs-t
(4vs-t) returns (T), the s-expression for a constant true value.
4vs-f
(4vs-f) returns (F), the s-expression for a constant false value.
4vs-xor
(4vs-xor a b) constructs a sexpr representing (xor a b).
4vs-or
(4vs-or a b) constructs a 4v-sexpr equivalent to (or a b).
4vs-iff
(4vs-iff a b) constructs a sexpr representing (iff a b).
4vs-buf
(4vs-buf a) constructs a 4v-sexpr equivalent to (buf a).
4vs-implies-lists
(4vs-implies-lists x y) pairwise impliess together the sexprs from the lists x and y, forming a new sexpr list.
4vs-xor-lists
(4vs-xor-lists x y) pairwise xors together the sexprs from two separate lists, forming a new sexpr list.
4vs-or-lists
(4vs-or-lists x y) pairwise ors together the sexprs from two separate lists, forming a new sexpr list.
4vs-or-list
(4vs-or-list x) reduction ors together all the sexprs in the list x, producing a single sexpr representing their disjunction.
4vs-implies
(4vs-implies a b) constructs a new sexpr representing (implies a b).
4vs-iff-lists
(4vs-iff-lists x y) pairwise iffs together the sexprs from the lists x and y, forming a new sexpr list.
4vs-and-lists
(4vs-and-lists x y) pairwise ands together the sexprs from two separate lists, forming a new sexpr list.