pub fn entails_certified(
premises: &[ProofExpr],
goal: &ProofExpr,
) -> Option<Verdict>Expand description
Decide premises ⊨ goal with the CDCL solver and independently certify an
Entailed verdict by RUP replay. None if the problem is not purely propositional over
recognisable atoms, OR if the solver claims UNSAT but the checker cannot confirm it (a
solver bug — fail closed, never report a false Entailed).