implement "detecting" conflict clauses

rust/solve/src/dpll.rs

@@ -14,6 +14,7 @@ fn from_vec(v: Vec<Var>) -> BoundVars {
    vars
}
/// 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 {
        if vars.contains(&v) {
@@ -29,3 +30,23 @@ fn test_is_clause_satisfied() {
    assert!(is_clause_satisfied(from_vec(vec!(1)), vec!(1)));
    assert!(!is_clause_satisfied(empty_vars(), vec!(1)));
}
/// A conflict clause is a clause whose atoms each are false.
fn is_clause_conflict(vars: BoundVars, clause: Clause) -> bool {
    for v in clause {
        if vars.contains(&v) {
            return false
        }
    }
    return true
}
#[test]
fn test_is_clause_conflict() {
    assert!(is_clause_conflict(empty_vars(), vec!(1)));
    assert!(is_clause_conflict(empty_vars(), vec!(1, 2, 3)));
    assert!(is_clause_conflict(from_vec(vec!(4)), vec!(1, 2, 3)));
    assert!(!is_clause_conflict(from_vec(vec!(1)), vec!(1)));
    assert!(!is_clause_conflict(from_vec(vec!(2)), vec!(1, 2)));
}