Z3での除外と組み込み

Question

Z3で要素の包含と除外をモデル化しようとしています。具体的には、異なる値を持つ要素を含めること、およびまだターゲットセットにない要素を除外することです。だから、基本的には、集合Uを持ち、Z3に、Uの要素だけが異なる値を持つ集合U_dを見つけさせたい。

私の現在のアプローチは、数量詞を使用しますが、彼らはU.

に表示された場合、私は、私はいつもU_dの要素を含めたいと述べている方法を理解悩みを抱えている

(set-option :produce-models true) 

;;; Two simple sorts. 
;;; Sets and Zs. 

(declare-sort Z 0) 
(declare-sort Set 0) 

;;; A set can contain a Z or not. 
;;; Zs can have a value. 

(declare-fun contains (Set Z) bool) 
(declare-fun value (Z) Int) 

;;; Two sets and two Z instances for use in the example. 

(declare-const set Set) 
(declare-const distinct_set Set) 

(declare-const A Z) 
(declare-const B Z) 

;;; The elements and sets are distinct.  

(assert (distinct A B)) 
(assert (distinct set distinct_set)) 

;;; Set 'set' contains A but not B 

(assert (= (contains set A) true)) 
(assert (= (contains set B) false)) 

;;; Assert that all elements contained by distinct_set have different values unless they're the same variable. 
(assert 
    (forall ((x Z) (y Z)) 
    (=> 
     (and 
      (contains distinct_set x) 
      (contains distinct_set y) 
      (= (value x) (value y))) 
     (= x y)))) 

;;; distinct_set can contain only elements that appear in set. 
;;; In other words, distinct_set is a proper set. 
(assert 
(forall ((x Z)) 
    (=> 
     (contains distinct_set x) 
     (contains set x)))) 

;;; Give elements some values. 
(assert (= (value A) 0)) 
(assert (= (value B) 1)) 

(push) 
(check-sat) 
(get-value ((contains distinct_set A))) 
(get-value ((contains distinct_set B))) 
(pop) 

それが生成割り当ては、次のとおりです。

私は希望

sat 
(((contains distinct_set A) false)) 
(((contains distinct_set B) false)) 

割り当ては、次のとおりです。

sat 
(((contains distinct_set A) true)) 
(((contains distinct_set B) false)) 

IアンダーAとBの両方にfalseを割り当てることは、論理的に正しい割り当てですが、私はそのようなケースを排除するような方法で状態をどのように表現するのか分かりません。

おそらく私は問題について正しく考えるつもりはありません。

アドバイスをいただければ幸いです。 :)

Answer 1

あなたは次の主張についてどう思いますか？

(assert 
(forall ((x Z)) 
     (=> (contains set x) 
      (exists ((y Z)) 
        (and (= (value x) (value y)) 
         (contains set y) 
         (contains distinct_set y)))))) 

はsetのすべての要素x（即ち、U）のために、y S。T.があることを述べていますyの

• 値はx
• yの値に等しいまたset
• yの要素がdistinct_setの要素（すなわち、U_d）

であるこのアサーションはことを確認します同じ値を持つsetに2つの要素がある場合、それらのうちの1つだけがdistinct_setの要素です。それはあなたが欲しいものですか？私たちはこの主張を追加した場合、Z3はまだ我々は(get-model)を使用してZ3が作成したモデルを検査した場合、我々はsetがAは異なる別の要素が含まれていることがわかります

(((contains distinct_set A) false)) 
(((contains distinct_set B) false)) 

モデルを生産する、という

注意。だから、唯一の要素Aを含むようにsetを強制するために、我々は、以下の二つの主張が冗長になりますが、この主張を追加した後

(assert 
(forall ((x Z)) 
     (= (contains set x) (= x A)))) 

を主張する必要があります。

(assert (= (contains set A) true)) 
(assert (= (contains set B) false)) 

を今、私たちはケースを考えてみましょうsetには、AとCという2つの値が含まれていますが、どちらも同じ値です。

• distinct_setがA

• distinct_setがAもC

• distinct_setAとC

が含まれているが含まれていませんが含まれていないモデルがあります：次のスクリプトはまたのような質問をします

スクリプト：

(set-option :produce-models true) 

;;; Two simple sorts. 
;;; Sets and Zs. 

(declare-sort Z 0) 
(declare-sort Set 0) 

;;; A set can contain a Z or not. 
;;; Zs can have a value. 

(declare-fun contains (Set Z) bool) 
(declare-fun value (Z) Int) 

;;; Two sets and two Z instances for use in the example. 

(declare-const set Set) 
(declare-const distinct_set Set) 

(declare-const A Z) 
(declare-const B Z) 
(declare-const C Z) 

;;; The elements and sets are distinct.  

(assert (distinct A B C)) 
(assert (distinct set distinct_set)) 

;;; set contains only A and C 
(assert 
(forall ((x Z)) 
     (= (contains set x) (or (= x A) (= x C))))) 

;;; Assert that all elements contained by distinct_set have different values unless they're the same variable. 
(assert 
    (forall ((x Z) (y Z)) 
    (=> 
     (and 
      (contains distinct_set x) 
      (contains distinct_set y) 
      (= (value x) (value y))) 
     (= x y)))) 

;;; distinct_set can contain only elements that appear in set. 
;;; In other words, distinct_set is a proper set. 
(assert 
(forall ((x Z)) 
    (=> 
     (contains distinct_set x) 
     (contains set x)))) 

;;; Give elements some values. 
(assert (= (value A) 0)) 
(assert (= (value B) 1)) 
(assert (= (value C) 0)) 

(assert 
(forall ((x Z)) 
     (=> (contains set x) 
      (exists ((y Z)) 
        (and (= (value x) (value y)) 
         (contains set y) 
         (contains distinct_set y)))))) 

(push) 
(check-sat) 
(get-model) 
(get-value ((contains distinct_set A))) 
(get-value ((contains distinct_set B))) 
(get-value ((contains distinct_set C))) 
(echo "Is there another model where A is not in distinct_set") 
(assert (not (contains distinct_set A))) 
(check-sat) 
(get-value ((contains distinct_set A))) 
(get-value ((contains distinct_set B))) 
(get-value ((contains distinct_set C))) 
(echo "Is there another model where A and C are not in distinct_set") 
(assert (not (contains distinct_set C))) 
(check-sat) 
(pop) ;; retracting the last two assertions 
(push) 
(echo "Is there a model where A and C are in distinct_set") 
(assert (contains distinct_set A)) 
(assert (contains distinct_set C)) 
(check-sat)