如何从Z3模型中获取真正的python值？
例如
p = Bool('p')
x = Real('x')
s = Solver()
s.add(Or(x < 5, x > 10), Or(p, x**2 == 2), Not(p))
s.check()
print s.model()[x]
print s.model()[p]
版画
-1.4142135623?
False
但那些是Z3对象而不是python float/bool对象.
我知道我可以使用is_true/ 检查布尔值is_false,但是如何优雅地将ints/reals/...转换回可用值(例如,不通过字符串并删除这个额外的?符号).