如何簡化兩個表達式的工會：Z3求解

Question

由SMT求解器產生的結果是：

(or (and (>= c1 2) (<= c1 4) (= (+ c0 c1 c2) 5) (= (+ c0 c1) 4)) 
    (and (>= c1 1) (<= c1 3) (= (+ c0 c1 c2) 5) (= (+ c0 c1) 4))) 

但我希望是這樣的：

(and (>= c1 1) (<= c1 4) (= (+ c0 c1 c2) 5) (= (+ c0 c1) 4) 

有人可以指導我實現這與Z3求解器？

鏈接：http://rise4fun.com/Z3/1Xz3

Answer 1

Z3不支持這種簡單化的。它不支持簡化爲「正常形式」。回想一下，Z3的主要接口是檢查公式是否可滿足或不可滿足。 如果您能夠確定哪些文字應在連詞中進行測試，您可以向SMT求解器詢問多個查詢以提取等同於公式的連詞。正如您的示例所示，這並不總是可以用語法的方式來完成。