veripb_parser/
wcnf_token.rs

1//! Tokenizer for WCNF MaxSAT files.
2
3use logos::Logos;
4
5/// Tokens used in the OPB format as specified by the [MaxSAT Evaluation 2022](https://maxsat-evaluations.github.io/2022/rules.html#input).
6#[derive(Debug, Logos, PartialEq, Eq)]
7#[logos(skip r"[ \t\r\n]")]
8pub enum WCNFToken {
9    /// Comment lines.
10    #[regex("c.*")]
11    Comment,
12
13    /// Identifier for a hard clause.
14    #[token("h")]
15    HardClause,
16
17    /// Integer used to identify literals or end clauses.
18    #[regex("[+-]?[0-9]+")]
19    Integer,
20}
21
22#[cfg(test)]
23mod test {
24    use logos::Logos;
25
26    use crate::wcnf_token::WCNFToken;
27
28    #[test]
29    fn comments() {
30        let mut lex = WCNFToken::lexer("c adfsde\ncsdae\nc\n");
31
32        assert_eq!(lex.next(), Some(Ok(WCNFToken::Comment)));
33        assert_eq!(lex.next(), Some(Ok(WCNFToken::Comment)));
34        assert_eq!(lex.next(), Some(Ok(WCNFToken::Comment)));
35        assert_eq!(lex.next(), None);
36    }
37
38    #[test]
39    fn hard_clause() {
40        let mut lex = WCNFToken::lexer("h 31 123 0");
41
42        assert_eq!(lex.next(), Some(Ok(WCNFToken::HardClause)));
43        assert_eq!(lex.next(), Some(Ok(WCNFToken::Integer)));
44        assert_eq!(lex.next(), Some(Ok(WCNFToken::Integer)));
45        assert_eq!(lex.next(), Some(Ok(WCNFToken::Integer)));
46        assert_eq!(lex.next(), None);
47    }
48
49    #[test]
50    fn soft_clauses() {
51        let mut lex = WCNFToken::lexer("-23442 1 2 0");
52
53        assert_eq!(lex.next(), Some(Ok(WCNFToken::Integer)));
54        assert_eq!(lex.next(), Some(Ok(WCNFToken::Integer)));
55        assert_eq!(lex.next(), Some(Ok(WCNFToken::Integer)));
56        assert_eq!(lex.next(), Some(Ok(WCNFToken::Integer)));
57        assert_eq!(lex.next(), None);
58    }
59}
veripb_parser/wcnf_token.rs

veripb_parser/
wcnf_token.rs
