Z3 là một chứng minh định lý hiệu suất cao được phát triển tại Microsoft Research. Z3 được sử dụng trong nhiều ứng dụng như. xác minh và thử nghiệm phần mềm/phần cứng, giải quyết ràng buộc, phân tích các hệ thống lai, bảo mật, sinh học (trong phân tích silico) và các vấn đề hình học Show Hướng dẫn này thể hiện các khả năng chính của Z3Py. API Z3 trong Python. Không cần nền tảng Python để đọc hướng dẫn này. Tuy nhiên, thật hữu ích khi học Python (một ngôn ngữ thú vị. ) tại một số thời điểm và có nhiều tài nguyên miễn phí tuyệt vời để làm như vậy (Hướng dẫn về Python) Bản phân phối Z3 cũng chứa C,. API Net và OCaml. Mã nguồn của Z3Py có sẵn trong bản phân phối Z3, vui lòng sửa đổi nó để đáp ứng nhu cầu của bạn. Mã nguồn cũng hướng dẫn cách sử dụng các tính năng mới trong Z3 4. 0. Các giao diện thú vị khác dành cho Z3 bao gồm Scala^Z3 và SBV Vui lòng gửi phản hồi, nhận xét và/hoặc chỉnh sửa tới leonardo@microsoft. com. Nhận xét của bạn rất có giá trị Bắt đầuHãy bắt đầu với ví dụ đơn giản sau x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)
The function Int('x') creates an integer variable in Z3 named x. The solve function solves a system of constraints. The example above uses two variables x and y, and three constraints. Z3Py like Python uses = for assignment. The operators <, <=, >, >=, == and != for comparison. In the example above, the expression x + 2*y == 7 is a Z3 constraint. Z3 can solve and crunch formulas. Các ví dụ tiếp theo cho thấy cách sử dụng công thức/biểu thức Z3 đơn giản hóa x = Int('x')
y = Int('y')
print simplify(x + y + 2*x + 3)
print simplify(x < y + x + 2)
print simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5))
Theo mặc định, Z3Py (dành cho web) hiển thị các công thức và biểu thức bằng ký hiệu toán học. Như thường lệ, ∧ là logic và, ∨ là logic hoặc, v.v. Lệnh set_option(html_mode=False) làm cho tất cả các công thức và biểu thức được hiển thị trong ký hiệu Z3Py. Đây cũng là chế độ mặc định cho phiên bản Z3Py ngoại tuyến đi kèm với bản phân phối Z3 x = Int('x')
y = Int('y')
print x**2 + y**2 >= 1
set_option(html_mode=False)
print x**2 + y**2 >= 1
Z3 cung cấp các chức năng để duyệt các biểu thức x = Int('x')
y = Int('y')
n = x + y >= 3
print "num args: ", n.num_args()
print "children: ", n.children()
print "1st child:", n.arg(0)
print "2nd child:", n.arg(1)
print "operator: ", n.decl()
print "op name: ", n.decl().name()
Z3 cung cấp tất cả các phép toán cơ bản. Z3Py sử dụng cùng một toán tử ưu tiên của ngôn ngữ Python. Giống như Python, ** là toán tử lũy thừa. Z3 có thể giải các ràng buộc đa thức phi tuyến x = Real('x')
y = Real('y')
solve(x**2 + y**2 > 3, x**3 + y < 5)
Thủ tục Real('x') tạo biến thực x. Z3Py có thể biểu diễn các số nguyên lớn tùy ý, số hữu tỷ (như trong ví dụ trên) và số đại số vô tỷ. Một số đại số vô tỉ là một nghiệm của đa thức có hệ số nguyên. Bên trong, Z3 thể hiện chính xác tất cả những con số này. Các số vô tỉ được hiển thị dưới dạng thập phân để dễ đọc kết quả x = Real('x')
y = Real('y')
solve(x**2 + y**2 == 3, x**3 == 2)
set_option(precision=30)
print "Solving, and displaying result with 30 decimal places"
solve(x**2 + y**2 == 3, x**3 == 2)
Thủ tục set_option dùng để cấu hình môi trường Z3. Nó được sử dụng để đặt các tùy chọn cấu hình chung, chẳng hạn như cách hiển thị kết quả. Tùy chọn set_option(precision=30) đặt số lượng vị trí thập phân được sử dụng khi hiển thị kết quả. Các ? . 2599210498? Ví dụ sau minh họa một lỗi phổ biến. Biểu thức 3/2 là một số nguyên Python chứ không phải số hữu tỷ Z3. Ví dụ này cũng chỉ ra các cách khác nhau để tạo số hữu tỷ trong Z3Py. Thủ tục Q(num, den) tạo một số hữu tỷ Z3 trong đó num là tử số và den là mẫu số. RealVal(1) tạo một số thực Z3 đại diện cho số 1 print 1/3
print RealVal(1)/3
print Q(1,3)
x = Real('x')
print x + 1/3
print x + Q(1,3)
print x + "1/3"
print x + 0.25
Số hữu tỷ cũng có thể được hiển thị trong ký hiệu thập phân x = Real('x')
solve(3*x == 1)
set_option(rational_to_decimal=True)
solve(3*x == 1)
set_option(precision=30)
solve(3*x == 1)
Một hệ thống ràng buộc có thể không có giải pháp. Trong trường hợp này, ta nói hệ thống không thỏa mãn ________số 8 Giống như trong Python, các bình luận bắt đầu bằng ký tự băm # và được kết thúc ở cuối dòng. Z3Py không hỗ trợ bình luận dài hơn một dòng # This is a comment
x = Real('x') # comment: creating x
print x**2 + 2*x + 2 # comment: printing polynomial
logic BooleanZ3 hỗ trợ toán tử Boolean. And, Or, Not, Implies (hàm ý), If (nếu-thì-khác). Hàm ý hai chiều được biểu diễn bằng đẳng thức ==. Ví dụ sau đây cho thấy cách giải quyết một tập hợp các ràng buộc Boolean đơn giản x = Int('x')
y = Int('y')
print simplify(x + y + 2*x + 3)
print simplify(x < y + x + 2)
print simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5))
0Các hằng số Boolean của Python True và False có thể được sử dụng để xây dựng các biểu thức Boolean Z3 x = Int('x')
y = Int('y')
print simplify(x + y + 2*x + 3)
print simplify(x < y + x + 2)
print simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5))
1Ví dụ sau sử dụng kết hợp các ràng buộc đa thức và Boolean x = Int('x')
y = Int('y')
print simplify(x + y + 2*x + 3)
print simplify(x < y + x + 2)
print simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5))
2Người giải quyếtZ3 cung cấp các bộ giải khác nhau. Lệnh giải quyết, được sử dụng trong các ví dụ trước, được triển khai bằng API bộ giải Z3. Việc triển khai có thể được tìm thấy trong tệp z3. py trong bản phân phối Z3. Ví dụ sau minh họa API bộ giải cơ bản x = Int('x')
y = Int('y')
print simplify(x + y + 2*x + 3)
print simplify(x < y + x + 2)
print simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5))
3Lệnh Solver() tạo một bộ giải cho mục đích chung. Các ràng buộc có thể được thêm vào bằng phương thức add. Chúng tôi nói rằng các ràng buộc đã được khẳng định trong bộ giải. Phương thức check() giải quyết các ràng buộc đã xác nhận. Kết quả là sat (thỏa mãn) nếu tìm thấy giải pháp. Kết quả là unsat (không thỏa mãn) nếu không có giải pháp nào tồn tại. Chúng tôi cũng có thể nói rằng hệ thống các ràng buộc được khẳng định là không khả thi. Cuối cùng, một bộ giải có thể không giải được một hệ ràng buộc và ẩn số được trả về Trong một số ứng dụng, chúng tôi muốn khám phá một số vấn đề tương tự có chung một số ràng buộc. Chúng ta có thể sử dụng các lệnh đẩy và bật để làm điều đó. Mỗi bộ giải duy trì một chồng các xác nhận. Lệnh đẩy tạo phạm vi mới bằng cách lưu kích thước ngăn xếp hiện tại. Lệnh pop loại bỏ bất kỳ xác nhận nào được thực hiện giữa nó và lệnh đẩy phù hợp. Phương thức kiểm tra luôn hoạt động trên nội dung của ngăn xếp xác nhận bộ giải Ví dụ sau là ví dụ mà Z3 không giải được. Bộ giải trả về ẩn số trong trường hợp này. Nhớ lại rằng Z3 có thể giải các ràng buộc đa thức phi tuyến, nhưng 2**x không phải là một đa thức x = Int('x')
y = Int('y')
print simplify(x + y + 2*x + 3)
print simplify(x < y + x + 2)
print simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5))
4Ví dụ sau đây cho thấy cách vượt qua các ràng buộc được khẳng định thành một bộ giải và cách thu thập số liệu thống kê hiệu suất cho phương pháp kiểm tra x = Int('x')
y = Int('y')
print simplify(x + y + 2*x + 3)
print simplify(x < y + x + 2)
print simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5))
5Kiểm tra lệnh trả về sat khi Z3 tìm thấy giải pháp cho tập hợp các ràng buộc được xác nhận. Ta nói Z3 thỏa mãn tập ràng buộc. Chúng tôi nói giải pháp là một mô hình cho tập hợp các ràng buộc được khẳng định. Một mô hình là một diễn giải làm cho mỗi ràng buộc được khẳng định là đúng. Ví dụ sau đây cho thấy các phương pháp cơ bản để kiểm tra các mô hình x = Int('x')
y = Int('y')
print simplify(x + y + 2*x + 3)
print simplify(x < y + x + 2)
print simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5))
6Trong ví dụ trên, hàm Reals('x y z') tạo các biến. x, y và z. Nó là viết tắt của x = Int('x')
y = Int('y')
print simplify(x + y + 2*x + 3)
print simplify(x < y + x + 2)
print simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5))
7Biểu thức m[x] trả về cách diễn giải của x trong mô hình m. Biểu thức "%s = %s" % (d. name(), m[d]) trả về một chuỗi trong đó %s đầu tiên được thay thế bằng tên của d (i. e. , d. name()) và %s thứ hai với phần trình bày bằng văn bản về cách diễn giải của d (i. e. , m[d]). Z3Py tự động chuyển đổi các đối tượng Z3 thành dạng văn bản khi cần Môn số họcZ3 hỗ trợ các biến thực và nguyên. Chúng có thể được trộn lẫn trong một vấn đề duy nhất. Giống như hầu hết các ngôn ngữ lập trình, Z3Py sẽ tự động thêm các lệnh cưỡng chế chuyển đổi biểu thức số nguyên thành số thực khi cần. Ví dụ sau minh họa các cách khác nhau để khai báo biến nguyên và biến thực x = Int('x')
y = Int('y')
print simplify(x + y + 2*x + 3)
print simplify(x < y + x + 2)
print simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5))
8Hàm ToReal chuyển biểu thức số nguyên thành biểu thức thực Z3Py hỗ trợ tất cả các phép tính số học cơ bản x = Int('x')
y = Int('y')
print simplify(x + y + 2*x + 3)
print simplify(x < y + x + 2)
print simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5))
9Đơn giản hóa lệnh áp dụng các phép biến đổi đơn giản trên các biểu thức Z3 x = Int('x')
y = Int('y')
print x**2 + y**2 >= 1
set_option(html_mode=False)
print x**2 + y**2 >= 1
0Lệnh help_simplify() in tất cả các tùy chọn có sẵn. Z3Py cho phép người dùng viết tùy chọn theo hai kiểu. Tên tùy chọn bên trong Z3 bắt đầu bằng. và các từ được phân tách bằng -. Các tùy chọn này có thể được sử dụng trong Z3Py. Z3Py cũng hỗ trợ các tên giống như Python, trong đó. bị chặn và - được thay thế bằng _. Ví dụ sau minh họa cách sử dụng cả hai kiểu x = Int('x')
y = Int('y')
print x**2 + y**2 >= 1
set_option(html_mode=False)
print x**2 + y**2 >= 1
1Z3Py hỗ trợ số lượng lớn tùy ý. Ví dụ sau minh họa cách thực hiện phép tính cơ bản bằng cách sử dụng số nguyên, số hữu tỷ và số vô tỷ lớn hơn. Z3Py chỉ hỗ trợ các số vô tỷ đại số. Các số vô tỷ đại số là đủ để trình bày các nghiệm của các hệ ràng buộc đa thức. Z3Py sẽ luôn hiển thị các số vô tỷ ở dạng ký hiệu thập phân vì nó thuận tiện hơn khi đọc. Biểu diễn bên trong có thể được trích xuất bằng phương thức sexpr(). Nó hiển thị biểu diễn bên trong Z3 cho các công thức và biểu thức toán học trong ký hiệu biểu thức s (giống Lisp) x = Int('x')
y = Int('y')
print x**2 + y**2 >= 1
set_option(html_mode=False)
print x**2 + y**2 >= 1
2Máy số họcCác CPU hiện đại và ngôn ngữ lập trình dòng chính sử dụng số học trên các vectơ bit có kích thước cố định. Số học máy có sẵn trong Z3Py dưới dạng Bit-Vectors. Chúng triển khai ngữ nghĩa chính xác của phép toán hai phần bù không dấu và có dấu Ví dụ sau minh họa cách tạo các biến và hằng số vectơ bit. Hàm BitVec('x', 16) tạo một biến vectơ bit trong Z3 có tên x với 16 bit. Để thuận tiện, các hằng số nguyên có thể được sử dụng để tạo các biểu thức vectơ bit trong Z3Py. Hàm BitVecVal(10, 32) tạo một vectơ bit có kích thước 32 chứa giá trị 10 x = Int('x')
y = Int('y')
print x**2 + y**2 >= 1
set_option(html_mode=False)
print x**2 + y**2 >= 1
3In contrast to programming languages, such as C, C++, C#, Java, there is no distinction between signed and unsigned bit-vectors as numbers. Instead, Z3 provides special signed versions of arithmetical operations where it makes a difference whether the bit-vector is treated as signed or unsigned. In Z3Py, the operators <, <=, >, >=, /, % and >> correspond to the signed versions. The corresponding unsigned operators are ULT, ULE, UGT, UGE, UDiv, URem and LShR. x = Int('x')
y = Int('y')
print x**2 + y**2 >= 1
set_option(html_mode=False)
print x**2 + y**2 >= 1
4Toán tử >> là phép dịch sang phải và << là phép dịch sang trái. Dịch chuyển logic sang phải là toán tử LShR x = Int('x')
y = Int('y')
print x**2 + y**2 >= 1
set_option(html_mode=False)
print x**2 + y**2 >= 1
5Chức năngKhông giống như các ngôn ngữ lập trình, nơi các hàm có tác dụng phụ, có thể đưa ra ngoại lệ hoặc không bao giờ quay lại, các hàm trong Z3 không có tác dụng phụ và hoàn toàn. Nghĩa là, chúng được xác định trên tất cả các giá trị đầu vào. Điều này bao gồm các chức năng, chẳng hạn như phân chia. Z3 dựa trên logic bậc nhất Với một ràng buộc chẳng hạn như x + y > 3, chúng ta đã nói rằng x và y là các biến. Trong nhiều sách giáo khoa, x và y được gọi là hằng số không giải thích được. Nghĩa là, chúng cho phép mọi diễn giải phù hợp với ràng buộc x + y > 3 Chính xác hơn, các ký hiệu hàm và hằng trong logic bậc nhất thuần túy không được giải thích hoặc miễn phí, điều đó có nghĩa là không có sự giải thích tiên nghiệm nào được đính kèm. Điều này trái ngược với các hàm thuộc về chữ ký của các lý thuyết, chẳng hạn như số học trong đó hàm + có cách giải thích tiêu chuẩn cố định (nó cộng hai số). Các hàm và hằng số không được giải thích là linh hoạt tối đa; Để minh họa các hàm và hằng số không giải thích được, hãy cho chúng tôi các hằng số nguyên không giải thích được (còn gọi là biến) x, y. Cuối cùng, hãy để f là một hàm không được giải thích, nhận một đối số kiểu (còn gọi là sắp xếp) số nguyên và cho kết quả là một giá trị số nguyên. Ví dụ minh họa cách người ta có thể buộc một diễn giải trong đó f áp dụng hai lần cho x lại dẫn đến x, nhưng f áp dụng một lần cho x khác với x x = Int('x')
y = Int('y')
print x**2 + y**2 >= 1
set_option(html_mode=False)
print x**2 + y**2 >= 1
6Giải pháp (diễn giải) cho f nên được đọc là f(0) là 1, f(1) là 0 và f(a) là 1 với mọi a khác 0 và 1 Trong Z3, chúng ta cũng có thể đánh giá các biểu thức trong mô hình cho một hệ ràng buộc. Ví dụ sau đây cho thấy cách sử dụng phương pháp đánh giá x = Int('x')
y = Int('y')
print x**2 + y**2 >= 1
set_option(html_mode=False)
print x**2 + y**2 >= 1
7Sự hài lòng và giá trịMột công thức/ràng buộc F hợp lệ nếu F luôn đánh giá là đúng đối với bất kỳ phép gán giá trị thích hợp nào cho các ký hiệu không được giải thích của nó. Một công thức/ràng buộc F có thể thỏa mãn nếu có một số phép gán giá trị thích hợp cho các ký hiệu không được giải thích của nó mà theo đó F đánh giá là đúng. Giá trị là về việc tìm kiếm bằng chứng của một tuyên bố; . Xét một công thức F chứa a và b. Chúng ta có thể đặt câu hỏi liệu F có hợp lệ hay không, nghĩa là liệu nó có luôn đúng với bất kỳ tổ hợp giá trị nào của a và b hay không. Nếu F luôn đúng thì Not(F) luôn sai, và khi đó Not(F) sẽ không có phép gán nào thỏa mãn (i. e. , dung dịch); . Nghĩa là, F có giá trị chính xác khi Not(F) không thỏa mãn (is unsatisfiable). Mặt khác, F thỏa mãn khi và chỉ khi Not(F) không hợp lệ (không hợp lệ). Ví dụ sau chứng minh định luật deMorgan Ví dụ sau định nghĩa lại chứng minh hàm Z3Py nhận công thức làm tham số. Hàm này tạo một bộ giải, thêm/xác nhận phủ định của công thức và kiểm tra xem phủ định có không thỏa mãn không. Việc thực hiện chức năng này là một phiên bản đơn giản hơn của lệnh Z3Py chứng minh x = Int('x')
y = Int('y')
print x**2 + y**2 >= 1
set_option(html_mode=False)
print x**2 + y**2 >= 1
8Liệt kê các hiểu biếtPython hỗ trợ hiểu danh sách. Khả năng hiểu danh sách cung cấp một cách ngắn gọn để tạo danh sách. Chúng có thể được sử dụng để tạo các biểu thức Z3 và các bài toán trong Z3Py. Ví dụ sau minh họa cách sử dụng khả năng hiểu danh sách Python trong Z3Py x = Int('x')
y = Int('y')
print x**2 + y**2 >= 1
set_option(html_mode=False)
print x**2 + y**2 >= 1
9Trong ví dụ trên, biểu thức "x%s" %i trả về một chuỗi trong đó %s được thay thế bằng giá trị của i Lệnh pp tương tự như print, nhưng nó sử dụng trình định dạng Z3Py cho danh sách và bộ dữ liệu thay vì trình định dạng của Python Z3Py cũng cung cấp các hàm để tạo vectơ của các biến Boolean, Integer và Real. Các chức năng này được thực hiện bằng cách sử dụng danh sách hiểu x = Int('x')
y = Int('y')
n = x + y >= 3
print "num args: ", n.num_args()
print "children: ", n.children()
print "1st child:", n.arg(0)
print "2nd child:", n.arg(1)
print "operator: ", n.decl()
print "op name: ", n.decl().name()
0phương trình động họcỞ trường trung học, học sinh học các phương trình động học. Các phương trình này mô tả mối quan hệ toán học giữa độ dời (d), thời gian (t), gia tốc (a), vận tốc ban đầu (v_i) và vận tốc cuối cùng (v_f). Trong ký hiệu Z3Py, chúng ta có thể viết các phương trình này dưới dạng x = Int('x')
y = Int('y')
n = x + y >= 3
print "num args: ", n.num_args()
print "children: ", n.children()
print "1st child:", n.arg(0)
print "2nd child:", n.arg(1)
print "operator: ", n.decl()
print "op name: ", n.decl().name()
1vấn đề 1Ima Rushin đang tiến đến đèn giao thông đang di chuyển với vận tốc 30. 0 mét/giây. Đèn chuyển sang màu vàng và Ima đạp phanh và trượt bánh để dừng lại. Nếu gia tốc của Ima là -8. 00 m/s2, từ đó xác định độ dời của ô tô trong quá trình trượt x = Int('x')
y = Int('y')
n = x + y >= 3
print "num args: ", n.num_args()
print "children: ", n.children()
print "1st child:", n.arg(0)
print "2nd child:", n.arg(1)
print "operator: ", n.decl()
print "op name: ", n.decl().name()
2vấn đề 2Ben Rushin đang đợi ở đèn giao thông. Cuối cùng khi nó chuyển sang màu xanh lục, Ben tăng tốc từ trạng thái nghỉ với tốc độ 6. 00 m/s2 trong thời gian 4. 10 giây. Xác định độ dời của xe ben trong khoảng thời gian trên x = Int('x')
y = Int('y')
n = x + y >= 3
print "num args: ", n.num_args()
print "children: ", n.children()
print "1st child:", n.arg(0)
print "2nd child:", n.arg(1)
print "operator: ", n.decl()
print "op name: ", n.decl().name()
3thủ thuật bitMột số hack cấp thấp rất phổ biến với các lập trình viên C. Chúng tôi sử dụng một số bản hack này trong quá trình triển khai Z3 Sức mạnh của haiCách hack này thường được sử dụng trong các chương trình C (bao gồm cả Z3) để kiểm tra xem một số nguyên của máy có phải là lũy thừa của hai hay không. Chúng ta có thể sử dụng Z3 để chứng minh nó thực sự hoạt động. Yêu cầu là x. = 0 &&. (x & (x - 1)) đúng khi và chỉ khi x là lũy thừa của hai x = Int('x')
y = Int('y')
n = x + y >= 3
print "num args: ", n.num_args()
print "children: ", n.children()
print "1st child:", n.arg(0)
print "2nd child:", n.arg(1)
print "operator: ", n.decl()
print "op name: ", n.decl().name()
4biển báo đối lậpCách hack đơn giản sau đây có thể được sử dụng để kiểm tra xem hai số nguyên máy có trái dấu hay không x = Int('x')
y = Int('y')
n = x + y >= 3
print "num args: ", n.num_args()
print "children: ", n.children()
print "1st child:", n.arg(0)
print "2nd child:", n.arg(1)
print "operator: ", n.decl()
print "op name: ", n.decl().name()
5câu đốChó, Mèo và ChuộtXét câu đố sau. Chi đúng 100 đô la và mua đúng 100 con vật. Chó có giá 15 đô la, mèo có giá 1 đô la và chuột có giá 25 xu mỗi con. Bạn phải mua ít nhất một trong mỗi. Bạn nên mua bao nhiêu cái mỗi loại? x = Int('x')
y = Int('y')
n = x + y >= 3
print "num args: ", n.num_args()
print "children: ", n.children()
print "1st child:", n.arg(0)
print "2nd child:", n.arg(1)
print "operator: ", n.decl()
print "op name: ", n.decl().name()
6SudokuSudoku là một câu đố rất phổ biến. Mục tiêu là chèn các số vào các ô để chỉ thỏa mãn một điều kiện. mỗi hàng, cột và hộp 3x3 phải chứa các chữ số từ 1 đến 9 chính xác một lần  Ví dụ sau mã hóa bài toán sudoku trong Z3. Các trường hợp sudoku khác nhau có thể được giải quyết bằng cách sửa đổi trường hợp ma trận. Ví dụ này sử dụng nhiều khả năng hiểu danh sách có sẵn trong ngôn ngữ lập trình Python x = Int('x')
y = Int('y')
n = x + y >= 3
print "num args: ", n.num_args()
print "children: ", n.children()
print "1st child:", n.arg(0)
print "2nd child:", n.arg(1)
print "operator: ", n.decl()
print "op name: ", n.decl().name()
7tám nữ hoàngCâu đố tám quân hậu là bài toán đặt tám quân hậu trên một bàn cờ 8x8 sao cho không có hai quân hậu nào tấn công lẫn nhau. Do đó, một giải pháp yêu cầu không có hai con hậu nào chia sẻ cùng một hàng, cột hoặc đường chéo x = Int('x')
y = Int('y')
n = x + y >= 3
print "num args: ", n.num_args()
print "children: ", n.children()
print "1st child:", n.arg(0)
print "2nd child:", n.arg(1)
print "operator: ", n.decl()
print "op name: ", n.decl().name()
8Ứng dụng. Sự cố cài đặtSự cố cài đặt bao gồm việc xác định xem có thể cài đặt một bộ gói mới trong hệ thống hay không. Ứng dụng này dựa trên bài viết OPIUM. Trình quản lý cài đặt/gỡ cài đặt gói tối ưu. Nhiều gói phụ thuộc vào các gói khác để cung cấp một số chức năng. Mỗi bản phân phối chứa một tệp siêu dữ liệu giải thích các yêu cầu của từng gói bản phân phối. Siêu dữ liệu chứa các chi tiết như tên, phiên bản, v.v. Quan trọng hơn, nó chứa các mệnh đề phụ thuộc và xung đột quy định các gói khác sẽ có trên hệ thống. Các mệnh đề phụ thuộc quy định các gói khác phải có mặt. Các điều khoản xung đột quy định các gói khác không được có mặt Vấn đề cài đặt có thể được giải quyết dễ dàng bằng Z3. Ý tưởng là xác định một biến Boolean cho mỗi gói. Biến này là đúng nếu gói phải có trong hệ thống. Nếu gói a phụ thuộc vào gói b, c và z, chúng tôi viết x = Int('x')
y = Int('y')
n = x + y >= 3
print "num args: ", n.num_args()
print "children: ", n.children()
print "1st child:", n.arg(0)
print "2nd child:", n.arg(1)
print "operator: ", n.decl()
print "op name: ", n.decl().name()
9DependsOn là một hàm Python đơn giản tạo ra các ràng buộc Z3 nắm bắt ngữ nghĩa của mệnh đề phụ thuộc x = Real('x')
y = Real('y')
solve(x**2 + y**2 > 3, x**3 + y < 5)
0Do đó, Depends(a, [b, c, z]) tạo ràng buộc x = Real('x')
y = Real('y')
solve(x**2 + y**2 > 3, x**3 + y < 5)
1Tức là người dùng cài gói a thì phải cài luôn gói b, c, z Nếu gói d xung đột với gói e, chúng tôi viết Xung đột (d, e). Xung đột cũng là một chức năng Python đơn giản x = Real('x')
y = Real('y')
solve(x**2 + y**2 > 3, x**3 + y < 5)
2Xung đột(d, e) tạo ra ràng buộc Or(Not(d), Not(e)). Với hai chức năng này, chúng ta có thể dễ dàng mã hóa ví dụ trong bài Thuốc phiện (Phần 2) trong Z3Py thành x = Real('x')
y = Real('y')
solve(x**2 + y**2 > 3, x**3 + y < 5)
3Lưu ý rằng ví dụ chứa ràng buộc x = Real('x')
y = Real('y')
solve(x**2 + y**2 > 3, x**3 + y < 5)
4Nghĩa là. để cài đặt c, chúng ta phải cài đặt d hoặc e và f hoặc g Bây giờ, chúng tôi tinh chỉnh ví dụ trước. Đầu tiên, chúng tôi sửa đổi DependsOn để cho phép chúng tôi viết DependsOn(b, d) thay vì DependsOn(b, [d]). Chúng tôi cũng viết một hàm install_check trả về danh sách các gói phải được cài đặt trong hệ thống. Chức năng Xung đột cũng được sửa đổi. Bây giờ nó có thể nhận được nhiều đối số x = Real('x')
y = Real('y')
solve(x**2 + y**2 > 3, x**3 + y < 5)
5Sử dụng Z3Py cục bộZ3Py là một phần của bản phân phối Z3. Nó nằm trong thư mục con python. Để sử dụng cục bộ, bạn phải đưa lệnh sau vào tập lệnh Python của mình x = Real('x')
y = Real('y')
solve(x**2 + y**2 > 3, x**3 + y < 5)
6Thư mục lối vào Z3 Python phải nằm trong biến môi trường PYTHONPATH của bạn. Z3Py sẽ tự động tìm kiếm thư viện Z3 (z3. dll (Windows), libz3. so (Linux) hoặc libz3. dylib (OSX)). Bạn cũng có thể khởi tạo thủ công Z3Py bằng lệnh |
