pub fn cdcl_entails(premises: &[ProofExpr], goal: &ProofExpr) -> Option<bool>Expand description
Does premises ⊨ goal (propositionally)? Encodes premises ∧ ¬goal to CNF and runs
CDCL: UNSAT ⇒ entailed. None if the problem is not purely propositional over
recognisable atoms (caller falls back). This is the Untrusted tier — the verdict
with no emitted proof, for the raw-speed comparison against Z3.