不支持布爾函數作爲假設嗎？

Question

在以下示例中，我嘗試使用「（declare-const p（Int）Bool）」等未解釋的布爾函數，而不是每個假設的單個布爾常量。但它不起作用（它給編譯錯誤）。

(set-option :produce-unsat-cores true) 
(set-option :produce-models true) 

(declare-fun p (Int) Bool) 
      ;(declare-const p1 Bool) 
      ;(declare-const p2 Bool) 
      ; (declare-const p3 Bool) 

;; We assert (=> p C) to track C using p 
(declare-const x Int) 
(declare-const y Int) 
(assert (=> (p 1) (> x 10))) 
;; An Boolean constant may track more than one formula 
(assert (=> (p 1) (> y x))) 

(assert (=> (p 2) (< y 5))) 
(assert (=> (p 3) (> y 0))) 

(check-sat (p 1) (p 2) (p 3)) 
(get-unsat-core) 

輸出

Z3(18, 16): ERROR: invalid check-sat command, 'not' expected, assumptions must be Boolean literals 
Z3(19, 19): ERROR: unsat core is not available 

我所知，這是不可能的（不支持）使用布爾函數。這背後有什麼理由嗎？有沒有不同的方式來做到這一點？

Answer 1

我們有這個限制，因爲Z3在解決問題之前應用了許多簡化。其中一些將重寫公式和術語。 Z3實際解決的問題通常與輸入問題有很大不同。我們會追溯簡化的假設到原來的假設，或者引入輔助變量。限制爲布爾文字避免了這個問題，並使界面非常乾淨。請注意，此限制不會限制表現力。如果您認爲聲明許多布爾變量來跟蹤不同的斷言太煩人了。我建議你看看Z3的新的Python前端Z3Py。使用比SMT 2.0更方便。以下是您在Z3Py中的示例：http://rise4fun.com/Z3Py/cL 在此示例中，不是創建未解釋的謂詞p，而是「矢量」（實際上，它是一個Python列表）o創建布爾常量。

Z3Py online tutorial包含很多例子。

也可以在Z3Py中實現創建輔助變量的方法。 這是做這個伎倆的腳本。我定義了一個功能check_ext，可以完成所有的管道工作。 http://rise4fun.com/Z3Py/B4