veripb_parser/
opb_token.rs

1//! Tokenizer for constraints in OPB format.
2
3use logos::Logos;
4
5/// Tokens used in the OPB format as [specified by the PB competition 2024](https://www.cril.univ-artois.fr/PB24/OPBgeneral.pdf).
6#[derive(Debug, Logos, PartialEq, Eq)]
7#[logos(skip r"[ \t\r\n]")]
8pub enum OPBToken {
9    /// Comment lines.
10    #[regex("\\*.*")]
11    Comment,
12
13    /// Integer used for coefficients or degree (right-hand side).
14    #[regex("[+-]?[0-9]+")]
15    Integer,
16
17    /// OPB variable.
18    #[regex("[a-zA-Z_][_a-zA-Z0-9\\-\\^\\[\\]\\{\\}]+")]
19    Var,
20
21    /// Negation symbol for a literal.
22    #[token("~")]
23    Negation,
24
25    /// Greater than or equal comparison for PB constraint.
26    #[token(">=")]
27    GreaterEqual,
28
29    /// Less than or equal comparison for PB constraint.
30    #[token("<=")]
31    LessEqual,
32
33    /// Equal comparison for PB constraint.
34    #[token("=")]
35    Equal,
36
37    /// Semicolon which should end a PB constraint.
38    #[token(";")]
39    Semicolon,
40
41    /// Label to start the objective function that should be minimized.
42    #[token("min:")]
43    Minimize,
44
45    /// Label to start the objective function that should be maximized. While we support maximization objectives in the OPB file, internally the objective is always minimized.
46    #[token("max:")]
47    Maximize,
48
49    /// Constraint labels similar to the ones used in the proof format.
50    #[regex("@[a-zA-Z0-9_^\\[\\]\\{\\}]+")]
51    Label,
52}
53
54#[cfg(test)]
55mod test {
56    use logos::Logos;
57
58    use crate::opb_token::OPBToken;
59
60    #[test]
61    fn integer() {
62        let mut lex = OPBToken::lexer("424 -424 +424 +004");
63
64        assert_eq!(lex.next(), Some(Ok(OPBToken::Integer)));
65        assert_eq!(lex.next(), Some(Ok(OPBToken::Integer)));
66        assert_eq!(lex.next(), Some(Ok(OPBToken::Integer)));
67        assert_eq!(lex.next(), Some(Ok(OPBToken::Integer)));
68        assert_eq!(lex.slice().parse::<i64>().unwrap(), 4);
69        assert_eq!(lex.next(), None);
70    }
71
72    #[test]
73    fn variable() {
74        let mut lex = OPBToken::lexer("x12 _x12 xaK2-[]{}_^");
75
76        assert_eq!(lex.next(), Some(Ok(OPBToken::Var)));
77        assert_eq!(lex.next(), Some(Ok(OPBToken::Var)));
78        assert_eq!(lex.next(), Some(Ok(OPBToken::Var)));
79        assert_eq!(lex.next(), None);
80    }
81
82    #[test]
83    fn comment() {
84        let mut lex = OPBToken::lexer("*sdf sdafsd ffsdf sdf asdf dsfsdf 12 sda f\n*\n11");
85
86        assert_eq!(lex.next(), Some(Ok(OPBToken::Comment)));
87        assert_eq!(lex.next(), Some(Ok(OPBToken::Comment)));
88        assert_eq!(lex.next(), Some(Ok(OPBToken::Integer)));
89        assert_eq!(lex.next(), None);
90    }
91}
veripb_parser/opb_token.rs

veripb_parser/
opb_token.rs
