kdrag.utils.sanity_check_consistency

kdrag.utils.sanity_check_consistency(thms: list[ExprRef | Proof], timeout=1000)

Sanity check theorems or proofs for consistency. If they are inconsistent, raise an error. Otherwise, return the result of the check. A sat result shows consistency, but an unknown result does not imply anything.

It may be nice to try and apply this function to your axioms or theory in CI.

>>> x,y = smt.Ints("x y")
>>> sanity_check_consistency([x == y])
sat

Parameters:

thms (list[ExprRef | Proof])