集z3中的最大值

Question

我是一个与Z3合作的新人。

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

例如： [1, 6, 5] - 越大6 [1, 6, 5]Ë[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）中的最大值和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)