|
|
@ -74,9 +74,9 @@ fn test_is_unknown() {
|
|
74
|
74
|
}
|
|
75
|
75
|
|
|
76
|
76
|
/// A satisfied clause is a clause where at least one atom is true.
|
|
77
|
|
fn is_clause_satisfied(vars: BoundVars, clause: Clause) -> bool {
|
|
|
77
|
fn is_clause_satisfied(vars: &BoundVars, clause: Clause) -> bool {
|
|
78
|
78
|
for v in clause {
|
|
79
|
|
if vars.contains(&v) {
|
|
|
79
|
if is_true(vars, v) {
|
|
80
|
80
|
return true
|
|
81
|
81
|
}
|
|
82
|
82
|
}
|
|
|
@ -86,14 +86,14 @@ fn is_clause_satisfied(vars: BoundVars, clause: Clause) -> bool {
|
|
86
|
86
|
|
|
87
|
87
|
#[test]
|
|
88
|
88
|
fn test_is_clause_satisfied() {
|
|
89
|
|
assert!(is_clause_satisfied(from_vec(vec!(1)), vec!(1)));
|
|
90
|
|
assert!(!is_clause_satisfied(empty_vars(), vec!(1)));
|
|
|
89
|
assert!(is_clause_satisfied(&from_vec(vec!(1)), vec!(1)));
|
|
|
90
|
assert!(!is_clause_satisfied(&empty_vars(), vec!(1)));
|
|
91
|
91
|
}
|
|
92
|
92
|
|
|
93
|
93
|
/// A conflict clause is a clause whose atoms each are false.
|
|
94
|
|
fn is_clause_conflict(vars: BoundVars, clause: Clause) -> bool {
|
|
|
94
|
fn is_clause_conflict(vars: &BoundVars, clause: Clause) -> bool {
|
|
95
|
95
|
for v in clause {
|
|
96
|
|
if vars.contains(&v) {
|
|
|
96
|
if is_true(vars, v) {
|
|
97
|
97
|
return false
|
|
98
|
98
|
}
|
|
99
|
99
|
}
|
|
|
@ -103,9 +103,9 @@ fn is_clause_conflict(vars: BoundVars, clause: Clause) -> bool {
|
|
103
|
103
|
|
|
104
|
104
|
#[test]
|
|
105
|
105
|
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)));
|
|
109
|
|
assert!(!is_clause_conflict(from_vec(vec!(1)), vec!(1)));
|
|
110
|
|
assert!(!is_clause_conflict(from_vec(vec!(2)), vec!(1, 2)));
|
|
|
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)));
|
|
|
109
|
assert!(!is_clause_conflict(&from_vec(vec!(1)), vec!(1)));
|
|
|
110
|
assert!(!is_clause_conflict(&from_vec(vec!(2)), vec!(1, 2)));
|
|
111
|
111
|
}
|