pub struct Literal(/* private fields */);
Expand description
A possibly negated variable
There are three kinds of variables: constants (Literal::FALSE
and
Literal::TRUE
), circuit inputs, and gates.
Concerning ordering, the following properties hold: Given two Literal
s
a, b
, a <= b
is equivalent to the lexicographic comparison
(a.positive(), a.is_negative()) <= (b.positive(), b.is_negative())
.
Furthermore, Literal::FALSE <= a
holds (and thus Literal::TRUE <= a
if
a != Literal::FALSE
).
Implementations§
Source§impl Literal
impl Literal
Sourcepub const MAX_INPUT: usize = 4_611_686_018_427_387_901usize
pub const MAX_INPUT: usize = 4_611_686_018_427_387_901usize
Maximum input number representable as literal
Sourcepub const MAX_GATE: usize = 4_611_686_018_427_387_903usize
pub const MAX_GATE: usize = 4_611_686_018_427_387_903usize
Maximum gate number representable as literal
Sourcepub const FALSE: Self
pub const FALSE: Self
Literal representing the constant ⊥
This is literal is considered to be positive (i.e., not negated):
assert!(Literal::FALSE.is_positive());
assert!(Literal::FALSE < Literal::TRUE);
Sourcepub const TRUE: Self
pub const TRUE: Self
Literal representing the constant ⊤
This is literal is considered to be negated:
assert!(Literal::TRUE.is_negative());
assert!(Literal::TRUE < Literal::from_input(false, 0));
assert!(Literal::TRUE < Literal::from_gate(false, 0));
Sourcepub const UNDEF: Self
pub const UNDEF: Self
Undefined literal
This is considered to be a positive (i.e., not negated) input, but its
variable number is larger than Self::MAX_INPUT
. Attempting to create
this literal using Self::from_input()
will trigger a debug
assertion.
assert!(Literal::UNDEF.is_positive());
assert!(Literal::UNDEF.is_input());
assert_eq!(Literal::UNDEF.get_input(), Some(Literal::MAX_INPUT + 1));
Sourcepub const fn from_input(negative: bool, input: Var) -> Self
pub const fn from_input(negative: bool, input: Var) -> Self
Create a new literal from an input variable
Sourcepub const fn from_gate(negative: bool, gate: Var) -> Self
pub const fn from_gate(negative: bool, gate: Var) -> Self
Create a new literal from a gate number
Sourcepub const fn is_positive(self) -> bool
pub const fn is_positive(self) -> bool
Is the literal positive?
Same as !self.is_negative()
assert!(Literal::from_input(false, 42).is_positive());
assert!(!Literal::from_input(true, 1337).is_positive());
Sourcepub const fn is_negative(self) -> bool
pub const fn is_negative(self) -> bool
Is the literal negative?
Same as !self.is_positive()
assert!(Literal::from_gate(true, 42).is_negative());
assert!(!Literal::from_gate(false, 1337).is_negative());
Sourcepub const fn positive(self) -> Self
pub const fn positive(self) -> Self
Get the positive variant of this literal
assert!(Literal::from_input(true, 42).positive().is_positive());
Sourcepub const fn negative(self) -> Self
pub const fn negative(self) -> Self
Get the negative variant of this literal
assert_eq!(Literal::from_input(true, 42), Literal::from_input(false, 42).negative());
assert!(Literal::from_input(false, 42).negative().is_negative());
Sourcepub const fn is_input(self) -> bool
pub const fn is_input(self) -> bool
Does this literal refer to an input?
assert!(Literal::from_input(false, 42).is_input());
assert!(!Literal::FALSE.is_input());
assert!(!Literal::TRUE.is_input());
assert!(!Literal::from_gate(false, 1337).is_input());
Sourcepub const fn is_gate(self) -> bool
pub const fn is_gate(self) -> bool
Check if this literal refers to a gate
assert!(Literal::from_gate(false, 42).is_gate());
assert!(!Literal::FALSE.is_gate());
assert!(!Literal::TRUE.is_gate());
assert!(!Literal::from_input(false, 1337).is_gate());
Sourcepub const fn get_input(self) -> Option<Var>
pub const fn get_input(self) -> Option<Var>
Get the input number (if this literal refers to an input)
assert_eq!(Literal::from_input(false, 42).get_input(), Some(42));
assert_eq!(Literal::FALSE.get_input(), None);
assert_eq!(Literal::TRUE.get_input(), None);
assert_eq!(Literal::from_gate(false, 42).get_input(), None);
Sourcepub const fn get_gate_no(self) -> Option<Var>
pub const fn get_gate_no(self) -> Option<Var>
Get the gate number (if this literal refers to an input)
assert_eq!(Literal::from_gate(false, 42).get_gate_no(), Some(42));
assert_eq!(Literal::FALSE.get_gate_no(), None);
assert_eq!(Literal::TRUE.get_gate_no(), None);
assert_eq!(Literal::from_input(false, 42).get_gate_no(), None);
See also: Circuit::gate()
Sourcepub fn apply_gate_map(self, gate_map: &[Literal]) -> Self
pub fn apply_gate_map(self, gate_map: &[Literal]) -> Self
Map this literal based on gate_map
If this literal refers to a gate, the method performs a lookup for the
gate number in gate_map
. If the gate number is in bounds, the return
value is the mapped literal with its sign adjusted, otherwise the return
value is Literal::UNDEF
. Non-gate literals are returned as they are.