概述
例如.
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来检查布尔值,但是如何优雅地将int / reals / …转换回可用的值(例如,不经过字符串和切除这个额外的符号).
p = Bool('p')
x = Real('x')
s = Solver()
s.add(Or(x < 5,Not(p))
s.check()
m = s.model()
print m[p],m[x]
print "is_true(m[p]):",is_true(m[p])
print "is_false(m[p]):",is_false(m[p])
print "is_int_value(m[x]):",is_int_value(m[x])
print "is_rational_value(m[x]):",is_rational_value(m[x])
print "is_algebraic_value(m[x]):",is_algebraic_value(m[x])
r = m[x].approx(20) # r is an approximation of m[x] with precision 1/10^20
print "is_rational_value(r):",is_rational_value(r)
print r.numerator_as_long()
print r.denominator_as_long()
print float(r.numerator_as_long())/float(r.denominator_as_long())总结
以上是编程之家为你收集整理的Z3 / Python从模型中获取python值全部内容，希望文章能够帮你解决Z3 / Python从模型中获取python值所遇到的程序开发问题。
如果您也喜欢它,动动您的小指点个赞吧
602392714
清零编程群