Z3 дополнительные условия (предложение ite) в модели массива, когда множественный массив в типе записи - PullRequest
Новая
       8

Z3 дополнительные условия (предложение ite) в модели массива, когда множественный массив в типе записи

0 голосов
/ 13 сентября 2018

Я столкнулся с неожиданным поведением в z3, когда запись содержит несколько именованных массивов одного типа: 

(declare-datatypes () ((Record_lengths (Record_lengths (array (Array Int Int))))))
(declare-datatypes () ((ROI (ROI (array (Array Int Int))))))
(declare-datatypes () ((Record (Record (lengths Record_lengths) (roi ROI)))))
(declare-fun rec () Record)
(assert (= (select (array (lengths rec)) 1) 0))
(get-model)

Я ожидал, что будет одно решение, где rec.lengths [1]= 0, все остальные значения по умолчанию или случайные значения.Однако селектор lengths всегда получает дополнительное предложение ite: 

(model 
  (define-fun rec () Record
    (Record (Record_lengths (_ as-array k!1)) (ROI (_ as-array k!0))))
  (define-fun k!0 ((x!0 Int)) Int
    (ite (= x!0 2) 4
      4))
  (define-fun k!1 ((x!0 Int)) Int
    (ite (= x!0 1) 0
    (ite (= x!0 2) 3 ;this is unexpected
      0)))
)

Кажется, что число этих дополнительных предложений находится в некотором роде связи с количеством одинаковых типов массива в записи.Как в этом примере: Record_lengths и ROI имеют один и тот же тип, и если я добавлю еще ROI тип к Record, тогда увеличится и количество дополнительных предложений.

Вот постоянная ссылка например: https://rise4fun.com/Z3/geoo

1 Ответ

0 голосов
/ 13 сентября 2018

Решатели SMT не гарантируют, что сгенерированные модели являются «минимальными» в любом смысле. Конечно, до тех пор, пока модель, которую они генерируют, удовлетворяет всем вашим ограничениям.

Сказав это, вы можете использовать опцию для частичных моделей и получить "меньшие" примеры. Я помещаю меньше в кавычки, потому что, опять же, здесь нет понятия минимума; то, что решатель считает частью модели, и то, что можно пропустить, может варьироваться в зависимости от эвристики, между прочим. Вы можете добавить: 

(set-option :model.partial true)

в начало вашего сценария, чтобы увидеть, какое влияние это окажет.

...