pub fn derivation(
num_vars: usize,
original: &[Vec<Lit>],
log: &[Vec<Lit>],
targets: &[usize],
) -> Option<Lrat>Expand description
The trimmed LRAT derivation of the clauses of log that targets names (by index) from original, every clause of
log RUP from the formula and the clauses before it: a step for each target and for each log clause a step it
leans on needs, in log order, the j-th log clause numbered after the formula’s. None when a target, or a clause
one needs, is not RUP in its place, or a target names no log clause.