Равенство констант в решателе Z3 SMT

Я использую решатель Z3 SMT от Microsoft и пытаюсь определить константы пользовательского вида. Кажется, что такие константы по умолчанию не являются неравными. Предположим, у вас есть следующая программа:

(declare-sort S 0)

(declare-const x S)
(declare-const y S)

(assert (= x y))
(check-sat)

Это даст «sat», потому что вполне возможно, что две константы одного и того же типа равны. Поскольку я делаю модель, в которой константы должны отличаться друг от друга, это означает, что мне нужно будет добавить аксиому вида

(assert (not (= x y)))

для каждой пары констант одного и того же вида. Мне было интересно, есть ли способ сделать это общим, чтобы каждая константа сортировки была уникальной по умолчанию.


logic solver z3 smt
person marczoid    schedule 14.10.2012    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Вы можете использовать типы данных для кодирования типов перечисления, которые можно найти во многих языках программирования. В следующем примере сортировка S состоит из трех элементов, и они отличаются друг от друга.

(declare-datatypes () ((S a b c)))

Вот полный пример: http://rise4fun.com/Z3/ncPc

(declare-datatypes () ((S a b c)))

(echo "a and b are different")
(simplify (= a b))

; x must be equal to a, b or c
(declare-const x S)

; since x != a, then it must be b or c
(assert (not (= x a)))
(check-sat)
(get-model)
; in the next check-sat x must be c
(assert (not (= x b)))
(check-sat)
(get-model)

Другая возможность — использовать distinct.

(assert (distinct a b c d e))
person Leonardo de Moura    schedule 14.10.2012
comment
Спасибо за быстрый ответ. Я решил пойти на первое решение, оно кажется немного более элегантным. Между прочим, мне очень понравилась ваша лекция на летней школе SAT/SMT 2012 в Тренто! - person marczoid; 15.10.2012
comment
Спасибо! Я рад слышать, что вам понравилось. - person Leonardo de Moura; 15.10.2012