Z3/Python nhận giá trị trăn từ mẫu

Question

Làm thế nào tôi có thể nhận được giá trị trăn thực từ mô hình Z3?

Ví dụ:

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] 

in

-1.4142135623? 
False 

nhưng đó là đối tượng Z3 và không trăn đối tượng phao/bool.

tôi biết rằng tôi có thể kiểm tra các giá trị boolean sử dụng is_true/is_false, nhưng làm thế nào tôi có thể thanh lịch chuyển đổi ints/real/... trở về giá trị sử dụng (không phải trải qua chuỗi và cắt đi thêm ? biểu tượng này, ví dụ) .

Answer 1

Đối với các giá trị Boolean, bạn có thể sử dụng các chức năng is_true và is_false. Các giá trị số có thể là số nguyên, hợp lý hoặc đại số. Chúng tôi có thể sử dụng các chức năng is_int_value, is_rational_value và is_algebraic_value để kiểm tra từng trường hợp. Trường hợp nguyên là đơn giản nhất, chúng ta có thể sử dụng phương thức as_long() để chuyển đổi giá trị số nguyên Z3 thành một Python dài. Đối với các giá trị hợp lý, chúng ta có thể sử dụng các phương thức numerator() và denominator() để thu được các số nguyên Z3 đại diện cho tử số và mẫu số. Các phương pháp numerator_as_long() và denominator_as_long() là các phím tắt cho self.numerator().as_long() và self.denominator().as_long(). Cuối cùng, các số đại số được sử dụng để biểu diễn các số vô tỉ. Lớp AlgebraicNumRef có phương thức được gọi là approx(self, precision). Nó trả về một số hợp lý Z3 xấp xỉ số đại số với độ chính xác 1/10^precision. Đây là một ví dụ về cách sử dụng phương pháp này. Nó cũng có sẵn trực tuyến tại: http://rise4fun.com/Z3Py/Mkw

p = Bool('p') 
x = Real('x') 
s = Solver() 
s.add(Or(x < 5, x > 10), Or(p, x**2 == 2), 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())