solhop_types/
dimacs.rs

1use crate::{Lit, Var};
2use regex::Regex;
3use std::io::BufRead;
4
5/// Dimacs formula.
6#[derive(Debug, PartialEq, Clone)]
7pub enum Dimacs {
8    /// Unweighted formula.
9    Cnf {
10        /// Number of variables.
11        n_vars: usize,
12        /// Clauses.
13        clauses: Vec<Vec<Lit>>,
14    },
15    /// Weighted formula.
16    Wcnf {
17        /// Number of variables.
18        n_vars: usize,
19        /// Clauses with their weights.
20        clauses: Vec<(Vec<Lit>, u64)>,
21        /// Weight corresponding to hard clause.
22        hard_weight: Option<u64>,
23    },
24}
25
26/// Parse dimacs from buffer reader.
27pub fn parse_dimacs_from_buf_reader<F>(reader: &mut F) -> Dimacs
28where
29    F: std::io::BufRead,
30{
31    let mut n_clauses = 0usize;
32    let mut n_vars = 0usize;
33    let mut clauses = vec![];
34    let mut weights: Vec<u64> = vec![];
35    let mut hard_weight = None;
36    let mut is_wcnf = false;
37
38    for line in reader.lines() {
39        let line = line.unwrap();
40        let line = line.trim();
41        if line.is_empty() {
42            continue;
43        }
44        if line.starts_with('c') {
45            continue;
46        } else if line.starts_with('p') {
47            let re_cnf = Regex::new(r"^p\s+cnf\s+(\d+)\s+(\d+)").unwrap();
48            let re_wcnf = Regex::new(r"^p\s+wcnf\s+(\d+)\s+(\d+)(?:\s+(\d+))?").unwrap();
49            if let Some(cap) = re_cnf.captures(&line) {
50                n_vars = cap[1].parse().unwrap();
51                n_clauses = cap[2].parse().unwrap();
52            } else if let Some(cap) = re_wcnf.captures(&line) {
53                is_wcnf = true;
54                n_vars = cap[1].parse().unwrap();
55                n_clauses = cap[2].parse().unwrap();
56                hard_weight = cap.get(3).map(|m| m.as_str().parse().unwrap()); // cap[3].parse().unwrap();
57            }
58        } else {
59            let re = Regex::new(r"(-?\d+)").unwrap();
60            let mut cl = vec![];
61            let mut weight = 0u64;
62            for (i, cap) in re.captures_iter(&line).enumerate() {
63                if i == 0 && is_wcnf {
64                    weight = cap[1].parse::<u64>().unwrap();
65                    continue;
66                }
67                let l = match cap[1].parse::<i32>().unwrap() {
68                    0 => continue,
69                    n => n,
70                };
71                let var = Var::new((l.abs() - 1) as usize);
72                let lit = if l > 0 { var.pos_lit() } else { var.neg_lit() };
73                cl.push(lit);
74            }
75            clauses.push(cl);
76            weights.push(weight);
77            if clauses.len() == n_clauses {
78                break;
79            }
80        }
81    }
82
83    if is_wcnf {
84        Dimacs::Wcnf {
85            n_vars,
86            clauses: clauses.into_iter().zip(weights).collect(),
87            hard_weight,
88        }
89    } else {
90        Dimacs::Cnf { n_vars, clauses }
91    }
92}
93
94/// Parse a cnf/wcnf dimacs file.
95pub fn parse_dimacs_from_file(filename: &std::path::Path) -> Dimacs {
96    let file = std::fs::File::open(filename).expect("File not found");
97    let mut reader = std::io::BufReader::new(file);
98    parse_dimacs_from_buf_reader(&mut reader)
99}
100
101#[cfg(test)]
102mod tests {
103    use super::*;
104    #[test]
105    fn it_works() {
106        let wcnf = "p wcnf 1 2\n\
107        2 1 0\n\
108        3 -1 0
109        ";
110        let var_1 = Var::new(0);
111        assert_eq!(
112            parse_dimacs_from_buf_reader(&mut std::io::BufReader::new(wcnf.as_bytes())),
113            Dimacs::Wcnf {
114                n_vars: 1,
115                hard_weight: None,
116                clauses: vec![(vec![var_1.pos_lit()], 2), (vec![var_1.neg_lit()], 3)]
117            }
118        );
119    }
120}
solhop_types/dimacs.rs

solhop_types/
dimacs.rs
