pub fn try_assignment_witness(
num_vars: usize,
db: &[Vec<Lit>],
clause: &[Lit],
witness: &Witness,
) -> Option<Vec<Lit>>Expand description
Reduce a Witness to a standard PR assignment witness for clause against db,
returning Some(ω) only when ω genuinely satisfies pr::is_pr — so the caller can emit a
dpr-trim-checkable line — and None when the witness is irreducibly SR.
For an Witness::Assignment this just re-verifies the witness it already carries. For a
Witness::Substitution σ it tries the canonical reduction ω = {¬σ(l) : l ∈ C} and, since
that need not satisfy C, a small family of candidates seeded by each satisfying literal of
C. Every candidate is checked by pr::is_pr before being returned, so the function can never
hand back an unsound witness.