[−][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.