Tôi sẽ tạo một mảng với kích thước cố định và khởi tạo nó với một số giá trị.Tạo một mảng với kích thước cố định và khởi tạo nó
Ví dụ, C++ mã sau:
a[0] = 10;
a[1] = 23;
a[2] = 27;
a[3] = 12;
a[4] = 19;
a[5] = 31;
a[6] = 41;
a[7] = 7;
Có một số tiện ích trong Z3 để mô hình nó?
Z3 hỗ trợ lý thuyết mảng, nhưng thường được sử dụng để mã hóa mảng không bị chặn hoặc mảng rất lớn. Bởi lớn, tôi có nghĩa là số lượng truy cập mảng (tức là, chọn) trong công thức của bạn là nhỏ hơn nhiều so với kích thước thực tế của mảng. Chúng ta nên tự hỏi: "chúng ta thực sự cần mảng để mô hình hóa/giải quyết vấn đề X?". Đối với các mảng kích thước cố định như trong ví dụ của bạn, chúng ta có thể sử dụng một biến khác cho mỗi vị trí mảng. Ví dụ: a0 cho a[0], a1 cho a[1], vv Tất nhiên, nếu chúng ta không sử dụng lý thuyết, sau đó mã hóa một truy cập mảng như a[i] phải được mã hóa như một thuật ngữ if-then-else lớn như
(ite (= i 0) a0 (ite (= i 1) a1 ...))
Nếu kích thước mảng được biết đến và nhỏ, thì đây thường là phương pháp hiệu quả nhất để mã hóa sự cố.
Mặt khác, nếu bạn quyết định sử dụng các lý thuyết mảng, bạn có thể mã hóa các khởi tạo trong câu hỏi của bạn như sau:
(declare-const a (Array Int Int))
(assert (= (select a 0) 10))
...
(assert (= (select a 7) 7))
Dưới đây là toàn bộ ví dụ mã hóa dưới dạng SMT 2.0:
Lưu ý rằng để mã hóa cập nhật trên mảng này. Ví dụ, câu lệnh C a[3] = 5, chúng ta phải tạo một biến mảng mới biểu diễn mảng sau phép gán này. Cách nhỏ gọn nhất sử dụng biểu thức store:
(declare-const a1 (Array Int Int))
(assert (= a1 (store a 3 5)))
Dưới đây là ví dụ đầy đủ về bản cập nhật.
Bạn cũng có thể xem xét API Python/C++ /. Chúng cho phép chúng tôi mã hóa các ví dụ giống như của bạn theo cách nhỏ gọn hơn nhiều. Ý tưởng là triển khai các hàm mã hóa các mẫu thường được sử dụng như khởi tạo mảng. Đây là ví dụ khởi tạo mảng của bạn bằng Python:
Liên kết cuối cùng đã chết – Elazar