[][src]Function varisat::prop::binary::propagate_binary

pub fn propagate_binary(
    ctx: Const<BinaryClausesP, Mut<TrailP, Mut<ImplGraphP, Mut<AssignmentP, Ref<Context>>>>>,
    lit: Lit
) -> Result<(), Conflict>

Propagate all literals implied by the given literal via binary clauses.

On conflict return the binary clause propgating the conflicting assignment.