Struct Lit 

pub struct Lit(/* private fields */);

A SAT literal.

Note that all AIG nodes do not correspond to a SAT literal. For example, AigNode::False node do not map to any literal, but rather is omitted as false boolean variables can be removed from a clause without changing the problem. Clauses that contain a true boolean variable (ie a complemented edge to AigNode::False node) are obviously true and don’t need to be emitted.

These cases are handled by the internal LitRes data structure.

Implementations

impl Lit

pub fn get_idx(&self) -> i64

Trait Implementations

impl Clone for Lit

fn clone(&self) -> Lit

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Copy for Lit

impl Debug for Lit

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Eq for Lit

impl From<i64> for Lit

fn from(value: i64) -> Self

Converts to this type from the input type.

impl Not for Lit

type Output = Lit

The resulting type after applying the ! operator.

fn not(self) -> Self::Output

Performs the unary ! operation.

impl PartialEq for Lit

fn eq(&self, other: &Lit) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for Lit

impl TryFrom<u64> for Lit

type Error = TryFromIntError

The type returned in the event of a conversion error.

fn try_from(value: NodeId) -> Result<Self, Self::Error>

Performs the conversion.