Function varisat::prop::propagate

pub fn propagate(
    ctx: Const<ClauseDbP, Const<BinaryClausesP, Mut<WatchlistsP, Mut<TrailP, Mut<ImplGraphP, Mut<ClauseAllocP, Mut<AssignmentP, Ref<Context>>>>>>>>
) -> Result<(), Conflict>

Propagate enqueued assignments.

Returns when all enqueued assignments are propagated, including newly propagated assignemnts, or if there is a conflict.

On conflict the first propagation that would assign the opposite value to an already assigned literal is returned.