Function varisat::analyze_conflict::analyze_conflict

pub fn analyze_conflict<'a>(
    ctx: Const<TrailP, Const<ProofP<'a>, Const<ImplGraphP, Const<ClauseAllocP, Mut<VsidsP, Mut<AnalyzeConflictP, Ref<Context<'a>>>>>>>>, 
    conflict: Conflict
) -> usize

Learns a new clause by analyzing a conflict.

Returns the lowest decision level that makes the learned clause asserting.