#[repr(u8)]pub enum BCDDOp {
Show 15 variants
And = 0,
Xor = 1,
Ite = 2,
Substitute = 3,
Restrict = 4,
Forall = 5,
Exists = 6,
Unique = 7,
ForallAnd = 8,
ForallXor = 9,
ExistAnd = 10,
ExistXor = 11,
UniqueAnd = 12,
UniqueNand = 13,
UniqueXor = 14,
}Expand description
Native operators of this BDD implementation
Variants§
And = 0
Xor = 1
Ite = 2
If-then-else
Substitute = 3
Restrict = 4
Forall = 5
Forall quantification
Exists = 6
Existential quantification
Unique = 7
Unique quantification
ForallAnd = 8
ForallXor = 9
ExistAnd = 10
ExistXor = 11
UniqueAnd = 12
UniqueNand = 13
Usually, we don’t need ⊼ since we have ∧ and a cheap ¬ operation.
However, ∃! v. ¬φ is not equivalent to ¬∃! v. φ, so we use
∃! v. φ ⊼ ψ (i.e., a special ⊼ operator) for the combined
apply-quantify algorithm.
UniqueXor = 14
Trait Implementations§
Source§impl Ord for BCDDOp
impl Ord for BCDDOp
Source§impl PartialOrd for BCDDOp
impl PartialOrd for BCDDOp
impl Copy for BCDDOp
impl Eq for BCDDOp
impl StructuralPartialEq for BCDDOp
Auto Trait Implementations§
impl Freeze for BCDDOp
impl RefUnwindSafe for BCDDOp
impl Send for BCDDOp
impl Sync for BCDDOp
impl Unpin for BCDDOp
impl UnwindSafe for BCDDOp
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more