странное значение модели Z3

Question

Я использую последнюю версию Z3 3.2. Я получаю неожиданный ответ от команды «get-value». Вот небольшой скрипт, который я бегу в режиме совместимом SMT-Lib2:

(set-option :produce-models true) 
(declare-datatypes() ((Object o0 null))) 
(declare-fun IF (Object) Int) 
(declare-fun i2() Int) 
(assert (= (IF o0) i2)) 
(assert (= (IF null) 0)) 
(check-sat) 
(get-value (i2)) 

Отклик:

((i2 (IF o0))) 

Я ожидаю, чтобы получить только "0" назад. Есть ли способ попросить Z3 оценить возвращаемый термин для константы юниверса?

Вот полная модель:

(model 
;; universe for Object: 
;; Object!val!0 
;; ----------- 
;; definitions for universe elements: 
(declare-fun Object!val!0() Object) 
;; cardinality constraint: 
(forall ((x Object)) (= x Object!val!0)) 
;; ----------- 
(define-fun i2() Int 
(IF o0)) 
(define-fun IF ((x!1 Object)) Int 
    (ite (= x!1 Object!val!0) 0 
    0)) 
) 

Я тоже озадачен, почему о0 не определен в модели.

Answer 1

Это исправлено в Z3 4.0. Z3 4.0 скоро выйдет. Тем временем вы можете использовать его онлайн: http://rise4fun.com/Z3/75y

Эта ссылка может использоваться для выполнения вашего примера. Z3 4.0 дает ожидаемый результат.

Что касается ошибки, основной проблемой является то, что Z3 обрабатывает объект как неинтерпретированный вид. В Z3 3.2, вы можете обойти эту ошибку, включив

(опция набор-: авто-конфигурации ложь)

в начале вашего скрипта.