z3 - 集合 z3 中的最大值

Question

我是 Z3 的新手。

想知道如何计算一个集合和两个不同集合的最大值。

例如:[1, 6, 5] - 较大的是 6[1, 6, 5] e [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))

但我不能通过整数离开集合，即获取已设置的值。

你能帮帮我吗？

谢谢

Answer 1

以下编码是否适合您的目的？也可以在线获得 here .

; 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)