veripb_parser/
cnf_parser.rs

1//! Parsing functions for DIMACS CNF format.
2//!
3//! The DIMACS CNF format is used to represent SAT formulas in CNF. It was first used in the 2nd DIMACS implementation challenge.
4//!
5//! Tokenization is performed using [`CNFToken`].
6
7use logos::{Lexer, Logos};
8use std::path::Path;
9use veripb_formula::prelude::*;
10
11use crate::{cnf_token::CNFToken, error::ParserError, parser::get_lines};
12
13/// Parse a formula from a DIMACS CNF file.
14pub fn parse_cnf_from_file<P>(filename: P) -> Result<(Formula, usize), ParserError>
15where
16    P: AsRef<Path>,
17{
18    let mut database = Formula::default();
19    let mut num_vars = 0;
20    let lines = get_lines(&filename)?;
21    let mut parsed_header = false;
22    let mut current_lits = Vec::new();
23
24    for (line_number, line) in lines.map_while(Result::ok).enumerate() {
25        let mut lex = CNFToken::lexer(&line);
26
27        if parsed_header {
28            while let Some(token) = lex.next() {
29                match token {
30                    Ok(CNFToken::Integer(Ok(integer))) => match integer {
31                        0 => {
32                            let clause =
33                                Clause::from_unnormalized_lits(current_lits.clone()).into();
34                            database.constraints.push(clause);
35                            current_lits.clear();
36                        }
37                        ..0 => {
38                            current_lits.push(Lit::from_var((-integer) as usize, true));
39                        }
40                        1.. => {
41                            current_lits.push(Lit::from_var((integer) as usize, false));
42                        }
43                    },
44                    Ok(CNFToken::Integer(Err(_))) => {
45                        return Err(ParserError::token_error_with_file(
46                            lex.span(),
47                            "64 bit integer",
48                            filename.as_ref().to_string_lossy().to_string(),
49                            line_number,
50                        ))
51                    }
52                    Ok(CNFToken::Comment) => {}
53                    _ => {
54                        return Err(ParserError::token_error_with_file(
55                            lex.span(),
56                            "integer or comment",
57                            filename.as_ref().to_string_lossy().to_string(),
58                            line_number,
59                        ));
60                    }
61                }
62            }
63        } else {
64            match lex.next() {
65                Some(Ok(CNFToken::ProblemHeader)) => {
66                    let header = parse_header(&mut lex).map_err(|e| {
67                        e.add_file_and_line(
68                            filename.as_ref().to_string_lossy().to_string(),
69                            line_number,
70                        )
71                        .unwrap()
72                    })?;
73                    num_vars = header.0;
74                    database.reserve_exact(header.1);
75                    parsed_header = true;
76                }
77                Some(Ok(CNFToken::Comment)) => {}
78                _ => {
79                    return Err(ParserError::token_error_with_file(
80                        lex.span(),
81                        "CNF header or comment",
82                        filename.as_ref().to_string_lossy().to_string(),
83                        line_number,
84                    ));
85                }
86            }
87        }
88    }
89
90    if parsed_header {
91        Ok((database, num_vars))
92    } else {
93        Err(ParserError::NoHeader)
94    }
95}
96
97/// Parse the problem header of an DIMACS CNF file.
98#[inline]
99fn parse_header(lex: &mut Lexer<CNFToken>) -> Result<(usize, usize), ParserError> {
100    if let Some(Ok(CNFToken::Integer(Ok(num_vars)))) = lex.next() {
101        if let Some(Ok(CNFToken::Integer(Ok(num_clauses)))) = lex.next() {
102            return Ok((num_vars as usize, num_clauses as usize));
103        }
104    }
105
106    Err(ParserError::token_error(lex.span(), "integer in isize"))
107}
veripb_parser/cnf_parser.rs

veripb_parser/
cnf_parser.rs
