7
Tôi đang cố mã hóa QBF theo cú pháp smt-lib 2 cho z3. Chạy kết quả z3 trong một cảnh báoĐịnh lượng và mẫu (công thức QBF)
CẢNH BÁO: thất bại trong việc tìm ra một khuôn mẫu cho lượng hóa (lượng hóa id: 14 k)
và kết quả satisfiability là "không rõ".
Mã này là như sau:
(declare-fun R (Bool Bool Bool Bool) Bool)
(assert
(forall ((x2 Bool) (x3 Bool))
(exists ((y Bool))
(forall ((x1 Bool))
(R x1 x2 x3 y)
)
)
)
)
(check-sat)
Tôi đã thoát khỏi những cảnh báo bằng cách viết lại mã để
(set-option :auto-config false)
(set-option :mbqi false)
(declare-fun R (Bool Bool Bool Bool) Bool)
(declare-fun x1() Bool)
(declare-fun x2() Bool)
(declare-fun x3() Bool)
(declare-fun y() Bool)
(assert
(forall ((x2 Bool) (x3 Bool))
(!
(exists ((y Bool))
(!
(forall ((x1 Bool))
(!
(R x1 x2 x3 y)
:pattern((R x1 x2 x3 y)))
)
:pattern((R x1 x2 x3 y)))
)
:pattern((R x1 x2 x3 y)))
)
)
(check-sat)
Kết quả cho ngồi truy vấn, tuy nhiên, vẫn còn "không rõ".
Tôi đoán rằng tôi cần lấy mẫu đúng không? Làm cách nào để chỉ định chúng cho các số lượng lồng nhau? Ví dụ đơn giản với định lượng dường như hoạt động mà không có chú thích mẫu.
Câu trả lời cho What is the reason behind the warning message in Z3: "failed to find a pattern for quantifier (quantifier id: k!18) " và hướng dẫn z3 không giúp tôi quá nhiều, thật không may.