Ubdd-constructors
Basic functions for constructing UBDDs.
Subtopics
- 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 in xs with the list of
UBDDs l, i.e., it maps q-compose across xs.
- Qv
- (qv i) constructs a UBDD which evaluates to true exactly when the
ith BDD variable is true.
- Q-compose
- (q-compose x l) composes the UBDD x with the list of UBDDs
l.
- 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.
