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

use logos::Logos;
use veripb_formula::prelude::*;
use veripb_parser::{
    opb_token::OPBToken, substitution_parser::parse_substitution,
    substitution_token::SubstitutionToken,
};

#[test]
fn parse_substitution_from_scratch() {
    let mut var_names = VarNameManager::default();
    let x1 = var_names.add_by_name("x1");
    let x2 = var_names.add_by_name("x2");
    let x3 = var_names.add_by_name("x3");
    let x4 = var_names.add_by_name("x4");

    let mut lex = SubstitutionToken::lexer("x1 0 x2 1 x3 x1 x4 ~x1");

    let sub = parse_substitution(&mut lex, &mut var_names).expect("Parsing error!");

    assert_eq!(sub.get(x1), Some(SubstitutionValue::FALSE));
    assert_eq!(sub.get(x2), Some(SubstitutionValue::TRUE));
    assert_eq!(
        sub.get(x3),
        Some(SubstitutionValue::lit(Lit::from_var(x1, false)))
    );
    assert_eq!(
        sub.get(x4),
        Some(SubstitutionValue::lit(Lit::from_var(x1, true)))
    );
    assert_eq!(sub.get(4), None);
}

#[test]
fn parse_substitution_var_twice_in_domain() {
    let mut var_names = VarNameManager::default();

    let mut lex = SubstitutionToken::lexer("x1 0 x1 1 x3 x1 x4 ~x1");

    let sub = parse_substitution(&mut lex, &mut var_names);

    assert!(sub.is_err());
}

#[test]
fn parse_substitution_change_lexer() {
    let mut var_names = VarNameManager::default();
    let x1 = var_names.add_by_name("x1");
    let x2 = var_names.add_by_name("x2");
    let x3 = var_names.add_by_name("x3");
    let x4 = var_names.add_by_name("x4");

    let lex = OPBToken::lexer("x1 0 x2 1 x3 x1 x4 ~x1");

    let sub = parse_substitution(&mut lex.morph(), &mut var_names).expect("Parsing error!");

    assert_eq!(sub.get(x1), Some(SubstitutionValue::FALSE));
    assert_eq!(sub.get(x2), Some(SubstitutionValue::TRUE));
    assert_eq!(
        sub.get(x3),
        Some(SubstitutionValue::lit(Lit::from_var(x1, false)))
    );
    assert_eq!(
        sub.get(x4),
        Some(SubstitutionValue::lit(Lit::from_var(x1, true)))
    );
    assert_eq!(sub.get(4), None);
}

#[test]
fn parse_substitution_with_map_symbol() {
    let mut var_names = VarNameManager::default();
    let x1 = var_names.add_by_name("x1");
    let x2 = var_names.add_by_name("x2");
    let x3 = var_names.add_by_name("x3");
    let x4 = var_names.add_by_name("x4");

    let mut lex = SubstitutionToken::lexer("x1 -> 0 x2 1 x3 → x1 x4 -> ~x1");

    let sub = parse_substitution(&mut lex, &mut var_names).expect("Parsing error!");

    assert_eq!(sub.get(x1), Some(SubstitutionValue::FALSE));
    assert_eq!(sub.get(x2), Some(SubstitutionValue::TRUE));
    assert_eq!(
        sub.get(x3),
        Some(SubstitutionValue::lit(Lit::from_var(x1, false)))
    );
    assert_eq!(
        sub.get(x4),
        Some(SubstitutionValue::lit(Lit::from_var(x1, true)))
    );
    assert_eq!(sub.get(4), None);
}