Исключение и включение в 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)) 

I Unders и что назначение 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)