集合 z3 中的最大值 [英] max value in set z3

问题描述

我是 Z3 的新手.

想知道如何计算一组和两个不同组的最大值.

Would like to know how I can calculate the maximum value of a set and two different sets.

例如:[1, 6, 5] - 6[1, 6, 5] e [10, 7, 2] - 6 越大

For example: [1, 6, 5] - The greater is 6 [1, 6, 5] e [10, 7, 2] - The greater is 6

我用下面的代码来设置:

I use the following code to set:

    (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)中的最大值.

And now would like to know how can I calculate the largest value in the set (set) and the largest value in sets (set and distinct_set).

如果是所有整数只是因为它很容易做到:

If it was for all integers was only because it was easy to do:

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

但是我不能用集合的整数离开，即得到已经设置的值.

But I can not leave with sets by their integers, ie, get the values ​​that have set.

你能帮我吗?

谢谢

推荐答案

以下编码对于您的目的是否合理?它也可以在线使用这里.

Is the following encoding reasonable for your purposes? It is also available online 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)

这篇关于集合 z3 中的最大值的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！