implement is_true, is_false and is_unknown

rust/solve/src/dpll.rs

@@ -14,6 +14,49 @@ fn from_vec(v: Vec<Var>) -> BoundVars {
    vars
}
fn is_true(vars: &BoundVars, var: Var) -> bool {
    vars.contains(&var) || !vars.contains(&-var)
}
#[test]
fn test_is_true() {
    let vars = &from_vec(vec!(1, -2));
    assert!(is_true(vars, 1));
    assert!(is_true(vars, -2));
    assert!(!is_true(vars, -1));
    assert!(!is_true(vars, 2));
}
fn is_false(vars: &BoundVars, var: Var) -> bool {
    !vars.contains(&var) || vars.contains(&-var)
}
#[test]
fn test_is_false() {
    let vars = &from_vec(vec!(1, -2));
    assert!(is_false(vars, -1));
    assert!(is_false(vars, 2));
    assert!(!is_false(vars, 1));
    assert!(!is_false(vars, -2));
}
fn is_unknown(vars: &BoundVars, var: Var) -> bool {
    !vars.contains(&var) && !vars.contains(&-var)
}
#[test]
fn test_is_unknown() {
    let vars = &from_vec(vec!(1, -2));
    assert!(is_unknown(vars, 3));
    assert!(is_unknown(vars, -3));
    assert!(is_unknown(vars, 4));
    assert!(is_unknown(vars, -4));
    assert!(!is_unknown(vars, 1));
    assert!(!is_unknown(vars, -1));
    assert!(!is_unknown(vars, 2));
    assert!(!is_unknown(vars, -2));
}
/// A satisfied clause is a clause where at least one atom is true.
fn is_clause_satisfied(vars: BoundVars, clause: Clause) -> bool {
    for v in clause {