veripb 3.0.2

VeriPB is a proof checker for verifying pseudo-Boolean certificates of satisfiability, unsatisfiability, and optimality bounds.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61

use std::rc::Rc;

use logos::Lexer;
use veripb_formula::prelude::DBConstraint;
use veripb_parser::error::ParserError;

use crate::prelude::*;

#[derive(Debug)]
pub struct HeaderRule;

impl HeaderRule {
    #[inline]
    pub fn parse(lex: Lexer<RuleToken>, context: &mut Context) -> Result<Self, ParserError> {
        let mut lex = lex.morph();
        context.major_version = Some(IntegerToken::parse(&mut lex)? as u8);
        // Skip the dot separating major and minor version.
        lex.bump(1);
        context.minor_version = Some(IntegerToken::parse(&mut lex)? as u8);

        Ok(HeaderRule)
    }
}

impl Rule for HeaderRule {
    #[inline]
    fn compute(
        &mut self,
        context: &mut Context,
        _database: &mut Database,
    ) -> Result<Vec<Rc<DBConstraint>>, CheckingError> {
        if context.major_version.unwrap() < 2 {
            return Err(CheckingError::UnsupportedProofVersion);
        }
        Ok(vec![])
    }
}

#[cfg(test)]
mod tests {
    use logos::Logos;
    use veripb_formula::prelude::VarNameManager;

    use crate::{args::Args, context::Context, rules::RuleToken};

    use super::HeaderRule;

    #[test]
    fn parse_version() {
        let lex = RuleToken::lexer("2.1");
        let mut context = Context::new(Args::default(), VarNameManager::default());

        assert_eq!(context.major_version, None);
        assert_eq!(context.minor_version, None);

        HeaderRule::parse(lex, &mut context).unwrap();

        assert_eq!(context.major_version, Some(2));
        assert_eq!(context.minor_version, Some(1));
    }
}