ブール関数を前提として 'check-sat'をサポートしていませんか？

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が実際に解決する問題は、入力問題とは非常に異なることがよくあります。単純化された仮定を元の仮定に戻して追跡したり、補助変数を導入したりします。ブールリテラルに制限することでこの問題を回避し、インターフェイスをきれいにすることができます。この制限は表現力を制限しないことに注意してください。あなたが異なるアサーションを追跡するために多くのブール変数を宣言するのはあまりにも迷惑であると思うなら。私はあなたがZ3Pyと呼ばれる新しいPythonフロントエンドZ3を見てみることをお勧めします。 SMT 2.0よりもはるかに便利です。 http://rise4fun.com/Z3Py/cL この例では、未解釈の述語pを作成する代わりに、 "ベクトル"（実際にはPythonのリストです）が作成されます。ブール定数が作成されます。

Z3Py online tutorialには多くの例があります。

補助変数を作成するアプローチをZ3Pyに実装することもできます。 トリックを行うスクリプトは次のとおりです。すべての配管作業を行う関数check_extを定義しました。 http://rise4fun.com/Z3Py/B4