1

少し前に、セットを含む制約のモデルを取得するために Z3 を使用する方法を尋ねました (セットを含む制約のモデルを取得するために Z3 を使用する方法はありますか? )。このため、私の場合は拡張配列理論がうまく機能します。

今、私はシーケンス（操作の長さ、メンバーシップ、（不）等式、おそらくスライス）とマップで同じ問題を抱えています。つまり、公理化は集合と同じ問題を引き起こします。拡張配列理論を使用してシーケンスとマップをエンコードすることも考えていますが、これを行うための良い方法をまだ思い付くことができていません。

正確なモデルを取得するためにシーケンスとマップをエンコードする方法について、誰か考えがありますか?

4

1 に答える 1

2

Z3 では、配列は基本的にマップです。整数のリストから整数への「配列」を作成する方法の例を次に示します。

(declare-const a (Array (List Int) Int))
(declare-const l1 (List Int))
(declare-const l2 (List Int))
(assert (= (select a l1) 0))
(assert (= (select a l2) 0))
(check-sat)
(get-model)

シーケンスの場合、量指定子を使用してエンコードできます。Z3 は、多くの決定可能なフラグメントに対して完全です。それらのほとんどはZ3 チュートリアルで説明されています。これが可能なエンコーディングです。

;; In this example, we are encoding sequences of T.
;; Let us make T == Int
(define-sort T () Int)

;; We represent a sequence as a pair: function + length
(declare-fun S1-data (Int) T)
(declare-const S1-len  Int)

(declare-fun S2-data (Int) T)
(declare-const S2-len  Int)

(declare-fun S3-data (Int) T)
(declare-const S3-len  Int)

;; This encoding has one limitation, we can't have sequences of sequences; nor have sequences as arguments of functions.

;; Here is how we assert that the sequences S1 and S2 are equal.
(push)
(assert (= S1-len S2-len)) 
(assert (forall ((i Int)) (=> (and (<= 0 i) (< i S1-len)) (= (S1-data i) (S2-data i)))))
;; To make the example more interesting, let us assume S1-len > 0
(assert (> S1-len 0))
(check-sat)
(get-model)
(pop)

;; Here is how we say that sequence S3 is the concatenation of sequences S1 and S2.
(push)
(assert (= S3-len (+ S1-len S2-len)))
(assert (forall ((i Int)) (=> (and (<= 0 i) (< i S1-len)) (= (S3-data i) (S1-data i)))))
(assert (forall ((i Int)) (=> (and (<= 0 i) (< i S2-len)) (= (S3-data (+ i S1-len)) (S2-data i)))))
;; let us assert that S1-len and S2-len > 1
(assert (> S1-len 1))
(assert (> S2-len 1))
;; let us also assert that S3(0) != S3(1)
(assert (not (= (S3-data 0) (S3-data 1))))
(check-sat)
(get-model)
(pop)

;; Here is how we encode that sequence S2 is sequence S1 with one extra element a
(push)
(declare-const a T)
(assert (> a 10))
(assert (= S2-len (+ 1 S1-len)))
(assert (= (S2-data S1-len) a))
(assert (forall ((i Int)) (=> (and (<= 0 i) (< i S1-len)) (= (S2-data i) (S1-data i)))))
;; let us also assert that S1-len > 1
(assert (> S1-len 1))
(check-sat)
(get-model)
(pop)
于 2013-10-13T17:07:47.057 に答える