veripb-parser 0.1.2

VeriPB parsing library for OPB, WCNF, and DIMACS CNF formats.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70

use veripb_formula::prelude::PBConstraint;
use veripb_parser::cnf_parser::parse_cnf_from_file;

#[test]
fn parse_cnf_normal() {
    let (formula, num_vars) = match parse_cnf_from_file("./tests/instances/cnf_normal.cnf") {
        Ok(formula) => formula,
        Err(e) => {
            eprintln!("Parsing error: {e:?}");
            panic!();
        }
    };

    assert_eq!(formula.len(), 2, "Formula should contain 2 clauses.");
    assert_eq!(num_vars, 3, "Formula should contain 3 variables.");
}

#[test]
fn parse_cnf_header_init() {
    let (formula, num_vars) = match parse_cnf_from_file("./tests/instances/cnf_header_init.cnf") {
        Ok(formula) => formula,
        Err(e) => {
            eprintln!("Parsing error: {e:?}");
            panic!();
        }
    };

    assert_eq!(
        formula.capacity(),
        732,
        "Formula should have capacity for 732 clauses."
    );
    assert_eq!(
        num_vars, 42,
        "Formula should have capacity for 42 variables."
    );
}

#[test]
fn parse_cnf_duplicate_lit() {
    let (formula, num_vars) = match parse_cnf_from_file("./tests/instances/cnf_duplicate_lit.cnf") {
        Ok(formula) => formula,
        Err(e) => {
            eprintln!("Parsing error: {e:?}");
            panic!();
        }
    };

    assert_eq!(formula.len(), 2, "Formula should contain 2 clauses.");
    assert_eq!(num_vars, 3, "Formula should contain 3 variables.");
    assert_eq!(formula.constraints[0].len(), 3);
    assert_eq!(formula.constraints[1].len(), 2);
}

#[test]
fn parse_cnf_opposing_literals() {
    let (formula, num_vars) =
        match parse_cnf_from_file("./tests/instances/cnf_opposing_literals.cnf") {
            Ok(formula) => formula,
            Err(e) => {
                eprintln!("Parsing error: {e:?}");
                panic!();
            }
        };

    assert_eq!(formula.len(), 2, "Formula should contain 2 clauses.");
    assert_eq!(num_vars, 3, "Formula should contain 3 variables.");
    assert_eq!(formula.constraints[0].len(), 4);
    assert_eq!(formula.constraints[1].len(), 3);
}