|
|
@ -75,13 +75,7 @@ fn test_is_unknown() {
|
|
75
|
75
|
|
|
76
|
76
|
/// A satisfied clause is a clause where at least one atom is true.
|
|
77
|
77
|
fn is_clause_satisfied(vars: &BoundVars, clause: Clause) -> bool {
|
|
78
|
|
for v in clause {
|
|
79
|
|
if is_true(vars, v) {
|
|
80
|
|
return true
|
|
81
|
|
}
|
|
82
|
|
}
|
|
83
|
|
|
|
84
|
|
return false
|
|
|
78
|
clause.iter().any(|v| is_true(vars, *v))
|
|
85
|
79
|
}
|
|
86
|
80
|
|
|
87
|
81
|
#[test]
|
|
|
@ -92,20 +86,14 @@ fn test_is_clause_satisfied() {
|
|
92
|
86
|
|
|
93
|
87
|
/// A conflict clause is a clause whose atoms each are false.
|
|
94
|
88
|
fn is_clause_conflict(vars: &BoundVars, clause: Clause) -> bool {
|
|
95
|
|
for v in clause {
|
|
96
|
|
if is_true(vars, v) {
|
|
97
|
|
return false
|
|
98
|
|
}
|
|
99
|
|
}
|
|
100
|
|
|
|
101
|
|
return true
|
|
|
89
|
clause.iter().all(|v| is_false(vars, *v))
|
|
102
|
90
|
}
|
|
103
|
91
|
|
|
104
|
92
|
#[test]
|
|
105
|
93
|
fn test_is_clause_conflict() {
|
|
106
|
|
assert!(is_clause_conflict(&empty_vars(), vec!(1)));
|
|
107
|
|
assert!(is_clause_conflict(&empty_vars(), vec!(1, 2, 3)));
|
|
108
|
|
assert!(is_clause_conflict(&from_vec(vec!(4)), vec!(1, 2, 3)));
|
|
|
94
|
assert!(is_clause_conflict(&from_vec(vec!(-1)), vec!(1)));
|
|
|
95
|
assert!(is_clause_conflict(&from_vec(vec!(-1, -2, -3)), vec!(1, 2, 3)));
|
|
|
96
|
assert!(is_clause_conflict(&from_vec(vec!(-1, -2, -3, 4)), vec!(1, 2, 3)));
|
|
109
|
97
|
assert!(!is_clause_conflict(&from_vec(vec!(1)), vec!(1)));
|
|
110
|
98
|
assert!(!is_clause_conflict(&from_vec(vec!(2)), vec!(1, 2)));
|
|
111
|
99
|
}
|