Exclusion and inclusion in Z3

Question

I am trying to model inclusion and exclusion of elements in sets with Z3. In particular inclusion of elements with distinct values, and exclusion of elements not already in a target set. So basically I want to have a set U and have Z3 find a set U_d that only contains elements of U with distinct values.

My current approach uses quantifiers, but I'm having trouble understanding how to state that I want to always include elements in U_d if they appear in U.

( set-option :produce-models true)

;;; Two simple sorts.
;;; Sets and Zs.

( declare-sort Z   0 )
( declare-sort Set 0 )

;;; A set can contain a Z or not.
;;; Zs can have a value.

( declare-fun contains (Set Z) bool )
( declare-fun value (Z) Int )

;;; Two sets and two Z instances for use in the example.

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

( declare-const A Z )
( declare-const B Z )

;;; The elements and sets are distinct.     

( assert ( distinct A B ) )
( assert ( distinct set distinct_set ) )

;;; Set 'set' contains A but not B

( assert ( = ( contains set A ) true ) )
( assert ( = ( contains set B ) false ) )

;;; Assert that all elements contained by distinct_set have different values unless they're the same variable.
( assert
  ( forall ( (x Z) (y Z) )
    ( =>
        ( and 
            ( contains distinct_set x )
            ( contains distinct_set y )
            ( = ( value x ) ( value y ) ) )
        ( = x y ) )))

;;; distinct_set can contain only elements that appear in set.
;;; In other words, distinct_set is a proper set.
( assert
( forall ( ( x Z ) )
    ( =>
        ( contains distinct_set x )
        ( contains set x ))))

;;; Give elements some values.
( assert ( = (value A) 0 ) )
( assert ( = (value B) 1 ) )

( push )
( check-sat )
( get-value (( contains distinct_set A )))
( get-value (( contains distinct_set B )))
( pop )

The assignments it produces are:

sat
((( contains distinct_set A ) false))
((( contains distinct_set B ) false))

The assignments I would like are:

sat
((( contains distinct_set A ) true))
((( contains distinct_set B ) false))

I understand that an assignment of false to both A and B is a logically correct assignment, but I don't know how to state things in such a way as to rule those sorts of cases out.

Perhaps I'm not thinking about the problem correctly.

Any advice would be much appreciated. :)

Answer 1

What do you think of the following assertion?

(assert
(forall ((x Z))
        (=> (contains set x)
            (exists ((y Z))
                    (and (= (value x) (value y))
                         (contains set y)
                         (contains distinct_set y))))))

It says that for every element x of set (i.e., U), there is a y s.t.

• value of y is equal to value of x
• y is also an element of set
• y is an element of distinct_set (i.e., U_d)

This assertion makes sure that if there are two elements in set with the same value, then one and only one of them is an element of distinct_set. Is that what you want?

Note that, if we just add this assertion, Z3 will still produce a model where

((( contains distinct_set A ) false))
((( contains distinct_set B ) false))

If we inspect the model produced by Z3 using (get-model), we will notice that set contains another element different from A. So, to force set to contain only the element A, we have to assert

(assert
 (forall ((x Z))
         (= (contains set x) (= x A))))

After you add this assertion, the following two assertions become redundant:

( assert ( = ( contains set A ) true ) )
( assert ( = ( contains set B ) false ) )

Now, let us consider the case where set contains two values: A and C, and they both have the same value. The following script also asks questions such as: is there a model where

• distinct_set does not contain A

• distinct_set does not contain A nor C

• distinct_set contains A and C

Script:

( set-option :produce-models true)

;;; Two simple sorts.
;;; Sets and Zs.

( declare-sort Z   0 )
( declare-sort Set 0 )

;;; A set can contain a Z or not.
;;; Zs can have a value.

( declare-fun contains (Set Z) bool )
( declare-fun value (Z) Int )

;;; Two sets and two Z instances for use in the example.

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

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

;;; The elements and sets are distinct.     

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

;;; set contains only A and C
 (assert
 (forall ((x Z))
         (= (contains set x) (or (= x A) (= x C)))))

;;; Assert that all elements contained by distinct_set have different values unless they're the same variable.
( assert
  ( forall ( (x Z) (y Z) )
    ( =>
        ( and 
            ( contains distinct_set x )
            ( contains distinct_set y )
            ( = ( value x ) ( value y ) ) )
        ( = x y ) )))

;;; distinct_set can contain only elements that appear in set.
;;; In other words, distinct_set is a proper set.
( assert
( forall ( ( x Z ) )
   ( =>
       ( contains distinct_set x )
       ( contains set x ))))

;;; Give elements some values.
( assert ( = (value A) 0 ) )
( assert ( = (value B) 1 ) )
( assert ( = (value C) 0 ) )

(assert
(forall ((x Z))
        (=> (contains set x)
            (exists ((y Z))
                    (and (= (value x) (value y))
                         (contains set y)
                         (contains distinct_set y))))))

( push )
( check-sat )
( get-model )
( get-value (( contains distinct_set A )))
( get-value (( contains distinct_set B )))
( get-value (( contains distinct_set C )))
( echo "Is there another model where A is not in distinct_set")
( assert (not ( contains distinct_set A )))
(check-sat)
( get-value (( contains distinct_set A )))
( get-value (( contains distinct_set B )))
( get-value (( contains distinct_set C )))
( echo "Is there another model where A and C are not in distinct_set")
( assert (not ( contains distinct_set C )))
(check-sat)
( pop ) ;; retracting the last two assertions
( push )
( echo "Is there a model where A and C are in distinct_set")
( assert ( contains distinct_set A ))
( assert ( contains distinct_set C ))
( check-sat )