Исключение и включение в Z3

Question

Я пытаюсь смоделировать включение и исключение элементов в наборах с Z3. В частности, включение элементов с различными значениями и исключение элементов, которые еще не включены в целевой набор. Поэтому в основном я хочу иметь набор U и Z3 найти набор U_d, который содержит только элементы U с различными значениями.

В моем текущем подходе используются квантификаторы, но у меня возникают проблемы с пониманием того, как утверждать, что я хочу всегда включать элементы в U_d, если они появляются в 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 )

Выполняемые задания:

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

Я хотел бы получить следующие задания:

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

Я понимаю, что присвоение false как A, так и B является логически правильным назначением, но я не знаю, как сформулировать вещи таким образом, чтобы исключить подобные случаи.

Возможно, я не думаю о проблеме правильно.

Любой совет будет высоко ценится. :)

Answer 1

Что вы думаете о следующем утверждении?

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

В нем говорится, что для каждого элемента x из set (т. Е. U) существует y s.t.

• значение y равно значению x
• y также является элементом set
• y является элементом distinct_set (т.е. U_d)

Это утверждение гарантирует, что если в set есть два элемента с одинаковым значением, то один и только один из них является элементом distinct_set. Это то, что вы хотите?

Обратите внимание, что, если мы просто добавим это утверждение, Z3 все равно создаст модель, в которой

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

Если мы проверим модель, созданную Z3 с использованием (get-model), мы заметим, что set содержит другой элемент, отличный от A. Итак, чтобы заставить set содержать только элемент A, мы должны утверждать

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

После добавления этого утверждения следующие два утверждения становятся избыточными:

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

Теперь рассмотрим случай, когда set содержит два значения: A и C, и оба имеют одинаковое значение. Следующий скрипт также задает такие вопросы, как: есть ли модель, где

• distinct_set не содержит A

• distinct_set не содержит A и C

• distinct_set содержит A и C

Сценарий:

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