Skip to main content

structured_leaf_dag

logicaffeine_proof::cofactor

Function structured_leaf_dag 

Source 
pub fn structured_leaf_dag(
    n: usize,
    clauses: &CanonClauses,
) -> Option<StructuredDag>
Expand description

Build the structured-leaf cofactor DAG over the fixed order 0..n: a node is a leaf when it is ⊥ or when a specialist crushes it (structured_leaf); otherwise it branches. Identical cofactors at the same depth share a node. None iff the formula is satisfiable.