Basic functions for constructing UBDDs.

- Q-and
`(q-and &rest args)`constructs a UBDD representing the conjunction of its arguments.- Q-ite
- Optimized way to construct a new if-then-else UBDD.
- Q-or
`(q-or &rest args)`constructs a UBDD representing the disjunction of its arguments.- Q-implies
`(q-implies x y)`constructs a UBDD representing(implies x y) .- Q-iff
`(q-iff a b &rest args)`constructs a UBDD representing an equality/iff-equivalence.- Q-and-c2
`(q-and-c2 x y)`constructs a UBDD representing(and x (not y)) .- Q-and-c1
`(q-and-c1 x y)`constructs a UBDD representing(and (not x) y) .- Q-or-c2
`(q-or-c2 x y)`constructs a UBDD representing(or x (not y)) .- Q-not
- Negate a UBDD.
- Q-ite-fn
- Basic way to construct a new if-then-else UBDD.
- Q-xor
`(q-xor a b &rest args)`constructs a UBDD representing the exclusive OR of its arguments.- Cheap-and-expensive-arguments
- Sort arguments into those that we think are definitely cheap to evaluate versus those that may be expensive.
- Q-and-is-nil
`(q-and-is-nil x y)`determines whether(q-and x y) is always false.- Q-compose-list
`(q-compose-list xs l)`composes each UBDD inxs with the list of UBDDsl , i.e., it maps q-compose acrossxs .- Qv
`(qv i)`constructs a UBDD which evaluates to true exactly when thei th BDD variable is true.- Q-compose
`(q-compose x l)`composes the UBDDx with the list of UBDDsl .- Q-and-is-nilc2
`(q-and-is-nilc2 x y)`determines whether(q-and x (q-not y)) is always false.- Q-nor
`(q-nor &rest args)`constructs a UBDD representing the NOR of its arguments.- Q-nand
`(q-nand &rest args)`constructs a UBDD representing the NAND of its arguments.