1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
//! Propagation of binary clauses.
use partial_ref::{partial, PartialRef};
use varisat_formula::Lit;
use crate::context::{parts::*, Context};
use super::{enqueue_assignment, Conflict, Reason};
/// Propagate all literals implied by the given literal via binary clauses.
///
/// On conflict return the binary clause propgating the conflicting assignment.
pub fn propagate_binary(
mut ctx: partial!(
Context,
mut AssignmentP,
mut ImplGraphP,
mut TrailP,
BinaryClausesP,
),
lit: Lit,
) -> Result<(), Conflict> {
let (binary_clauses, mut ctx) = ctx.split_part(BinaryClausesP);
for &implied in binary_clauses.implied(lit) {
let assignment = ctx.part(AssignmentP);
if assignment.lit_is_false(implied) {
return Err(Conflict::Binary([implied, !lit]));
} else if !assignment.lit_is_true(implied) {
enqueue_assignment(ctx.borrow(), implied, Reason::Binary([!lit]));
}
}
Ok(())
}
|
