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

use logos::Logos;
use veripb_formula::prelude::*;
use veripb_parser::{
    assignment_parser::parse_bool_assignment_into, assignment_token::AssignmentToken,
};

#[test]
fn read_assignment_without_resize() {
    let mut var_names = VarNameManager::default();
    let x1 = var_names.add_by_name("x1");
    let x2 = var_names.add_by_name("x83e42");
    let x3 = var_names.add_by_name("s452345llkj4dse435");
    let x4 = var_names.add_by_name("rs3s322ed3e3d");
    let x5 = var_names.add_by_name("x8fewsafssfwsa3w82");
    let mut assignment = Assignment::with_size(var_names.len());

    let mut lex = AssignmentToken::lexer("x1 ~s452345llkj4dse435 x8fewsafssfwsa3w82");
    parse_bool_assignment_into(&mut lex, &mut var_names, &mut assignment).expect("Parsing error!");

    assert_eq!(assignment.get_value(x1), BoolValue::Assigned(true));
    assert_eq!(assignment.get_value(x2), BoolValue::Unassigned);
    assert_eq!(assignment.get_value(x3), BoolValue::Assigned(false));
    assert_eq!(assignment.get_value(x4), BoolValue::Unassigned);
    assert_eq!(assignment.get_value(x5), BoolValue::Assigned(true));
}

#[test]
fn read_assignment_with_resize() {
    let mut var_names = VarNameManager::default();
    let x1 = var_names.add_by_name("x1");
    let x2 = var_names.add_by_name("x83e42");
    let x3 = var_names.add_by_name("s452345llkj4dse435");
    let x4 = var_names.add_by_name("rs3s322ed3e3d");
    let mut assignment = Assignment::with_size(var_names.len());

    let mut lex = AssignmentToken::lexer("x1 ~s452345llkj4dse435 x8fewsafssfwsa3w82");
    parse_bool_assignment_into(&mut lex, &mut var_names, &mut assignment).expect("Parsing error!");

    assert_eq!(assignment.get_value(x1), BoolValue::Assigned(true));
    assert_eq!(assignment.get_value(x2), BoolValue::Unassigned);
    assert_eq!(assignment.get_value(x3), BoolValue::Assigned(false));
    assert_eq!(assignment.get_value(x4), BoolValue::Unassigned);
    assert_eq!(
        assignment.get_value(var_names.get_idx("x8fewsafssfwsa3w82").unwrap()),
        BoolValue::Assigned(true)
    );
    assert_eq!(assignment.len(), 5);
}