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
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125

use malachite_bigint::BigInt;
use num_traits::{One, Zero};
use veripb_parser::wcnf_parser::parse_wcnf_from_file;

#[test]
fn parse_wcnf_empty() {
    let (formula, var_names) = match parse_wcnf_from_file("./tests/instances/empty.wcnf") {
        Ok(formula) => formula,
        Err(e) => {
            eprintln!("Parsing error: {e:?}");
            panic!();
        }
    };

    assert_eq!(formula.len(), 0, "Formula should contain 0 clauses.");
    assert_eq!(
        formula.objective.as_ref().unwrap().len(),
        0,
        "Objective should contain 0 terms."
    );
    assert!(
        formula.objective.as_ref().unwrap().constant.is_zero(),
        "Objective constant should be 0."
    );
    assert_eq!(var_names.len(), 0, "Formula should contain 0 variables.");
}

#[test]
fn parse_wcnf_empty_soft() {
    let (formula, var_names) =
        match parse_wcnf_from_file("./tests/instances/empty_soft_clause.wcnf") {
            Ok(formula) => formula,
            Err(e) => {
                eprintln!("Parsing error: {e:?}");
                panic!();
            }
        };

    assert_eq!(formula.len(), 0, "Formula should contain 0 clauses.");
    assert_eq!(
        formula.objective.as_ref().unwrap().len(),
        0,
        "Objective should contain 0 terms."
    );
    assert_eq!(
        formula.objective.as_ref().unwrap().constant,
        BigInt::one(),
        "Objective constant should be 1."
    );
    assert_eq!(var_names.len(), 0, "Formula should contain 0 variables.");
}

#[test]
fn parse_maxsat_1() {
    let (formula, var_names) = match parse_wcnf_from_file("./tests/instances/maxsat_mix.wcnf") {
        Ok(formula) => formula,
        Err(e) => {
            eprintln!("Parsing error: {e:?}");
            panic!();
        }
    };

    assert_eq!(formula.len(), 3, "Formula should contain 3 clauses.");
    assert_eq!(
        formula.objective.as_ref().unwrap().len(),
        1,
        "Objective should contain 1 terms."
    );
    assert_eq!(
        formula.objective.as_ref().unwrap().constant,
        BigInt::zero(),
        "Objective constant should be 0."
    );
    assert_eq!(var_names.len(), 5, "Formula should contain 5 variables.");
}

#[test]
fn parse_maxsat_2() {
    let (formula, var_names) =
        match parse_wcnf_from_file("./tests/instances/maxsat_new_format.wcnf") {
            Ok(formula) => formula,
            Err(e) => {
                eprintln!("Parsing error: {e:?}");
                panic!();
            }
        };

    assert_eq!(formula.len(), 7, "Formula should contain 7 clauses.");
    assert_eq!(
        formula.objective.as_ref().unwrap().len(),
        4,
        "Objective should contain 4 terms."
    );
    assert_eq!(
        formula.objective.as_ref().unwrap().constant,
        BigInt::zero(),
        "Objective constant should be 0."
    );
    assert_eq!(var_names.len(), 8, "Formula should contain 8 variables.");
}

#[test]
fn parse_maxsat_cancelling_objective_lits() {
    let (formula, var_names) =
        match parse_wcnf_from_file("./tests/instances/maxsat_cancelling_objective_lits.wcnf") {
            Ok(formula) => formula,
            Err(e) => {
                eprintln!("Parsing error: {e:?}");
                panic!();
            }
        };

    assert_eq!(formula.len(), 0, "Formula should contain 0 clauses.");
    assert_eq!(
        formula.objective.as_ref().unwrap().len(),
        1,
        "Objective should contain 1 terms."
    );
    assert_eq!(
        formula.objective.as_ref().unwrap().constant,
        1038862559.into(),
        "Objective constant should be 1038862559."
    );
    assert_eq!(var_names.len(), 1, "Formula should contain 1 variables.");
}