重寫公式

在this paper（3.2節）中，它表示z3在執行任何其他步驟之前應用公式的重寫/簡化。重寫公式

假設我在QF_UF中有一個公式，它由多個assert語句組成。是否有任何重寫規則會以某種方式「打破不同的斷言陳述之間的障礙」？或者，反過來問：我能確定重寫規則只適用於本地，「在一個斷言聲明中」。

例如，請考慮下面的公式：

(set-logic QF_UF) 
(set-option :auto-config false) 
(set-option :PROOF_MODE 2) 

(declare-fun a() Bool) 
(assert a) 
(assert (not a)) 

(check-sat) 
(get-proof)

我可以肯定的是，證明將包含一項決議，一步證明False，或者是有可能，False將被重寫/簡化步驟總結？

我問的原因是，對於我的應用程序，每個assert語句都有一個特殊的語義。對幾個assert陳述進行重寫/簡化會導致對我不可用的結果證明（或至少：非常難以使用）。

來源

2012-04-24 Georg

你能描述你是什麼試圖做什麼？爲什麼跨幾個斷言的重寫/簡化會使結果無法使用？請注意，在搜索期間，Z3將執行多個斷言的推理步驟。這是否也會使證據無法使用？ – 2012-04-24 16:21:30

我正試圖重寫「純」分辨率證明的證明。出於應用程序特定的原因，在一個assert語句中發生的簡化和重寫對我來說並不重要。也就是說，我會簡單地假設assert語句已經包含公式的簡化版本。所有關於聲明陳述的推理步驟都是我感興趣的，我必須以某種方式處理它們。如果我能確定斷言中沒有發生簡化，那麼當我重寫時，我會遇到一個（困難）案件難以處理。我希望這可以讓它更清楚一點。 – Georg 2012-04-25 09:02:22

Z3 3.2應用了幾個預處理步驟。使用(set-option :auto-config false)將禁用它們中的大部分。你還應該包括以下兩個選項：

（設置選項：傳播 - 布爾假）

（設置選項：傳播值假）

來源

2012-04-25 18:12:27

感謝您的信息。這些選項是否可以保證不會發生聲明陳述中的重寫/簡化？ – Georg 2012-05-02 05:19:13

是的，它會保證在Z3 3.2中。 – 2012-05-02 14:45:13

回答

相關問題