logicaffeine_proof/
dimacs.rs

1//! DIMACS CNF parsing and printing — the SAT-competition interchange format, and the front
2//! door for running arbitrary instances through the solver.
3//!
4//! The format is a header `p cnf <num_vars> <num_clauses>`, optional `c …` comment lines,
5//! then a stream of signed integers: each clause is terminated by `0`, a clause may span
6//! several lines, and several clauses may share a line. We parse **fail-closed** — a missing
7//! or garbled header, a literal naming a variable beyond `num_vars`, a non-integer token, or
8//! a final clause with no terminating `0` is a typed error, never a quietly mangled formula.
9//!
10//! The header clause COUNT is deliberately advisory: real instances miscount and competition
11//! solvers tolerate it, so we keep the clauses we actually read rather than rejecting on a
12//! count mismatch. The variable COUNT, by contrast, bounds the literals and is enforced.
13
14use crate::cdcl::{Lit, Solver};
15
16/// A parsed CNF formula: `num_vars` variables and clauses over packed [`Lit`]s.
17#[derive(Clone, Debug, PartialEq, Eq)]
18pub struct DimacsCnf {
19    pub num_vars: usize,
20    pub clauses: Vec<Vec<Lit>>,
21}
22
23/// Why a DIMACS input was rejected. Better a typed error than a silently wrong formula.
24#[derive(Clone, Debug, PartialEq, Eq)]
25pub enum DimacsError {
26    /// Clause data appeared before any `p cnf …` header (or no header at all).
27    MissingHeader,
28    /// A header line was present but was not `p cnf <nat> <nat>`.
29    MalformedHeader(String),
30    /// A literal named `var`, whose magnitude exceeds the declared `num_vars`.
31    VarOutOfRange { var: i64, num_vars: usize },
32    /// A non-integer token appeared in the clause body.
33    InvalidToken(String),
34    /// The input ended mid-clause: literals with no terminating `0`.
35    UnterminatedClause,
36}
37
38impl DimacsCnf {
39    /// Load the clauses into a fresh [`Solver`] over `num_vars` variables.
40    pub fn into_solver(&self) -> Solver {
41        let mut s = Solver::new(self.num_vars);
42        for c in &self.clauses {
43            s.add_clause(c.clone());
44        }
45        s
46    }
47}
48
49/// Parse a DIMACS CNF string. See the module docs for the fail-closed contract.
50pub fn parse(input: &str) -> Result<DimacsCnf, DimacsError> {
51    let mut header: Option<usize> = None;
52    let mut clauses: Vec<Vec<Lit>> = Vec::new();
53    let mut current: Vec<Lit> = Vec::new();
54
55    for line in input.lines() {
56        let line = line.trim();
57        if line.is_empty() || line.starts_with('c') {
58            continue;
59        }
60        if let Some(rest) = line.strip_prefix("p ") {
61            if header.is_some() {
62                return Err(DimacsError::MalformedHeader(line.to_string()));
63            }
64            let mut it = rest.split_whitespace();
65            match (it.next(), it.next(), it.next(), it.next()) {
66                (Some("cnf"), Some(nv), Some(nc), None) => {
67                    let num_vars =
68                        nv.parse::<usize>().map_err(|_| DimacsError::MalformedHeader(line.to_string()))?;
69                    nc.parse::<usize>().map_err(|_| DimacsError::MalformedHeader(line.to_string()))?;
70                    header = Some(num_vars);
71                }
72                _ => return Err(DimacsError::MalformedHeader(line.to_string())),
73            }
74            continue;
75        }
76        // A clause-body line: a header must already have been seen.
77        let num_vars = header.ok_or(DimacsError::MissingHeader)?;
78        for tok in line.split_whitespace() {
79            let n: i64 = tok.parse().map_err(|_| DimacsError::InvalidToken(tok.to_string()))?;
80            if n == 0 {
81                clauses.push(std::mem::take(&mut current));
82            } else {
83                let v = n.unsigned_abs();
84                if v as usize > num_vars {
85                    return Err(DimacsError::VarOutOfRange { var: n, num_vars });
86                }
87                current.push(Lit::new((v - 1) as u32, n > 0));
88            }
89        }
90    }
91
92    let num_vars = header.ok_or(DimacsError::MissingHeader)?;
93    if !current.is_empty() {
94        return Err(DimacsError::UnterminatedClause);
95    }
96    Ok(DimacsCnf { num_vars, clauses })
97}
98
99/// Render a [`DimacsCnf`] back to DIMACS text. `parse(print(x)) == x`.
100pub fn print(cnf: &DimacsCnf) -> String {
101    let mut out = format!("p cnf {} {}\n", cnf.num_vars, cnf.clauses.len());
102    for clause in &cnf.clauses {
103        for l in clause {
104            let v = (l.var() + 1) as i64;
105            out.push_str(&(if l.is_positive() { v } else { -v }).to_string());
106            out.push(' ');
107        }
108        out.push_str("0\n");
109    }
110    out
111}
logicaffeine_proof/dimacs.rs

logicaffeine_proof/
dimacs.rs
