[][src]Function varisat::prop::long::propagate_long

pub fn propagate_long(
    ctx: Mut<ClauseAllocP, Mut<WatchlistsP, Mut<TrailP, Mut<ImplGraphP, Mut<AssignmentP, Ref<Context>>>>>>,
    lit: Lit
) -> Result<(), Conflict>

Propagate all literals implied by long clauses watched by the given literal.

On conflict return the clause propgating the conflicting assignment.

See prop::watch for the invariants that this has to uphold.