Skip to main content

resolve_masks

Function resolve_masks 

Source
pub fn resolve_masks(a: MaskClause, b: MaskClause) -> Option<MaskClause>
Expand description

Resolve two mask clauses on their single clashing variable. Some(resolvent) iff exactly one variable appears positively in one and negatively in the other (a second clash would make every resolvent a tautology — the same single-pivot rule as Subcube::resolve). The resolvent is automatically tautology-free.