kdrag.utils.prune

kdrag.utils.prune(thm: BoolRef | QuantifierRef | Proof, by=[], timeout=1000) → list[ExprRef | Proof]

Prune the theorems used using unsat core. Helpful to speedup future proof verification.

>>> p,q,r = smt.Bools("p q r")
>>> sorted(prune(p & q, [p, q, r]), key=lambda b: b.decl().name())
[p, q]