|
|
@ -16,6 +16,22 @@ struct CNF {
|
|
16
|
16
|
clauses: Vec<Vec<i32>>
|
|
17
|
17
|
}
|
|
18
|
18
|
|
|
|
19
|
/// Parses a CNF formula in DIMAC format.
|
|
|
20
|
///
|
|
|
21
|
/// # Examples
|
|
|
22
|
///
|
|
|
23
|
/// A simple example for a formula in DIMAC format is below:
|
|
|
24
|
///
|
|
|
25
|
/// ```text
|
|
|
26
|
/// p cnf 5 3
|
|
|
27
|
/// 1 2 3 0
|
|
|
28
|
/// -2 3 4 0
|
|
|
29
|
/// 4 5 0
|
|
|
30
|
/// ```
|
|
|
31
|
///
|
|
|
32
|
/// The above represents a formula with 5 variables and 3 clauses. The first
|
|
|
33
|
/// line specifies this. Each following line represents a clause with possibly
|
|
|
34
|
/// negated literals, terminated by 0 and a newline.
|
|
19
|
35
|
fn parse_dimac(dimac: &str) -> Result<CNF, String> {
|
|
20
|
36
|
let mut lines = dimac.lines();
|
|
21
|
37
|
let mut num_vars;
|