6

z3 で修士論文に取り組んでいるときに、理解できない奇妙なことがわかりました。あなたが私を助けてくれることを願っています。:)

私が書いたsmtファイルは次のようになります。

(set-logic QF_UF)
(set-info :smt-lib-version 2.0)

;Declare sort Node and its objects.
(declare-sort Node 0)
(declare-fun n0 () Node)
(declare-fun n1 () Node)

;Predicate
(declare-fun dead_0 (Node) Bool)
;Abbreviation
(declare-fun I () Bool)

;initial configuration
(assert(= I (and 
(not(= n0 n1))
(not(dead_0 n0))
(dead_0 n1))))

;Predicate
(declare-fun dead_1 (Node) Bool)
;variable
(declare-fun m0_1 () Node)

;Abbreviation for Transformation
(declare-fun TL1_1 () Bool)

;Transformation1neuerKnoten1
(assert(or (= m0_1 n0)(= m0_1 n1)))

;Is the whole formula satisfiable?
(assert(= (and I TL1_1) true))
(check-sat)
(get-model)

z3 をデフォルト オプション付きのコマンド ライン ツールとして使用すると、すべてがうまく機能します。生成されたモデルには以下が含まれます。

;; universe for Node:
;;   Node!val!0 Node!val!1 
;; -----------

と

(define-fun n0 () Node
Node!val!0)
(define-fun n1 () Node
Node!val!1)
(define-fun m0_1 () Node
Node!val!0)

したがって、変数 m0_1 はノード n0 にバインドされます。

次に、.z3 のみを含む ini ファイルで使用しましたCASE_SPLIT=5。結果は奇妙なモデルでした。私の意見では、違いは基本的に、変数 m0_1 がノード n0 または n1 のいずれにもバインドされていないことです。生成されたモデルには以下が含まれます。

;; universe for Node:
;;   Node!val!2 Node!val!0 Node!val!1 
;; -----------

と

(define-fun n0 () Node
Node!val!0)
(define-fun n1 () Node
Node!val!1)
(define-fun m0_1 () Node
Node!val!2)

私の質問は次のとおりです。なぜ z3 は別のノード ( Node!val!2) を作成し、変数m0_1がこの新しいノードにバインドされているのはなぜですか? 私は、私の主張の 1 つ ( (assert(or (= m0_1 n0)(= m0_1 n1)))) がこれを禁止すると考えていました。

前もって感謝します！:)

4

1 に答える 1

5

Z3には、「関連性の伝播」と呼ばれる機能があります。この機能は、数量詞を含む問題には非常に効果的ですが、通常、数量詞のない問題にはオーバーヘッドがあります。コマンドラインオプションRELEVANCY=0は、関連性の伝播を無効にするRELEVANCY=2か、RELEVANCY=1有効にします。このオプションCASE_SPLIT=5は、関連性の伝播が有効になっていることを前提としています。を提供するCASE_SPLIT=5 RELEVANCY=0と、Z3は警告メッセージを生成します

WARNING: relevacy must be enabled to use option CASE_SPLIT=3, 4 or 5

そして、オプションを無視します。

さらに、デフォルトでは、Z3は「自動構成」機能を使用します。この機能は、入力式をスキャンし、特定のインスタンスのZ3構成を調整します。したがって、あなたの例では、次のことが起こります。

  1. オプションを提供しますCASE_SPLIT=5
  2. Z3がコマンドラインオプションを検証すると、関連性の伝播が無効になり、警告メッセージは生成されません。
  3. Z3は自動構成手順を実行します。この例では数量詞がないため、関連性の伝播が無効になりますRELEVANCY=0。現在、一貫性のない構成が使用されており、Z3は間違った結果を生成します。

この問題を回避するには、を使用する場合は、 （自動構成を無効にする）および（関連性の伝播を有効にする）CASE_SPLIT=5も使用する必要があります。したがって、コマンドラインは次のようになります。AUTO_CONFIG=falseRELEVANCY=2

z3 CASE_SPLIT=5 AUTO_CONFIG=false RELEVANCY=2 file.smt2

CASE_SPLIT=5次のリリース（Z3 4.2）では、自動構成が有効になっているときにユーザーが設定しようとすると、警告メッセージを表示するようにZ3を作成します。

于 2012-09-20T15:48:39.720 に答える