stalmarck_sat/parser/
dimacs.rs

1use std::fs::File;
2use std::io::{BufRead, BufReader};
3use std::path::Path;
4
5use crate::core::formula::Formula;
6use crate::Result;
7
8/// Parser for DIMACS CNF format
9#[derive(Debug, Default)]
10pub struct Parser {
11    error_message: String,
12    has_error_flag: bool,
13}
14
15impl Parser {
16    /// Create a new parser instance
17    pub fn new() -> Self {
18        Self::default()
19    }
20
21    /// Parse a DIMACS CNF file
22    pub fn parse_dimacs<P: AsRef<Path>>(&mut self, _path: P) -> Result<Formula> {
23        // Reset error state
24        self.error_message.clear();
25        self.has_error_flag = false;
26
27        // Open the file
28        let file = match File::open(_path) {
29            Ok(file) => file,
30            Err(e) => {
31                self.error_message = format!("Failed to open file: {}", e);
32                self.has_error_flag = true;
33                return Err(crate::Error::Io(e));
34            }
35        };
36
37        // Read the file
38        let reader = BufReader::new(file);
39        let mut formula = Formula::new();
40
41        // Process each line
42        for (line_num, line_result) in reader.lines().enumerate() {
43            // Read the line
44            let line = match line_result {
45                Ok(line) => line,
46                Err(e) => {
47                    self.error_message = format!("Error reading line {}: {}", line_num + 1, e);
48                    self.has_error_flag = true;
49                    return Err(crate::Error::Io(e));
50                }
51            };
52
53            let line = line.trim();
54
55            // Skip empty lines and comments
56            if line.is_empty() || line.starts_with('c') {
57                continue;
58            }
59
60            // Parse the problem line
61            if line.starts_with('p') {
62                let tokens: Vec<&str> = line.split_whitespace().collect();
63                if tokens.len() >= 4 && tokens[1] == "cnf" {
64                    if let Ok(num_vars) = tokens[2].parse::<usize>() {
65                        formula.set_num_variables(num_vars);
66
67                        // Also parse the number of clauses and reserve space
68                        if let Ok(num_clauses) = tokens[3].parse::<usize>() {
69                            formula.reserve_clauses(num_clauses);
70                        } else {
71                            self.error_message =
72                                format!("Invalid number of clauses in line {}", line_num + 1);
73                            self.has_error_flag = true;
74                            return Err(crate::Error::Parse(self.error_message.clone()));
75                        }
76                    } else {
77                        self.error_message =
78                            format!("Invalid number of variables in line {}", line_num + 1);
79                        self.has_error_flag = true;
80                        return Err(crate::Error::Parse(self.error_message.clone()));
81                    }
82                }
83                continue;
84            }
85
86            // Add clause to formula
87            let mut clause = Vec::new();
88
89            for token in line.split_whitespace() {
90                let literal = match token.parse::<i32>() {
91                    Ok(literal) => literal,
92                    Err(e) => {
93                        self.error_message =
94                            format!("Invalid literal in line {}: {}", line_num + 1, e);
95                        self.has_error_flag = true;
96                        return Err(crate::Error::Parse(self.error_message.clone()));
97                    }
98                };
99
100                // Stop parsing if we encounter 0
101                if literal == 0 {
102                    break;
103                }
104
105                // Push literal to clause
106                clause.push(literal);
107            }
108
109            // Push clause to formula
110            if !clause.is_empty() {
111                formula.add_clause(clause);
112            }
113        }
114
115        // Just return the empty formula for now
116        Ok(formula)
117    }
118
119    /// Check if the parser encountered an error
120    pub fn has_error(&self) -> bool {
121        self.has_error_flag
122    }
123
124    /// Get the error message if there was an error
125    pub fn get_error(&self) -> &str {
126        &self.error_message
127    }
128}
stalmarck_sat/parser/dimacs.rs

stalmarck_sat/parser/
dimacs.rs
