2

私はZ3で働く新しい人です。

セットと2つの異なるセットの最大値を計算する方法を知りたいです。

例： [1, 6, 5]-大きい方は [1, 6, 5]6e-[10, 7, 2]大きい方は6

次のコードを使用して設定します。

    (declare-sort Set 0)

(declare-fun contains (Set Int) bool)

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

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

( assert ( =  A 0 ) )
( assert ( =  B 1 ) )
( assert ( =  C 2 ) )

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

(assert
 (forall ((x Int))
         (= (contains set x) (or (= x A) (= x C)))))

そして、セット（set）の最大値とセット（setおよびdistinct_set）の最大値を計算する方法を知りたいと思います。

それがすべての整数に当てはまるのは、それが簡単だったからです。

(define-fun max ((x Int) (y Int)) Int
  (ite (< x y) y x))

しかし、私はそれらの整数によるセットを残すことはできません、すなわち、セットされた値を取得します。

手伝って頂けますか？

ありがとう

4

1 に答える 1

6

次のエンコーディングは目的に適していますか? こちらからオンラインでも入手できます。

; We Enconde each set S of integers as a function S : Int -> Bool
(declare-fun S1 (Int) Bool)
; To assert that A and C are elements of S1, we just assert (S1 A) and (S1 C) 
(declare-const A Int)
(declare-const C Int)
(assert (S1 A))
(assert (S1 C))
; To say that B is not an element of S1, we just assert (not (S1 B))
(declare-const B Int)
(assert (not (S1 B)))

; Now, let max_S1 be the max value in S1
(declare-const max_S1 Int)
; Then, we now that max_S1 is an element of S1, that is
(assert (S1 max_S1))
; All elements in S1 are smaller than or equal to max_S1
(assert (forall ((x Int)) (=> (S1 x) (not (>= x (+ max_S1 1))))))

; Now, let us define a set S2 and S3
(declare-fun S2 (Int) Bool)
(declare-fun S3 (Int) Bool)
; To assert that S3 is equal to the union of S1 and S2, we just assert
(assert (forall ((x Int)) (= (S3 x) (or (S1 x) (S2 x)))))

; To assert that S3 is not equal to S1 we assert
(assert (exists ((x Int)) (not (= (S3 x) (S1 x)))))

(check-sat)

; Now let max_S3 be the maximal value of S3
(declare-const max_S3 Int)
(assert (S3 max_S3))
(assert (forall ((x Int)) (=> (S3 x) (not (>= x (+ max_S3 1))))))

; the set of constraints is still satisfiable
(check-sat)

; Now, let us assert that max_S3 < max_S1.
; It should be unsat, since S3 is a super set of S1
(assert (< max_S3 max_S1))
(check-sat)
于 2013-03-14T02:13:50.183 に答える