Отдельные значения массива в решателе z3 SMT

Некоторое время я пытался выполнить довольно простое требование: я объявил новый тип данных

(declare-datatypes () ((A (mk_A (key Int) (var1 Int) (var2 Int)))))

где key должен действовать как первичный ключ в базе данных, т. е. каждый отдельный экземпляр A должен иметь другое значение key. Контейнер различных экземпляров (функций) выглядит следующим образом:

(declare-const A_instances (Array Int A))

Все идет нормально. Я попытался создать утверждение, чтобы все экземпляры в A_instances имели другое поле key. Таким образом, для каждого индекса i в A_instances (key (select A_instances i)) должны быть разными. Однако он возвращает unknown.

У кого-нибудь есть предложения?


z3 smt
person paubo147    schedule 29.08.2014    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Одним из возможных решений является

(declare-datatypes () ((A (mk_A (key Int) (var1 Int) (var2 Int)))))
(declare-const A_instances (Array Int A))
(declare-fun j () Int)
(assert (forall ((i Int))  (implies (distinct i j) 
                           (distinct (key (select A_instances i))  
                                     (key (select A_instances j)))        )   ))
(check-sat)

и соответствующий вывод

sat
person Juan Ospina    schedule 29.08.2014