Có thể sử dụng Z3 để xử lý trước sự cố không?

Question

Thực hiện nghiên cứu mới về máy giải quyết SMT nhiều lần bị cản trở bởi thực tế là các vấn đề sẵn có đòi hỏi rất nhiều thủ thuật và kỹ thuật tiền xử lý không liên quan trực tiếp đến các thủ tục quyết định. Chúng thường không được xuất bản hoặc mất thời gian để triển khai và tối ưu hóa đúng cách, và ngoài ra, việc so sánh và hiểu biết về những người giải quyết khác nhau khá khó khăn.

Có thể sử dụng Z3 làm bộ xử lý trước có vấn đề và đổ nó ra dưới dạng được xử lý trước (bản thân z3 dùng để giải quyết vấn đề)?

Tôi không thấy bất kỳ tùy chọn dòng lệnh nào, nhưng tôi đoán rằng có thể có một số cách để đạt được điều này, thông qua chiến lược, thông qua giao diện python hoặc thậm chí viết thêm một số mã.

Answer 1

Có, Z3 có thể được sử dụng làm bộ xử lý trước. Lệnh apply cho phép người dùng áp dụng chiến thuật và kết xuất nó dưới dạng điểm chuẩn SMT 2.0. Dưới đây là một ví dụ (cũng có sẵn trực tuyến tại http://rise4fun.com/Z3/eutO):

(declare-const x Real) 
(declare-const y Real) 

(assert (forall ((n Real)) (or (< x n) (< n y)))) 
(assert (= (< x y) (< x 100.0))) 

(apply (then qe nnf) :print false :print-benchmark true) 

Trong ví dụ trên, nới lỏng tiền tệ (loại bỏ lượng hóa) và nnf (phủ định-bình thường-form) chiến thuật được áp dụng cho các vấn đề đầu vào.

Một số điểm bổ sung:

• Một số chiến thuật chỉ tạo ra kết quả equisatisfiable. Do đó, một mô hình cho điểm chuẩn kết quả không nhất thiết phải là một mô hình cho công thức ban đầu. Chúng ta có thể yêu cầu Z3 kết xuất "model-converter" liên quan (tùy chọn :print-model-converter true). Trình chuyển đổi mô hình mã hóa các bước được Z3 sử dụng để chuyển đổi một mô hình cho công thức kết quả thành một mô hình cho công thức ban đầu. Tuy nhiên, không có tiêu chuẩn cho việc chuyển đổi mô hình in ấn, và Z3 không thể đọc các mô tả này. Tất nhiên, chúng ta có thể dán mọi thứ lại với nhau bằng cách sử dụng các API có lập trình.

• Một bộ chiến thuật nhỏ sản xuất theo (chỉ kết quả ngồi có thể tin cậy) hoặc hơn (chỉ các kết quả không đáng tin cậy mới có thể tin cậy) xấp xỉ. Chúng thường được sử dụng trong mô hình hoặc tìm kiếm bằng chứng. Khi Z3 hiển thị mục tiêu kết quả, nó sẽ thông báo với kết quả là chính xác (sat và unsat có thể được tin cậy).