Przeglądaj źródła

change is_true and is_false to work properly with unknowns

this means we *always* do the checks for both `var` and `-var`, and that
you can only really "trust" `is_true` and `is_false` if they return
true, otherwise you'd have to use `is_unknown` as well.
Lucas Stadler 10 lat temu
rodzic
commit
1a75ade163
1 zmienionych plików z 18 dodań i 2 usunięć
  1. 18 2
      rust/solve/src/dpll.rs

+ 18 - 2
rust/solve/src/dpll.rs

15
}
15
}
16
16
17
fn is_true(vars: &BoundVars, var: Var) -> bool {
17
fn is_true(vars: &BoundVars, var: Var) -> bool {
18
    vars.contains(&var) || !vars.contains(&-var)
18
    let t = vars.contains(&var);
19
    let nt = vars.contains(&-var);
20
    if t || nt {
21
        t || !nt
22
    } else {
23
        false
24
    }
19
}
25
}
20
26
21
#[test]
27
#[test]
25
    assert!(is_true(vars, -2));
31
    assert!(is_true(vars, -2));
26
    assert!(!is_true(vars, -1));
32
    assert!(!is_true(vars, -1));
27
    assert!(!is_true(vars, 2));
33
    assert!(!is_true(vars, 2));
34
    assert!(!is_true(vars, 3));
35
    assert!(!is_true(vars, -3));
28
}
36
}
29
37
30
fn is_false(vars: &BoundVars, var: Var) -> bool {
38
fn is_false(vars: &BoundVars, var: Var) -> bool {
31
    !vars.contains(&var) || vars.contains(&-var)
39
    let t = vars.contains(&var);
40
    let nt = vars.contains(&-var);
41
    if t || nt {
42
        !t || nt
43
    } else {
44
        false
45
    }
32
}
46
}
33
47
34
#[test]
48
#[test]
38
    assert!(is_false(vars, 2));
52
    assert!(is_false(vars, 2));
39
    assert!(!is_false(vars, 1));
53
    assert!(!is_false(vars, 1));
40
    assert!(!is_false(vars, -2));
54
    assert!(!is_false(vars, -2));
55
    assert!(!is_false(vars, 3));
56
    assert!(!is_false(vars, -3));
41
}
57
}
42
58
43
fn is_unknown(vars: &BoundVars, var: Var) -> bool {
59
fn is_unknown(vars: &BoundVars, var: Var) -> bool {