cnf_parser/
token.rs

1use core::num::{
2    NonZeroI32,
3    NonZeroU32,
4};
5
6pub enum Token {
7    Problem(Problem),
8    Literal(Literal),
9    ClauseEnd,
10}
11
12impl From<Problem> for Token {
13    #[inline]
14    fn from(problem: Problem) -> Self {
15        Self::Problem(problem)
16    }
17}
18
19impl From<Literal> for Token {
20    #[inline]
21    fn from(literal: Literal) -> Self {
22        Self::Literal(literal)
23    }
24}
25
26/// The problem definition.
27///
28/// This is parsed at most once for every CNF input.
29/// Used to hint the underlying solver for the expected number of variables
30/// and clauses of the CNF input.
31#[derive(Debug, Copy, Clone, PartialEq, Eq)]
32pub struct Problem {
33    /// The number of variables in the CNF problem.
34    pub num_variables: u32,
35    /// The number of clauses in the CNF problem.
36    pub num_clauses: u32,
37}
38
39impl Problem {
40    /// Creates a new problem with the given variable and clause numbers.
41    pub(crate) fn new(num_variables: u32, num_clauses: u32) -> Self {
42        Self {
43            num_variables,
44            num_clauses,
45        }
46    }
47}
48
49/// A clause literal.
50#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
51pub struct Literal {
52    value: NonZeroI32,
53}
54
55impl Literal {
56    /// Creates a new literal from the given `i32` value.
57    ///
58    /// Returns `None` if `value` is zero.
59    pub(crate) fn new(value: NonZeroI32) -> Literal {
60        Self { value }
61    }
62
63    /// Returns `true` if the literal is positive.
64    #[inline]
65    pub fn is_positive(self) -> bool {
66        self.value.get().is_positive()
67    }
68
69    /// Returns `true` if the literal is negative.
70    #[inline]
71    pub fn is_negative(self) -> bool {
72        self.is_positive()
73    }
74
75    /// Returns the variable ID of the literal.
76    #[inline]
77    pub fn variable(self) -> NonZeroU32 {
78        NonZeroU32::new(self.value.get().abs() as u32)
79            .expect("encountered invalid zero literal")
80    }
81
82    /// Returns the raw value representation of the literal.
83    #[inline]
84    pub fn into_value(self) -> NonZeroI32 {
85        self.value
86    }
87}
cnf_parser/token.rs

cnf_parser/
token.rs
