veripb_parser/
cnf_token.rs

1//! Tokenizer for DIMACS CNF formulas.
2
3use std::num::ParseIntError;
4
5use logos::Logos;
6
7/// Tokens used in the OPB format as [specified by the PB competition 2024](https://www.cril.univ-artois.fr/PB24/OPBgeneral.pdf).
8#[derive(Debug, Logos, PartialEq, Eq)]
9#[logos(skip r"[ \t\r\n]")]
10pub enum CNFToken {
11    /// Comment lines.
12    #[regex("c.*")]
13    Comment,
14
15    /// DIMACS CNF problem header identifier.
16    #[token("p cnf")]
17    ProblemHeader,
18
19    /// Integer used to for number of variables, number of clauses, to identify literals, or to end clause.
20    #[regex("[+-]?[0-9]+", |lex| Some(lex.slice().parse()))]
21    Integer(Result<isize, ParseIntError>),
22}
23
24#[cfg(test)]
25mod test {
26    use logos::Logos;
27
28    use crate::cnf_token::CNFToken;
29
30    #[test]
31    fn comments() {
32        let mut lex = CNFToken::lexer("c adfsde\ncsdae\nc\n");
33
34        assert_eq!(lex.next(), Some(Ok(CNFToken::Comment)));
35        assert_eq!(lex.next(), Some(Ok(CNFToken::Comment)));
36        assert_eq!(lex.next(), Some(Ok(CNFToken::Comment)));
37        assert_eq!(lex.next(), None);
38    }
39
40    #[test]
41    fn header() {
42        let mut lex = CNFToken::lexer("p cnf 31 123");
43
44        assert_eq!(lex.next(), Some(Ok(CNFToken::ProblemHeader)));
45        assert_eq!(lex.next(), Some(Ok(CNFToken::Integer(Ok(31)))));
46        assert_eq!(lex.next(), Some(Ok(CNFToken::Integer(Ok(123)))));
47        assert_eq!(lex.next(), None);
48    }
49
50    #[test]
51    fn clauses() {
52        let mut lex = CNFToken::lexer("1 2 0\n2 3 0");
53
54        assert_eq!(lex.next(), Some(Ok(CNFToken::Integer(Ok(1)))));
55        assert_eq!(lex.next(), Some(Ok(CNFToken::Integer(Ok(2)))));
56        assert_eq!(lex.next(), Some(Ok(CNFToken::Integer(Ok(0)))));
57        assert_eq!(lex.next(), Some(Ok(CNFToken::Integer(Ok(2)))));
58        assert_eq!(lex.next(), Some(Ok(CNFToken::Integer(Ok(3)))));
59        assert_eq!(lex.next(), Some(Ok(CNFToken::Integer(Ok(0)))));
60        assert_eq!(lex.next(), None);
61    }
62}
veripb_parser/cnf_token.rs

veripb_parser/
cnf_token.rs
