python - z3 - 获取函数的域

Question

我必须使用 Z3 和 python 检索函数的 codomain。那可能吗？具体来说，我可能有一个表达式，如：f(var) = (var + 1) << 1，我想找出表达式可能假设的值的范围。有任何想法吗？