kdrag.smt.is_uninterp

kdrag.smt.is_uninterp(x: ExprRef) → bool

Check if uninterpreted function. >>> x = z3.Real(“x”) >>> f = z3.Function(“f”, RealSort(), RealSort()) >>> is_uninterp(x) True >>> is_uninterp(f(x)) True >>> is_uninterp(x + 1) False >>> is_uninterp(z3.RealVal(42.1)) False