kdrag.theories.real.arb.bounds

kdrag.theories.real.arb.bounds(e: ArithRef) → tuple[ArithRef, ArithRef]

Get the bounds of a z3 expression. >>> bounds(1) (1, 1) >>> bounds(smt.RealVal(1) + smt.RealVal(2)) (3, 3)