pub fn quotient_dag<C: Congruence + ?Sized>(
n: usize,
clauses: &CanonClauses,
cong: &C,
) -> Option<QuotientDag>Expand description
Build the cofactor DAG quotiented by cong: memoize on the canonical form, branch on the first
live variable of the (canonicalized) subproblem, and merge ~-equivalent cofactors, recording
the realizing twist on each edge. Returns None iff the formula is satisfiable.